From 3de4f29a87770adfdbcbc6becf72bbddac225121 Mon Sep 17 00:00:00 2001
From: Joshua Moerman <lakseru@gmail.com>
Date: Tue, 7 Apr 2015 08:40:46 +0200
Subject: [PATCH] Adds a file to determine reachability with a subalphabet
 (bug!)

---
 src/reachability.cpp | 79 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 79 insertions(+)
 create mode 100644 src/reachability.cpp

diff --git a/src/reachability.cpp b/src/reachability.cpp
new file mode 100644
index 0000000..27088c6
--- /dev/null
+++ b/src/reachability.cpp
@@ -0,0 +1,79 @@
+#include <mealy.hpp>
+#include <read_mealy_from_dot.hpp>
+
+#include <fstream>
+#include <iostream>
+#include <queue>
+#include <vector>
+
+using namespace std;
+
+int main(int argc, char *argv[]){
+	if(argc != 3) return 1;
+
+	const string filename = argv[1];
+	const string machince_positions_filename = argv[2];
+
+	// Read machine and its positions
+	const auto machine_translation = read_mealy_from_dot(filename);
+	const auto & machine = machine_translation.first;
+	const auto & translation = machine_translation.second;
+
+	vector<pair<double, double>> positions(machine.graph_size);
+	ifstream position_file(machince_positions_filename);
+	for(auto & p : positions){
+		position_file >> p.first >> p.second;
+	}
+
+	// read subalphabet
+	cout << "Machine is read, please provide a subalphabet" << endl;
+	vector<input> subalphabet;
+	string i;
+	while(cin >> i){
+		const input x = translation.input_indices.at(i);
+		subalphabet.push_back(x);
+	}
+
+	// visit with subalphabet
+	vector<bool> visited(machine.graph_size, false);
+	queue<state> work;
+	work.push(0);
+	while(!work.empty()){
+		const state s = work.front();
+		work.pop();
+
+		if(visited[s.base()]) continue;
+		visited[s.base()] = true;
+
+		for(auto x : subalphabet){
+			const state t = apply(machine, s, x).to;
+			if(!visited[t.base()]) work.push(t);
+		}
+	}
+
+	// write to dot
+	ofstream out(filename + ".reachable.dot");
+	out << "digraph {\n";
+
+	for(state s = 0; s < machine.graph_size; ++s){
+		bool is_visited = visited[s.base()];
+		out << "\t" << "s" << s << " [";
+		out << "color=\"" << (is_visited ? "green" : "red") << "\"" << ", ";
+		out << "pos=\"" << positions[s.base()].first << "," << positions[s.base()].second << "\"";
+		out << "]\n";
+	}
+
+	for(state s = 0; s < machine.graph_size; ++s){
+		vector<bool> visited(machine.graph_size, false);
+		visited[s.base()] = true;
+		for(input i = 0; i < machine.input_size; ++i){
+			const auto t = apply(machine, s, i).to;
+			if(visited[t.base()]) continue;
+			out << "\t" << "s" << s << " -> " << "s" << t << "\n";
+			visited[t.base()] = true;
+		}
+	}
+
+	out << "}" << endl;
+}
+