lightweight consistency check for SMT coloring

paynt/cli.py

@@ -11,6 +11,7 @@
 import paynt.synthesizer.synthesizer
 import paynt.synthesizer.synthesizer_cegis
 import paynt.synthesizer.policy_tree
+import paynt.synthesizer.decision_tree
 
 import click
 import sys
@@ -117,14 +118,19 @@ def setup_logger(log_path = None):
     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")
+    help="if set, MDP abstraction scheduler will be used for splitting, otherwise game abstraction scheduler will be used")
 @click.option("--mdp-discard-unreachable-choices", is_flag=True, default=False,
-    help="# if set, unreachable choices will be discarded from the splitting scheduler")
+    help="if set, unreachable choices will be discarded from the splitting scheduler")
 @click.option("--mdp-use-randomized-abstraction", is_flag=True, default=False,
-    help="# if set, randomized abstraction guess-and-verify will be used instead of game abstraction;" +
+    help="if set, randomized abstraction guess-and-verify will be used instead of game abstraction;" +
     " MDP abstraction scheduler will be used for splitting"
 )
 
+@click.option("--tree-depth", default=0, type=int,
+    help="decision tree synthesis: tree depth")
+@click.option("--tree-enumeration", is_flag=True, default=False,
+    help="decision tree synthesis: if set, all trees of size at most tree_depth will be enumerated")
+
 @click.option(
     "--constraint-bound", type=click.FLOAT, help="bound for creating constrained POMDP for cassandra models",
 )
@@ -147,6 +153,7 @@ def paynt_run(
     export_fsc_storm, export_fsc_paynt, export_evaluation,
     all_in_one, all_in_one_maxmem,
     mdp_split_wrt_mdp, mdp_discard_unreachable_choices, mdp_use_randomized_abstraction,
+    tree_depth, tree_enumeration,
     constraint_bound,
     ce_generator,
     profiling
@@ -169,6 +176,9 @@ def paynt_run(
     paynt.synthesizer.policy_tree.SynthesizerPolicyTree.discard_unreachable_choices = mdp_discard_unreachable_choices
     paynt.synthesizer.policy_tree.SynthesizerPolicyTree.use_randomized_abstraction = mdp_use_randomized_abstraction
 
+    paynt.synthesizer.decision_tree.SynthesizerDecisionTree.tree_depth = tree_depth
+    paynt.synthesizer.decision_tree.SynthesizerDecisionTree.tree_enumeration = tree_enumeration
+
     storm_control = None
     if storm_pomdp:
         storm_control = paynt.quotient.storm_pomdp_control.StormPOMDPControl()
@@ -193,7 +203,7 @@ def paynt_run(
 
 def print_profiler_stats(profiler):
     stats = pstats.Stats(profiler)
-    NUM_LINES = 20
+    NUM_LINES = 10
 
     logger.debug("cProfiler info:")
     stats.sort_stats('tottime').print_stats(NUM_LINES)

paynt/parser/sketch.py

@@ -2,7 +2,6 @@
 import payntbind
 
 import paynt.models.model_builder
-
 import paynt.quotient.quotient
 import paynt.quotient.mdp
 import paynt.quotient.pomdp
@@ -15,12 +14,12 @@
 from paynt.parser.prism_parser import PrismParser
 
 import uuid
+import os
+import json
 
 import logging
 logger = logging.getLogger(__name__)
 
-import os
-
 
 def substitute_suffix(string, delimiter, replacer):
     '''Subsitute the suffix behind the last delimiter.'''
@@ -88,7 +87,17 @@ def load_sketch(cls, sketch_path, properties_path,
                 explicit_quotient = paynt.models.model_builder.ModelBuilder.from_drn(sketch_path)
                 specification = PrismParser.parse_specification(properties_path, relative_error)
                 filetype = "drn"
-            except:
+                project_path = os.path.dirname(sketch_path)
+                valuations_path = project_path + "/state_valuations.json"
+                state_valuations = None
+                if os.path.exists(valuations_path) and os.path.isfile(valuations_path):
+                    with open(valuations_path) as file:
+                        state_valuations = json.load(file)
+                if state_valuations is not None:
+                    logger.info(f"found state_valuations.json, adding to the model...")
+                    explicit_quotient = payntbind.synthesis.addStateValuations(explicit_quotient,state_valuations)
+            except Exception as e:
+                print(e)
                 pass
         if filetype is None:
             try:
@@ -115,9 +124,8 @@ def load_sketch(cls, sketch_path, properties_path,
 
         assert filetype is not None, "unknow format of input file"
         logger.info("sketch parsing OK")
-
-        paynt.verification.property.Property.initialize()
 
+        paynt.verification.property.Property.initialize()
         updated = payntbind.synthesis.addMissingChoiceLabels(explicit_quotient)
         if updated is not None: explicit_quotient = updated
         if not payntbind.synthesis.assertChoiceLabelingIsCanonic(explicit_quotient.nondeterministic_choice_indices,explicit_quotient.choice_labeling,False):
@@ -139,7 +147,7 @@ def load_sketch(cls, sketch_path, properties_path,
             exit(0)
 
         return Sketch.build_quotient_container(prism, jani_unfolder, explicit_quotient, family, coloring, specification, obs_evaluator, decpomdp_manager)
-    
+
 
     @classmethod
     def load_sketch_as_all_in_one(cls, sketch_path, properties_path):