mirror of
https://github.com/Jaxan/hybrid-ads.git
synced 2025-04-27 23:17:44 +02:00
Adds partition refinement, and reading mealy machine
This commit is contained in:
commit
c2f58c4c94
12 changed files with 273216 additions and 0 deletions
15
CMakeLists.txt
Normal file
15
CMakeLists.txt
Normal file
|
@ -0,0 +1,15 @@
|
||||||
|
project(Yannakakis)
|
||||||
|
cmake_minimum_required(VERSION 2.8)
|
||||||
|
|
||||||
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++1y")
|
||||||
|
|
||||||
|
find_package(Boost REQUIRED COMPONENTS program_options filesystem system serialization)
|
||||||
|
include_directories(SYSTEM ${Boost_INCLUDE_DIRS})
|
||||||
|
set(libs ${libs} ${Boost_LIBRARIES})
|
||||||
|
|
||||||
|
# add_subdirectory("contrib")
|
||||||
|
add_subdirectory("lib")
|
||||||
|
add_subdirectory("src")
|
||||||
|
|
||||||
|
# file(GLOB resources "resources/*")
|
||||||
|
# file(COPY ${resources} DESTINATION ${CMAKE_BINARY_DIR})
|
272803
esm-manual-controller.dot
Normal file
272803
esm-manual-controller.dot
Normal file
File diff suppressed because it is too large
Load diff
9
lib/CMakeLists.txt
Normal file
9
lib/CMakeLists.txt
Normal file
|
@ -0,0 +1,9 @@
|
||||||
|
|
||||||
|
file(GLOB_RECURSE sources "*.cpp")
|
||||||
|
file(GLOB_RECURSE headers "*.hpp")
|
||||||
|
|
||||||
|
set(libs)
|
||||||
|
|
||||||
|
add_library(common ${headers} ${sources})
|
||||||
|
target_link_libraries(common ${libs})
|
||||||
|
target_include_directories(common PUBLIC ".")
|
2
lib/dummy.cpp
Normal file
2
lib/dummy.cpp
Normal file
|
@ -0,0 +1,2 @@
|
||||||
|
static int x=x;
|
||||||
|
|
39
lib/mealy.hpp
Normal file
39
lib/mealy.hpp
Normal file
|
@ -0,0 +1,39 @@
|
||||||
|
#pragma once
|
||||||
|
|
||||||
|
#include <map>
|
||||||
|
#include <string>
|
||||||
|
#include <vector>
|
||||||
|
|
||||||
|
/*
|
||||||
|
* 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,
|
||||||
|
* but partiality still can occur.
|
||||||
|
*/
|
||||||
|
struct Mealy {
|
||||||
|
struct edge {
|
||||||
|
size_t to = -1;
|
||||||
|
size_t output = -1;
|
||||||
|
};
|
||||||
|
|
||||||
|
std::map<std::string, size_t> nodes_indices;
|
||||||
|
std::map<std::string, size_t> input_indices;
|
||||||
|
std::map<std::string, size_t> output_indices;
|
||||||
|
|
||||||
|
// state -> input -> (output, state)
|
||||||
|
std::vector<std::vector<edge>> graph;
|
||||||
|
|
||||||
|
// these are actually redundant!
|
||||||
|
size_t graph_size = 0;
|
||||||
|
size_t input_size = 0;
|
||||||
|
size_t output_size = 0;
|
||||||
|
};
|
||||||
|
|
||||||
|
inline auto is_complete(const Mealy & m){
|
||||||
|
for(int n = 0; n < m.graph_size; ++n){
|
||||||
|
if(m.graph[n].size() != m.input_size) return false;
|
||||||
|
for(auto && e : m.graph[n]) if(e.to == -1 || e.output == -1) return false;
|
||||||
|
}
|
||||||
|
return true;
|
||||||
|
}
|
88
lib/partition.hpp
Normal file
88
lib/partition.hpp
Normal file
|
@ -0,0 +1,88 @@
|
||||||
|
#pragma once
|
||||||
|
|
||||||
|
#include <list>
|
||||||
|
#include <numeric>
|
||||||
|
#include <type_traits>
|
||||||
|
#include <utility>
|
||||||
|
#include <vector>
|
||||||
|
|
||||||
|
#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
|
||||||
|
}
|
||||||
|
|
||||||
|
template <typename R>
|
||||||
|
size_t elems_in(R range){
|
||||||
|
size_t ret = 0;
|
||||||
|
|
||||||
|
auto b = range.first;
|
||||||
|
auto e = range.second;
|
||||||
|
while(b++ != e) ret++;
|
||||||
|
return ret;
|
||||||
|
}
|
||||||
|
|
||||||
|
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))
|
||||||
|
{
|
||||||
|
std::iota(begin(elements), end(elements), 0);
|
||||||
|
}
|
||||||
|
|
||||||
|
auto find(size_t element){
|
||||||
|
return find_table[element];
|
||||||
|
}
|
||||||
|
|
||||||
|
auto size() const {
|
||||||
|
return blocks.size();
|
||||||
|
}
|
||||||
|
|
||||||
|
template <typename F>
|
||||||
|
auto refine(BlockRef 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");
|
||||||
|
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);
|
||||||
|
while(it != ed){
|
||||||
|
const auto x = *it;
|
||||||
|
const auto y = function(x);
|
||||||
|
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});
|
||||||
|
it++;
|
||||||
|
} else {
|
||||||
|
auto current = it++;
|
||||||
|
elements.splice(++ar->second, elements, current);
|
||||||
|
*ar = {ar->first, current};
|
||||||
|
}
|
||||||
|
find_table[x] = ar;
|
||||||
|
}
|
||||||
|
|
||||||
|
return make_pair(r2, r1);
|
||||||
|
}
|
||||||
|
|
||||||
|
private:
|
||||||
|
Elements elements;
|
||||||
|
std::list<Block> blocks;
|
||||||
|
std::vector<BlockRef> find_table;
|
||||||
|
};
|
79
lib/read_mealy_from_dot.cpp
Normal file
79
lib/read_mealy_from_dot.cpp
Normal file
|
@ -0,0 +1,79 @@
|
||||||
|
#include "read_mealy_from_dot.hpp"
|
||||||
|
|
||||||
|
#include "mealy.hpp"
|
||||||
|
|
||||||
|
#include <fstream>
|
||||||
|
#include <iostream>
|
||||||
|
#include <sstream>
|
||||||
|
#include <string>
|
||||||
|
|
||||||
|
using namespace std;
|
||||||
|
|
||||||
|
template <typename T>
|
||||||
|
T get(istream& in){
|
||||||
|
T t;
|
||||||
|
in >> t;
|
||||||
|
return t;
|
||||||
|
}
|
||||||
|
|
||||||
|
Mealy read_mealy_from_dot(istream& in, int verbose){
|
||||||
|
Mealy m;
|
||||||
|
|
||||||
|
string line;
|
||||||
|
stringstream ss;
|
||||||
|
while(getline(in, line)){
|
||||||
|
const auto i = line.find("->");
|
||||||
|
if(i == string::npos) continue;
|
||||||
|
|
||||||
|
// get from and to state
|
||||||
|
ss.str(line);
|
||||||
|
ss.seekg(0);
|
||||||
|
const auto lh = get<string>(ss);
|
||||||
|
const auto arrow = get<string>(ss);
|
||||||
|
const auto rh = get<string>(ss);
|
||||||
|
|
||||||
|
// get label
|
||||||
|
const auto l1 = line.find('\"');
|
||||||
|
const auto l2 = line.find('\"', l1+1);
|
||||||
|
if(l1 == string::npos || l2 == string::npos) continue;
|
||||||
|
ss.str(line.substr(l1+1, l2-(l1+1)));
|
||||||
|
ss.seekg(0);
|
||||||
|
|
||||||
|
const auto input = get<string>(ss);
|
||||||
|
const auto slash = get<string>(ss);
|
||||||
|
const auto output = get<string>(ss);
|
||||||
|
|
||||||
|
if(verbose >= 2){
|
||||||
|
cout << lh << '\t' << rh << '\t' << input << '\t' << output << endl;
|
||||||
|
}
|
||||||
|
|
||||||
|
// 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++;
|
||||||
|
|
||||||
|
// add edge
|
||||||
|
m.graph.resize(m.graph_size);
|
||||||
|
auto & v = m.graph[m.nodes_indices[lh]];
|
||||||
|
v.resize(m.input_size);
|
||||||
|
v[m.input_indices[input]] = {m.nodes_indices[rh], m.output_indices[output]};
|
||||||
|
}
|
||||||
|
|
||||||
|
if(verbose >= 1){
|
||||||
|
cout << "input_alphabet = \n";
|
||||||
|
for(auto && i : m.input_indices) cout << i.first << " ";
|
||||||
|
cout << endl;
|
||||||
|
|
||||||
|
cout << "output_alphabet = \n";
|
||||||
|
for(auto && o : m.output_indices) cout << o.first << " ";
|
||||||
|
cout << endl;
|
||||||
|
}
|
||||||
|
|
||||||
|
return m;
|
||||||
|
}
|
||||||
|
|
||||||
|
Mealy read_mealy_from_dot(const string& filename, int verbose){
|
||||||
|
ifstream file(filename);
|
||||||
|
return read_mealy_from_dot(file, verbose);
|
||||||
|
}
|
7
lib/read_mealy_from_dot.hpp
Normal file
7
lib/read_mealy_from_dot.hpp
Normal file
|
@ -0,0 +1,7 @@
|
||||||
|
#pragma once
|
||||||
|
|
||||||
|
#include <iosfwd>
|
||||||
|
|
||||||
|
struct Mealy;
|
||||||
|
Mealy read_mealy_from_dot(const std::string & filename, int verbose);
|
||||||
|
Mealy read_mealy_from_dot(std::istream & input, int verbose);
|
46
prime-lstar-13.dot
Normal file
46
prime-lstar-13.dot
Normal file
|
@ -0,0 +1,46 @@
|
||||||
|
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;
|
||||||
|
}
|
10
src/CMakeLists.txt
Normal file
10
src/CMakeLists.txt
Normal file
|
@ -0,0 +1,10 @@
|
||||||
|
|
||||||
|
set (CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR})
|
||||||
|
|
||||||
|
file(GLOB sources "*.cpp")
|
||||||
|
|
||||||
|
foreach(source ${sources})
|
||||||
|
get_filename_component(exec ${source} NAME_WE)
|
||||||
|
add_executable(${exec} ${source})
|
||||||
|
target_link_libraries(${exec} common ${libs})
|
||||||
|
endforeach()
|
87
src/main.cpp
Normal file
87
src/main.cpp
Normal file
|
@ -0,0 +1,87 @@
|
||||||
|
#include <partition.hpp>
|
||||||
|
#include <mealy.hpp>
|
||||||
|
#include <read_mealy_from_dot.hpp>
|
||||||
|
|
||||||
|
#include <cassert>
|
||||||
|
#include <queue>
|
||||||
|
#include <vector>
|
||||||
|
#include <type_traits>
|
||||||
|
|
||||||
|
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 {
|
||||||
|
vector<size_t> states;
|
||||||
|
vector<splijtboom> children;
|
||||||
|
|
||||||
|
const splijtboom * parent = nullptr;
|
||||||
|
};
|
||||||
|
|
||||||
|
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++;
|
||||||
|
}
|
||||||
|
if(count >= 2) return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
template <typename Fun>
|
||||||
|
const splijtboom & lca(const splijtboom & root, Fun && f){
|
||||||
|
static_assert(is_same<decltype(f(0)), bool>::value, "f should return a bool");
|
||||||
|
lca_impl(root, f);
|
||||||
|
}
|
||||||
|
|
||||||
|
int main(int argc, char *argv[]){
|
||||||
|
if(argc < 2) return 1;
|
||||||
|
if(argc > 2) verbose = argc - 2;
|
||||||
|
|
||||||
|
const auto g = read_mealy_from_dot(argv[1], verbose);
|
||||||
|
assert(is_complete(g));
|
||||||
|
|
||||||
|
const auto N = g.graph.size();
|
||||||
|
const auto P = g.input_indices.size();
|
||||||
|
const auto Q = g.output_indices.size();
|
||||||
|
|
||||||
|
partition_refine part(N);
|
||||||
|
cout << "starting with " << part.size() << " blocks / " << N << " states" << endl;
|
||||||
|
|
||||||
|
queue<partition_refine::BlockRef> work;
|
||||||
|
const auto push = [&work](auto br){ work.push(br); };
|
||||||
|
const auto pop = [&work](){ const auto r = work.front(); work.pop(); return r; };
|
||||||
|
|
||||||
|
push(part.find(0));
|
||||||
|
|
||||||
|
while(!work.empty()){
|
||||||
|
auto block = pop();
|
||||||
|
if(elems_in(*block) == 1) continue;
|
||||||
|
|
||||||
|
bool splitted = false;
|
||||||
|
for(int symbol = 0; symbol < P; ++symbol){
|
||||||
|
auto new_blocks = part.refine(block, [symbol, &g](size_t state){
|
||||||
|
return g.graph[state][symbol].output;
|
||||||
|
}, Q);
|
||||||
|
|
||||||
|
if(elems_in(new_blocks) == 1){
|
||||||
|
// continue with other input symbols
|
||||||
|
// (refine always updates the block)
|
||||||
|
block = new_blocks.first;
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
|
||||||
|
// a succesful split, add the children
|
||||||
|
while(new_blocks.first != new_blocks.second){
|
||||||
|
push(new_blocks.first++);
|
||||||
|
}
|
||||||
|
splitted = true;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
if(!splitted) cout << "no split :(" << endl;
|
||||||
|
cout << "we have " << part.size() << " blocks / " << N << " states" << endl;
|
||||||
|
}
|
||||||
|
cout << "jippiejeejjo" << endl;
|
||||||
|
}
|
||||||
|
|
31
src/partition_test.cpp
Normal file
31
src/partition_test.cpp
Normal file
|
@ -0,0 +1,31 @@
|
||||||
|
#include <partition.hpp>
|
||||||
|
|
||||||
|
#include <iostream>
|
||||||
|
|
||||||
|
using namespace std;
|
||||||
|
|
||||||
|
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;
|
||||||
|
|
||||||
|
bs = p.refine(p.find(0), [](size_t x){ return x % 2; }, 2);
|
||||||
|
cout << elems_in(bs) << endl;
|
||||||
|
|
||||||
|
bs = p.refine(p.find(0), [](size_t x){ return x % 3; }, 3);
|
||||||
|
cout << elems_in(bs) << endl;
|
||||||
|
|
||||||
|
bs = p.refine(p.find(0), [](size_t x){ return x % 5; }, 5);
|
||||||
|
cout << elems_in(bs) << endl;
|
||||||
|
|
||||||
|
bs = p.refine(p.find(0), [](size_t x){ return x % 7; }, 7);
|
||||||
|
cout << elems_in(bs) << endl;
|
||||||
|
|
||||||
|
for(int i = 0; i < 50; ++i){
|
||||||
|
cout << i << ":\t";
|
||||||
|
const auto block = *p.find(i);
|
||||||
|
for(auto && x : block) cout << x << " ";
|
||||||
|
cout << endl;
|
||||||
|
}
|
||||||
|
}
|
Loading…
Add table
Reference in a new issue