Merge branch 'master' into mdp

randriu · Sep 27, 2024 · be963fa · be963fa
2 parents d6d0d33 + f4cd5f7
commit be963fa
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 3 deletions.
diff --git a/paynt/quotient/storm_pomdp_control.py b/paynt/quotient/storm_pomdp_control.py
@@ -178,12 +178,14 @@ def interactive_storm_start(self, storm_timeout):
 
         control_thread.join()
 
-        self.belief_explorer = belmc.get_interactive_belief_explorer()
-
     # resume interactive belief model checker, should be called only after belief model checker was previously started
     def interactive_storm_resume(self, storm_timeout):
         control_thread = Thread(target=self.interactive_control, args=(belmc, False, storm_timeout,))
 
+        if self.storm_terminated:
+            logger.info("Storm already terminated")
+            return
+
         logger.info("Interactive Storm resumed")
         control_thread.start()
 
@@ -234,7 +236,7 @@ def interactive_control(self, belmc, start, storm_timeout):
         # Update cut-off FSC values provided by PAYNT
         if not start:
             logger.info("Updating FSC values in Storm")
-            self.belief_explorer.set_fsc_values(self.paynt_export)
+            belmc.set_fsc_values(self.paynt_export)
             belmc.continue_unfolding()
 
         # wait for Storm to start exploring
@@ -245,6 +247,7 @@ def interactive_control(self, belmc, start, storm_timeout):
 
         sleep(storm_timeout)
         if self.storm_terminated:
+            logger.info("Storm terminated")
             return
         logger.info("Pausing Storm")
         belmc.pause_unfolding()

diff --git a/paynt/synthesizer/synthesizer_pomdp.py b/paynt/synthesizer/synthesizer_pomdp.py
@@ -152,6 +152,7 @@ def strategy_iterative_storm(self, unfold_imperfect_only, unfold_storm=True):
                 self.storm_control.paynt_export = self.quotient.extract_policy(assignment)
                 self.storm_control.paynt_bounds = self.quotient.specification.optimality.optimum
                 self.storm_control.paynt_fsc_size = self.quotient.policy_size(self.storm_control.latest_paynt_result)
+                self.storm_control.latest_paynt_result_fsc = self.quotient.assignment_to_fsc(self.storm_control.latest_paynt_result)
 
             self.storm_control.update_data()