diff --git a/paynt/quotient/fsc.py b/paynt/quotient/fsc.py index 0502328d4..b91b55261 100644 --- a/paynt/quotient/fsc.py +++ b/paynt/quotient/fsc.py @@ -111,3 +111,11 @@ def fill_zero_updates(self): for node in range(self.num_nodes): self.update_function[node] = [0] * self.num_observations + # this fixes FSCs contructed from not fully unfolded quotients + # careful this can be used only when the current state of the FSC is correct + def fill_implicit_actions_and_updates(self): + for node in range(self.num_nodes): + for obs in range(self.num_observations): + if self.action_function[node][obs] == None: + self.action_function[node][obs] = self.action_function[0][obs] + self.update_function[node][obs] = self.update_function[0][obs] diff --git a/paynt/quotient/pomdp.py b/paynt/quotient/pomdp.py index f0f9a29ae..93af82bc6 100644 --- a/paynt/quotient/pomdp.py +++ b/paynt/quotient/pomdp.py @@ -731,6 +731,9 @@ def assignment_to_fsc(self, assignment): option = assignment.hole_options(hole)[0] fsc.update_function[memory][obs] = option + # fixing the FSC for not fully unrolled quotients + fsc.fill_implicit_actions_and_updates() + fsc.check(observation_to_actions) return fsc diff --git a/paynt/quotient/storm_pomdp_control.py b/paynt/quotient/storm_pomdp_control.py index 23d0e2823..d9b31c45a 100644 --- a/paynt/quotient/storm_pomdp_control.py +++ b/paynt/quotient/storm_pomdp_control.py @@ -20,7 +20,8 @@ class StormPOMDPControl: storm_bounds = None # under-approximation value from Storm # PAYNT data and FSC export - latest_paynt_result = None + latest_paynt_result = None # holds the synthesised assignment + latest_paynt_result_fsc = None # holds the FSC built from assignment paynt_bounds = None paynt_export = [] diff --git a/paynt/synthesizer/synthesizer_ar_storm.py b/paynt/synthesizer/synthesizer_ar_storm.py index fb25afdaf..98d608001 100644 --- a/paynt/synthesizer/synthesizer_ar_storm.py +++ b/paynt/synthesizer/synthesizer_ar_storm.py @@ -134,6 +134,7 @@ def synthesize_one(self, family): self.storm_control.paynt_export = self.quotient.extract_policy(satisfying_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() logger.info("Pausing synthesis") self.s_queue.get()