Splits the main file in more files.

lib/adaptive_distinguishing_sequence.hpp

@@ -0,0 +1,23 @@
+#pragma once
+
+#include "mealy.hpp"
+
+#include <vector>
+#include <utility>
+
+struct dist_seq {
+	dist_seq(size_t N, size_t depth)
+	: CI(N)
+	, depth(depth)
+	{
+		for(size_t i = 0; i < N; ++i)
+			CI[i] = {i, i};
+	}
+
+	// current, initial
+	std::vector<std::pair<state, state>> CI;
+	std::vector<input> word;
+	std::vector<dist_seq> children;
+	size_t depth;
+};
+

lib/create_adaptive_distinguishing_sequence.cpp

@@ -0,0 +1,85 @@
+#include "create_adaptive_distinguishing_sequence.hpp"
+#include "logging.hpp"
+#include "splitting_tree.hpp"
+
+#include <algorithm>
+#include <functional>
+#include <iostream>
+#include <queue>
+#include <vector>
+
+using namespace std;
+
+result2 create_adaptive_distinguishing_sequence(const result & splitting_tree){
+	const auto & root = splitting_tree.root;
+	const auto & succession = splitting_tree.successor_cache;
+	const auto N = root.states.size();
+
+	result2 r(N);
+	auto & root_seq = r.sequence;
+
+	{
+		queue<reference_wrapper<dist_seq>> work2;
+		work2.push(root_seq);
+
+		while(!work2.empty()){
+			dist_seq & node = work2.front();
+			work2.pop();
+
+			if(node.CI.size() < 2) continue;
+			if(node.depth > 500) continue;
+
+			vector<bool> states(N, false);
+			for(auto && state : node.CI){
+				states[state.first.base()] = true;
+			}
+
+			const auto & oboom = lca(root, [&states](state state) -> bool{
+				return states[state.base()];
+			});
+
+			if(oboom.children.empty()) continue;
+
+			node.word = oboom.seperator;
+			for(auto && c : oboom.children){
+				dist_seq new_c(0, node.depth + 1);
+
+				size_t i = 0;
+				size_t j = 0;
+
+				while(i < node.CI.size() && j < c.states.size()){
+					if(node.CI[i].first < c.states[j]) {
+						i++;
+					} else if(node.CI[i].first > c.states[j]) {
+						j++;
+					} else {
+						const auto curr = succession[oboom.depth][node.CI[i].first.base()];
+						const auto init = node.CI[i].second;
+						new_c.CI.push_back({curr, init});
+						i++;
+						j++;
+					}
+				}
+
+				// woops. fixme
+				sort(begin(new_c.CI), end(new_c.CI));
+
+				if(!new_c.CI.empty()){
+					node.children.push_back(move(new_c));
+				}
+			}
+
+			// FIXME: can not happen????
+			if(node.children.size() == 1) {
+				fire_once([]{ cerr << "WARNING: Only one child in dist seq\n"; });
+				continue;
+			}
+
+			for(auto & c : node.children) {
+				work2.push(c);
+			}
+		}
+	}
+
+	return r;
+}

lib/create_adaptive_distinguishing_sequence.hpp

@@ -0,0 +1,16 @@
+#pragma once
+
+#include "adaptive_distinguishing_sequence.hpp"
+#include "create_splitting_tree.hpp"
+
+struct result2 {
+	result2(size_t N)
+	: sequence(N, 0)
+	{}
+
+	// The adaptive distinguishing sequence as described in Lee & Yannakakis
+	// This is really a tree!
+	dist_seq sequence;
+};
+
+result2 create_adaptive_distinguishing_sequence(result const & splitting_tree);

lib/create_splitting_tree.cpp

