sanity checks for family split

paynt/quotient/mdp.py

@@ -278,7 +278,7 @@ class MdpQuotient(paynt.quotient.quotient.Quotient):
     # if true, an explicit action executing a random choice of an available action will be added to each state
     add_dont_care_action = False
     # if true, irrelevant states will not be considered for tree mapping
-    filter_deterministic_states = False
+    filter_deterministic_states = True
 
     @classmethod
     def get_state_valuations(cls, model):
@@ -497,10 +497,6 @@ def build_unsat_result(self):
         return spec_result
 
     def build(self, family):
-        # logger.debug("building sub-MDP...")
-        # print("\nfamily = ", family, flush=True)
-        # family.parent_info = None
-
         if family.parent_info is None:
             choices = self.coloring.selectCompatibleChoices(family.family)
         else:
@@ -515,25 +511,24 @@ def build(self, family):
 
     def are_choices_consistent(self, choices, family):
         ''' Separate method for profiling purposes. '''
-        return self.coloring.areChoicesConsistent(choices, family.family)
+        consistent,hole_selection = self.coloring.areChoicesConsistent(choices, family.family)
+        for hole,options in enumerate(hole_selection):
+            assert len(options) == len(set(options)), str(hole_selection)
+            for option in options:
+                assert option in family.hole_options(hole), \
+                f"option {option} for hole {hole} ({mdp.family.hole_name(hole)}) is not in the family"
+        return consistent,hole_selection
 
 
     def scheduler_is_consistent(self, mdp, prop, result):
         ''' Get hole options involved in the scheduler selection. '''
-
         scheduler = result.scheduler
         assert scheduler.memoryless and scheduler.deterministic
         state_to_choice = self.scheduler_to_state_to_choice(mdp, scheduler)
         choices = self.state_to_choice_to_choices(state_to_choice)
         if self.specification.is_single_property:
             mdp.family.scheduler_choices = choices
         consistent,hole_selection = self.are_choices_consistent(choices, mdp.family)
-
-        for hole,options in enumerate(hole_selection):
-            for option in options:
-                assert option in mdp.family.hole_options(hole), \
-                f"option {option} for hole {hole} ({mdp.family.hole_name(hole)}) is not in the family"
-
         return hole_selection, consistent
 
 
@@ -600,6 +595,7 @@ def split(self, family):
         parent_info.scheduler_choices = family.scheduler_choices
         # parent_info.unsat_core_hint = self.coloring.unsat_core.copy()
         subfamilies = family.split(splitter,suboptions)
+        assert family.size == sum([family.size for family in subfamilies])
         for subfamily in subfamilies:
             subfamily.add_parent_info(parent_info)
         return subfamilies

payntbind/src/synthesis/quotient/ColoringSmt.cpp

@@ -162,18 +162,14 @@ ColoringSmt<ValueType>::ColoringSmt(
 
             timers["ColoringSmt::1-3-2"].start();
             for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) {
-                timers["ColoringSmt::1-3-2-1"].start();
                 uint64_t num_clauses = getRoot()->paths[path].size()-1;
                 uint64_t action = choice_to_action[choice];
                 clause_array[num_clauses++] = terminals[path]->action_expression[action];
-                timers["ColoringSmt::1-3-2-1"].stop();
-                timers["ColoringSmt::1-3-2-2"].start();
                 if(action == dont_care_action) {
                     for(uint64_t unavailable_action: ~state_available_actions[state]) {
                         clause_array[num_clauses++] = terminals[path]->action_expression[unavailable_action];
                     }
                 }
-                timers["ColoringSmt::1-3-2-2"].stop();
                 choice_path_expresssion[choice].push_back(z3::expr(ctx, Z3_mk_or(ctx, num_clauses, clause_array.ptr())));
                 // choice_path_expresssion[choice].push_back(Z3_mk_or(ctx, num_clauses, clause_array.ptr()));
             }
