further results of debugging on large test sets

lib/splitting_tree.cpp

@@ -10,6 +10,7 @@
 #include <utility>
 #include <unordered_set>
 #include <tuple>
+#include <iostream>
 
 using namespace std;
 
@@ -91,7 +92,7 @@ unordered_set<state> is_valid_for(const size_t &N, const mealy &g, list<list<sta
 void add_push_new_block(deque<work_set> &work_list, list<list<state>> const &new_blocks, splitting_tree &boom,
                         unordered_set<state> &valid_list, bool update_valid_map)
 {
-    boom.children.push_back(vector<splitting_tree>());
+    boom.children.emplace_back();
     boom.children.back().assign(new_blocks.size(), splitting_tree(0, boom.depth + 1));
 
     size_t i = 0;
@@ -110,7 +111,7 @@ void add_push_new_block(deque<work_set> &work_list, list<list<state>> const &new
                 if (valid_list.count(s) > 0)
                     new_valid_list.emplace(s);
             }
-            if (new_valid_list.size() == 0)
+            if (new_valid_list.empty())
             {
                 //this means that none of the states of this child are actually valid for this split.
                 //this child will therefore never be used by the algorithm and can be pruned.
@@ -146,6 +147,13 @@ void add_push_new_block(deque<work_set> &work_list, list<list<state>> const &new
         }
     }
 
+    //todo: haal dit weg zodra bug gefixed is.
+    if(!boom.states.size() == accumulate(begin(boom.children.back()), end(boom.children.back()), 0ul,
+                                         [](size_t l, const splitting_tree &r)
+                                         {
+                                             return l + r.states.size();
+                                         }))
+        throw runtime_error("assert failed");
     assert(boom.children.size()==boom.separators.size());
     if(boom.children.size()>1)
         assert(boom.valid_map.size()>0);
@@ -154,6 +162,7 @@ void add_push_new_block(deque<work_set> &work_list, list<list<state>> const &new
                                             {
                                                 return l + r.states.size();
                                             }));
+
 };
 
 