@@ -0,0 +1,153 @@
+#include "create_splitting_tree.hpp"
+#include "logging.hpp"
+
+#include <functional>
+#include <iostream>
+#include <queue>
+#include <utility>
+
+using namespace std;
+
+template <typename T>
+std::vector<T> concat(std::vector<T> const & l, std::vector<T> const & r){
+	std::vector<T> ret(l.size() + r.size());
+	auto it = copy(begin(l), end(l), begin(ret));
+	copy(begin(r), end(r), it);
+	return ret;
+}
+
+result create_splitting_tree(const Mealy& g){
+	const auto N = g.graph.size();
+	const auto P = g.input_indices.size();
+	const auto Q = g.output_indices.size();
+
+	result r(N);
+	auto & part = r.partition;
+	auto & root = r.root;
+	auto & succession = r.successor_cache;
+
+	/* We'll use a queue to keep track of leaves we have to investigate;
+	 * In some cases we cannot split, and have to wait for other parts of the
+	 * tree. We keep track of how many times we did no work. If this is too
+	 * much, there is no complete splitting tree.
+	 */
+	queue<pair<partition_refine::BlockRef, reference_wrapper<splijtboom>>> work;
+	size_t days_without_progress = 0;
+
+	// Some lambda functions capturing some state, makes the code a bit easier :)
+	const auto push = [&work](auto br, auto & sp) { work.push({br, sp}); };
+	const auto pop = [&work]() { const auto r = work.front(); work.pop(); return r; };
+	const auto add_push_new_block = [&](auto new_blocks, auto & boom) {
+		const auto nb = distance(new_blocks.first, new_blocks.second);
+		boom.children.assign(nb, splijtboom(0, boom.depth + 1));
+
+		auto i = 0;
+		while(new_blocks.first != new_blocks.second){
+			for(auto && s : *new_blocks.first){
+				boom.children[i].states.push_back(s);
+			}
+
+			push(new_blocks.first++, boom.children[i++]);
+		}
+	};
+	const auto is_valid = [N, &g](auto blocks, auto symbol){
+		for(auto && block : blocks) {
+			partition_refine s_part(block);
+			const auto new_blocks = s_part.refine(*s_part.begin(), [symbol, &g](state state){
+				return apply(g, state, symbol).to.base();
+			}, N);
+			for(auto && new_block : new_blocks){
+				if(distance(new_block.begin(), new_block.end()) != 1) return false;
+			}
+		}
+		return true;
+	};
+	const auto update_succession = [N, &succession](state s, state t, size_t depth){
+		if(succession.size() < depth+1) succession.resize(depth+1, vector<state>(N, -1));
+		succession[depth][s.base()] = t;
+	};
+
+	// We'll start with the root, obviously
+	push(part.begin(), root);
+	while(!work.empty()){
+		const auto block_boom = pop();
+		const auto block = block_boom.first;
+		splijtboom & boom = block_boom.second;
+		const auto depth = boom.depth;
+
+		if(boom.states.size() == 1) continue;
+
+		// First try to split on output
+		for(input symbol = 0; symbol < P; ++symbol){
+			const auto new_blocks = part.refine(*block, [symbol, depth, &g, &update_succession](state state){
+				const auto ret = apply(g, state, symbol);
+				update_succession(state, ret.to, depth);
+				return ret.output.base();
+			}, Q);
+
+			// no split -> continue with other input symbols
+			if(new_blocks.size() == 1) continue;
+
+			// not a valid split -> continue
+			if(!is_valid(new_blocks, symbol)) continue;
+
+			// a succesful split, update partition and add the children
+			boom.seperator = {symbol};
+			const auto range = part.replace(block, move(new_blocks));
+			add_push_new_block(range, boom);
+
+			goto has_split;
+		}
+
+		// Then try to split on state
+		for(input symbol = 0; symbol < P; ++symbol){
+			vector<bool> successor_states(N, false);
+			for(auto && state : *block){
+				successor_states[apply(g, state, symbol).to.base()] = true;
+			}
+
+			const auto & oboom = lca(root, [&successor_states](state state) -> bool{
+				return successor_states[state.base()];
+			});
+
+			// a leaf, hence not a split -> try other symbols
+			if(oboom.children.empty()) continue;
+
+			// possibly a succesful split, construct the children
+			const auto word = concat({symbol}, oboom.seperator);
+			const auto new_blocks = part.refine(*block, [word, depth, &g, &update_succession](state state){
+				const auto ret = apply(g, state, begin(word), end(word));
+				update_succession(state, ret.to, depth);
+				return ret.output.base();
+			}, Q);
+
+			// not a valid split -> continue
+			if(!is_valid(new_blocks, symbol)) continue;
+
+			if(new_blocks.size() == 1){
+				fire_once([]{ cerr << "WARNING: Refinement did not give finer partition, can not happen\n"; });
+				continue;
+			}
+
+			// update partition and add the children
+			boom.seperator = word;
+			const auto range = part.replace(block, move(new_blocks));
+			add_push_new_block(range, boom);
+
+			goto has_split;
+		}
+
+		// We tried all we could, but did not succeed => declare incompleteness.
+		if(days_without_progress++ >= work.size()) {
+			r.is_complete = false;
+			return r;
+		}
+		push(block, boom);
+		continue;
+
+		has_split:
+		days_without_progress = 0;
+	}
+
+	return r;
+}

