more Saynt refactoring

randriu · Dec 10, 2024 · 26828a7 · 26828a7
1 parent 4894d7b
commit 26828a7
Show file tree

Hide file tree

Showing 3 changed files with 40 additions and 44 deletions.
diff --git a/paynt/quotient/pomdp_family.py b/paynt/quotient/pomdp_family.py
@@ -63,10 +63,12 @@ def observation_is_trivial(self, obs):
     def build_pomdp(self, family):
         ''' Construct the sub-POMDP from the given hole assignment. '''
         assert family.size == 1, "expecting family of size 1"
-
         choices = self.coloring.selectCompatibleChoices(family.family)
         mdp,state_map,choice_map = self.restrict_quotient(choices)
         pomdp = self.obs_evaluator.add_observations_to_submdp(mdp,state_map)
+        # for state,quotient_state in enumerate(state_map):
+        #     assert pomdp.observations[state] == self.state_to_observation[quotient_state]
+        # assert pomdp.nr_observations == self.num_observations
         return SubPomdp(pomdp,self,state_map,choice_map)
 
 

diff --git a/paynt/quotient/storm_pomdp_control.py b/paynt/quotient/storm_pomdp_control.py
@@ -145,22 +145,21 @@ def run_storm_analysis(self):
         value = result.upper_bound if self.quotient.specification.optimality.minimizing else result.lower_bound
         size = self.get_belief_controller_size(result, self.paynt_fsc_size)
 
+
+        print(f'-----------Storm-----------')
+        print(f'Value = {value} | Time elapsed = {round(storm_timer.read(),1)}s | FSC size = {size}', flush=True)
         if self.get_result is not None:
             # TODO not important for the paper but it would be nice to have correct FSC here as well
-
             if self.storm_options == "overapp":
-                print(f'-----------Storm----------- \
-                \nValue = {value} | Time elapsed = {round(storm_timer.read(),1)}s | FSC size = {size}\n', flush=True)
                 #print(".....")
                 #print(result.upper_bound)
                 #print(result.lower_bound)
+                pass
             else:
-                print(f'-----------Storm----------- \
-                \nValue = {value} | Time elapsed = {round(storm_timer.read(),1)}s | FSC size = {size}\nFSC (dot) = {result.induced_mc_from_scheduler.to_dot()}\n', flush=True)
+                print(f'FSC (dot) = {result.induced_mc_from_scheduler.to_dot()}\n', flush=True)
             exit()
 
-        print(f'-----------Storm----------- \
-              \nValue = {value} | Time elapsed = {round(storm_timer.read(),1)}s | FSC size = {size}\nFSC (dot) = {result.induced_mc_from_scheduler.to_dot()}\n', flush=True)
+        # print(f'\nFSC (dot) = {result.induced_mc_from_scheduler.to_dot()}\n', flush=True)
 
         self.store_storm_result(result)
 

diff --git a/paynt/synthesizer/synthesizer_pomdp.py b/paynt/synthesizer/synthesizer_pomdp.py
@@ -2,9 +2,8 @@
 
 from .statistic import Statistic
 import paynt.synthesizer.synthesizer_ar
-from .synthesizer_ar_storm import SynthesizerARStorm
-from .synthesizer_hybrid import SynthesizerHybrid
-from .synthesizer_multicore_ar import SynthesizerMultiCoreAR
+import paynt.synthesizer.synthesizer_hybrid
+import paynt.synthesizer.synthesizer_ar_storm
 
 import paynt.quotient.quotient
 import paynt.quotient.pomdp
@@ -27,24 +26,20 @@ class SynthesizerPomdp:
 
     def __init__(self, quotient, method, storm_control):
         self.quotient = quotient
-        self.use_storm = False
         self.synthesizer = None
         if method == "ar":
             self.synthesizer = paynt.synthesizer.synthesizer_ar.SynthesizerAR
-        elif method == "ar_multicore":
-            self.synthesizer = SynthesizerMultiCoreAR
         elif method == "hybrid":
-            self.synthesizer = SynthesizerHybrid
+            self.synthesizer = paynt.synthesizer.synthesizer_hybrid.SynthesizerHybrid
         self.total_iters = 0
 
+        self.storm_control = storm_control
         if storm_control is not None:
