From 4253233358fea919bd98f5b9bc6e960e2d8f3c2d Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Thu, 19 Mar 2015 16:18:08 +0100 Subject: [PATCH] Adds a independent alphabet-translation struct. Adds a thingy I needed for gephi --- .gitignore | 3 + lib/mealy.hpp | 23 ++------ lib/read_mealy_from_dot.cpp | 46 ++++++++++++---- lib/read_mealy_from_dot.hpp | 35 +++++++++++- lib/splitting_tree.cpp | 4 +- src/conf-hyp.cpp | 106 ------------------------------------ src/conf.cpp | 27 +++++---- src/main.cpp | 8 ++- src/metrics.cpp | 6 +- src/pre_gephi_tool.cpp | 64 ++++++++++++++++++++++ src/stats.cpp | 2 +- 11 files changed, 169 insertions(+), 155 deletions(-) delete mode 100644 src/conf-hyp.cpp create mode 100644 src/pre_gephi_tool.cpp diff --git a/.gitignore b/.gitignore index a9376ac..6ebfe63 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,9 @@ +.DS_Store + *.dot *.png *.pdf *_seq *splitting_tree *test_suite + diff --git a/lib/mealy.hpp b/lib/mealy.hpp index 5cee652..7c01efd 100644 --- a/lib/mealy.hpp +++ b/lib/mealy.hpp @@ -7,11 +7,13 @@ #include /* - * Structure used for reading mealy files from dot files. * Everything is indexed by size_t's, so that we can index vectors - * in constant time. The maps contain the original values corresponding - * to these size_t's. Can only represent deterministic machines, + * in constant time. Can only represent deterministic machines, * but partiality still can occur. + * + * Note that graph_size == graph.size() and that input_size equals the size + * of the biggest row in graph. Finally output_size bounds the number of + * outputs. These values are redundant, but nice to have here. */ struct mealy { struct edge { @@ -19,14 +21,9 @@ struct mealy { output output = -1; }; - std::map nodes_indices; - std::map input_indices; - std::map output_indices; - // state -> input -> (output, state) std::vector> graph; - // these are actually redundant! size_t graph_size = 0; size_t input_size = 0; size_t output_size = 0; @@ -53,13 +50,3 @@ auto apply(mealy const & m, state state, Iterator b, Iterator e){ } return ret; } - -// Used to invert the input_indices and output_indices maps -template -std::vector create_reverse_map(std::map const & indices){ - std::vector ret(indices.size()); - for(auto&& p : indices){ - ret[p.second.base()] = p.first; - } - return ret; -} diff --git a/lib/read_mealy_from_dot.cpp b/lib/read_mealy_from_dot.cpp index 3342567..11b2354 100644 --- a/lib/read_mealy_from_dot.cpp +++ b/lib/read_mealy_from_dot.cpp @@ -17,13 +17,16 @@ T get(istream& in){ return t; } -mealy read_mealy_from_dot(istream& in){ +mealy read_mealy_from_dot(std::istream & in, translation & t){ mealy m; + std::map state_indices; + state max_state = 0; + string line; stringstream ss; while(getline(in, line)){ - if(line.find("}") != string::npos) return m; + if(line.find("}") != string::npos) break; const auto i = line.find("->"); if(i == string::npos) continue; @@ -47,18 +50,22 @@ mealy read_mealy_from_dot(istream& in){ const auto output = get(ss); // 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++; - if(m.input_indices.count(input) < 1) m.input_indices[input] = m.input_size++; - if(m.output_indices.count(output) < 1) m.output_indices[output] = m.output_size++; + if(state_indices.count(lh) < 1) state_indices[lh] = max_state++; + if(state_indices.count(rh) < 1) state_indices[rh] = max_state++; + if(t.input_indices.count(input) < 1) t.input_indices[input] = t.max_input++; + if(t.output_indices.count(output) < 1) t.output_indices[output] = t.max_output++; // add edge - m.graph.resize(m.graph_size); - auto & v = m.graph[m.nodes_indices[lh].base()]; - v.resize(m.input_size); - v[m.input_indices[input].base()] = {m.nodes_indices[rh], m.output_indices[output]}; + m.graph.resize(max_state.base()); + auto & v = m.graph[state_indices[lh].base()]; + v.resize(t.max_input.base()); + v[t.input_indices[input].base()] = {state_indices[rh], t.output_indices[output]}; } + m.graph_size = max_state.base(); + m.input_size = t.max_input.base(); + m.output_size = t.max_output.base(); + assert(m.graph_size > 0); assert(m.input_size > 0); assert(m.output_size > 0); @@ -66,7 +73,22 @@ mealy read_mealy_from_dot(istream& in){ return m; } -mealy read_mealy_from_dot(const string& filename){ + +mealy read_mealy_from_dot(const string & filename, translation & t){ ifstream file(filename); - return read_mealy_from_dot(file); + return read_mealy_from_dot(file, t); +} + + +std::pair read_mealy_from_dot(istream & in){ + translation t; + const auto m = read_mealy_from_dot(in, t); + return {move(m), move(t)}; +} + + +std::pair read_mealy_from_dot(const string & filename){ + translation t; + const auto m = read_mealy_from_dot(filename, t); + return {move(m), move(t)}; } diff --git a/lib/read_mealy_from_dot.hpp b/lib/read_mealy_from_dot.hpp index e73e8ba..8836d9f 100644 --- a/lib/read_mealy_from_dot.hpp +++ b/lib/read_mealy_from_dot.hpp @@ -1,7 +1,38 @@ #pragma once +#include "types.hpp" + #include +#include +#include + +/* + * These maps record the translation used while reading. + */ +struct translation { + std::map input_indices; + input max_input = 0; + + std::map output_indices; + output max_output = 0; +}; struct mealy; -mealy read_mealy_from_dot(const std::string & filename); -mealy read_mealy_from_dot(std::istream & input); + +// Read a mealy machine while extending the translation +mealy read_mealy_from_dot(std::istream & in, translation & t); +mealy read_mealy_from_dot(const std::string & filename, translation & t); + +// Read a mealy machine, starting with the empty translation +std::pair read_mealy_from_dot(std::istream & in); +std::pair read_mealy_from_dot(const std::string & filename); + +// Used to invert the input_indices and output_indices maps +template +std::vector create_reverse_map(std::map const & indices){ + std::vector ret(indices.size()); + for(auto&& p : indices){ + ret[p.second.base()] = p.first; + } + return ret; +} diff --git a/lib/splitting_tree.cpp b/lib/splitting_tree.cpp index f7b0474..adfe3ac 100644 --- a/lib/splitting_tree.cpp +++ b/lib/splitting_tree.cpp @@ -27,8 +27,8 @@ splitting_tree &lca_impl2(splitting_tree & node){ result create_splitting_tree(const mealy& g, options opt){ const auto N = g.graph.size(); - const auto P = g.input_indices.size(); - const auto Q = g.output_indices.size(); + const auto P = g.input_size; + const auto Q = g.output_size; result r(N); auto & root = r.root; diff --git a/src/conf-hyp.cpp b/src/conf-hyp.cpp deleted file mode 100644 index e799537..0000000 --- a/src/conf-hyp.cpp +++ /dev/null @@ -1,106 +0,0 @@ -#include -#include - -#include - -#include -#include -#include - -using namespace std; - -template -vector resize_new(vector const & in, size_t N){ - vector ret(N); - copy_n(in.begin(), N, ret.begin()); - return ret; -} - -vector conform(mealy const & spec, vector const & spec_o_map, mealy const & impl, vector const & impl_o_map, vector> const & suite){ - for(auto && test : suite){ - state s = 0; - state t = 0; - - size_t count = 0; - for(auto && i : test){ - const auto i1 = spec.input_indices.at(i); - const auto r1 = apply(spec, s, i1); - const auto o1 = spec_o_map[r1.output.base()]; - s = r1.to; - - const auto i2 = spec.input_indices.at(i); - const auto r2 = apply(impl, t, i2); - const auto o2 = impl_o_map[r2.output.base()]; - t = r2.to; - - if(o1 != o2){ - return resize_new(test, count+1); - } - count++; - } - } - - return {}; -} - -vector> open_suite(string suite_filename){ - boost::iostreams::filtering_istream suite_file; - suite_file.push(boost::iostreams::gzip_decompressor()); - suite_file.push(boost::iostreams::file_descriptor_source(suite_filename)); - boost::archive::text_iarchive archive(suite_file); - - vector> suite; - archive >> suite; - return suite; -} - -int main(int argc, char *argv[]){ - const size_t N = 136; - vector< pair> > machines_and_maps(N); - vector< vector> > suites(N); - for(int i = 0; i < N; ++i){ - cout << "reading " << i << "\r" << flush; - - const string filename = "hyp." + to_string(i) + ".obf.dot"; - machines_and_maps[i].first = read_mealy_from_dot(filename); - machines_and_maps[i].second = create_reverse_map(machines_and_maps[i].first.output_indices); - - const string suite_filename = filename + "test_suite"; - suites[i] = open_suite(suite_filename); - } - cout << "done reading" << endl; - - const string red = "\x1b[31m"; - const string yellow = "\x1b[33m"; - const string cyan = "\x1B[36m"; - const string reset = "\033[0m"; - - size_t fails = 0; - for(int i = 0; i < N; ++i){ - for(int j = 0; j < N; ++j){ - cout << "checking " << i << " against " << j << "\r" << flush; - const auto & spec = machines_and_maps[i]; - const auto & impl = machines_and_maps[j]; - const auto & suite = suites[i]; - const auto result = conform(spec.first, spec.second, impl.first, impl.second, suite); - - if(i == j && !result.empty()){ - cout << cyan << "FAIL: " << i << " " << j << " is the same machine" << reset << endl; - fails++; - } - - if(i < j && result.empty()){ - cout << red << "FAIL: " << i << " " << j << " no flaw detected" << reset << endl; - fails++; - } - - if(i > j && result.empty()){ - cout << yellow << "FAIL: " << i << " " << j << " no flaw detected" << reset << endl; - fails++; - } - } - } - cout << "done checking" << endl; - cout << "total of " << fails << " fails out of " << N*N << endl; -} - diff --git a/src/conf.cpp b/src/conf.cpp index 1d644d8..894b1e5 100644 --- a/src/conf.cpp +++ b/src/conf.cpp @@ -5,6 +5,7 @@ #include #include +#include #include using namespace std; @@ -16,21 +17,27 @@ vector resize_new(vector const & in, size_t N){ return ret; } -vector conform(mealy const & spec, vector const & spec_o_map, mealy const & impl, vector const & impl_o_map, vector> const & suite){ +struct mealy_with_maps { + mealy machine; + map inputs; + vector outputs; +}; + +vector conform(mealy_with_maps const & spec, mealy_with_maps const & impl, vector> const & suite){ for(auto && test : suite){ state s = 0; state t = 0; size_t count = 0; for(auto && i : test){ - const auto i1 = spec.input_indices.at(i); - const auto r1 = apply(spec, s, i1); - const auto o1 = spec_o_map[r1.output.base()]; + const auto i1 = spec.inputs.at(i); + const auto r1 = apply(spec.machine, s, i1); + const auto o1 = spec.outputs[r1.output.base()]; s = r1.to; - const auto i2 = spec.input_indices.at(i); - const auto r2 = apply(impl, t, i2); - const auto o2 = impl_o_map[r2.output.base()]; + const auto i2 = impl.inputs.at(i); + const auto r2 = apply(impl.machine, t, i2); + const auto o2 = impl.outputs[r2.output.base()]; t = r2.to; if(o1 != o2){ @@ -58,14 +65,14 @@ int main(int argc, char *argv[]){ if(argc != 3) return 1; const auto spec = read_mealy_from_dot(argv[1]); - const auto spec_o_map = create_reverse_map(spec.output_indices); + const auto spec_o_map = create_reverse_map(spec.second.output_indices); const auto impl = read_mealy_from_dot(argv[2]); - const auto impl_o_map = create_reverse_map(impl.output_indices); + const auto impl_o_map = create_reverse_map(impl.second.output_indices); const auto suite = open_suite(argv[1] + string("test_suite")); - const auto counter_example = conform(spec, spec_o_map, impl, impl_o_map, suite); + const auto counter_example = conform({spec.first, spec.second.input_indices, spec_o_map}, {impl.first, impl.second.input_indices, impl_o_map}, suite); if(counter_example.empty()){ cerr << "No counter example found" << endl; } diff --git a/src/main.cpp b/src/main.cpp index 4ce3d0b..8021057 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -38,7 +38,7 @@ int main(int argc, char *argv[]){ const bool randomize_hopcroft = true; const bool randomize_lee_yannakakis = true; - const auto machine = [&]{ + const auto machine_and_translation = [&]{ time_logger t("reading file " + filename); if(use_stdio){ return read_mealy_from_dot(cin); @@ -47,6 +47,9 @@ int main(int argc, char *argv[]){ } }(); + const auto & machine = machine_and_translation.first; + const auto & translation = machine_and_translation.second; + auto all_pair_seperating_sequences_fut = async([&]{ const auto splitting_tree_hopcroft = [&]{ time_logger t("creating hopcroft splitting tree"); @@ -85,7 +88,7 @@ int main(int argc, char *argv[]){ }); auto inputs_fut = std::async([&]{ - return create_reverse_map(machine.input_indices); + return create_reverse_map(translation.input_indices); }); auto relevant_inputs_fut = std::async([&]{ @@ -191,6 +194,7 @@ int main(int argc, char *argv[]){ if(random_part){ time_logger t("outputting all random tests"); + cerr << "*** K > " << k_max << endl; std::random_device rd; std::mt19937 generator(rd()); diff --git a/src/metrics.cpp b/src/metrics.cpp index 47ef325..91f1414 100644 --- a/src/metrics.cpp +++ b/src/metrics.cpp @@ -34,7 +34,9 @@ int main(int argc, char *argv[]){ if(argc != 2) return 1; const string filename = argv[1]; - const auto machine = read_mealy_from_dot(filename); + const auto result = read_mealy_from_dot(filename); + const auto & machine = result.first; + const auto & translation = result.second; // vector> table(machine.input_size); // for(input i = 0; i < machine.input_size; ++i){ @@ -45,7 +47,7 @@ int main(int argc, char *argv[]){ for(state s = 0; s < machine.graph_size; ++s){ size_t scores[3] = {0, 0, 0}; for(input i = 0; i < machine.input_size; ++i){ - const auto test1 = apply(machine, s, i).output != machine.output_indices.at("quiescence"); + const auto test1 = apply(machine, s, i).output != translation.output_indices.at("quiescence"); const auto test2 = apply(machine, s, i).to != s; scores[test1 + test2]++; diff --git a/src/pre_gephi_tool.cpp b/src/pre_gephi_tool.cpp new file mode 100644 index 0000000..4a31a68 --- /dev/null +++ b/src/pre_gephi_tool.cpp @@ -0,0 +1,64 @@ +#include +#include +#include + +#include +#include +#include +#include +#include +#include + +using namespace std; + +int main(int argc, char *argv[]){ + if(argc != 3) return 1; + + const string hypo_filename = argv[1]; + const string mach_filename = argv[2]; + + translation t; + + const auto hypothesis = read_mealy_from_dot(hypo_filename, t); + const auto machine = read_mealy_from_dot(mach_filename, t); + + auto input_to_string = create_reverse_map(t.input_indices); + auto output_to_string = create_reverse_map(t.output_indices); + + vector visited(machine.graph_size, false); + { + const auto state_cover = create_transfer_sequences(hypothesis, 0); + for(auto && p : state_cover){ + state s = 0; + for(auto && i : p){ + visited[s.base()] = true; + s = apply(machine, s, i).to; + } + visited[s.base()] = true; + } + } + + { + ofstream out("gephi.dot"); + out << "digraph g {\n"; + + for(state s = 0; s < machine.graph_size; ++s){ + out << "\t" << "s" << s << " ["; + out << "visited=\"" << (visited[s.base()] ? "1" : "0") << "\""; + out << "]\n"; + } + + for(state s = 0; s < machine.graph_size; ++s){ + for(input i = 0; i < machine.input_size; ++i){ + const auto ret = apply(machine, s, i); + out << "\t" << "s" << s << " -> " << "s" << ret.to << " ["; + out << "input=\"" << input_to_string[i.base()] << "\", "; + out << "output=\"" << output_to_string[ret.output.base()] << "\""; + out << "]\n"; + } + } + + out << "}" << endl; + } +} + diff --git a/src/stats.cpp b/src/stats.cpp index 6b55a53..23e1a4d 100644 --- a/src/stats.cpp +++ b/src/stats.cpp @@ -10,7 +10,7 @@ using namespace std; void print_stats_for_machine(string filename){ - const auto machine = read_mealy_from_dot(filename); + const auto machine = read_mealy_from_dot(filename).first; cout << "machine " << filename << " has\n"; cout << '\t' << machine.graph_size << " states\n";