From ae6861f0009c64887be7118446bb5e3dc356dd97 Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Fri, 8 Dec 2023 15:48:44 +0100 Subject: [PATCH] Return one policy if policy for all MDPs exists --- paynt/synthesizer/policy_tree.py | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/paynt/synthesizer/policy_tree.py b/paynt/synthesizer/policy_tree.py index 6e25a425d..2ef362199 100644 --- 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