fix unset choices of GameAbstractionSolver

randriu · Dec 15, 2023 · 3f4d137 · 3f4d137
1 parent e766514
commit 3f4d137
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 12 deletions.
diff --git a/paynt/quotient/models.py b/paynt/quotient/models.py
@@ -82,12 +82,8 @@ def initial_state(self):
         return self.model.initial_states[0]
 
     def model_check_formula(self, formula):
-        if not self.is_deterministic:
-            return stormpy.synthesis.verify_mdp(Property.environment,self.model,formula,True)
         return stormpy.model_checking(
-            self.model, formula,
-            extract_scheduler=(not self.is_deterministic),
-            environment=Property.environment
+            self.model, formula, extract_scheduler=True, environment=Property.environment
         )
 
     def model_check_property(self, prop, alt = False):

diff --git a/paynt/synthesizer/policy_tree.py b/paynt/synthesizer/policy_tree.py
@@ -432,7 +432,11 @@ def solve_game_abstraction(self, family, prop, game_solver):
 
     def parse_game_scheduler(self, game_solver):
         state_values = game_solver.solution_state_values
-        state_to_choice = game_solver.solution_state_to_quotient_choice
+        state_to_choice = game_solver.solution_state_to_quotient_choice.copy()
+        # fix unset choices
+        for state,choice in enumerate(state_to_choice):
+            if choice == self.quotient.quotient_mdp.nr_choices:
+                state_to_choice[state] = None
         # uncomment this to use only reachable choices of the game scheduler
         # state_to_choice = self.quotient.keep_reachable_choices_of_scheduler(state_to_choice)
         scheduler_choices = self.quotient.state_to_choice_to_choices(state_to_choice)
@@ -462,13 +466,11 @@ def verify_family(self, family, game_solver, prop):
                 mdp_family_result.policy = policy
                 mdp_family_result.policy_source = "policy search"
                 return mdp_family_result
-
 
         if family.size == 1:
             mdp_family_result.policy = self.solve_singleton(family,prop)
             mdp_family_result.policy_source = "singleton"
             return mdp_family_result
-
 
         game_policy,game_value,game_sat = self.solve_game_abstraction(family,prop,game_solver)
         if game_sat:
@@ -657,10 +659,7 @@ def synthesize_policy_for_family(self, family, prop, all_sat=False, iteration_li
             for index, mdp_subfamily in enumerate(sat_mdp_families):
                 self.quotient.build_with_second_coloring(mdp_subfamily, self.action_coloring, current_action_family) # maybe copy to new family?
 
-                mc_result = stormpy.model_checking(
-                    current_action_family.mdp.model, prop.formula, extract_scheduler=True, environment=Property.environment)
-                value = mc_result.at(current_action_family.mdp.initial_state)
-                primary_result = paynt.verification.property_result.PropertyResult(prop, mc_result, value)
+                primary_result = current_action_family.mdp.model_check_property(prop)
                 self.stat.iteration(current_action_family.mdp)
 
                 # discard the family as soon as one MDP is unsat