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

Adds script to complete partial dots

This commit is contained in:
Joshua Moerman 2015-12-22 12:27:53 +01:00
parent b990221c3c
commit 5fe44a2179
3 changed files with 118 additions and 18 deletions

View file

@ -15,7 +15,7 @@ static string easy_substr(string const & s, size_t begin, size_t end){
return s.substr(begin, end - begin); return s.substr(begin, end - begin);
} }
mealy read_mealy_from_txt(std::istream & in) { mealy read_mealy_from_txt(std::istream & in, bool check) {
mealy m; mealy m;
state max_state = 0; state max_state = 0;
@ -54,16 +54,16 @@ mealy read_mealy_from_txt(std::istream & in) {
if (m.graph_size == 0) throw runtime_error("Empty state set"); if (m.graph_size == 0) throw runtime_error("Empty state set");
if (m.input_size == 0) throw runtime_error("Empty input set"); if (m.input_size == 0) throw runtime_error("Empty input set");
if (m.output_size == 0) throw runtime_error("Empty output set"); if (m.output_size == 0) throw runtime_error("Empty output set");
if (!is_complete(m)) throw runtime_error("Partial machine"); if (check && !is_complete(m)) throw runtime_error("Partial machine");
return m; return m;
} }
mealy read_mealy_from_txt(const std::string & filename) { mealy read_mealy_from_txt(const std::string & filename, bool check) {
std::ifstream file(filename); std::ifstream file(filename);
return read_mealy_from_txt(file); return read_mealy_from_txt(file, check);
} }
mealy read_mealy_from_dot(std::istream & in, translation & t){ mealy read_mealy_from_dot(std::istream & in, translation & t, bool check){
mealy m; mealy m;
std::unordered_map<std::string, state> state_indices; std::unordered_map<std::string, state> state_indices;
@ -116,27 +116,27 @@ mealy read_mealy_from_dot(std::istream & in, translation & t){
if(m.graph_size == 0) throw runtime_error("Empty state set"); if(m.graph_size == 0) throw runtime_error("Empty state set");
if(m.input_size == 0) throw runtime_error("Empty input set"); if(m.input_size == 0) throw runtime_error("Empty input set");
if(m.output_size == 0) throw runtime_error("Empty output set"); if(m.output_size == 0) throw runtime_error("Empty output set");
if(!is_complete(m)) throw runtime_error("Partial machine"); if(check && !is_complete(m)) throw runtime_error("Partial machine");
return m; return m;
} }
mealy read_mealy_from_dot(const string & filename, translation & t){ mealy read_mealy_from_dot(const string & filename, translation & t, bool check){
ifstream file(filename); ifstream file(filename);
return read_mealy_from_dot(file, t); return read_mealy_from_dot(file, t, check);
} }
std::pair<mealy, translation> read_mealy_from_dot(istream & in){ std::pair<mealy, translation> read_mealy_from_dot(istream & in, bool check){
translation t; translation t;
const auto m = read_mealy_from_dot(in, t); const auto m = read_mealy_from_dot(in, t, check);
return {move(m), move(t)}; return {move(m), move(t)};
} }
std::pair<mealy, translation> read_mealy_from_dot(const string & filename){ std::pair<mealy, translation> read_mealy_from_dot(const string & filename, bool check){
translation t; translation t;
const auto m = read_mealy_from_dot(filename, t); const auto m = read_mealy_from_dot(filename, t, check);
return {move(m), move(t)}; return {move(m), move(t)};
} }

View file

@ -12,18 +12,18 @@ struct translation;
/// \brief reads a mealy machine from plain txt file as provided by A. T. Endo /// \brief reads a mealy machine from plain txt file as provided by A. T. Endo
/// States, inputs and outputs in these files are already integral, so no need for translation /// States, inputs and outputs in these files are already integral, so no need for translation
mealy read_mealy_from_txt(std::istream & in); mealy read_mealy_from_txt(std::istream & in, bool check = true);
mealy read_mealy_from_txt(std::string const & filename); mealy read_mealy_from_txt(std::string const & filename, bool check = true);
/// \brief reads a mealy machine from dot files as generated by learnlib /// \brief reads a mealy machine from dot files as generated by learnlib
/// Here we need a translation, which is extended during parsing /// Here we need a translation, which is extended during parsing
mealy read_mealy_from_dot(std::istream & in, translation & t); mealy read_mealy_from_dot(std::istream & in, translation & t, bool check = true);
mealy read_mealy_from_dot(std::string const & filename, translation & t); mealy read_mealy_from_dot(std::string const & filename, translation & t, bool check = true);
/// \brief reads a mealy machine from dot files as generated by learnlib /// \brief reads a mealy machine from dot files as generated by learnlib
/// Here the translation starts out empty and is returned in the end /// Here the translation starts out empty and is returned in the end
std::pair<mealy, translation> read_mealy_from_dot(std::istream & in); std::pair<mealy, translation> read_mealy_from_dot(std::istream & in, bool check = true);
std::pair<mealy, translation> read_mealy_from_dot(std::string const & filename); std::pair<mealy, translation> read_mealy_from_dot(std::string const & filename, bool check = true);
/// \brief For non-integral formats we use a translation to integers /// \brief For non-integral formats we use a translation to integers

100
src/complete.cpp Normal file
View file

@ -0,0 +1,100 @@
#include <adaptive_distinguishing_sequence.hpp>
#include <read_mealy.hpp>
#include <separating_family.hpp>
#include <splitting_tree.hpp>
#include <test_suite.hpp>
#include <transfer_sequences.hpp>
#include <trie.hpp>
#include <docopt.h>
#include <future>
#include <iostream>
#include <random>
#include <string>
using namespace std;
static const char USAGE[] =
R"(FSM-completer (only dot), also renames the state names
Usage:
methods [options] <file>
Options:
-h, --help Show current help
--version Show version
--sink Completion with sink
--loop Completion with self loops (default)
--output <out> Output for new transitions (leave empty for fresh output)
)";
void write_mealy_to_dot(const mealy & m, const translation & translation, std::ostream & out) {
const auto inputs = create_reverse_map(translation.input_indices);
const auto output = create_reverse_map(translation.output_indices);
out << "digraph {\n";
for (state s = 0; s < m.graph_size; ++s) {
for (input i = 0; i < m.input_size; ++i) {
if (!defined(m, s, i)) continue;
const auto ret = apply(m, s, i);
out << s << " -> " << ret.to << " [label=\"" << inputs[i] << " / " << output[ret.out]
<< "\"]\n";
}
}
out << "}\n";
}
int main(int argc, char * argv[]) {
const auto args = docopt::docopt(USAGE, {argv + 1, argv + argc}, true, __DATE__ __TIME__);
const string filename = args.at("<file>").asString();
auto mt = read_mealy_from_dot(filename, false);
auto & machine = mt.first;
auto & translation = mt.second;
if (!is_complete(machine)) {
const auto out = [&]() -> output {
if (args.at("--output")) {
const string out_str = args.at("--output").asString();
if (translation.output_indices.count(out_str)) {
// reuse old output
return translation.output_indices[out_str];
}
}
// else: grab a new one
string newo = "SILENT";
while(translation.output_indices.count(newo)) newo += '0';
return translation.output_indices[newo] = machine.output_size++;
}();
if (args.at("--sink").asBool()) {
// add sink
const auto new_state = machine.graph_size++;
machine.graph.resize(machine.graph_size);
for (state s = 0; s < machine.graph_size; ++s) {
machine.graph[s].resize(machine.input_size);
for (input i = 0; i < machine.input_size; ++i) {
if (defined(machine, s, i)) continue;
machine.graph[s][i] = mealy::edge(new_state, out);
}
}
} else {
// add self loops
for (state s = 0; s < machine.graph_size; ++s) {
machine.graph[s].resize(machine.input_size);
for (input i = 0; i < machine.input_size; ++i) {
if (defined(machine, s, i)) continue;
machine.graph[s][i] = mealy::edge(s, out);
}
}
}
}
write_mealy_to_dot(machine, translation, cout);
}