diff --git a/lib/splitting_tree.hpp b/lib/splitting_tree.hpp index 8dfd0e3..d77b50e 100644 --- a/lib/splitting_tree.hpp +++ b/lib/splitting_tree.hpp @@ -7,8 +7,9 @@ #include struct splijtboom { - splijtboom(size_t N) + splijtboom(size_t N, size_t depth) : states(N) + , depth(depth) { std::iota(begin(states), end(states), 0); } @@ -16,7 +17,8 @@ struct splijtboom { std::vector states; std::vector children; std::vector seperator; - int mark = 0; + size_t depth = 0; + int mark = 0; // used for some algorithms... }; template diff --git a/prime-lstar-13.dot b/prime-lstar-13.dot deleted file mode 100644 index a59d8c2..0000000 --- a/prime-lstar-13.dot +++ /dev/null @@ -1,46 +0,0 @@ -digraph g { -__start0 [label="" shape="none"]; - - s0 [shape="circle" label="0"]; - s1 [shape="circle" label="1"]; - s2 [shape="circle" label="2"]; - s3 [shape="circle" label="3"]; - s4 [shape="circle" label="4"]; - s5 [shape="circle" label="5"]; - s6 [shape="circle" label="6"]; - s7 [shape="circle" label="7"]; - s8 [shape="circle" label="8"]; - s9 [shape="circle" label="9"]; - s0 -> s1 [label="INCR / OK"]; - s0 -> s0 [label="DECR / ERROR"]; - s0 -> s0 [label="GET / NO"]; - s1 -> s2 [label="INCR / OK"]; - s1 -> s0 [label="DECR / OK"]; - s1 -> s1 [label="GET / NO"]; - s2 -> s4 [label="INCR / OK"]; - s2 -> s1 [label="DECR / OK"]; - s2 -> s2 [label="GET / YES"]; - s3 -> s9 [label="INCR / OK"]; - s3 -> s4 [label="DECR / OK"]; - s3 -> s3 [label="GET / NO"]; - s4 -> s3 [label="INCR / OK"]; - s4 -> s2 [label="DECR / OK"]; - s4 -> s4 [label="GET / YES"]; - s5 -> s6 [label="INCR / OK"]; - s5 -> s9 [label="DECR / OK"]; - s5 -> s5 [label="GET / NO"]; - s6 -> s7 [label="INCR / OK"]; - s6 -> s5 [label="DECR / OK"]; - s6 -> s6 [label="GET / YES"]; - s7 -> s8 [label="INCR / OK"]; - s7 -> s6 [label="DECR / OK"]; - s7 -> s7 [label="GET / NO"]; - s8 -> s3 [label="INCR / OK"]; - s8 -> s7 [label="DECR / OK"]; - s8 -> s8 [label="GET / NO"]; - s9 -> s5 [label="INCR / OK"]; - s9 -> s3 [label="DECR / OK"]; - s9 -> s9 [label="GET / YES"]; - -__start0 -> s0; -} \ No newline at end of file diff --git a/src/main.cpp b/src/main.cpp index 8106e29..119576f 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -6,6 +6,7 @@ #include #include +#include #include #include #include @@ -13,6 +14,16 @@ using namespace std; +template +ostream & operator<<(ostream& out, vector 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 @@ -28,23 +39,27 @@ int main(int argc, char *argv[]){ 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); assert(is_complete(g)); + 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); - cout << "starting with " << part.size() << " blocks / " << N << " states" << endl; + splijtboom root(N, 0); + vector> succession; queue>> 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.children.assign(nb, splijtboom(0, boom.depth + 1)); auto i = 0; while(new_blocks.first != new_blocks.second){ @@ -71,15 +86,23 @@ int main(int argc, char *argv[]){ } 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(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()){ - auto block_boom = pop(); - auto block = block_boom.first; + 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"; @@ -91,8 +114,10 @@ int main(int argc, char *argv[]){ // First try to split on output for(input symbol = 0; symbol < P; ++symbol){ - const auto new_blocks = part.refine(*block, [symbol, &g](state state){ - return apply(g, state, symbol).output.base(); + 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 @@ -116,7 +141,7 @@ int main(int argc, char *argv[]){ successor_states[apply(g, state, symbol).to.base()] = true; } - auto & oboom = lca(root, [&successor_states](state state) -> bool{ + const auto & oboom = lca(root, [&successor_states](state state) -> bool{ return successor_states[state.base()]; }); @@ -125,15 +150,17 @@ int main(int argc, char *argv[]){ // possibly a succesful split, construct the children const auto word = concat({symbol}, oboom.seperator); - const auto new_blocks = part.refine(*block, [word, &g](size_t state){ - return apply(g, state, begin(word), end(word)).output.base(); + 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"; + // cerr << "WARNING: Refinement did not give finer partition, can not happen\n"; continue; } @@ -145,19 +172,126 @@ int main(int argc, char *argv[]){ goto has_split; } - cout << "no split :(" << endl; + // cout << "no split :(" << endl; if(days_without_progress++ >= work.size()) { - cerr << "No distinguishing seq found!\n"; + 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; + // cout << "blocks: " << part.size() << ", states: " << N << ", work: " << work.size() << endl; days_without_progress = 0; } + cerr << "\tdone\n"; - write_splitting_tree_to_dot(root, filename + ".splitting_tree.dot"); + cerr << "* Write splitting tree\n"; + write_splitting_tree_to_dot(root, filename + "." + filename_thingy + "splitting_tree"); + 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 I; + vector C; + vector word; + vector children; + } root_seq(N); + + cerr << "* Lee and Yannakaki II\n"; + { + queue> work2; + work2.push(root_seq); + + while(!work2.empty()){ + dist_seq & node = work2.front(); + work2.pop(); + + if(node.C.size() < 2) continue; + + vector 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"; + { + ofstream out(filename + "." + filename_thingy + "dist_seq"); + out << "digraph distinguishing_sequence {\n"; + + // breadth first + int global_id = 0; + queue>> 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; }