diff --git a/paynt/quotient/pomdp_family.py b/paynt/quotient/pomdp_family.py index 340cc77e..681e07b4 100644 --- a/paynt/quotient/pomdp_family.py +++ b/paynt/quotient/pomdp_family.py @@ -63,10 +63,12 @@ def observation_is_trivial(self, obs): def build_pomdp(self, family): ''' Construct the sub-POMDP from the given hole assignment. ''' assert family.size == 1, "expecting family of size 1" - choices = self.coloring.selectCompatibleChoices(family.family) mdp,state_map,choice_map = self.restrict_quotient(choices) pomdp = self.obs_evaluator.add_observations_to_submdp(mdp,state_map) + # for state,quotient_state in enumerate(state_map): + # assert pomdp.observations[state] == self.state_to_observation[quotient_state] + # assert pomdp.nr_observations == self.num_observations return SubPomdp(pomdp,self,state_map,choice_map) diff --git a/paynt/quotient/storm_pomdp_control.py b/paynt/quotient/storm_pomdp_control.py index 23845cf3..949a4666 100644 --- a/paynt/quotient/storm_pomdp_control.py +++ b/paynt/quotient/storm_pomdp_control.py @@ -145,22 +145,21 @@ def run_storm_analysis(self): value = result.upper_bound if self.quotient.specification.optimality.minimizing else result.lower_bound size = self.get_belief_controller_size(result, self.paynt_fsc_size) + + print(f'-----------Storm-----------') + print(f'Value = {value} | Time elapsed = {round(storm_timer.read(),1)}s | FSC size = {size}', flush=True) if self.get_result is not None: # TODO not important for the paper but it would be nice to have correct FSC here as well - if self.storm_options == "overapp": - print(f'-----------Storm----------- \ - \nValue = {value} | Time elapsed = {round(storm_timer.read(),1)}s | FSC size = {size}\n', flush=True) #print(".....") #print(result.upper_bound) #print(result.lower_bound) + pass else: - print(f'-----------Storm----------- \ - \nValue = {value} | Time elapsed = {round(storm_timer.read(),1)}s | FSC size = {size}\nFSC (dot) = {result.induced_mc_from_scheduler.to_dot()}\n', flush=True) + print(f'FSC (dot) = {result.induced_mc_from_scheduler.to_dot()}\n', flush=True) exit() - print(f'-----------Storm----------- \ - \nValue = {value} | Time elapsed = {round(storm_timer.read(),1)}s | FSC size = {size}\nFSC (dot) = {result.induced_mc_from_scheduler.to_dot()}\n', flush=True) + # print(f'\nFSC (dot) = {result.induced_mc_from_scheduler.to_dot()}\n', flush=True) self.store_storm_result(result) diff --git a/paynt/synthesizer/synthesizer_pomdp.py b/paynt/synthesizer/synthesizer_pomdp.py index 9f0affab..fb1304c8 100644 --- a/paynt/synthesizer/synthesizer_pomdp.py +++ b/paynt/synthesizer/synthesizer_pomdp.py @@ -2,9 +2,8 @@ from .statistic import Statistic import paynt.synthesizer.synthesizer_ar -from .synthesizer_ar_storm import SynthesizerARStorm -from .synthesizer_hybrid import SynthesizerHybrid -from .synthesizer_multicore_ar import SynthesizerMultiCoreAR +import paynt.synthesizer.synthesizer_hybrid +import paynt.synthesizer.synthesizer_ar_storm import paynt.quotient.quotient import paynt.quotient.pomdp @@ -27,24 +26,20 @@ class SynthesizerPomdp: def __init__(self, quotient, method, storm_control): self.quotient = quotient - self.use_storm = False self.synthesizer = None if method == "ar": self.synthesizer = paynt.synthesizer.synthesizer_ar.SynthesizerAR - elif method == "ar_multicore": - self.synthesizer = SynthesizerMultiCoreAR elif method == "hybrid": - self.synthesizer = SynthesizerHybrid + self.synthesizer = paynt.synthesizer.synthesizer_hybrid.SynthesizerHybrid self.total_iters = 0 + self.storm_control = storm_control if storm_control is not None: - self.use_storm = True - self.storm_control = storm_control self.storm_control.quotient = self.quotient self.storm_control.pomdp = self.quotient.pomdp self.storm_control.spec_formulas = self.quotient.specification.stormpy_formulae() self.synthesis_terminate = False - self.synthesizer = SynthesizerARStorm # SAYNT only works with abstraction refinement + self.synthesizer = paynt.synthesizer.synthesizer_ar_storm.SynthesizerARStorm # SAYNT only works with abstraction refinement if self.storm_control.iteration_timeout is not None: self.saynt_timer = paynt.utils.timer.Timer() self.synthesizer.saynt_timer = self.saynt_timer @@ -281,31 +276,31 @@ def strategy_iterative(self, unfold_imperfect_only): #break def run(self, optimum_threshold=None): - # choose the synthesis strategy: - if self.use_storm: - logger.info("Storm POMDP option enabled") - logger.info("Storm settings: iterative - {}, get_storm_result - {}, storm_options - {}, prune_storm - {}, unfold_strategy - {}, use_storm_cutoffs - {}".format( - (self.storm_control.iteration_timeout, self.storm_control.paynt_timeout, self.storm_control.storm_timeout), self.storm_control.get_result, - self.storm_control.storm_options, self.storm_control.incomplete_exploration, (self.storm_control.unfold_storm, self.storm_control.unfold_cutoff), self.storm_control.use_cutoffs - )) - # start SAYNT - if self.storm_control.iteration_timeout is not None: - self.iterative_storm_loop(timeout=self.storm_control.iteration_timeout, - paynt_timeout=self.storm_control.paynt_timeout, - storm_timeout=self.storm_control.storm_timeout, - iteration_limit=0) - # run PAYNT for a time given by 'self.storm_control.get_result' and then run Storm using the best computed FSC at cut-offs - elif self.storm_control.get_result is not None: - if self.storm_control.get_result: - self.run_synthesis_timeout(self.storm_control.get_result) - self.storm_control.run_storm_analysis() - # run Storm and then use the obtained result to enhance PAYNT synthesis - else: - self.storm_control.get_storm_result() - self.strategy_storm(unfold_imperfect_only=True, unfold_storm=self.storm_control.unfold_storm) + if self.storm_control is None: + # Pure PAYNT POMDP synthesis + self.strategy_iterative(unfold_imperfect_only=True) + return - self.print_synthesized_controllers() - # Pure PAYNT POMDP synthesis + # SAYNT + logger.info("Storm POMDP option enabled") + logger.info("Storm settings: iterative - {}, get_storm_result - {}, storm_options - {}, prune_storm - {}, unfold_strategy - {}, use_storm_cutoffs - {}".format( + (self.storm_control.iteration_timeout, self.storm_control.paynt_timeout, self.storm_control.storm_timeout), self.storm_control.get_result, + self.storm_control.storm_options, self.storm_control.incomplete_exploration, (self.storm_control.unfold_storm, self.storm_control.unfold_cutoff), self.storm_control.use_cutoffs + )) + # start SAYNT + if self.storm_control.iteration_timeout is not None: + self.iterative_storm_loop(timeout=self.storm_control.iteration_timeout, + paynt_timeout=self.storm_control.paynt_timeout, + storm_timeout=self.storm_control.storm_timeout, + iteration_limit=0) + # run PAYNT for a time given by 'self.storm_control.get_result' and then run Storm using the best computed FSC at cut-offs + elif self.storm_control.get_result is not None: + if self.storm_control.get_result: + self.run_synthesis_timeout(self.storm_control.get_result) + self.storm_control.run_storm_analysis() + # run Storm and then use the obtained result to enhance PAYNT synthesis else: - # self.strategy_iterative(unfold_imperfect_only=False) - self.strategy_iterative(unfold_imperfect_only=True) + self.storm_control.get_storm_result() + self.strategy_storm(unfold_imperfect_only=True, unfold_storm=self.storm_control.unfold_storm) + + self.print_synthesized_controllers()