lib/create_splitting_tree.hpp

@@ -0,0 +1,30 @@
+#pragma once
+
+#include "mealy.hpp"
+#include "partition.hpp"
+#include "splitting_tree.hpp"
+
+#include <vector>
+
+struct result {
+	result(size_t N)
+	: root(N, 0)
+	, partition(N)
+	, successor_cache()
+	, is_complete(true)
+	{}
+
+	// The splitting tree as described in Lee & Yannakakis
+	splijtboom root;
+
+	// The running partition of states
+	partition_refine partition;
+
+	// Encodes f_u : depth -> state -> state, where only the depth of u is of importance
+	std::vector<std::vector<state>> successor_cache;
+
+	// false <-> no adaptive distinguishing sequence
+	bool is_complete;
+};
+
+result create_splitting_tree(Mealy const & m);

lib/logging.hpp

@@ -0,0 +1,10 @@
+#pragma once
+
+#include <mutex>
+
+// Works particularly nice with lambda's, as they give naturally unique types :)
+template <typename F>
+void fire_once(F && f){
+	static std::once_flag flag;
+	std::call_once(flag, f);
+}

lib/mealy.hpp

@@ -6,6 +6,9 @@
 #include <string>
 #include <vector>
 
+/* We use size_t's for easy indexing. But we do not want to mix states and
+ * inputs. We use phantom typing to "generate" distinguished types :).
+ */
 using state = phantom<size_t, struct state_tag>;
 using input = phantom<size_t, struct input_tag>;
 using output = phantom<size_t, struct output_tag>;

lib/partition.hpp

@@ -6,8 +6,6 @@
 #include <utility>
 #include <vector>
 
