diff --git a/paynt/synthesizer/synthesizer_ar_storm.py b/paynt/synthesizer/synthesizer_ar_storm.py index eba4f54d8..29012d115 100644 --- a/paynt/synthesizer/synthesizer_ar_storm.py +++ b/paynt/synthesizer/synthesizer_ar_storm.py @@ -76,7 +76,7 @@ def verify_family(self, family): self.quotient.build(family) self.stat.iteration_mdp(family.mdp.states) - res = self.check_specification_for_mdp(mdp, family.constraint_indices) + res = self.quotient.check_specification_for_mdp(family.mdp, family.constraint_indices) family.analysis_result = res if family.analysis_result.improving_value is not None: diff --git a/paynt/synthesizer/synthesizer_pomdp.py b/paynt/synthesizer/synthesizer_pomdp.py index 9264df5d0..fdc891496 100644 --- a/paynt/synthesizer/synthesizer_pomdp.py +++ b/paynt/synthesizer/synthesizer_pomdp.py @@ -366,12 +366,11 @@ def solve_mdp(self, family): # solve quotient MDP self.quotient.build(family) - mdp = family.mdp - spec = self.check_specification_for_mdp(mdp, family.constraint_indices) + spec = self.quotient.check_specification_for_mdp(family.mdp, family.constraint_indices) # nothing more to do if optimality cannot be improved if not spec.optimality_result.can_improve: - return mdp, spec, None, None, None, None + return family.mdp, spec, None, None, None, None # hole scores = sum of scores wrt individual formulae hole_scores = {} @@ -391,7 +390,7 @@ def solve_mdp(self, family): # scores = result.primary_scores scores = hole_scores - return mdp, spec, selection, choice_values, expected_visits, scores + return family.mdp, spec, selection, choice_values, expected_visits, scores def strategy_expected_uai(self):