Merge branch 'randriu:master' into master

paynt/cli.py

@@ -9,7 +9,6 @@
 import paynt.quotient.storm_pomdp_control
 import paynt.quotient.mdp
 
-import paynt.synthesizer.all_in_one
 import paynt.synthesizer.synthesizer
 import paynt.synthesizer.synthesizer_cegis
 import paynt.synthesizer.policy_tree
@@ -114,13 +113,6 @@ def setup_logger(log_path = None):
 @click.option("--export-evaluation", type=click.Path(), default=None,
     help="base filename to output evaluation result")
 
-@click.option(
-    "--all-in-one", type=click.Choice(["sparse", "bdd"]), default=None, show_default=True,
-    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")
 @click.option("--mdp-discard-unreachable-choices", is_flag=True, default=False,
@@ -157,7 +149,6 @@ 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_maxmem,
     mdp_split_wrt_mdp, mdp_discard_unreachable_choices, mdp_use_randomized_abstraction,
     tree_depth, tree_enumeration, add_dont_care_action,
     constraint_bound,
@@ -198,14 +189,10 @@ def paynt_run(
 
     sketch_path = os.path.join(project, sketch)
     properties_path = os.path.join(project, props)
-    if all_in_one is None:
-        quotient = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path, export, relative_error, precision, constraint_bound)
-        synthesizer = paynt.synthesizer.synthesizer.Synthesizer.choose_synthesizer(quotient, method, fsc_synthesis, storm_control)
-        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, all_in_one_maxmem, family)
-        all_in_one_analysis.run()
+    quotient = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path, export, relative_error, precision, constraint_bound)
+    synthesizer = paynt.synthesizer.synthesizer.Synthesizer.choose_synthesizer(quotient, method, fsc_synthesis, storm_control)
+    synthesizer.run(optimum_threshold)
+
     if profiling:
         profiler.disable()
         print_profiler_stats(profiler)

paynt/parser/sketch.py

