fix missing model checking call

randriu · Apr 1, 2024 · ae027d7 · ae027d7
1 parent 4602d95
commit ae027d7
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 5 deletions.
diff --git 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
@@ -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):