From 44bc3d091b3a8ebfbfea0c8e37e88437c8a350f9 Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Wed, 18 Sep 2024 20:50:42 +0200 Subject: [PATCH 1/2] Fixing SAYNT double free problem --- paynt/quotient/storm_pomdp_control.py | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/paynt/quotient/storm_pomdp_control.py b/paynt/quotient/storm_pomdp_control.py index 1fe9f8b5..bc6c3867 100644 --- a/paynt/quotient/storm_pomdp_control.py +++ b/paynt/quotient/storm_pomdp_control.py @@ -178,8 +178,6 @@ 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,)) @@ -234,7 +232,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 From c5d86ae2b681b405580291c4ca258ab8ebc6db2e Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Sun, 22 Sep 2024 00:52:17 +0200 Subject: [PATCH 2/2] Fixing SAYNT --- paynt/quotient/storm_pomdp_control.py | 5 +++++ paynt/synthesizer/synthesizer_pomdp.py | 1 + 2 files changed, 6 insertions(+) diff --git a/paynt/quotient/storm_pomdp_control.py b/paynt/quotient/storm_pomdp_control.py index bc6c3867..de620649 100644 --- a/paynt/quotient/storm_pomdp_control.py +++ b/paynt/quotient/storm_pomdp_control.py @@ -182,6 +182,10 @@ def interactive_storm_start(self, storm_timeout): 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() @@ -243,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 index f753cf73..594dbe4e 100644 --- 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()