@@ -132,7 +132,7 @@ def load_sketch(cls, sketch_path, properties_path,
             logger.warning("WARNING: choice labeling for the quotient is not canonic")
 
         make_rewards_action_based(explicit_quotient)
-        logger.debug("constructed explicit quotient having {} states and {} actions".format(
+        logger.debug("constructed explicit quotient having {} states and {} choices".format(
             explicit_quotient.nr_states, explicit_quotient.nr_choices))
 
         specification.check()

paynt/synthesizer/decision_tree.py

@@ -14,13 +14,11 @@ class SynthesizerDecisionTree(paynt.synthesizer.synthesizer_ar.SynthesizerAR):
     tree_depth = 0
     # if set, all trees of size at most tree_depth will be enumerated
     tree_enumeration = False
-    # TODO
+    # if set, the optimal k-tree will be used to jumpstart the synthesis of the (k+1)-tree
     use_tree_hint = True
 
     def __init__(self, *args):
         super().__init__(*args)
-        self.tree_hint = None
-        self.tree_hint_size = None
 
     @property
     def method_name(self):
@@ -46,12 +44,6 @@ def verify_hole_selection(self, family, hole_selection):
             family.analysis_result.can_improve = True
             self.update_optimum(family)
 
-            family_value = family.analysis_result.optimality_result.primary.value
-            if(abs(family_value-assignment_value) < 1e-3):
-                # logger.info(f"harmonization leads to family skip")
-                self.num_harmonization_skip += 1
-                family.analysis_result.can_improve = False
-
 
     def harmonize_inconsistent_scheduler(self, family):
         self.num_harmonizations += 1
@@ -93,80 +85,55 @@ def verify_family(self, family):
             return
         self.harmonize_inconsistent_scheduler(family)
 
+    def counters_reset(self):
+        self.num_families_considered = 0
+        self.num_families_skipped = 0
+        self.num_families_model_checked = 0
+        self.num_schedulers_preserved = 0
+        self.num_harmonizations = 0
+        self.num_harmonization_succeeded = 0
 
-    def presplit(self, subfamily):
-        family = self.quotient.family
-
-        # fix subfamily first
-        for hole in range(family.num_holes):
-            all_options = family.hole_options(hole)
-            if subfamily.hole_num_options(hole) == family.hole_num_options(hole):
-                continue
-            if not self.quotient.is_variable_hole[hole]:
-                continue
-            options = [option for option in all_options if option<=subfamily.hole_options(hole)[0]]
-            subfamily.hole_set_options(hole,options)
-
-        subfamilies = [subfamily]
-        prototype_family = subfamily.copy()
-        for hole in range(family.num_holes):
-            if prototype_family.hole_num_options(hole) == family.hole_num_options(hole):
-                continue;
-            prototype_options = prototype_family.hole_options(hole)
-            suboptions_list = []
-            all_options = family.hole_options(hole)
-            if not self.quotient.is_variable_hole[hole]:
-                complement = [option for option in all_options if option not in prototype_options]
-                suboptions_list.append(complement)
-            else:
-                complement = [option for option in all_options if option>prototype_options[-1]]
-                if len(complement)>0:
-                    suboptions_list.append(complement)
-
-            for suboptions in suboptions_list:
-                new_subfamily = prototype_family.copy()
-                new_subfamily.hole_set_options(hole,suboptions)
-                subfamilies.append(new_subfamily)
-            prototype_family.hole_set_options(hole,all_options)
-        return subfamilies
+    def counters_print(self):
+        logger.info(f"families considered: {self.num_families_considered}")
+        logger.info(f"families skipped by construction: {self.num_families_skipped}")
+        logger.info(f"families with schedulers preserved: {self.num_schedulers_preserved}")
+        logger.info(f"families model checked: {self.num_families_model_checked}")
+        logger.info(f"harmonizations attempted: {self.num_harmonizations}")
+        logger.info(f"harmonizations succeeded: {self.num_harmonization_succeeded}")
+        print()
 
     def synthesize_tree(self, depth:int):
+        self.counters_reset()
         self.quotient.set_depth(depth)
         self.synthesize(keep_optimum=True)
+        self.counters_print()
 
     def synthesize_tree_sequence(self, opt_result_value):
-        self.tree_hint = None
-
+        tree_hint = None
         for depth in range(SynthesizerDecisionTree.tree_depth+1):
+            print()
             self.quotient.set_depth(depth)
             best_assignment_old = self.best_assignment
 
             family = self.quotient.family
             self.explored = 0
+            self.counters_reset()
             self.stat = paynt.synthesizer.statistic.Statistic(self)
-            print()
             self.stat.start(family)
+            self.synthesis_timer = paynt.utils.timer.Timer()
+            self.synthesis_timer.start()
             families = [family]
 
-            if self.tree_hint is not None and SynthesizerDecisionTree.use_tree_hint:
+            if SynthesizerDecisionTree.use_tree_hint and tree_hint is not None:
                 subfamily = family.copy()
-                # find the correct application point
-                application_node = self.quotient.decision_tree.root
-                # for _ in range(self.tree_hint_size,depth):
-                #     application_node = application_node.child_true
-                application_node.apply_hint(subfamily,self.tree_hint)
-
-                # presplit
-                # families = self.presplit(subfamily)
-                # assert family.size == sum([f.size for f in families])
-
-                # hint,
+                self.quotient.decision_tree.root.apply_hint(subfamily,tree_hint)
                 families = [subfamily,family]
 
             for family in families:
                 self.synthesize_one(family)
             self.stat.finished_synthesis()
             self.stat.print()
+            self.counters_print()
 
             new_assignment_synthesized = self.best_assignment != best_assignment_old
             if new_assignment_synthesized:
@@ -181,29 +148,19 @@ def synthesize_tree_sequence(self, opt_result_value):
                 if abs( (self.best_assignment_value-opt_result_value)/opt_result_value ) < 1e-3:
                     break
 
-                self.tree_hint = self.quotient.decision_tree.root
-                self.tree_hint.associate_assignment(self.best_assignment)
-                self.tree_hint_size = depth
+                tree_hint = self.quotient.decision_tree.root
+                tree_hint.associate_assignment(self.best_assignment)
 
             if self.resource_limit_reached():
                 break
 
 
-
-    def run(self, optimum_threshold=None, export_evaluation=None):
+    def run(self, optimum_threshold=None):
         paynt_mdp = paynt.models.models.Mdp(self.quotient.quotient_mdp)
         mc_result = paynt_mdp.model_check_property(self.quotient.get_property())
         opt_result_value = mc_result.value
         logger.info(f"the optimal scheduler has value: {opt_result_value}")
 
-        self.num_families_considered = 0
-        self.num_families_skipped = 0
-        self.num_families_model_checked = 0
-        self.num_schedulers_preserved = 0
-        self.num_harmonizations = 0
-        self.num_harmonization_succeeded = 0
-        self.num_harmonization_skip = 0
-
         if self.quotient.specification.has_optimality:
             epsilon = 1e-1
             mc_result_positive = opt_result_value > 0
@@ -228,28 +185,11 @@ def run(self, optimum_threshold=None, export_evaluation=None):
         else:
             logger.info("no admissible assignment found")
         time_total = paynt.utils.timer.GlobalTimer.read()
-        logger.info(f"synthesis time: {round(time_total, 2)} s")
-
-        print()
-        logger.info(f"families considered: {self.num_families_considered}")
-        logger.info(f"families skipped by construction: {self.num_families_skipped}")
-        logger.info(f"families with schedulers preserved: {self.num_schedulers_preserved}")
-        logger.info(f"families model checked: {self.num_families_model_checked}")
-        logger.info(f"harmonizations attempted: {self.num_harmonizations}")
-        logger.info(f"harmonizations succeeded: {self.num_harmonization_succeeded}")
-        logger.info(f"harmonizations lead to family skip: {self.num_harmonization_skip}")
+        # logger.info(f"synthesis time: {round(time_total, 2)} s")
 
         print()
         for name,time in self.quotient.coloring.getProfilingInfo():
             time_percent = round(time/time_total*100,1)
             print(f"{name} = {time} s ({time_percent} %)")
-        print()
-
-        # splits_total = sum(self.quotient.splitter_count)
-        # if splits_total == 0: splits_total = 1
-        # splitter_freq = [ round(splits/splits_total*100,1) for splits in self.quotient.splitter_count]
-        # for hole,freq in enumerate(splitter_freq):
-        #     print(self.quotient.family.hole_name(hole),freq)
-        # print()
 
         return self.best_assignment

paynt/synthesizer/policy_tree.py

@@ -790,6 +790,11 @@ def evaluate_all(self, family, prop, keep_value_only=False):
             evaluations.append(evaluation)
         return evaluations
 
+
+    def run(self, optimum_threshold=None):
+        return self.evaluate(export_filename_base=None)
+
+
     def export_evaluation_result(self, evaluations, export_filename_base):
         import json
         policies = self.policy_tree.extract_policies(self.quotient)

paynt/synthesizer/synthesizer.py

@@ -197,8 +197,5 @@ def synthesize(
         return assignment
 
 
-    def run(self, optimum_threshold=None, export_evaluation=None):
-        if isinstance(self.quotient, paynt.quotient.mdp_family.MdpFamilyQuotient):
-            return self.evaluate(export_filename_base=export_evaluation)
-        else:
-            return self.synthesize(optimum_threshold=optimum_threshold)
+    def run(self, optimum_threshold=None):
+        return self.synthesize(optimum_threshold=optimum_threshold)

paynt/synthesizer/synthesizer_ar.py

@@ -100,7 +100,7 @@ def update_optimum(self, family):
         self.quotient.specification.optimality.update_optimum(iv)
         self.best_assignment = ia
         self.best_assignment_value = iv
-        logger.info(f"value {round(iv,4)} achieved after {round(self.synthesis_timer.read(),2)} seconds")
+        # logger.info(f"value {round(iv,4)} achieved after {round(paynt.utils.timer.GlobalTimer.read(),2)} seconds")
         if isinstance(self.quotient, paynt.quotient.pomdp.PomdpQuotient):
             self.stat.new_fsc_found(family.analysis_result.improving_value, ia, self.quotient.policy_size(ia))
 

paynt/synthesizer/synthesizer_decpomdp.py

@@ -54,7 +54,7 @@ def strategy_iterative(self, unfold_imperfect_only):
             mem_size += 1
 
             #break
-
 
-    def run(self, optimum_threshold=None, export_evaluation=None):
+
+    def run(self, optimum_threshold=None):
         self.strategy_iterative(unfold_imperfect_only=True)

paynt/synthesizer/synthesizer_pomdp.py

@@ -366,7 +366,7 @@ def strategy_iterative(self, unfold_imperfect_only):
             #break
 
 
-    def run(self, optimum_threshold=None, export_evaluation=None):
+    def run(self, optimum_threshold=None):
         # choose the synthesis strategy:
         if self.use_storm:
             logger.info("Storm POMDP option enabled")

paynt/verification/property.py

@@ -141,9 +141,7 @@ def transform_until_to_eventually(self):
         self.__init__(prop)
 
     def property_copy(self):
-        formula_copy = self.formula.clone()
-        property_copy = stormpy.core.Property(self.name, formula_copy)
-        return property_copy
+        return stormpy.core.Property(self.name, self.property.raw_formula.clone())
 
     def copy(self):
         return Property(self.property_copy())

payntbind/src/synthesis/quotient/ColoringSmt.cpp

@@ -372,8 +372,7 @@ void ColoringSmt<ValueType>::loadUnsatCore(z3::expr_vector const& unsat_core_exp
         std::istringstream iss(expr.decl().name().str());
         char prefix; iss >> prefix;
         if(prefix == 'h' or prefix == 'z') {
-            // uint64_t hole; iss >> hole;
-            // this->unsat_core.emplace_back(hole,numPaths());
+            // uint64_t hole; iss >> prefix; iss >> hole;
             continue;
         }
         // prefix == 'p'
@@ -481,19 +480,41 @@ std::pair<bool,std::vector<std::vector<uint64_t>>> ColoringSmt<ValueType>::areCh
     if(PRINT_UNSAT_CORE)
         std::cout << "-- unsat core start --" << std::endl;
     timers["areChoicesConsistent::3 unsat core analysis"].start();
-    solver.push();
     for(auto [choice,path]: this->unsat_core) {
         const char *label = choice_path_label[choice][path].c_str();
         solver.add(choice_path_expresssion_harm[choice][path], label);
     }
+
+    z3::model model(ctx);
+
+    /*z3::expr_vector harmonizing_variable_domain(ctx);
+    for(uint64_t hole: harmonizing_hole_hint) {
+        harmonizing_variable_domain.push_back(harmonizing_variable == (int)hole);
+    }
+    solver.add(z3::mk_or(harmonizing_variable_domain), "harmonizing_domain");*/
+
+    /*bool harmonizing_hole_found = false;
+    for(uint64_t hole = 0; hole < family.numHoles(); ++hole) {
+        solver.push();
+        solver.add(harmonizing_variable == (int)hole, "harmonizing_domain");
+        if(check()) {
+            harmonizing_hole_found = true;
+            model = solver.get_model();
+            solver.pop();
+            break;
+        }
+        solver.pop();
+    }
+    STORM_LOG_THROW(harmonizing_hole_found, storm::exceptions::UnexpectedException, "harmonized UNSAT core is not SAT");*/
+
     solver.add(0 <= harmonizing_variable and harmonizing_variable < family.numHoles(), "harmonizing_domain");
     consistent = check();
     STORM_LOG_THROW(consistent, storm::exceptions::UnexpectedException, "harmonized UNSAT core is not SAT");
-    z3::model model = solver.get_model();
-    solver.pop();
-    solver.pop();
+    model = solver.get_model();
 
+    solver.pop();
     uint64_t harmonizing_hole = model.eval(harmonizing_variable).get_numeral_uint64();
+
     getRoot()->loadHoleAssignmentFromModel(model,hole_options_vector);
     getRoot()->loadHoleAssignmentFromModelHarmonizing(model,hole_options_vector,harmonizing_hole);
     if(hole_options_vector[harmonizing_hole][0] > hole_options_vector[harmonizing_hole][1]) {

payntbind/src/synthesis/quotient/ColoringSmt.h

@@ -133,7 +133,6 @@ class ColoringSmt {
     /** Check whether (in the subfamily) the choice is enabled. */
     bool isChoiceEnabled(Family const& subfamily, uint64_t state, uint64_t choice);
 
-    /** TODO */
     bool PRINT_UNSAT_CORE = false;
     void loadUnsatCore(z3::expr_vector const& unsat_core_expr, Family const& subfamily);