Refactors a bit

lib/adaptive_distinguishing_sequence.cpp

@@ -39,7 +39,7 @@ adaptive_distinguishing_sequence create_adaptive_distinguishing_sequence(const r
 
 		if(oboom.children.empty()) continue;
 
-		node.word = oboom.seperator;
+		node.word = oboom.separator;
 		for(auto && c : oboom.children){
 			adaptive_distinguishing_sequence new_c(0, node.depth + 1);
 

lib/characterization_family.hpp

@@ -1,29 +0,0 @@
-#pragma once
-
-#include "adaptive_distinguishing_sequence.hpp"
-#include "separating_matrix.hpp"
-#include "types.hpp"
-
-/// \brief From the LY algorithm we generate characterizations sets (as in the Chow framework)
-/// If the adaptive distinguihsing sequence is complete, then we do not need to augment the LY
-/// result. This results in a separating family, which is stronger than a characterization set.
-/// However, if it is not complete, we augment it with sequences from the Wp-method.
-
-/// \brief A set (belonging to some state) of characterizing sequences
-/// It contains global_suffixes which should be used for testing whether the state is correct. Once
-/// we know the states make sense, we can test the transitions with the smaller set local_suffixes.
-/// There is some redundancy in this struct, but we have plenty of memory at our disposal.
-/// Note that even the global_suffixes may really on the state (because of the adaptiveness of the
-/// LY distinguishing sequence).
-struct characterization_set {
-	std::vector<word> global_suffixes;
-	std::vector<word> local_suffixes;
-};
-
-/// \brief A family (indexed by states) of characterizations
-using characterization_family = std::vector<characterization_set>;
-
-/// \brief Creates the characterization family from the results of the LY algorithm
-/// If the sequence is complete, we do not need the separating_matrix
-characterization_family create_seperating_family(const adaptive_distinguishing_sequence & sequence,
-                                                 const splitting_tree & separating_sequences);

lib/read_mealy.cpp

@@ -27,10 +27,10 @@ mealy read_mealy_from_txt(std::istream & in) {
 		state from, to;
 		input i;
 		output o;
-		string seperator;
+		string separator;
 
 		stringstream ss(line);
-		ss >> from >> seperator >> i >> seperator >> o >> seperator >> to;
+		ss >> from >> separator >> i >> separator >> o >> separator >> to;
 
 		if (from >= max_state) max_state = from + 1;
 		if (to >= max_state) max_state = to + 1;

lib/separating_family.cpp

@@ -1,4 +1,6 @@
-#include "characterization_family.hpp"
+#include "separating_family.hpp"
+#include "adaptive_distinguishing_sequence.hpp"
+#include "splitting_tree.hpp"
 #include "trie.hpp"
 
 #include <boost/range/algorithm.hpp>
@@ -10,12 +12,12 @@
 
 using namespace std;
 
-characterization_family create_seperating_family(const adaptive_distinguishing_sequence & sequence,
-                                                 const splitting_tree & separating_sequences) {
+separating_family create_separating_family(const adaptive_distinguishing_sequence & sequence,
+                                           const splitting_tree & separating_sequences) {
 	const auto N = sequence.CI.size();
 
 	vector<trie> suffixes(N);
-	characterization_family ret(N);
+	separating_family ret(N);
 
 	// First we accumulate the kind-of-UIOs and the separating words we need. We will do this with a
 	// breath first search. If we encouter a set of states which is not a singleton, we add
@@ -40,7 +42,8 @@ characterization_family create_seperating_family(const adaptive_distinguishing_s
 				const auto s = p.second;
 				states[s] = true;
 			}
-			const auto root = lca(separating_sequences, [&states](auto z) -> bool { return states[z]; });
+			const auto root
+			    = lca(separating_sequences, [&states](auto z) -> bool { return states[z]; });
 
 			vector<word> stack_of_words;
 			const function<void(splitting_tree const &)> recursor = [&](splitting_tree const & n) {
@@ -53,7 +56,7 @@ characterization_family create_seperating_family(const adaptive_distinguishing_s
 						}
 					}
 				} else {
-					if (n.mark > 1) stack_of_words.push_back(n.seperator);
+					if (n.mark > 1) stack_of_words.push_back(n.separator);
 					for (auto const & c : n.children) {
 						recursor(c);
 					}
@@ -68,9 +71,7 @@ characterization_family create_seperating_family(const adaptive_distinguishing_s
 				const auto s = p.second;
 				auto & current_suffixes = suffixes[s];
 
-				// they are the same (FIXME)
 				ret[s].local_suffixes = flatten(current_suffixes);
-				ret[s].global_suffixes = flatten(current_suffixes);
 				current_suffixes.clear();
 			}
 

lib/separating_family.hpp

@@ -0,0 +1,26 @@
+#pragma once
+
+#include "types.hpp"
+
+struct adaptive_distinguishing_sequence;
+struct splitting_tree;
+
+/// \brief From the LY algorithm we generate a separating family
+/// If the adaptive distinguihsing sequence is complete, then we do not need to augment the LY
+/// result. If it is not complete, we augment it with sequences from the HSI-method. In both cases
+/// the result is a separating family (as defined in LY).
+
+/// \brief A set (belonging to some state) of separating sequences
+/// It only has local_suffixes, as all suffixes are "harmonized", meaning that sequences share
+/// prefixes among the family. With this structure we can define the HSI-method and DS-method. Our
+/// method is a hybrid one. Families are always indexed by state.
+struct separating_set {
+	std::vector<word> local_suffixes;
+};
+
+using separating_family = std::vector<separating_set>;
+
+/// \brief Creates the separating family from the results of the LY algorithm
+/// If the sequence is complete, we do not need the sequences in the splitting tree.
+separating_family create_separating_family(const adaptive_distinguishing_sequence & sequence,
+                                           const splitting_tree & separating_sequences);

lib/separating_matrix.cpp

@@ -1,53 +0,0 @@
-#include "separating_matrix.hpp"
-
-#include <cassert>
-#include <functional>
-#include <queue>
-
-using namespace std;
-
-separating_matrix create_all_pair_seperating_sequences(const splitting_tree & root){
-	const auto N = root.states.size();
-	separating_matrix all_pair_seperating_sequences(N, separating_row(N));
-
-	queue<reference_wrapper<const splitting_tree>> work;
-	work.push(root);
-
-	// total complexity is O(n^2), as we're visiting each pair only once :)
-	while(!work.empty()){
-		const splitting_tree & node = work.front();
-		work.pop();
-
-		auto it = begin(node.children);
-		auto ed = end(node.children);
-
-		while(it != ed){
-			auto jt = next(it);
-			while(jt != ed){
-				for(auto && s : it->states){
-					for(auto && t : jt->states){
-						assert(all_pair_seperating_sequences[t][s].empty());
-						assert(all_pair_seperating_sequences[s][t].empty());
-						all_pair_seperating_sequences[t][s] = node.seperator;
-						all_pair_seperating_sequences[s][t] = node.seperator;
-					}
-				}
-				jt++;
-			}
-			it++;
-		}
-
-		for(auto && c : node.children){
-			work.push(c);
-		}
-	}
-
-	for(size_t i = 0; i < N; ++i){
-		for(size_t j = 0; j < N; ++j){
-			if(i == j) continue;
-			assert(!all_pair_seperating_sequences[i][j].empty());
-		}
-	}
-
-	return all_pair_seperating_sequences;
-}

lib/separating_matrix.hpp

@@ -1,13 +0,0 @@
-#pragma once
-
-#include "types.hpp"
-#include "splitting_tree.hpp"
-
-
-/// A separating matrix is a matrix indexed by states, which assigns to each
-/// pair of (inequivalent) states a separating sequences. This can be done by
-/// the classical Hopcroft or Moore algorithm
-using separating_row = std::vector<word>;
-using separating_matrix = std::vector<separating_row>;
-
-separating_matrix create_all_pair_seperating_sequences(splitting_tree const & root);

lib/splitting_tree.cpp

@@ -112,7 +112,7 @@ result create_splitting_tree(const mealy & g, options opt) {
 				if (opt.check_validity && !is_valid(new_blocks, symbol)) continue;
 
 				// a succesful split, update partition and add the children
-				boom.seperator = {symbol};
+				boom.separator = {symbol};
 				add_push_new_block(new_blocks, boom);
 
 				goto has_split;
@@ -135,10 +135,10 @@ result create_splitting_tree(const mealy & g, options opt) {
 				if (oboom.children.empty()) continue;
 
 				// If we want to enforce the right order, we should :D
-				if (opt.assert_minimal_order && oboom.seperator.size() != current_order) continue;
+				if (opt.assert_minimal_order && oboom.separator.size() != current_order) continue;
 
 				// possibly a succesful split, construct the children
-				const vector<input> word = concat(vector<input>(1, symbol), oboom.seperator);
+				const vector<input> word = concat(vector<input>(1, symbol), oboom.separator);
 				const auto new_blocks = partition_(
 				    begin(boom.states),
 				    end(boom.states), [word, depth, &g, &update_succession](state state) {
@@ -153,7 +153,7 @@ result create_splitting_tree(const mealy & g, options opt) {
 				assert(new_blocks.size() > 1);
 
 				// update partition and add the children
-				boom.seperator = word;
+				boom.separator = word;
 				add_push_new_block(new_blocks, boom);
 
 				goto has_split;

lib/splitting_tree.hpp

@@ -10,7 +10,7 @@ struct splitting_tree {
 
 	std::vector<state> states;
 	std::vector<splitting_tree> children;
-	word seperator;
+	word separator;
 	size_t depth = 0;
 	mutable int mark = 0; // used for some algorithms...
 };

lib/test_suite.cpp

@@ -7,7 +7,7 @@
 using namespace std;
 
 void test(const mealy & specification, const transfer_sequences & prefixes,
-          const characterization_family & separating_family, size_t k_max, const writer & output) {
+          const separating_family & separating_family, size_t k_max, const writer & output) {
 	vector<word> all_sequences(1);
 
 	for (size_t k = 0; k <= k_max; ++k) {
@@ -33,7 +33,7 @@ void test(const mealy & specification, const transfer_sequences & prefixes,
 }
 
 void randomized_test(const mealy & specification, const transfer_sequences & prefixes,
-                     const characterization_family & separating_family, size_t min_k,
+                     const separating_family & separating_family, size_t min_k,
                      const writer & output) {
 	clog << "*** K >= " << min_k << endl;
 

lib/test_suite.hpp

@@ -1,7 +1,7 @@
 #pragma once
 
-#include "characterization_family.hpp"
 #include "mealy.hpp"
+#include "separating_family.hpp"
 #include "transfer_sequences.hpp"
 #include "types.hpp"
 
@@ -14,11 +14,11 @@ struct writer {
 
 /// \brief Performs exhaustive tests with \p k_max extra states (harmonized, e.g. HSI / DS)
 void test(mealy const & specification, transfer_sequences const & prefixes,
-          characterization_family const & separating_family, size_t k_max, writer const & output);
+          separating_family const & separating_family, size_t k_max, writer const & output);
 
 /// \brief Performs random non-exhaustive tests for more states (harmonized, e.g. HSI / DS)
 [[noreturn]] void randomized_test(mealy const & specification, transfer_sequences const & prefixes,
-                                  characterization_family const & separating_family, size_t min_k,
+                                  separating_family const & separating_family, size_t min_k,
                                   writer const & output);
 
 /// \brief returns a writer which simply writes everything to cout (via inputs)

lib/write_tree_to_dot.cpp

@@ -24,9 +24,9 @@ static const auto id = [](auto x) { return x; };
 void write_splitting_tree_to_dot(const splitting_tree & root, ostream & out_) {
 	write_tree_to_dot(root, [](const splitting_tree & node, ostream & out) {
 		print_vec(out, node.states, " ", id);
-		if (!node.seperator.empty()) {
+		if (!node.separator.empty()) {
 			out << "\\n";
-			print_vec(out, node.seperator, " ", id);
+			print_vec(out, node.separator, " ", id);
 		}
 	}, out_);
 }

src/main.cpp

@@ -3,8 +3,7 @@
 #include <mealy.hpp>
 #include <reachability.hpp>
 #include <read_mealy.hpp>
-#include <characterization_family.hpp>
-#include <separating_matrix.hpp>
+#include <separating_family.hpp>
 #include <splitting_tree.hpp>
 #include <test_suite.hpp>
 #include <transfer_sequences.hpp>
@@ -58,7 +57,7 @@ int main(int argc, char *argv[]) try {
 	const auto & machine = reachable_submachine(move(machine_and_translation.first), 0);
 	const auto & translation = machine_and_translation.second;
 
-	auto all_pair_seperating_sequences = [&]{
+	auto all_pair_separating_sequences = [&]{
 		const auto splitting_tree_hopcroft = [&]{
 			time_logger t("creating hopcroft splitting tree");
 			return create_splitting_tree(machine, randomize_hopcroft ? randomized_hopcroft_style : hopcroft_style);
@@ -102,9 +101,9 @@ int main(int argc, char *argv[]) try {
 	// const auto all_pair_seperating_sequences = all_pair_seperating_sequences_fut.get();
 	// const auto sequence = sequence_fut.get();
 
-	const auto seperating_family = [&]{
+	const auto separating_family = [&]{
 		time_logger t("making seperating family");
-		return create_seperating_family(sequence, all_pair_seperating_sequences);
+		return create_separating_family(sequence, all_pair_separating_sequences);
 	}();
 
 	// const auto transfer_sequences = transfer_sequences_fut.get();
@@ -112,12 +111,12 @@ int main(int argc, char *argv[]) try {
 
 	if(streaming){
 		time_logger t("outputting all preset tests");
-		test(machine, transfer_sequences, seperating_family, k_max, default_writer(inputs));
+		test(machine, transfer_sequences, separating_family, k_max, default_writer(inputs));
 	}
 
 	if(random_part){
 		time_logger t("outputting all random tests");
-		randomized_test(machine, transfer_sequences, seperating_family, k_max+1, default_writer(inputs));
+		randomized_test(machine, transfer_sequences, separating_family, k_max+1, default_writer(inputs));
 	}
 
 } catch (exception const & e) {

src/methods.cpp

@@ -1,10 +1,9 @@
 #include <adaptive_distinguishing_sequence.hpp>
 #include <read_mealy.hpp>
-#include <characterization_family.hpp>
-#include <separating_matrix.hpp>
-#include <trie.hpp>
+#include <separating_family.hpp>
 #include <splitting_tree.hpp>
 #include <transfer_sequences.hpp>
+#include <trie.hpp>
 
 #include <future>
 #include <string>
@@ -12,6 +11,17 @@
 
 using namespace std;
 
+enum Method {
+	hsi_method,
+	ds_plus_method,
+};
+
+static Method parse_method(string const & s) {
+	if (s == "--W-method") return hsi_method;
+	if (s == "--DS-method") return ds_plus_method;
+	throw runtime_error("No valid method specified");
+}
+
 int main(int argc, char * argv[]) {
 	if (argc != 4) {
 		cerr << "usage: methods <file> <mode> <k_max>\n";
@@ -19,11 +29,10 @@ int main(int argc, char * argv[]) {
 	}
 
 	const string filename = argv[1];
-	const string mode = argv[2];
-	const bool use_no_LY = mode == "--W-method";
+	const Method method = parse_method(argv[2]);
 	const size_t k_max = std::stoul(argv[3]);
 
-	const auto machine = [&]{
+	const auto machine = [&] {
 		if (filename.find(".txt") != string::npos) {
 			return read_mealy_from_txt(filename);
 		} else if (filename.find(".dot") != string::npos) {
@@ -35,7 +44,7 @@ int main(int argc, char * argv[]) {
 	}();
 
 	auto sequence_fut = async([&] {
-		if (use_no_LY) {
+		if (method == hsi_method) {
 			return create_adaptive_distinguishing_sequence(result(machine.graph_size));
 		}
 		const auto tree = create_splitting_tree(machine, randomized_lee_yannakakis_style);
@@ -63,7 +72,7 @@ int main(int argc, char * argv[]) {
 
 	clog << "getting sequence and pairs" << endl;
 	auto suffixes_fut = async([&] {
-		return create_seperating_family(sequence_fut.get(), pairs_fut.get());
+		return create_separating_family(sequence_fut.get(), pairs_fut.get());
 	});
 
 	clog << "getting prefixes, middles and suffixes" << endl;
@@ -81,8 +90,7 @@ int main(int argc, char * argv[]) {
 		for (auto && m : middles) {
 			const state s2 = apply(machine, s1, begin(m), end(m)).to;
 			const word w2 = concat(w1, m);
-			const auto & suffixes_for_state = (m.size() == k_max) ? suffixes[s2].local_suffixes
-			                                                      : suffixes[s2].global_suffixes;
+			const auto & suffixes_for_state = suffixes[s2].local_suffixes;
 			for (auto && s : suffixes_for_state) {
 				word test = concat(w2, s);
 				test_suite.insert(test);