diff --git a/paynt/synthesizer/synthesizer_ar_storm.py b/paynt/synthesizer/synthesizer_ar_storm.py index 31d442da1..a1daa9d60 100644 --- a/paynt/synthesizer/synthesizer_ar_storm.py +++ b/paynt/synthesizer/synthesizer_ar_storm.py @@ -17,7 +17,7 @@ class SynthesizerARStorm(Synthesizer): # buffer containing subfamilies to be checked after the main restricted family subfamilies_buffer = None - unresticted_family = None + main_family = None # if True, Storm over-approximation will be run to help with family pruning storm_pruning = False @@ -115,6 +115,10 @@ def synthesize_one(self, family): self.quotient.discarded = 0 satisfying_assignment = None + + if self.main_family is not None: + family = self.main_family + families = [family] while families: diff --git a/paynt/synthesizer/synthesizer_pomdp.py b/paynt/synthesizer/synthesizer_pomdp.py index 62ac12b36..85beb677c 100644 --- a/paynt/synthesizer/synthesizer_pomdp.py +++ b/paynt/synthesizer/synthesizer_pomdp.py @@ -177,9 +177,9 @@ def strategy_iterative_storm(self, unfold_imperfect_only, unfold_storm=True): subfamilies = [] self.synthesizer.subfamilies_buffer = subfamilies - self.synthesizer.unresticted_family = family + self.synthesizer.main_family = main_family - assignment = self.synthesize(main_family) + assignment = self.synthesize(family) if assignment is not None: self.storm_control.latest_paynt_result = assignment @@ -287,7 +287,7 @@ def strategy_storm(self, unfold_imperfect_only, unfold_storm=True): # for x in range(2): if self.storm_control.is_storm_better == False: - self.storm_control.parse_result(self.quotient) + self.storm_control.parse_results(self.quotient) paynt.quotient.pomdp.PomdpQuotient.current_family_index = mem_size @@ -356,9 +356,9 @@ def strategy_storm(self, unfold_imperfect_only, unfold_storm=True): subfamilies = [] self.synthesizer.subfamilies_buffer = subfamilies - self.synthesizer.unresticted_family = family + self.synthesizer.main_family = main_family - assignment = self.synthesize(main_family) + assignment = self.synthesize(family) if assignment is not None: self.storm_control.latest_paynt_result = assignment