1
Fork 0
mirror of https://github.com/Jaxan/hybrid-ads.git synced 2025-04-27 15:07:45 +02:00

Adds other kind of split

This commit is contained in:
Joshua Moerman 2015-02-16 16:59:05 +01:00
parent c2f58c4c94
commit c945740cb5
2 changed files with 143 additions and 25 deletions

View file

@ -37,3 +37,17 @@ inline auto is_complete(const Mealy & m){
}
return true;
}
inline auto apply(Mealy const & m, size_t state, size_t input){
return m.graph[state][input];
}
template <typename Iterator>
auto apply(Mealy const & m, size_t state, Iterator b, Iterator e){
Mealy::edge ret;
while(b != e){
ret = apply(m, state, *b++);
state = ret.to;
}
return ret;
}

View file

@ -1,38 +1,58 @@
#include <partition.hpp>
#include <mealy.hpp>
#include <partition.hpp>
#include <read_mealy_from_dot.hpp>
#include <cassert>
#include <numeric>
#include <queue>
#include <vector>
#include <type_traits>
#include <vector>
using namespace std;
int verbose = 0;
// TODO: I was working on this...
// I didn't know how to do lca for this case...
struct splijtboom {
splijtboom(size_t N)
: states(N)
{
iota(begin(states), end(states), 0);
}
vector<size_t> states;
vector<splijtboom> children;
const splijtboom * parent = nullptr;
vector<size_t> seperator;
int mark = 0;
};
template <typename Fun>
bool lca_impl(const splijtboom & node, Fun && f){
int count = 0;
for(auto && c : node.children){
if(lca_impl(c, f)) count++;
void lca_impl1(splijtboom & node, Fun && f){
node.mark = 0;
if(!node.children.empty()){
for(auto && c : node.children){
lca_impl1(c, f);
if(c.mark) node.mark++;
}
} else {
for(auto && s : node.states){
if(f(s)) node.mark++;
}
}
if(count >= 2) return true;
}
splijtboom & lca_impl2(splijtboom & node){
if(node.mark > 1) return node;
for(auto && c : node.children){
if(c.mark > 0) return lca_impl2(c);
}
return node; // this is a leaf
}
template <typename Fun>
const splijtboom & lca(const splijtboom & root, Fun && f){
splijtboom & lca(splijtboom & root, Fun && f){
static_assert(is_same<decltype(f(0)), bool>::value, "f should return a bool");
lca_impl(root, f);
lca_impl1(root, f);
return lca_impl2(root);
}
int main(int argc, char *argv[]){
@ -47,22 +67,34 @@ int main(int argc, char *argv[]){
const auto Q = g.output_indices.size();
partition_refine part(N);
splijtboom root(N);
cout << "starting with " << part.size() << " blocks / " << N << " states" << endl;
queue<partition_refine::BlockRef> work;
const auto push = [&work](auto br){ work.push(br); };
queue<pair<partition_refine::BlockRef, reference_wrapper<splijtboom>>> work;
const auto push = [&work](auto br, auto & sp){ work.push({br, sp});
cout << "pushed "; for(auto && x : sp.states) cout << x; cout << endl; };
const auto pop = [&work](){ const auto r = work.front(); work.pop(); return r; };
push(part.find(0));
push(part.find(0), root);
while(!work.empty()){
auto block = pop();
if(elems_in(*block) == 1) continue;
auto block_boom = pop();
auto block = block_boom.first;
splijtboom & boom = block_boom.second;
bool splitted = false;
for(int symbol = 0; symbol < P; ++symbol){
cout << "current\t";
for(auto s : boom.states) cout << s << " ";
cout << endl;
if(boom.states.size() == 1) continue;
// if(elems_in(*block) == 1) continue;
cout << "considering" << endl;
// First try to split on output
for(size_t symbol = 0; symbol < P; ++symbol){
auto new_blocks = part.refine(block, [symbol, &g](size_t state){
return g.graph[state][symbol].output;
return apply(g, state, symbol).output;
}, Q);
if(elems_in(new_blocks) == 1){
@ -73,14 +105,86 @@ int main(int argc, char *argv[]){
}
// a succesful split, add the children
const auto nb = distance(new_blocks.first, new_blocks.second);
boom.children.assign(nb, splijtboom(0));
boom.seperator = {symbol};
auto i = 0;
while(new_blocks.first != new_blocks.second){
push(new_blocks.first++);
for(auto && s : *new_blocks.first){
boom.children[i].states.push_back(s);
}
push(new_blocks.first++, boom.children[i++]);
}
splitted = true;
break;
cout << "splitted output into " << nb << endl;
goto has_split;
}
if(!splitted) cout << "no split :(" << endl;
// Then try to split on state
for(size_t symbol = 0; symbol < P; ++symbol){
vector<bool> successor_states(N, false);
for(auto && state : *block){
successor_states[g.graph[state][symbol].to] = true;
}
auto & oboom = lca(root, [&successor_states](size_t state) -> bool{
return successor_states[state];
});
if(oboom.children.empty()){
// a leaf, hence not a split, try other symbols
continue;
}
cout << "split\t";
for(auto s : oboom.states) cout << s << " ";
cout << endl;
cout << "into ";
for(auto & c : oboom.children) {
for(auto s : c.states) cout << s << " ";
cout << "- ";
}
cout << endl;
// a succesful split, construct the children
boom.seperator.resize(oboom.seperator.size() + 1);
auto it = begin(boom.seperator);
*it++ = symbol;
copy(begin(oboom.seperator), end(oboom.seperator), it);
auto new_blocks = part.refine(block, [&boom, &g](size_t state){
return apply(g, state, begin(boom.seperator), end(boom.seperator)).output;
}, Q);
if(elems_in(new_blocks) == 1){
throw logic_error("Refinement did not give finer partition, can not happen");
}
const auto nb = distance(new_blocks.first, new_blocks.second);
boom.children.assign(nb, splijtboom(0));
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++]);
}
cout << "splitted state into " << nb << endl;
goto has_split;
}
push(block, boom);
cout << "no split :(" << endl;
has_split:
cout << "we have " << part.size() << " blocks / " << N << " states" << endl;
cout << "and still " << work.size() << " work" << endl << endl;
}
cout << "jippiejeejjo" << endl;
}