mirror of
https://github.com/Jaxan/hybrid-ads.git
synced 2025-04-27 15:07:45 +02:00
Added restriction to reachable sub machine
This commit is contained in:
parent
2dd5d326cb
commit
098f0e9bff
3 changed files with 67 additions and 3 deletions
56
lib/reachability.cpp
Normal file
56
lib/reachability.cpp
Normal file
|
@ -0,0 +1,56 @@
|
||||||
|
#include "reachability.hpp"
|
||||||
|
#include "mealy.hpp"
|
||||||
|
|
||||||
|
#include <map>
|
||||||
|
#include <queue>
|
||||||
|
#include <vector>
|
||||||
|
|
||||||
|
using namespace std;
|
||||||
|
|
||||||
|
mealy reachable_submachine(const mealy& in, state start) {
|
||||||
|
using state_out = state;
|
||||||
|
state_out max_state = 0;
|
||||||
|
map<state, state_out> new_state;
|
||||||
|
vector<bool> visited(in.graph_size, false);
|
||||||
|
|
||||||
|
mealy out;
|
||||||
|
|
||||||
|
queue<state> work;
|
||||||
|
work.push(start);
|
||||||
|
while (!work.empty()) {
|
||||||
|
state s = work.front();
|
||||||
|
work.pop();
|
||||||
|
|
||||||
|
if (visited[s]) continue;
|
||||||
|
visited[s] = true;
|
||||||
|
|
||||||
|
if (!new_state.count(s)) new_state[s] = max_state++;
|
||||||
|
state_out s2 = new_state[s];
|
||||||
|
|
||||||
|
for (input i = 0; i < in.input_size; ++i) {
|
||||||
|
const auto ret = apply(in, s, i);
|
||||||
|
const output o = ret.output;
|
||||||
|
const state t = ret.to;
|
||||||
|
|
||||||
|
if (!new_state.count(t)) new_state[t] = max_state++;
|
||||||
|
state_out t2 = new_state[t];
|
||||||
|
|
||||||
|
if (out.graph.size() < max_state) out.graph.resize(max_state);
|
||||||
|
if (out.graph[s2].size() < in.input_size) out.graph[s2].resize(in.input_size);
|
||||||
|
out.graph[s2][i] = {t2, o};
|
||||||
|
|
||||||
|
if (!visited[t]) work.push(t);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
out.graph_size = max_state;
|
||||||
|
out.input_size = in.input_size;
|
||||||
|
out.output_size = in.output_size;
|
||||||
|
|
||||||
|
if(out.graph_size == 0) throw runtime_error("Empty state set");
|
||||||
|
if(out.input_size == 0) throw runtime_error("Empty input set");
|
||||||
|
if(out.output_size == 0) throw runtime_error("Empty output set");
|
||||||
|
if(!is_complete(out)) throw runtime_error("Partial machine");
|
||||||
|
|
||||||
|
return out;
|
||||||
|
}
|
7
lib/reachability.hpp
Normal file
7
lib/reachability.hpp
Normal file
|
@ -0,0 +1,7 @@
|
||||||
|
#pragma once
|
||||||
|
|
||||||
|
#include "types.hpp"
|
||||||
|
|
||||||
|
struct mealy;
|
||||||
|
|
||||||
|
mealy reachable_submachine(const mealy& in, state start);
|
|
@ -1,6 +1,7 @@
|
||||||
#include <adaptive_distinguishing_sequence.hpp>
|
#include <adaptive_distinguishing_sequence.hpp>
|
||||||
#include <logging.hpp>
|
#include <logging.hpp>
|
||||||
#include <mealy.hpp>
|
#include <mealy.hpp>
|
||||||
|
#include <reachability.hpp>
|
||||||
#include <read_mealy_from_dot.hpp>
|
#include <read_mealy_from_dot.hpp>
|
||||||
#include <seperating_family.hpp>
|
#include <seperating_family.hpp>
|
||||||
#include <seperating_matrix.hpp>
|
#include <seperating_matrix.hpp>
|
||||||
|
@ -25,8 +26,8 @@ int main(int argc, char *argv[]) try {
|
||||||
const auto k_max = stoul(argv[2]);
|
const auto k_max = stoul(argv[2]);
|
||||||
|
|
||||||
const string mode = argv[3];
|
const string mode = argv[3];
|
||||||
const bool streaming = mode == "stream";
|
const bool streaming = mode == "stream" || mode == "stop";
|
||||||
const bool random_part = streaming;
|
const bool random_part = streaming && mode != "stop";
|
||||||
const bool statistics = mode == "stats";
|
const bool statistics = mode == "stats";
|
||||||
|
|
||||||
const bool use_distinguishing_sequence = true;
|
const bool use_distinguishing_sequence = true;
|
||||||
|
@ -44,7 +45,7 @@ int main(int argc, char *argv[]) try {
|
||||||
}
|
}
|
||||||
}();
|
}();
|
||||||
|
|
||||||
const auto & machine = machine_and_translation.first;
|
const auto & machine = reachable_submachine(move(machine_and_translation.first), 0);
|
||||||
const auto & translation = machine_and_translation.second;
|
const auto & translation = machine_and_translation.second;
|
||||||
|
|
||||||
auto all_pair_seperating_sequences_fut = async([&]{
|
auto all_pair_seperating_sequences_fut = async([&]{
|
||||||
|
|
Loading…
Add table
Reference in a new issue