Merge pull request #29 from TheGreatfpmK/new-master

Return one policy if policy for all MDPs exists
randriu · Dec 8, 2023 · 8332ada · 8332ada
2 parents 3e60576 + ae6861f
commit 8332ada
Showing 1 changed file with 6 additions and 4 deletions.
diff --git a/paynt/synthesizer/policy_tree.py b/paynt/synthesizer/policy_tree.py
@@ -615,7 +615,7 @@ def synthesize_policy_for_family(self, family, prop, all_sat=False, iteration_li
         :returns whether all SAT MDPs are solved using a single policy
         :returns a list of UNSAT MDPs
         :returns a list of SAT MDPs
-        :returns to each SAT MDP, a corresponding policy
+        :returns one policy if all SAT MDPs are solved using single policy or list containing a corresponding policy for each SAT MDP
         '''
         sat_mdp_families = []
         sat_mdp_policies = []
@@ -701,10 +701,12 @@ def synthesize_policy_for_family(self, family, prop, all_sat=False, iteration_li
                 if scores[splitter] > 1:
                     break
             else:
+                policy = self.quotient.empty_policy()
                 for index, (result, family) in enumerate(zip(current_results, sat_mdp_families)):
-                    policy = self.quotient.scheduler_to_policy(result.result.scheduler, family.mdp)
-                    sat_mdp_policies[index] = policy
-                return True, unsat_mdp_families, sat_mdp_families, sat_mdp_policies
+                    mdp_policy = self.quotient.scheduler_to_policy(result.result.scheduler, family.mdp)
+                    policy = merge_policies([policy, mdp_policy])
+                    assert policy is not None
+                return True, unsat_mdp_families, sat_mdp_families, policy
 
             if False in current_results:
                 continue