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.

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

Adding SMG model checker to payntbind #43

Merged
merged 7 commits into from
Jul 14, 2024

Conversation

TheGreatfpmK
Copy link
Collaborator

@TheGreatfpmK TheGreatfpmK commented Jul 14, 2024

Adding a taken implementation of SMG model checker from TEMPEST (https://github.com/PrangerStefan/TempestSynthesis) to payntbind.
This model checker works on the Smg class from Storm, which holds general turn-based SMGs. Therefore, this model checker should be future-proof if we would like to play around with more than two players and so on. I only tested reachability properties! See how to specify the rPATL properties here: https://prismmodelchecker.org/games/properties.php. Note the player indexing starts from 0 for the players i.e. Player1's index is 0. The results are the same as those of PRISM-Games.

I added a binding "smg_model_checking" which expects the SMG and formula to be checked, and returns a model checking result with values for each state and a scheduler.

I also changed the models in models/posg to the new DRN format that we can export from PRISM-Games thanks to Dave. For now I kept the old POMDP models there as well, but we can remove it once we verify the parser.

Depends on moves-rwth/stormpy#173

@TheGreatfpmK TheGreatfpmK merged commit 362d4c6 into randriu:master Jul 14, 2024
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant