diff --git a/models/archive/cav24-policy-trees/dpm-switch-big-q10/sketch.props b/models/archive/cav24-policy-trees/dpm-switch-q10-big/sketch.props similarity index 100% rename from models/archive/cav24-policy-trees/dpm-switch-big-q10/sketch.props rename to models/archive/cav24-policy-trees/dpm-switch-q10-big/sketch.props diff --git a/models/archive/cav24-policy-trees/dpm-switch-big-q10/sketch.templ b/models/archive/cav24-policy-trees/dpm-switch-q10-big/sketch.templ similarity index 100% rename from models/archive/cav24-policy-trees/dpm-switch-big-q10/sketch.templ rename to models/archive/cav24-policy-trees/dpm-switch-q10-big/sketch.templ diff --git a/paynt/cli.py b/paynt/cli.py index 64fab21a6..92dda7354 100644 --- a/paynt/cli.py +++ b/paynt/cli.py @@ -113,8 +113,10 @@ def setup_logger(log_path = None): @click.option( "--all-in-one", type=click.Choice(["sparse", "bdd"]), default=None, show_default=True, - help="all in one MDP approach", + help="use all-in-one MDP abstraction", ) +@click.option("--all-in-one-maxmem", default=4096, type=int, + help="memory limit (MB) for the all-in-one abstraction") @click.option("--mdp-split-wrt-mdp", is_flag=True, default=False, help="# if set, MDP abstraction scheduler will be used for splitting, otherwise game abstraction scheduler will be used") @@ -145,7 +147,7 @@ def paynt_run( storm_pomdp, iterative_storm, get_storm_result, storm_options, prune_storm, use_storm_cutoffs, unfold_strategy_storm, export_fsc_storm, export_fsc_paynt, export_evaluation, - all_in_one, + all_in_one, all_in_one_maxmem, mdp_split_wrt_mdp, mdp_discard_unreachable_choices, mdp_use_randomized_abstraction, constraint_bound, ce_generator, @@ -185,7 +187,7 @@ def paynt_run( synthesizer.run(optimum_threshold, export_evaluation) else: all_in_one_program, specification, family = paynt.parser.sketch.Sketch.load_sketch_as_all_in_one(sketch_path, properties_path) - all_in_one_analysis = paynt.synthesizer.all_in_one.AllInOne(all_in_one_program, specification, all_in_one, family) + all_in_one_analysis = paynt.synthesizer.all_in_one.AllInOne(all_in_one_program, specification, all_in_one, all_in_one_maxmem, family) all_in_one_analysis.run() if profiling: profiler.disable() diff --git a/paynt/synthesizer/all_in_one.py b/paynt/synthesizer/all_in_one.py index 852b5bd35..f3ccd1cfd 100644 --- a/paynt/synthesizer/all_in_one.py +++ b/paynt/synthesizer/all_in_one.py @@ -8,7 +8,7 @@ class AllInOne: - def __init__(self, all_in_one_program, specification, approach, family): + def __init__(self, all_in_one_program, specification, approach, memory_limit_mb, family): self.properties = specification.all_properties() self.threshold = self.properties[0].threshold @@ -22,7 +22,7 @@ def __init__(self, all_in_one_program, specification, approach, family): build_timer.start() if self.approach == 'bdd': - stormpy.set_settings(["--sylvan:maxmem", "16000"]) # set memory usage by the symbolic approach + stormpy.set_settings(["--sylvan:maxmem", str(memory_limit_mb)]) # set memory usage by the symbolic approach self.model = stormpy.build_symbolic_model(all_in_one_program) self.filter = stormpy.create_filter_initial_states_symbolic(self.model) elif self.approach == 'sparse':