mirror of
https://github.com/Jaxan/hybrid-ads.git
synced 2025-04-27 15:07:45 +02:00
Restructures partition-API. Adds LY-validity check.
This commit is contained in:
parent
556abfa569
commit
f4f5f5713f
3 changed files with 134 additions and 127 deletions
|
@ -8,81 +8,94 @@
|
|||
|
||||
#include <iostream>
|
||||
|
||||
namespace std {
|
||||
template <typename Iterator>
|
||||
auto begin(pair<Iterator, Iterator> p) { return p.first; }
|
||||
template <typename Iterator>
|
||||
auto end(pair<Iterator, Iterator> p) { return ++p.second; } // Kind of stupid
|
||||
}
|
||||
using Elements = std::list<size_t>;
|
||||
|
||||
template <typename R>
|
||||
size_t elems_in(R range){
|
||||
size_t ret = 0;
|
||||
struct Block {
|
||||
Elements::iterator first;
|
||||
Elements::iterator second;
|
||||
|
||||
auto b = range.first;
|
||||
auto e = range.second;
|
||||
while(b++ != e) ret++;
|
||||
return ret;
|
||||
}
|
||||
auto begin() const { return first; }
|
||||
auto end() const { return std::next(second); }
|
||||
|
||||
bool operator==(Block const & rh) const {
|
||||
return first == rh.first && second == rh.second;
|
||||
}
|
||||
};
|
||||
|
||||
struct partition_refine {
|
||||
using Elements = std::list<size_t>;
|
||||
using Block = std::pair<Elements::iterator, Elements::iterator>;
|
||||
using Blocks = std::list<Block>;
|
||||
using BlockRef = Blocks::iterator;
|
||||
|
||||
partition_refine(size_t n)
|
||||
: elements(n, 0)
|
||||
, blocks{{begin(elements), --end(elements)}}
|
||||
, find_table(n, begin(blocks))
|
||||
, blocks{{elements.begin(), --elements.end()}}
|
||||
{
|
||||
std::iota(begin(elements), end(elements), 0);
|
||||
std::iota(elements.begin(), elements.end(), 0);
|
||||
}
|
||||
|
||||
auto find(size_t element){
|
||||
return find_table[element];
|
||||
}
|
||||
partition_refine(Block b)
|
||||
: elements(b.begin(), b.end())
|
||||
, blocks{{elements.begin(), --elements.end()}}
|
||||
{}
|
||||
|
||||
auto size() const {
|
||||
return blocks.size();
|
||||
partition_refine() = delete;
|
||||
partition_refine(partition_refine const &) = delete;
|
||||
partition_refine& operator=(partition_refine const &) = delete;
|
||||
partition_refine(partition_refine&&) = default;
|
||||
partition_refine& operator=(partition_refine&&) = default;
|
||||
|
||||
auto size() const { return blocks.size(); }
|
||||
auto begin() { return blocks.begin(); }
|
||||
auto end() { return blocks.end(); }
|
||||
|
||||
// Deprecated since there is no more O(1) lookup
|
||||
auto find(size_t x){
|
||||
for(auto & b : blocks){
|
||||
auto it = std::find(b.begin(), b.end(), x);
|
||||
if(it != b.begin()) return b;
|
||||
}
|
||||
|
||||
return Block{};
|
||||
}
|
||||
|
||||
template <typename F>
|
||||
auto refine(BlockRef br, F && function, size_t output_size){
|
||||
auto refine(Block br, F && function, size_t output_size){
|
||||
static_assert(std::is_same<decltype(function(0)), size_t>::value, "Function should return size_t");
|
||||
if(br == BlockRef{}) throw std::logic_error("Passing null ref");
|
||||
if(br == blocks.end()) throw std::logic_error("Invalid block");
|
||||
if(br->first == elements.end() || br->second == elements.end()) throw std::logic_error("Invalid block range");
|
||||
if(br == Block{}) throw std::logic_error("Empty block range");
|
||||
if(br.first == elements.end() || br.second == elements.end()) throw std::logic_error("Invalid block range");
|
||||
|
||||
Blocks new_blocks;
|
||||
std::vector<BlockRef> A(output_size);
|
||||
|
||||
auto b = *br;
|
||||
auto r1 = blocks.erase(br);
|
||||
auto r2 = r1;
|
||||
|
||||
auto it = begin(b);
|
||||
auto ed = end(b);
|
||||
auto it = br.begin();
|
||||
auto ed = br.end();
|
||||
while(it != ed){
|
||||
const auto x = *it;
|
||||
const auto y = function(x);
|
||||
const auto y = function(*it);
|
||||
if(y >= output_size) throw std::runtime_error("Output is too big");
|
||||
|
||||
auto & ar = A[y];
|
||||
if(ar == BlockRef{}){
|
||||
r2 = ar = blocks.insert(r2, {it, it});
|
||||
ar = new_blocks.insert(new_blocks.end(), {it, it});
|
||||
it++;
|
||||
} else {
|
||||
auto current = it++;
|
||||
elements.splice(++ar->second, elements, current);
|
||||
*ar = {ar->first, current};
|
||||
}
|
||||
find_table[x] = ar;
|
||||
}
|
||||
|
||||
return make_pair(r2, r1);
|
||||
return new_blocks;
|
||||
}
|
||||
|
||||
auto replace(BlockRef br, Blocks new_blocks){
|
||||
const auto it = blocks.erase(br);
|
||||
const auto b = new_blocks.begin();
|
||||
const auto e = std::prev(new_blocks.end());
|
||||
blocks.splice(it, new_blocks);
|
||||
return make_pair(b, std::next(e));
|
||||
}
|
||||
|
||||
private:
|
||||
Elements elements;
|
||||
std::list<Block> blocks;
|
||||
std::vector<BlockRef> find_table;
|
||||
Blocks blocks;
|
||||
};
|
||||
|
|
154
src/main.cpp
154
src/main.cpp
|
@ -4,11 +4,12 @@
|
|||
#include <splitting_tree.hpp>
|
||||
#include <write_splitting_tree_to_dot.hpp>
|
||||
|
||||
#include <algorithm>
|
||||
#include <cassert>
|
||||
#include <numeric>
|
||||
#include <iostream>
|
||||
#include <iterator>
|
||||
#include <queue>
|
||||
#include <type_traits>
|
||||
#include <vector>
|
||||
#include <utility>
|
||||
|
||||
using namespace std;
|
||||
|
||||
|
@ -39,10 +40,41 @@ int main(int argc, char *argv[]){
|
|||
cout << "starting with " << part.size() << " blocks / " << N << " states" << endl;
|
||||
|
||||
queue<pair<partition_refine::BlockRef, reference_wrapper<splijtboom>>> 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 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));
|
||||
|
||||
push(part.find(0), root);
|
||||
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++]);
|
||||
}
|
||||
|
||||
if(verbose){
|
||||
cout << "splitted output into " << nb << endl;
|
||||
}
|
||||
};
|
||||
const auto is_valid = [N, &g](auto blocks, auto symbol){
|
||||
for(auto && block : blocks) {
|
||||
partition_refine s_part(block);
|
||||
const auto new_blocks = s_part.refine(*s_part.begin(), [symbol, &g](state state){
|
||||
return apply(g, state, symbol).to.base();
|
||||
}, N);
|
||||
for(auto && new_block : new_blocks){
|
||||
if(distance(new_block.begin(), new_block.end()) != 1) return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
};
|
||||
|
||||
push(part.begin(), root);
|
||||
|
||||
size_t days_without_progress = 0;
|
||||
|
||||
while(!work.empty()){
|
||||
auto block_boom = pop();
|
||||
|
@ -56,42 +88,23 @@ int main(int argc, char *argv[]){
|
|||
}
|
||||
|
||||
if(boom.states.size() == 1) continue;
|
||||
// if(elems_in(*block) == 1) continue;
|
||||
|
||||
if(verbose){
|
||||
cout << "considering" << endl;
|
||||
}
|
||||
|
||||
// First try to split on output
|
||||
for(input symbol = 0; symbol < P; ++symbol){
|
||||
auto new_blocks = part.refine(block, [symbol, &g](state state){
|
||||
const auto new_blocks = part.refine(*block, [symbol, &g](state state){
|
||||
return apply(g, state, symbol).output.base();
|
||||
}, Q);
|
||||
|
||||
if(elems_in(new_blocks) == 1){
|
||||
// continue with other input symbols
|
||||
// (refine always updates the block)
|
||||
block = new_blocks.first;
|
||||
continue;
|
||||
}
|
||||
// no split -> continue with other input symbols
|
||||
if(new_blocks.size() == 1) continue;
|
||||
|
||||
// a succesful split, add the children
|
||||
const auto nb = distance(new_blocks.first, new_blocks.second);
|
||||
boom.children.assign(nb, splijtboom(0));
|
||||
// not a valid split -> continue
|
||||
if(!is_valid(new_blocks, symbol)) continue;
|
||||
|
||||
// a succesful split, update partition and add the children
|
||||
boom.seperator = {symbol};
|
||||
|
||||
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++]);
|
||||
}
|
||||
|
||||
if(verbose){
|
||||
cout << "splitted output into " << nb << endl;
|
||||
}
|
||||
const auto range = part.replace(block, move(new_blocks));
|
||||
add_push_new_block(range, boom);
|
||||
|
||||
goto has_split;
|
||||
}
|
||||
|
@ -107,61 +120,42 @@ int main(int argc, char *argv[]){
|
|||
return successor_states[state.base()];
|
||||
});
|
||||
|
||||
if(oboom.children.empty()){
|
||||
// a leaf, hence not a split, try other symbols
|
||||
// a leaf, hence not a split -> try other symbols
|
||||
if(oboom.children.empty()) continue;
|
||||
|
||||
// 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();
|
||||
}, 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";
|
||||
continue;
|
||||
}
|
||||
|
||||
if(verbose){
|
||||
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.base();
|
||||
}, 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++]);
|
||||
}
|
||||
|
||||
if(verbose){
|
||||
cout << "splitted state into " << nb << endl;
|
||||
}
|
||||
// update partition and add the children
|
||||
boom.seperator = word;
|
||||
const auto range = part.replace(block, move(new_blocks));
|
||||
add_push_new_block(range, boom);
|
||||
|
||||
goto has_split;
|
||||
}
|
||||
push(block, boom);
|
||||
|
||||
cout << "no split :(" << endl;
|
||||
if(days_without_progress++ >= work.size()) {
|
||||
cerr << "No distinguishing seq found!\n";
|
||||
break;
|
||||
}
|
||||
push(block, boom);
|
||||
continue;
|
||||
|
||||
has_split:
|
||||
cout << "we have " << part.size() << " blocks / " << N << " states" << endl;
|
||||
cout << "and still " << work.size() << " work" << endl;
|
||||
cout << "blocks: " << part.size() << ", states: " << N << ", work: " << work.size() << endl;
|
||||
days_without_progress = 0;
|
||||
}
|
||||
|
||||
write_splitting_tree_to_dot(root, filename + ".splitting_tree.dot");
|
||||
|
|
|
@ -8,23 +8,23 @@ int main(int argc, char *argv[]){
|
|||
partition_refine p(50);
|
||||
|
||||
auto bs = p.refine(p.find(0), [](size_t x){ return x % 1; }, 1);
|
||||
cout << elems_in(bs) << endl;
|
||||
cout << bs.size() << endl;
|
||||
|
||||
bs = p.refine(p.find(0), [](size_t x){ return x % 2; }, 2);
|
||||
cout << elems_in(bs) << endl;
|
||||
cout << bs.size() << endl;
|
||||
|
||||
bs = p.refine(p.find(0), [](size_t x){ return x % 3; }, 3);
|
||||
cout << elems_in(bs) << endl;
|
||||
cout << bs.size() << endl;
|
||||
|
||||
bs = p.refine(p.find(0), [](size_t x){ return x % 5; }, 5);
|
||||
cout << elems_in(bs) << endl;
|
||||
cout << bs.size() << endl;
|
||||
|
||||
bs = p.refine(p.find(0), [](size_t x){ return x % 7; }, 7);
|
||||
cout << elems_in(bs) << endl;
|
||||
cout << bs.size() << endl;
|
||||
|
||||
for(int i = 0; i < 50; ++i){
|
||||
cout << i << ":\t";
|
||||
const auto block = *p.find(i);
|
||||
const auto block = p.find(i);
|
||||
for(auto && x : block) cout << x << " ";
|
||||
cout << endl;
|
||||
}
|
||||
|
|
Loading…
Add table
Reference in a new issue