add option for all-in-one memory limit

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()

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':