-            self.use_storm = True
-            self.storm_control = storm_control
             self.storm_control.quotient = self.quotient
             self.storm_control.pomdp = self.quotient.pomdp
             self.storm_control.spec_formulas = self.quotient.specification.stormpy_formulae()
             self.synthesis_terminate = False
-            self.synthesizer = SynthesizerARStorm       # SAYNT only works with abstraction refinement
+            self.synthesizer = paynt.synthesizer.synthesizer_ar_storm.SynthesizerARStorm # SAYNT only works with abstraction refinement
             if self.storm_control.iteration_timeout is not None:
                 self.saynt_timer = paynt.utils.timer.Timer()
                 self.synthesizer.saynt_timer = self.saynt_timer
@@ -281,31 +276,31 @@ def strategy_iterative(self, unfold_imperfect_only):
             #break
 
     def run(self, optimum_threshold=None):
-        # choose the synthesis strategy:
-        if self.use_storm:
-            logger.info("Storm POMDP option enabled")
-            logger.info("Storm settings: iterative - {}, get_storm_result - {}, storm_options - {}, prune_storm - {}, unfold_strategy - {}, use_storm_cutoffs - {}".format(
-                        (self.storm_control.iteration_timeout, self.storm_control.paynt_timeout, self.storm_control.storm_timeout), self.storm_control.get_result,
-                        self.storm_control.storm_options, self.storm_control.incomplete_exploration, (self.storm_control.unfold_storm, self.storm_control.unfold_cutoff), self.storm_control.use_cutoffs
-            ))
-            # start SAYNT
-            if self.storm_control.iteration_timeout is not None:
-                self.iterative_storm_loop(timeout=self.storm_control.iteration_timeout,
-                                          paynt_timeout=self.storm_control.paynt_timeout,
-                                          storm_timeout=self.storm_control.storm_timeout,
-                                          iteration_limit=0)
-            # run PAYNT for a time given by 'self.storm_control.get_result' and then run Storm using the best computed FSC at cut-offs
-            elif self.storm_control.get_result is not None:
-                if self.storm_control.get_result:
-                    self.run_synthesis_timeout(self.storm_control.get_result)
-                self.storm_control.run_storm_analysis()
-            # run Storm and then use the obtained result to enhance PAYNT synthesis
-            else:
-                self.storm_control.get_storm_result()
-                self.strategy_storm(unfold_imperfect_only=True, unfold_storm=self.storm_control.unfold_storm)
+        if self.storm_control is None:
+            # Pure PAYNT POMDP synthesis
+            self.strategy_iterative(unfold_imperfect_only=True)
+            return
 
-            self.print_synthesized_controllers()
-        # Pure PAYNT POMDP synthesis
+        # SAYNT
+        logger.info("Storm POMDP option enabled")
+        logger.info("Storm settings: iterative - {}, get_storm_result - {}, storm_options - {}, prune_storm - {}, unfold_strategy - {}, use_storm_cutoffs - {}".format(
+                    (self.storm_control.iteration_timeout, self.storm_control.paynt_timeout, self.storm_control.storm_timeout), self.storm_control.get_result,
+                    self.storm_control.storm_options, self.storm_control.incomplete_exploration, (self.storm_control.unfold_storm, self.storm_control.unfold_cutoff), self.storm_control.use_cutoffs
+        ))
+        # start SAYNT
+        if self.storm_control.iteration_timeout is not None:
+            self.iterative_storm_loop(timeout=self.storm_control.iteration_timeout,
+                                      paynt_timeout=self.storm_control.paynt_timeout,
+                                      storm_timeout=self.storm_control.storm_timeout,
+                                      iteration_limit=0)
+        # run PAYNT for a time given by 'self.storm_control.get_result' and then run Storm using the best computed FSC at cut-offs
+        elif self.storm_control.get_result is not None:
+            if self.storm_control.get_result:
+                self.run_synthesis_timeout(self.storm_control.get_result)
+            self.storm_control.run_storm_analysis()
+        # run Storm and then use the obtained result to enhance PAYNT synthesis
         else:
-            # self.strategy_iterative(unfold_imperfect_only=False)
-            self.strategy_iterative(unfold_imperfect_only=True)
+            self.storm_control.get_storm_result()
+            self.strategy_storm(unfold_imperfect_only=True, unfold_storm=self.storm_control.unfold_storm)
+
+        self.print_synthesized_controllers()