From 3f4d13785241ad56b387f0fd29f57a733a869891 Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Fri, 15 Dec 2023 13:15:26 +0100 Subject: [PATCH] fix unset choices of GameAbstractionSolver --- paynt/quotient/models.py | 6 +----- paynt/synthesizer/policy_tree.py | 13 ++++++------- 2 files changed, 7 insertions(+), 12 deletions(-) diff --git a/paynt/quotient/models.py b/paynt/quotient/models.py index 2b6a2ce80..e623fd8e4 100644 --- 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 index 4bcf324e6..04bd9b1b4 100644 --- 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