Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use Linear Programming to initialize potencies #143

Merged
merged 39 commits into from
Sep 10, 2023
Merged

Use Linear Programming to initialize potencies #143

merged 39 commits into from
Sep 10, 2023

Conversation

Malleek
Copy link
Contributor

@Malleek Malleek commented Jun 20, 2023

No description provided.

@srba srba requested review from srba and petergjoel June 20, 2023 09:53
petergjoel
petergjoel reviewed Jun 21, 2023
View reviewed changes
include/PetriEngine/PQL/Contexts.h Outdated
@@ -235,6 +236,9 @@ namespace PetriEngine {

glp_prob* makeBaseLP() const;

mutable std::vector<uint32_t> xs;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

xs seems like a funky naming scheme? Also please use the _ prefix for fields.

src/VerifyPN.cpp Outdated
// queries[i] = pushNegation(simp_cond.formula, stats, context, false, false, true);
wasAGCPNApprox |= dynamic_cast<NotCondition*> (queries[i].get()) != nullptr;

potencies = simplificationContext.xs;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What happens when we have multiple queries?

src/VerifyPN.cpp Outdated
@@ -671,3 +671,138 @@ void simplify_queries( const MarkVal* marking,
return a;
}) && std::chrono::duration_cast<std::chrono::seconds>(end - begin).count() < options.queryReductionTimeout && to_handle > 0);
}

void simplify_queries_potency(const MarkVal* marking,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this code duplicated from somewhere ? It looks like it.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it is the function simplify_queries with less code, and with the potencies = [...] line added

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I could add 2 optional parameters to the simplify_queries function (bool isLp and initPotencies), and then do the correct things according to the bool isLP

@Malleek Malleek marked this pull request as ready for review August 29, 2023 08:28
@Malleek
Copy link
Contributor Author

Malleek commented Aug 29, 2023 •
edited
Loading

This latest version uses a function named initialize_potency to initialize the potencies before a RandomWalk or a RPFS. This function is called after the query rsimplification and the net reduction iff --use-lp-potencies option is enabled.
The new visitor PotencyVisitor constructs all the Linear programs of one query in initPotencyVisit, then solve the 10 first lp programs (solvePotency) during the exploration (explorePotency). The timeout for this is by default 10 seconds.
The solutions are summed in the initial potencies, and multiplied by 60.

The best version run on the 2023 Benchmark (10 lp solves, potency = 60 * solution + 1) compared to the current main branch gives the following results:

PT models
    Cardinality: 68 more answers (22291 VS 22223)
    Fireability: 124 more answers (21864 VS 21740)
CPN models
    Cardinality: 1 **less** answer (3771 VS 3772)
    Fireability: 2 more answers (3121 VS 3119)

@srba
Copy link
Member

srba commented Sep 5, 2023

Are these new options related to lp-initizalization of potencies?
--init-potency Initial potency timeout in seconds (default 10)
--interval-timeout Time in seconds before the max intervals is halved (default 10)
write --interval-timeout 0 to disable interval limits
If yes, then add that the second one is for potency initialization

Also, make
--use-lp-potencies Use LP for computing the initial potencies
the default option, so that it is run by default and add the switch --do-not-use-lp-potencies
to disable this LP initialization of potencies.

Finally, please, adjust the competition script accordingly, test it again (rerun the consistency and performance tests) and upload the new script tapaal.sh into 2024 competition scripts.

@Malleek
Copy link
Contributor Author

Malleek commented Sep 6, 2023 •
edited
Loading

The new changes are:

  • Potency initialization is enabled by default. It only runs when the strategy is RPFS or RandomWalk
  • Only one option: --init-potency-timeout . Write 0 to disable.
  • The new tapaal script is similar to the previous one, but uses --init-potency-timeout option

The consistency and performance tests ran on the last version give the following results (compared to the current main branch):

Everything is consistent.

PT models
    Cardinality: 61 more answers (22284 VS 22223)
    Fireability: 112 more answers (21852 VS 21740)
CPN models
    Cardinality: same nb of answers (3772 VS 3772)
    Fireability: 4 more answers (3123 VS 3119)

@srba srba merged commit eeebbf1 into TAPAAL:main Sep 10, 2023
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@srba srba srba approved these changes

@petergjoel petergjoel petergjoel approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@Malleek @srba @petergjoel