Fixed wrong explored% for SAYNT; fixed error after function rename

randriu · Feb 6, 2024 · ccb4e81 · ccb4e81
1 parent 54507af
commit ccb4e81
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 6 deletions.
diff --git a/paynt/synthesizer/synthesizer_ar_storm.py b/paynt/synthesizer/synthesizer_ar_storm.py
@@ -17,7 +17,7 @@ class SynthesizerARStorm(Synthesizer):
     # buffer containing subfamilies to be checked after the main restricted family
     subfamilies_buffer = None
 
-    unresticted_family = None
+    main_family = None
 
     # if True, Storm over-approximation will be run to help with family pruning
     storm_pruning = False
@@ -115,6 +115,10 @@ def synthesize_one(self, family):
         self.quotient.discarded = 0
 
         satisfying_assignment = None
+
+        if self.main_family is not None:
+            family = self.main_family
+
         families = [family]
 
         while families:

diff --git a/paynt/synthesizer/synthesizer_pomdp.py b/paynt/synthesizer/synthesizer_pomdp.py
@@ -177,9 +177,9 @@ def strategy_iterative_storm(self, unfold_imperfect_only, unfold_storm=True):
                 subfamilies = []
 
             self.synthesizer.subfamilies_buffer = subfamilies
-            self.synthesizer.unresticted_family = family
+            self.synthesizer.main_family = main_family
 
-            assignment = self.synthesize(main_family)
+            assignment = self.synthesize(family)
 
             if assignment is not None:
                 self.storm_control.latest_paynt_result = assignment
@@ -287,7 +287,7 @@ def strategy_storm(self, unfold_imperfect_only, unfold_storm=True):
         # for x in range(2):
 
             if self.storm_control.is_storm_better == False:
-                self.storm_control.parse_result(self.quotient)
+                self.storm_control.parse_results(self.quotient)
 
             paynt.quotient.pomdp.PomdpQuotient.current_family_index = mem_size
 
@@ -356,9 +356,9 @@ def strategy_storm(self, unfold_imperfect_only, unfold_storm=True):
                 subfamilies = []
 
             self.synthesizer.subfamilies_buffer = subfamilies
-            self.synthesizer.unresticted_family = family
+            self.synthesizer.main_family = main_family
 
-            assignment = self.synthesize(main_family)
+            assignment = self.synthesize(family)
 
             if assignment is not None:
                 self.storm_control.latest_paynt_result = assignment