From ae027d776b1112338d75d2c3170008e817d7c984 Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Mon, 1 Apr 2024 23:16:05 +0200 Subject: [PATCH] fix missing model checking call --- paynt/synthesizer/synthesizer_ar_storm.py | 2 +- paynt/synthesizer/synthesizer_pomdp.py | 7 +++---- 2 files changed, 4 insertions(+), 5 deletions(-) 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):