-#include <iostream>
-
 using Elements = std::list<size_t>;
 
 struct Block {

lib/read_mealy_from_dot.cpp

@@ -1,9 +1,7 @@
 #include "read_mealy_from_dot.hpp"
-
 #include "mealy.hpp"
 
 #include <fstream>
-#include <iostream>
 #include <sstream>
 #include <string>
 
@@ -16,7 +14,7 @@ T get(istream& in){
 	return t;
 }
 
-Mealy read_mealy_from_dot(istream& in, int verbose){
+Mealy read_mealy_from_dot(istream& in){
 	Mealy m;
 
 	string line;
@@ -43,10 +41,6 @@ Mealy read_mealy_from_dot(istream& in, int verbose){
 		const auto slash = get<string>(ss);
 		const auto output = get<string>(ss);
 
-		if(verbose >= 2){
-			cout << lh << '\t' << rh << '\t' << input << '\t' << output << endl;
-		}
-
 		// make fresh indices, if needed
 		if(m.nodes_indices.count(lh) < 1) m.nodes_indices[lh] = m.graph_size++;
 		if(m.nodes_indices.count(rh) < 1) m.nodes_indices[rh] = m.graph_size++;
@@ -60,20 +54,10 @@ Mealy read_mealy_from_dot(istream& in, int verbose){
 		v[m.input_indices[input].base()] = {m.nodes_indices[rh], m.output_indices[output]};
 	}
 
-	if(verbose >= 1){
-		cout << "input_alphabet = \n";
-		for(auto && i : m.input_indices) cout << i.first << " ";
-		cout << endl;
-
-		cout << "output_alphabet = \n";
-		for(auto && o : m.output_indices) cout << o.first << " ";
-		cout << endl;
-	}
-
 	return m;
 }
 
-Mealy read_mealy_from_dot(const string& filename, int verbose){
+Mealy read_mealy_from_dot(const string& filename){
 	ifstream file(filename);
-	return read_mealy_from_dot(file, verbose);
+	return read_mealy_from_dot(file);
 }

lib/read_mealy_from_dot.hpp

@@ -3,5 +3,5 @@
 #include <iosfwd>
 
 struct Mealy;
-Mealy read_mealy_from_dot(const std::string & filename, int verbose);
+Mealy read_mealy_from_dot(const std::string & filename);
-Mealy read_mealy_from_dot(std::istream & input, int verbose);
+Mealy read_mealy_from_dot(std::istream & input);

lib/splitting_tree.hpp

@@ -18,11 +18,11 @@ struct splijtboom {
 	std::vector<splijtboom> children;
 	std::vector<input> seperator;
 	size_t depth = 0;
-	int mark = 0; // used for some algorithms...
+	mutable int mark = 0; // used for some algorithms...
 };
 
 template <typename Fun>
-void lca_impl1(splijtboom & node, Fun && f){
+void lca_impl1(splijtboom const & node, Fun && f){
 	node.mark = 0;
 	if(!node.children.empty()){
 		for(auto && c : node.children){
@@ -50,3 +50,10 @@ splijtboom & lca(splijtboom & root, Fun && f){
 	lca_impl1(root, f);
 	return lca_impl2(root);
 }
+
+template <typename Fun>
+const splijtboom & lca(const splijtboom & root, Fun && f){
+	static_assert(std::is_same<decltype(f(0)), bool>::value, "f should return a bool");
+	lca_impl1(root, f);
+	return lca_impl2(const_cast<splijtboom&>(root));
+}

lib/write_splitting_tree_to_dot.cpp

@@ -1,52 +0,0 @@
-#include "write_splitting_tree_to_dot.hpp"
-#include "splitting_tree.hpp"
-
-#include <fstream>
-#include <functional>
-#include <ostream>
-#include <queue>
-#include <utility>
-
-using namespace std;
-
-template <typename T>
-ostream & operator<<(ostream& out, vector<T> const & x){
-	if(x.empty()) return out;
-
-	auto it = begin(x);
-	out << *it++;
-	while(it != end(x)) out << " " << *it++;
-	return out;
-}
-
-void write_splitting_tree_to_dot(const splijtboom& root, ostream& out){
-	out << "digraph splijtboom {\n";
-
-	// breadth first
-	int global_id = 0;
-	queue<pair<int, reference_wrapper<const splijtboom>>> work;
-	work.push({global_id++, root});
-	while(!work.empty()){
-		const auto id = work.front().first;
-		const splijtboom & node = work.front().second;
-		work.pop();
-
-		out << "\n\ts" << id << " [label=\"" << node.states;
-		if(!node.seperator.empty()) out << "\\n" << node.seperator;
-		out << "\"];\n";
-
-		for(auto && c : node.children){
-			int new_id = global_id++;
-			out << "\ts" << id << " -> " << "s" << new_id << ";\n";
-			work.push({new_id, c});
-		}
-	}
-
-	out << "}" << endl;
-}
-
-
-void write_splitting_tree_to_dot(const splijtboom& root, const string& filename){
-	ofstream file(filename);
-	write_splitting_tree_to_dot(root, file);
-}

lib/write_splitting_tree_to_dot.hpp

@@ -1,8 +0,0 @@
-#pragma once
-
-#include <iosfwd>
-
-struct splijtboom;
-
-void write_splitting_tree_to_dot(const splijtboom & root, std::ostream & out);
-void write_splitting_tree_to_dot(const splijtboom & root, std::string const & filename);

lib/write_tree_to_dot.cpp

@@ -0,0 +1,49 @@
+#include "write_tree_to_dot.hpp"
+#include "adaptive_distinguishing_sequence.hpp"
+#include "splitting_tree.hpp"
+
+#include <fstream>
+
+using namespace std;
+
+template <typename T>
+ostream & operator<<(ostream& out, vector<T> const & x){
+	if(x.empty()) return out;
+
+	auto it = begin(x);
+	out << *it++;
+	while(it != end(x)) out << " " << *it++;
+	return out;
+}
+
+
+void write_splitting_tree_to_dot(const splijtboom& root, ostream& out){
+	write_tree_to_dot(root, [](const splijtboom & node, ostream& out){
+		out << node.states;
+		if(!node.seperator.empty()){
+			out << "\\n" << node.seperator;
+		}
+	}, out);
+}
+
+void write_splitting_tree_to_dot(const splijtboom& root, const string& filename){
+	ofstream file(filename);
+	write_splitting_tree_to_dot(root, file);
+}
+
+void write_adaptive_distinguishing_sequence_to_dot(const dist_seq & root, ostream & out){
+	write_tree_to_dot(root, [](const dist_seq & node, ostream& out){
+		if(!node.word.empty()){
+			out << node.word;
+		} else {
+			vector<state> I(node.CI.size());
+			transform(begin(node.CI), end(node.CI), begin(I), [](auto p){ return p.second; });
+			out << "I = " << I;
+		}
+	}, out);
+}
+
+void write_adaptive_distinguishing_sequence_to_dot(const dist_seq & root, string const & filename){
+	ofstream file(filename);
+	write_adaptive_distinguishing_sequence_to_dot(root, file);
+}

lib/write_tree_to_dot.hpp

@@ -0,0 +1,45 @@
+#pragma once
+
+#include <functional>
+#include <ostream>
+#include <queue>
+#include <utility>
+
+// Generic printer for tree
+template <typename T, typename NodeString>
+void write_tree_to_dot(const T & tree, NodeString && node_string, std::ostream & out){
+	using namespace std;
+	out << "digraph g {\n";
+
+	// breadth first
+	int global_id = 0;
+	queue<pair<int, reference_wrapper<const T>>> work;
+	work.push({global_id++, tree});
+	while(!work.empty()){
+		const auto id = work.front().first;
+		const T & node = work.front().second;
+		work.pop();
+
+		out << "\n\ts" << id << " [label=\"";
+		node_string(node, out);
+		out << "\"];\n";
+
+		for(auto && c : node.children){
+			int new_id = global_id++;
+			out << "\ts" << id << " -> " << "s" << new_id << ";\n";
+			work.push({new_id, c});
+		}
+	}
+
+	out << "}" << endl;
+}
+
+
+// Specialized printing for splitting trees and dist seqs
+struct splijtboom;
+void write_splitting_tree_to_dot(const splijtboom & root, std::ostream & out);
+void write_splitting_tree_to_dot(const splijtboom & root, std::string const & filename);
+
+struct dist_seq;
+void write_adaptive_distinguishing_sequence_to_dot(const dist_seq & root, std::ostream & out);
+void write_adaptive_distinguishing_sequence_to_dot(const dist_seq & root, std::string const & filename);

src/main.cpp

@@ -1,297 +1,38 @@
-#include <mealy.hpp>
+#include <create_adaptive_distinguishing_sequence.hpp>
-#include <partition.hpp>
+#include <create_splitting_tree.hpp>
 #include <read_mealy_from_dot.hpp>
-#include <splitting_tree.hpp>
+#include <write_tree_to_dot.hpp>
-#include <write_splitting_tree_to_dot.hpp>
 
-#include <algorithm>
 #include <cassert>
-#include <fstream>
 #include <iostream>
-#include <iterator>
-#include <queue>
-#include <utility>
 
 using namespace std;
 
-template <typename T>
-ostream & operator<<(ostream& out, vector<T> const & x){
-	if(x.empty()) return out;
-
-	auto it = begin(x);
-	out << *it++;
-	while(it != end(x)) out << " " << *it++;
-	return out;
-}
-
-int verbose = 0;
-
-template <typename T>
-std::vector<T> concat(std::vector<T> const & l, std::vector<T> const & r){
-	std::vector<T> ret(l.size() + r.size());
-	auto it = copy(begin(l), end(l), begin(ret));
-	copy(begin(r), end(r), it);
-	return ret;
-}
-
 int main(int argc, char *argv[]){
-	if(argc < 2) return 1;
+	if(argc != 2) return 1;
-	if(argc > 2) verbose = argc - 2;
-
 	const string filename = argv[1];
 
 	cerr << "* Reading file " << filename << "\n";
-	const auto g = read_mealy_from_dot(filename, verbose);
+	const auto machine = read_mealy_from_dot(filename);
-	assert(is_complete(g));
+	assert(is_complete(machine));
 	cerr << "\tdone\n";
 
-	const auto N = g.graph.size();
-	const auto P = g.input_indices.size();
-	const auto Q = g.output_indices.size();
-
-	cerr << "* Setting up strucutres\n";
-	partition_refine part(N);
-	splijtboom root(N, 0);
-	vector<vector<state>> succession;
-
-	queue<pair<partition_refine::BlockRef, reference_wrapper<splijtboom>>> work;
-	const auto push = [&work](auto br, auto & sp) { work.push({br, sp}); };
-	const auto pop = [&work]() { const auto r = work.front(); work.pop(); return r; };
-	const auto add_push_new_block = [&](auto new_blocks, auto & boom) {
-		const auto nb = distance(new_blocks.first, new_blocks.second);
-		boom.children.assign(nb, splijtboom(0, boom.depth + 1));
-
-		auto i = 0;
-		while(new_blocks.first != new_blocks.second){
-			for(auto && s : *new_blocks.first){
-				boom.children[i].states.push_back(s);
-			}
-
-			push(new_blocks.first++, boom.children[i++]);
-		}
-
-		if(verbose){
-			cout << "splitted output into " << nb << endl;
-		}
-	};
-	const auto is_valid = [N, &g](auto blocks, auto symbol){
-		for(auto && block : blocks) {
-			partition_refine s_part(block);
-			const auto new_blocks = s_part.refine(*s_part.begin(), [symbol, &g](state state){
-				return apply(g, state, symbol).to.base();
-			}, N);
-			for(auto && new_block : new_blocks){
-				if(distance(new_block.begin(), new_block.end()) != 1) return false;
-			}
-		}
-		return true;
-	};
-	const auto update_succession = [N, &succession](state s, state t, size_t depth){
-		if(succession.size() < depth+1) succession.resize(depth+1, vector<state>(N, -1));
-		succession[depth][s.base()] = t;
-	};
-
-	push(part.begin(), root);
-	cerr << "\tdone\n";
-
-	size_t days_without_progress = 0;
-	string filename_thingy;
-
 	cerr << "* Starting Lee & Yannakakis I\n";
-	while(!work.empty()){
+	const auto splitting_tree = create_splitting_tree(machine);
-		const auto block_boom = pop();
-		const auto block = block_boom.first;
-		splijtboom & boom = block_boom.second;
-		const auto depth = boom.depth;
-
-		if(verbose){
-			cout << "current\t";
-			for(auto s : boom.states) cout << s << " ";
-			cout << endl;
-		}
-
-		if(boom.states.size() == 1) continue;
-
-		// First try to split on output
-		for(input symbol = 0; symbol < P; ++symbol){
-			const auto new_blocks = part.refine(*block, [symbol, depth, &g, &update_succession](state state){
-				const auto ret = apply(g, state, symbol);
-				update_succession(state, ret.to, depth);
-				return ret.output.base();
-			}, Q);
-
-			// no split -> continue with other input symbols
-			if(new_blocks.size() == 1) continue;
-
-			// not a valid split -> continue
-			if(!is_valid(new_blocks, symbol)) continue;
-
-			// a succesful split, update partition and add the children
-			boom.seperator = {symbol};
-			const auto range = part.replace(block, move(new_blocks));
-			add_push_new_block(range, boom);
-
-			goto has_split;
-		}
-
-		// Then try to split on state
-		for(input symbol = 0; symbol < P; ++symbol){
-			vector<bool> successor_states(N, false);
-			for(auto && state : *block){
-				successor_states[apply(g, state, symbol).to.base()] = true;
-			}
-
-			const auto & oboom = lca(root, [&successor_states](state state) -> bool{
-				return successor_states[state.base()];
-			});
-
-			// a leaf, hence not a split -> try other symbols
-			if(oboom.children.empty()) continue;
-
-			// possibly a succesful split, construct the children
-			const auto word = concat({symbol}, oboom.seperator);
-			const auto new_blocks = part.refine(*block, [word, depth, &g, &update_succession](state state){
-				const auto ret = apply(g, state, begin(word), end(word));
-				update_succession(state, ret.to, depth);
-				return ret.output.base();
-			}, Q);
-
-			// not a valid split -> continue
-			if(!is_valid(new_blocks, symbol)) continue;
-
-			if(new_blocks.size() == 1){
-				// cerr << "WARNING: Refinement did not give finer partition, can not happen\n";
-				continue;
-			}
-
-			// update partition and add the children
-			boom.seperator = word;
-			const auto range = part.replace(block, move(new_blocks));
-			add_push_new_block(range, boom);
-
-			goto has_split;
-		}
-
-		// cout << "no split :(" << endl;
-		if(days_without_progress++ >= work.size()) {
-			filename_thingy = "incomplete_";
-			cerr << "\t* No distinguishing seq found!\n";
-			break;
-		}
-		push(block, boom);
-		continue;
-
-		has_split:
-		// cout << "blocks: " << part.size() << ", states: " << N << ", work: " << work.size() << endl;
-		days_without_progress = 0;
-	}
 	cerr << "\tdone\n";
 
 	cerr << "* Write splitting tree\n";
-	write_splitting_tree_to_dot(root, filename + "." + filename_thingy + "splitting_tree");
+	const string tree_filename = splitting_tree.is_complete ? (filename + ".splitting_tree") : (filename + ".incomplete_splitting_tree");
+	write_splitting_tree_to_dot(splitting_tree.root, tree_filename);
 	cerr << "\tdone\n";
 
-	struct dist_seq {
-		dist_seq(size_t N)
-		: I(N)
-		, C(I)
-		{
-			iota(begin(I), end(I), 0);
-			iota(begin(C), end(C), 0);
-		}
-
-		vector<state> I;
-		vector<state> C;
-		vector<input> word;
-		vector<dist_seq> children;
-	} root_seq(N);
-
 	cerr << "* Lee and Yannakaki II\n";
-	{
+	const auto distinguishing_sequence = create_adaptive_distinguishing_sequence(splitting_tree);
-		queue<reference_wrapper<dist_seq>> work2;
-		work2.push(root_seq);
-
-		while(!work2.empty()){
-			dist_seq & node = work2.front();
-			work2.pop();
-
-			if(node.C.size() < 2) continue;
-
-			vector<bool> states(N, false);
-			for(auto && state : node.C){
-				states[state.base()] = true;
-			}
-
-			const auto & oboom = lca(root, [&states](state state) -> bool{
-				return states[state.base()];
-			});
-
-			if(oboom.children.empty()) continue;
-
-			node.word = oboom.seperator;
-			for(auto && c : oboom.children){
-				dist_seq new_c(0);
-
-				size_t i = 0;
-				size_t j = 0;
-
-				while(i < node.C.size() && j < c.states.size()){
-					if(node.C[i] < c.states[j]) {
-						i++;
-					} else if(node.C[i] > c.states[j]) {
-						j++;
-					} else {
-						new_c.I.push_back(node.I[i]);
-						new_c.C.push_back(succession[oboom.depth][node.C[i].base()]);
-						i++;
-						j++;
-					}
-				}
-
-				// woops. fixme
-				sort(begin(new_c.C), end(new_c.C));
-
-				if(!new_c.C.empty()){
-					node.children.push_back(move(new_c));
-				}
-			}
-
-			for(auto & c : node.children) {
-				work2.push(c);
-			}
-		}
-	}
 	cerr << "\tdone\n";
 
 	cerr << "* Write dist sequence\n";
-	{
+	const string dseq_filename = splitting_tree.is_complete ? (filename + ".dist_seq") : (filename + ".incomplete_dist_seq");
-		ofstream out(filename + "." + filename_thingy + "dist_seq");
+	write_adaptive_distinguishing_sequence_to_dot(distinguishing_sequence.sequence, dseq_filename);
-		out << "digraph distinguishing_sequence {\n";
-
-		// breadth first
-		int global_id = 0;
-		queue<pair<int, reference_wrapper<const dist_seq>>> work3;
-		work3.push({global_id++, root_seq});
-		while(!work3.empty()){
-			const auto id = work3.front().first;
-			const dist_seq & node = work3.front().second;
-			work3.pop();
-
-			if(!node.word.empty()){
-				out << "\n\ts" << id << " [label=\"" << node.word << "\"];\n";
-			} else {
-				out << "\n\ts" << id << " [label=\"I = " << node.I << "\"];\n";
-			}
-
-			for(auto && c : node.children){
-				int new_id = global_id++;
-				out << "\ts" << id << " -> " << "s" << new_id << ";\n";
-				work3.push({new_id, c});
-			}
-		}
-
-		out << "}" << endl;
-	}
 	cerr << "\tdone\n" << endl;
 }