@@ -381,8 +377,8 @@ BitVector ColoringSmt<ValueType>::selectCompatibleChoices(Family const& subfamil
                 // iterate over paths
                 for(uint64_t path: state_path_enabled[state]) {
                     uint64_t path_hole = path_action_hole[path];
-                    choice_enabled = subfamily.holeContains(path_hole,action);
                     // enable the choice if this action is the family
+                    choice_enabled = subfamily.holeContains(path_hole,action);
                     if(not choice_enabled and action == this->dont_care_action) {
                         // don't-care action can also be enabled if any unavailable action is in the family
                         for(uint64_t unavailable_action: ~state_available_actions[state]) {
@@ -655,6 +651,8 @@ std::pair<bool,std::vector<std::vector<uint64_t>>> ColoringSmt<ValueType>::areCh
     return std::make_pair(false,hole_options_vector);
 }
 
+template<typename ValueType>
+std::map<std::string,storm::utility::Stopwatch> ColoringSmt<ValueType>::timers;
 
 template class ColoringSmt<>;
 

payntbind/src/synthesis/quotient/ColoringSmt.h

@@ -78,7 +78,7 @@ class ColoringSmt {
         BitVector const& choices, Family const& subfamily
     );
 
-    std::map<std::string,storm::utility::Stopwatch> timers;
+    static std::map<std::string,storm::utility::Stopwatch> timers;
     std::vector<std::pair<std::string,double>> getProfilingInfo() {
         std::vector<std::pair<std::string,double>> profiling;
         for(auto const& [method,timer]: timers) {

payntbind/src/synthesis/quotient/TreeNode.cpp

@@ -168,7 +168,7 @@ uint64_t TerminalNode::getPathActionHole(std::vector<bool> const& path) {
 
 void TerminalNode::substituteActionExpressions() {
     for(uint64_t action = 0; action < num_actions; ++action) {
-        action_expression.push_back(action_hole.solver_variable == (int)action);
+        action_expression.push_back(action_hole.solver_variable == ctx.int_val(action));
     }
 }
 
@@ -389,26 +389,30 @@ void InnerNode::createPrefixSubstitutionsHarmonizing(std::vector<uint64_t> const
     for(uint64_t var = 0; var < numVariables(); ++var) {
         z3::expr const& vv = variable_hole[var].solver_variable;
         z3::expr const& state_var = state_valuation_int[var];
-        clauses_true[var] = ( not(decision_harm_is_variable[var] and state_var <= vv));
+        // clauses_true[var] = ( not(decision_harm_is_variable[var] and state_var <= vv));
+        clauses_true[var] = ( decision_harm_is_variable[var] and not(state_var <= vv) );
         array_true[var] = clauses_true[var];
-        clauses_false[var] = (not(decision_harm_is_variable[var] and state_var  > vv));
+        // clauses_false[var] = (not(decision_harm_is_variable[var] and state_var  > vv));
+        clauses_false[var] = ( decision_harm_is_variable[var] and not(state_var  > vv) );
         array_false[var] = clauses_false[var];
     }
-    harm_decision_true =  harmonizing_variable == ctx.int_val(decision_hole.hole) and z3::expr(ctx, Z3_mk_and(ctx, numVariables(), array_true.ptr()) );
-    harm_decision_false = harmonizing_variable == ctx.int_val(decision_hole.hole) and z3::expr(ctx, Z3_mk_and(ctx, numVariables(), array_false.ptr()) );
+    harm_decision_true =  harmonizing_variable == ctx.int_val(decision_hole.hole) and z3::expr(ctx, Z3_mk_or(ctx, numVariables(), array_true.ptr()) );
+    harm_decision_false = harmonizing_variable == ctx.int_val(decision_hole.hole) and z3::expr(ctx, Z3_mk_or(ctx, numVariables(), array_false.ptr()) );
 
     for(uint64_t var = 0; var < numVariables(); ++var) {
         Hole const& hole = variable_hole[var];
         z3::expr const& vv = variable_hole[var].solver_variable;
         z3::expr const& vvh = variable_hole[var].solver_variable_harm;
         z3::expr const& state_var = state_valuation_int[var];
-        clauses_true[var] = (not(decision_is_variable[var] and state_var <= vv) or (harm_is_hole[var] and not(state_var <= vvh) ) );
+        // clauses_true[var] = (not(decision_is_variable[var] and state_var <= vv) or (harm_is_hole[var] and not(state_var <= vvh) ) );
+        clauses_true[var] = decision_is_variable[var] and (not (state_var <= vv) or (harm_is_hole[var] and not(state_var <= vvh) ));
         array_true[var] = clauses_true[var];
-        clauses_false[var] = (not(decision_is_variable[var] and state_var  > vv) or (harm_is_hole[var] and not(state_var >  vvh) ) );
+        // clauses_false[var] = (not(decision_is_variable[var] and state_var  > vv) or (harm_is_hole[var] and not(state_var >  vvh) ) );
+        clauses_false[var] = decision_is_variable[var] and (not (state_var > vv) or (harm_is_hole[var] and not(state_var > vvh) ));
         array_false[var] = clauses_false[var];
     }
-    substituted_true = harm_decision_true or z3::expr(ctx, Z3_mk_and(ctx, numVariables(), array_true.ptr()) );
-    substituted_false = harm_decision_false or z3::expr(ctx, Z3_mk_and(ctx, numVariables(), array_false.ptr()) );
+    substituted_true = harm_decision_true or z3::expr(ctx, Z3_mk_or(ctx, numVariables(), array_true.ptr()) );
+    substituted_false = harm_decision_false or z3::expr(ctx, Z3_mk_or(ctx, numVariables(), array_false.ptr()) );
 
     child_true->createPrefixSubstitutionsHarmonizing(state_valuation, state_valuation_int, harmonizing_variable);
     child_false->createPrefixSubstitutionsHarmonizing(state_valuation, state_valuation_int, harmonizing_variable);