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

SMG abstraction for families of MDPs #52

Merged
merged 2 commits into from
Nov 25, 2024
Merged

SMG abstraction for families of MDPs #52

merged 2 commits into from
Nov 25, 2024

Conversation

randriu
Copy link
Owner

@randriu randriu commented Nov 22, 2024

Enables the use of SMG abstraction for families of MDPs:

  • simplified synthesis for families of MDPs by removing experimental features
  • introduced SMG abstraction for a quotient MDP and enabled its use via GameAbstrationSolver
  • SMG model checker was moved to a separate header file to be included by other modules

To enable the use of (PO)SMG abstraction for families of POMDPs:

  • Posmg and PosmgManager now use templates
  • Posmg module now has an additional method to create a POSMG from an SMG and observability classes

Copy link
Collaborator

@TheGreatfpmK TheGreatfpmK left a comment

Choose a reason for hiding this comment

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

Added small remarks otherwise looks good! Thanks a lot!

paynt/parser/drn_parser.py Show resolved Hide resolved
@@ -732,6 +679,7 @@ def split(self, family, prop, hole_selection, splitter, policy):
def evaluate_all(self, family, prop, keep_value_only=False):
assert not prop.reward, "expecting reachability probability propery"
game_solver = self.quotient.build_game_abstraction_solver(prop)
# game_solver.enable_profiling(True)
Copy link
Collaborator

Choose a reason for hiding this comment

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

Remove profiling comments unless we want to do more performance testing

@@ -27,7 +27,7 @@ def parse_drn(cls, sketch_path):
pomdp_path = sketch_path + '.tmp'
state_player_indications = DrnParser.pomdp_from_posmg(sketch_path, pomdp_path)
pomdp = DrnParser.read_drn(pomdp_path)
explicit_model = payntbind.synthesis.create_posmg(pomdp, state_player_indications)
explicit_model = payntbind.synthesis.posmgFromPomdp(pomdp, state_player_indications)
Copy link
Collaborator

Choose a reason for hiding this comment

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

I think we mostly use the python naming conventions for bound C++ functions? So I would change this to posmg_from_pomdp.

@randriu randriu merged commit b7ecfd3 into master Nov 25, 2024
2 checks 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.

2 participants