Fixed FSC construction from assignment for not fully unrolled memory;…

… added PAYNT FSC property in storm_pomdp_control

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]

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

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 = []
 

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()