mirror of
https://github.com/Jaxan/hybrid-ads.git
synced 2025-04-28 07:27:45 +02:00
Adds the construction of a splitting tree
This commit is contained in:
parent
f4f5f5713f
commit
7f923a4c1c
3 changed files with 153 additions and 63 deletions
|
@ -7,8 +7,9 @@
|
||||||
#include <vector>
|
#include <vector>
|
||||||
|
|
||||||
struct splijtboom {
|
struct splijtboom {
|
||||||
splijtboom(size_t N)
|
splijtboom(size_t N, size_t depth)
|
||||||
: states(N)
|
: states(N)
|
||||||
|
, depth(depth)
|
||||||
{
|
{
|
||||||
std::iota(begin(states), end(states), 0);
|
std::iota(begin(states), end(states), 0);
|
||||||
}
|
}
|
||||||
|
@ -16,7 +17,8 @@ struct splijtboom {
|
||||||
std::vector<state> states;
|
std::vector<state> states;
|
||||||
std::vector<splijtboom> children;
|
std::vector<splijtboom> children;
|
||||||
std::vector<input> seperator;
|
std::vector<input> seperator;
|
||||||
int mark = 0;
|
size_t depth = 0;
|
||||||
|
int mark = 0; // used for some algorithms...
|
||||||
};
|
};
|
||||||
|
|
||||||
template <typename Fun>
|
template <typename Fun>
|
||||||
|
|
|
@ -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;
|
|
||||||
}
|
|
164
src/main.cpp
164
src/main.cpp
|
@ -6,6 +6,7 @@
|
||||||
|
|
||||||
#include <algorithm>
|
#include <algorithm>
|
||||||
#include <cassert>
|
#include <cassert>
|
||||||
|
#include <fstream>
|
||||||
#include <iostream>
|
#include <iostream>
|
||||||
#include <iterator>
|
#include <iterator>
|
||||||
#include <queue>
|
#include <queue>
|
||||||
|
@ -13,6 +14,16 @@
|
||||||
|
|
||||||
using namespace std;
|
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;
|
int verbose = 0;
|
||||||
|
|
||||||
template <typename T>
|
template <typename T>
|
||||||
|
@ -28,23 +39,27 @@ int main(int argc, char *argv[]){
|
||||||
if(argc > 2) verbose = argc - 2;
|
if(argc > 2) verbose = argc - 2;
|
||||||
|
|
||||||
const string filename = argv[1];
|
const string filename = argv[1];
|
||||||
|
|
||||||
|
cerr << "* Reading file " << filename << "\n";
|
||||||
const auto g = read_mealy_from_dot(filename, verbose);
|
const auto g = read_mealy_from_dot(filename, verbose);
|
||||||
assert(is_complete(g));
|
assert(is_complete(g));
|
||||||
|
cerr << "\tdone\n";
|
||||||
|
|
||||||
const auto N = g.graph.size();
|
const auto N = g.graph.size();
|
||||||
const auto P = g.input_indices.size();
|
const auto P = g.input_indices.size();
|
||||||
const auto Q = g.output_indices.size();
|
const auto Q = g.output_indices.size();
|
||||||
|
|
||||||
|
cerr << "* Setting up strucutres\n";
|
||||||
partition_refine part(N);
|
partition_refine part(N);
|
||||||
splijtboom root(N);
|
splijtboom root(N, 0);
|
||||||
cout << "starting with " << part.size() << " blocks / " << N << " states" << endl;
|
vector<vector<state>> succession;
|
||||||
|
|
||||||
queue<pair<partition_refine::BlockRef, reference_wrapper<splijtboom>>> work;
|
queue<pair<partition_refine::BlockRef, reference_wrapper<splijtboom>>> work;
|
||||||
const auto push = [&work](auto br, auto & sp) { work.push({br, sp}); };
|
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 pop = [&work]() { const auto r = work.front(); work.pop(); return r; };
|
||||||
const auto add_push_new_block = [&](auto new_blocks, auto & boom) {
|
const auto add_push_new_block = [&](auto new_blocks, auto & boom) {
|
||||||
const auto nb = distance(new_blocks.first, new_blocks.second);
|
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;
|
auto i = 0;
|
||||||
while(new_blocks.first != new_blocks.second){
|
while(new_blocks.first != new_blocks.second){
|
||||||
|
@ -71,15 +86,23 @@ int main(int argc, char *argv[]){
|
||||||
}
|
}
|
||||||
return true;
|
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);
|
push(part.begin(), root);
|
||||||
|
cerr << "\tdone\n";
|
||||||
|
|
||||||
size_t days_without_progress = 0;
|
size_t days_without_progress = 0;
|
||||||
|
string filename_thingy;
|
||||||
|
|
||||||
|
cerr << "* Starting Lee & Yannakakis I\n";
|
||||||
while(!work.empty()){
|
while(!work.empty()){
|
||||||
auto block_boom = pop();
|
const auto block_boom = pop();
|
||||||
auto block = block_boom.first;
|
const auto block = block_boom.first;
|
||||||
splijtboom & boom = block_boom.second;
|
splijtboom & boom = block_boom.second;
|
||||||
|
const auto depth = boom.depth;
|
||||||
|
|
||||||
if(verbose){
|
if(verbose){
|
||||||
cout << "current\t";
|
cout << "current\t";
|
||||||
|
@ -91,8 +114,10 @@ int main(int argc, char *argv[]){
|
||||||
|
|
||||||
// First try to split on output
|
// First try to split on output
|
||||||
for(input symbol = 0; symbol < P; ++symbol){
|
for(input symbol = 0; symbol < P; ++symbol){
|
||||||
const auto new_blocks = part.refine(*block, [symbol, &g](state state){
|
const auto new_blocks = part.refine(*block, [symbol, depth, &g, &update_succession](state state){
|
||||||
return apply(g, state, symbol).output.base();
|
const auto ret = apply(g, state, symbol);
|
||||||
|
update_succession(state, ret.to, depth);
|
||||||
|
return ret.output.base();
|
||||||
}, Q);
|
}, Q);
|
||||||
|
|
||||||
// no split -> continue with other input symbols
|
// 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;
|
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()];
|
return successor_states[state.base()];
|
||||||
});
|
});
|
||||||
|
|
||||||
|
@ -125,15 +150,17 @@ int main(int argc, char *argv[]){
|
||||||
|
|
||||||
// possibly a succesful split, construct the children
|
// possibly a succesful split, construct the children
|
||||||
const auto word = concat({symbol}, oboom.seperator);
|
const auto word = concat({symbol}, oboom.seperator);
|
||||||
const auto new_blocks = part.refine(*block, [word, &g](size_t state){
|
const auto new_blocks = part.refine(*block, [word, depth, &g, &update_succession](state state){
|
||||||
return apply(g, state, begin(word), end(word)).output.base();
|
const auto ret = apply(g, state, begin(word), end(word));
|
||||||
|
update_succession(state, ret.to, depth);
|
||||||
|
return ret.output.base();
|
||||||
}, Q);
|
}, Q);
|
||||||
|
|
||||||
// not a valid split -> continue
|
// not a valid split -> continue
|
||||||
if(!is_valid(new_blocks, symbol)) continue;
|
if(!is_valid(new_blocks, symbol)) continue;
|
||||||
|
|
||||||
if(new_blocks.size() == 1){
|
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;
|
continue;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -145,19 +172,126 @@ int main(int argc, char *argv[]){
|
||||||
goto has_split;
|
goto has_split;
|
||||||
}
|
}
|
||||||
|
|
||||||
cout << "no split :(" << endl;
|
// cout << "no split :(" << endl;
|
||||||
if(days_without_progress++ >= work.size()) {
|
if(days_without_progress++ >= work.size()) {
|
||||||
cerr << "No distinguishing seq found!\n";
|
filename_thingy = "incomplete_";
|
||||||
|
cerr << "\t* No distinguishing seq found!\n";
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
push(block, boom);
|
push(block, boom);
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
has_split:
|
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;
|
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<state> I;
|
||||||
|
vector<state> C;
|
||||||
|
vector<input> word;
|
||||||
|
vector<dist_seq> children;
|
||||||
|
} root_seq(N);
|
||||||
|
|
||||||
|
cerr << "* Lee and Yannakaki II\n";
|
||||||
|
{
|
||||||
|
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";
|
||||||
|
{
|
||||||
|
ofstream out(filename + "." + filename_thingy + "dist_seq");
|
||||||
|
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;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Loading…
Add table
Reference in a new issue