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

Speed up counter example generation for PBESs using the winning strategy for the original #1748

Open
wants to merge 53 commits into
base: master
Choose a base branch
from
Open

Speed up counter example generation for PBESs using the winning strategy for the original #1748

wants to merge 53 commits into from

Conversation

mlaveaux
Copy link
Member

@mlaveaux mlaveaux commented Feb 26, 2024 •
edited
Loading

This is a branch implementing the two phase approach for counter example generation. There is a flag --naive-counter-example-instantiation to revert to the previous method for comparison.

  • Implement the approach for pbessolve.
  • Implement the approach for pbessolvesymbolic, including the strategy generation and checking.
  • Added random tests for both approaches, not yet all variants.

TODO:

  • Add translation for modal formulas into the SRF shape
  • Make it possible to use the pbessolve optimisations again.

@mlaveaux mlaveaux added the enhancement Something can be improved label Feb 26, 2024
@mlaveaux mlaveaux self-assigned this Feb 26, 2024
@mlaveaux mlaveaux force-pushed the feature/pbes-counterexamples branch 2 times, most recently from 3fd0436 to ce91a47 Compare February 27, 2024 09:42
@mlaveaux mlaveaux force-pushed the feature/pbes-counterexamples branch from cb18f1e to dced439 Compare June 5, 2024 15:09
@mlaveaux mlaveaux force-pushed the feature/pbes-counterexamples branch from ce58268 to 7ef8d84 Compare July 5, 2024 08:48
mlaveaux added 24 commits August 13, 2024 14:42
@mlaveaux
Added a preprocessing step to remove counter example information.
8016292
@mlaveaux
Apply the counter example removal step when the input has counterexam…
25e3aee 
…ple information.
@mlaveaux
Made it possible to remove either side of the counter example informa…
42076fd 
…tion.
@mlaveaux
Implemented an initial version of Anna's algorithm.
e17d76c
@mlaveaux
Compute the minimal structure graph first.
d2138e2
@mlaveaux
Apply the simplifier after removing counter example information.
4331cad
@mlaveaux
Added an option to run the naive algorithm, fixed issue with intersec…
6f56266 
…tion.
@mlaveaux
Avoid Tom's optimisation and fixed rewrite star ignoring the player.
cafb1a8
@mlaveaux
Print the minimal structure graph, although successors/predecessors a…
30e39c5 
…re wrong.
@mlaveaux
This include file had the slashes in the wrong way.
9db170e
@mlaveaux
Fixed compilation errors, and replaced boost::optional by std::optional.
f7cd23a
@mlaveaux
Fixed mistake in solving PBES without counter example information.
701619d
@mlaveaux
Fixed a failing assertion.
f777dd1
@mlaveaux
Deal correctly with the case where X has a self loop.
a8257d2 
 * Every propositional variable encountered (not in L) is in W so we
   add X itself to the ones that should be kept by rewrite*.
@mlaveaux
Do not generate the evidence when there is no counter example informa…
94b3704 
…tion.
@mlaveaux
Introduce a mapping from propositional variables to their vertices in…
4d8beed 
… the proof graph.
@mlaveaux
Changed to unordered_sets, and avoid regex construction.
24dc8dc
@mlaveaux
Initial version to compute a symbolic strategy.
38d791b
@mlaveaux
Moved the utility function to check if PBES has counter example infor…
6eefdbf 
…mation.
@mlaveaux
Moved the file extension utility function.
b56f9e2
@mlaveaux
Moved the rewrite_star implementation into the rewrite_psi, separatin…
d936c39 
…g it.
@mlaveaux
Adapted the interface.
4e7964e
@mlaveaux
Moved run_solve to its own function.
9e27962
@mlaveaux
Started to implement a pbesinst variant that takes a symbolic strategy.
d63ff41
mlaveaux added 19 commits August 13, 2024 14:42
@mlaveaux
Added an option to not merge simple data expressions.
04fc44a
@mlaveaux
Applied changes to the load and save lps functions.
efdb47e
@mlaveaux
Added a check for unified parameters of a PBES.
cf45695
@mlaveaux
Added a check for data unification.
e0fa807
@mlaveaux
Added a note that the simplifier does not necessarily yield an SRF pbes.
c399809
@mlaveaux
Added more print statements.
ae75585
@mlaveaux
Fixed some issues with the strategy computation.
476619a
@mlaveaux
Extended tests and fixed compilation errors.
dc95591
@mlaveaux
Fixed the tests and actually look up the strategy properly.
14017cf
@mlaveaux
Actually use the simplified pbes.
0cdf1e0
@mlaveaux
Added --check-strategy to verify the symbolic strategy.
6afc880
@mlaveaux
Always write the couner example file.
27858ac
@mlaveaux
Check for simulation of the counter example.
2b5a0f4
@mlaveaux
Actually disable chaining properly when asking for a strategy.
14223f8
@mlaveaux
Adapted the algoritm to unify parameters to ignore the counter exampl…
e575164 
…e equations.
@mlaveaux
Fixed compilation issue.
be04429
@mlaveaux
Link sylvan statically to avoid segmentation fault
df56075 
On MacOS there is a function called cache_get in the dynamic library libcache.dylib that conflicts with the cache_get in Sylvan. This causes the wrong function to be called, resulting in a segmentation fault.
@mlaveaux
For linux it seems necessary to enable PIC
fa2b848
@mlaveaux
Added the --naive-counter-example-instantiation option to pbessolvesy…
90e6bd7 
…mbolic

With this option enabled the PBES with counter example information will be
instantiated in a naive way, and only solved since we cannot reconstruct
the symbolic counter example this way.
@mlaveaux mlaveaux force-pushed the feature/pbes-counterexamples branch from a57ec46 to 90e6bd7 Compare August 13, 2024 14:09
@mlaveaux mlaveaux force-pushed the feature/pbes-counterexamples branch from fbe52dc to 1988c28 Compare September 12, 2024 14:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@mlaveaux mlaveaux

Labels
enhancement Something can be improved
Projects
mCRL2 Planning
Status: In Progress
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@mlaveaux