@@ -197,7 +206,7 @@ splitting_tree create_splitting_tree(const mealy &g)
             {
                 if (new_block.size() != 1)
                 {
-                    if (valid_set.size() == 0)
+                    if (valid_set.empty())
                     {
                         return false;
                     } else
@@ -215,7 +224,7 @@ splitting_tree create_splitting_tree(const mealy &g)
     };
 
     // We'll start with the root, obviously
-    work_list.push_back(work_set(root, true));
+    work_list.emplace_back(root, true);
 
     while (!work_list.empty())
     {
@@ -237,6 +246,10 @@ splitting_tree create_splitting_tree(const mealy &g)
 
         if (boom.states.size() == 1) continue;
 
+        //todo: debug code. verwijder dit zodra bug gefixed is.
+        if(boom.states.size()==2 &&(boom.states[0]==2705 || boom.states[0]==2959))
+            bool test = true;
+
         //possible progress is splitted into tree different categories: on output, on state and force_progress.
         //for each loop iteration, only one of these three categories is executed. the choise depends on the value of some flags.
 
@@ -280,7 +293,7 @@ splitting_tree create_splitting_tree(const mealy &g)
             //the forced progress might open new options, for which we check first before we force progress again.
             force_progress = false;
 
-            assert(valid_set.size() == 0 || [&valid_set](splitting_tree & boom)
+            assert(valid_set.empty()|| [&valid_set](splitting_tree & boom)
             {
                 for (state s : valid_set)
                 {
@@ -299,7 +312,7 @@ splitting_tree create_splitting_tree(const mealy &g)
             unordered_set<state> targets;
             //an empty set actually means its valid for everything, but you cant delete states from an empty set.
             //So we explicitly fill it here.
-            if (valid_set.size() < 1)
+            if (valid_set.empty())
                 targets = unordered_set<state>(boom.states.begin(),boom.states.end());
             else
                 targets = unordered_set<state>(valid_set);
@@ -321,7 +334,7 @@ splitting_tree create_splitting_tree(const mealy &g)
 
             for (input symbol : all_inputs)
             {
-                const auto new_blocks = partition_(
+                auto new_blocks = partition_(
                         begin(boom.states),
                         end(boom.states), [symbol, depth, &g](state state)
                         {
@@ -356,8 +369,9 @@ splitting_tree create_splitting_tree(const mealy &g)
                     continue;
                 }
 
+                assert(new_blocks.size()>1);
                 // a succesful split, save the required information for later.
-                splits.push_back({{symbol},move(new_blocks),move(new_valid_set)});
+                splits.emplace_back(vector(1,symbol),move(new_blocks),move(new_valid_set));
                 if(updated_separator)
                 {
                     best_split_index = splits.size()-1;
@@ -365,7 +379,7 @@ splitting_tree create_splitting_tree(const mealy &g)
 
 
                 //if a valid split has been found for all the targets the work is done and progression is made.
-                if (targets.size() == 0)
+                if (targets.empty())
                     goto has_split;
             }
 
@@ -389,8 +403,8 @@ splitting_tree create_splitting_tree(const mealy &g)
                 if (oboom.children.empty()) continue;
 
                 // possibly a succesful split, construct the children
-                const vector<input> word = concat(vector<input>(1, symbol), oboom.get_separator(valid_target_image));
-                const list<list<state>> new_blocks = partition_(
+                vector<input> word = concat(vector<input>(1, symbol), oboom.get_separator(valid_target_image));
+                list<list<state>> new_blocks = partition_(
                         begin(boom.states),
                         end(boom.states), [word, depth, &g](state state)
                         {
@@ -422,13 +436,13 @@ splitting_tree create_splitting_tree(const mealy &g)
                 assert(new_blocks.size() > 1);
 
                 // a succesful split, save the required information for later.
-                splits.push_back({move(word),move(new_blocks),move(new_valid_set)});
+                splits.emplace_back(move(word),move(new_blocks),move(new_valid_set));
                 if(updated_separator)
                 {
                     best_split_index = splits.size()-1;
                 }
 
-                if (targets.size() == 0)
+                if (targets.empty())
                     break;
 
             }
@@ -437,7 +451,7 @@ splitting_tree create_splitting_tree(const mealy &g)
             //there might however still be states left in targets for which there was no valid split.
             //for these states we use the recorded best general split so far instead.
 
-            //if the best general split is already queued, update ists valid_list to include the remaining targets.
+            //if the best general split is already queued, update its valid_list to include the remaining targets.
             if(best_split_index !=-1)
             {
                 for(state s : targets)
@@ -445,6 +459,24 @@ splitting_tree create_splitting_tree(const mealy &g)
                     get<2>(splits[best_split_index]).emplace(s);
                 }
 
+            } else if(best_separator.empty())
+            {
+                //if we get here then there was not a single input that could split any of the states from the others on either output state or output symbol.
+                //there are only two possible ways that this can happen. 1: the two states are equal, or 2: they could be split on output state but the work needed to
+                //determine the required separator is still in the work_list.
+                //option 1 is excluded because the specification is reduced and the names of the states differ.
+                //to resolve the problem we postpone this split and try to force progress elsewere first.
+                force_progress = true;
+                days_without_progress++;
+                //make sure we wont endlessly run in circles.
+                if(days_without_progress<= 3*work_list.size())
+                {
+                    //if we get here then the algorithm has failed.
+                    //we return the root anyway so we can inspect the partial solution in the output file.
+                    return root;
+                }
+                goto has_no_split;
+
             } else
             {
                 //if not, then queue it now using the stored info.
@@ -452,7 +484,8 @@ splitting_tree create_splitting_tree(const mealy &g)
                 {
                     best_seperator_valid_set.emplace(s);
                 }
-                splits.push_back(make_tuple(move(best_separator),move(best_separator_blocks),move(best_seperator_valid_set)));
+                assert(best_separator_blocks.size()>1);
+                splits.emplace_back(move(best_separator),move(best_separator_blocks),move(best_seperator_valid_set));
             }
 
             //push all the defined splits into the work_list now.
@@ -520,7 +553,7 @@ splitting_tree create_splitting_tree(const mealy &g)
 
         has_no_split:
         //no valid splits on the current work_set. put it back and try the next one.
-        work_list.push_back(work_set(boom, move(valid_set), false));
+        work_list.emplace_back(boom, move(valid_set), false);
 
         continue;
 

src/main.cpp

@@ -64,7 +64,7 @@ struct main_options {
 	//"coffe_machine.dot";
 	//"lee_yannakakis_difficult.dot";
 	//"lee_yannakakis_distinguishable.dot";
-	string input_filename = input_directory+"model3.dot";
+	string input_filename = input_directory+"esm-manual-controller.dot";
 	string output_filename = "";
 };