#include <cstdio>
#include <cstdlib>
#include <cassert>

#include <iostream>

#include <map>
#include <utility>
#include <string>
#include <set>

#include <vector>
#include <algorithm>
using namespace std;

//exploit set
typedef set<string> expset_t;

//exploit path
typedef struct {
	expset_t e_expset;
	vector<string> e_explist;
} exppath_t;

typedef vector<exppath_t> exppaths_t;

FILE * inFile;
FILE * outFile;
FILE * expFile;

map<string, int> node_label;	//node_str -> node_int
map<int, string> node_name;		//node_int -> node_str
set< pair<int, int> > edges;	//<node_int, node_int>
map< pair<int, int>, set<string> > edge_label;	//edge -> dot output edge labels
map< pair<int, int>, set<string> > edge_choices;	//edge -> different choices
set<int> reachable;
set<int> good;
int counter = 0;

vector<exppaths_t> min_exp_path;

//utility macros
#define REP(i, n) for (int i=0, _n=int(n); i<_n; ++i)

#define FOREACH(it, list) for (typeof((list).begin()) it = (list).begin();  \
                                                it != (list).end(); ++it)

//set utility
template <class T>
inline bool my_set_includes(const set<T> & a, const set<T> & b)
{
    return includes(a.begin(), a.end(), b.begin(), b.end());
}

bool can_improve_list(const exppath_t & exppath, const exppaths_t & exppaths)
{
	FOREACH(it, exppaths)
		if (my_set_includes(exppath.e_expset, it->e_expset))
			return false;
	return true;
}

void clean_list(const exppath_t & exppath, exppaths_t & exppaths)
{
//	cerr << "enter clean list" << endl;
	for (int i = 0; i < int(exppaths.size()); ++i)
		if (my_set_includes(exppaths[i].e_expset, exppath.e_expset)) {
//			cerr << "\tdebug i=" << i << " size=" << exppaths.size() << endl;
			exppaths[i] = exppaths[ exppaths.size()-1 ];
			exppaths.resize( exppaths.size()-1 );
//			cerr << "\tdebug now size = " << exppaths.size() << endl;
			--i;
		}
}

void break_str(string & s, string & n1, string & n2, string & edge)
{
	size_t i;

	if (s.size() > 0 && s[s.size()-1] == '\n')
		s = s.substr(0, s.size()-1);

	i = s.find('|');
	assert(0 <= i && i < s.size());
	n1 = s.substr(0, i);
	s = s.substr(i+1);

	i = s.find('|');
	assert(0 <= i && i < s.size());
	n2 = s.substr(0, i);
	edge = s.substr(i+1);
}

void input()
{
	char *line = NULL;
	size_t len = 0;

	while ( getline(&line, &len, inFile) != -1 ) {
		string str = line;
		string n1, n2, edge;
		int label1, label2;

		break_str(str, n1, n2, edge);

		if (node_label.count(n1) == 0) {
			node_label[n1] = counter;
			node_name[counter] = n1;
			++counter;
		}
		if (node_label.count(n2) == 0) {
			node_label[n2] = counter;
			node_name[counter] = n2;
			++counter;
		}
		label1 = node_label[n1];
		label2 = node_label[n2];
		edges.insert(make_pair(label1, label2));

		edge_choices[make_pair(label1, label2)].insert(edge);
	}
	if (line)
		free(line);
}

void output_dotfile()
{
	fprintf(outFile, "digraph G {\n");

	for (int i = 0; i < counter; ++i)
		if (good.count(i) > 0 && node_name[i] != "goal") {
			string nn = node_name[i];
			string st = "";
			if (nn.size() > 2 && nn.substr(0,2) == "g_") {
				st = ", style=filled";
				nn = nn.substr(2);
			}
			if (nn.size() > 2 && nn.substr(0,2) == "i_") {
				nn = nn.substr(2);
			}
			fprintf(outFile, "\tn%d [label=\"%s\"%s];\n", i, nn.c_str(), st.c_str());
		}

	FOREACH(it, edges) {
		int n1 = it->first;
		int n2 = it->second;
		if (good.count(n1) > 0 && good.count(n2) > 0) {
				string labels("");
				FOREACH(it_label, edge_label[*it])
					labels += *it_label + "\\n";
				if (labels != "")
					fprintf(outFile, "\tn%d->n%d [label=\"%s\"];\n", n1, n2,
							labels.c_str());
//				fprintf(outFile, "\tn%d->n%d;\n", n1, n2);
		}
	}

	fprintf(outFile, "}\n");
}

bool mark_good_nodes_onpath_recursive(int curr_node, const vector<string> & explist,
										int explist_id, vector<int> path_nodes)
{
	if ( explist_id == int(explist.size()) ) {
		if ( edges.count(make_pair(curr_node, node_label["goal"])) > 0 ) {
			REP(i, path_nodes.size()) {
				good.insert(path_nodes[i]);
				if (i > 0) {
					pair<int, int> edge = make_pair(path_nodes[i-1], path_nodes[i]);
					edge_label[edge].insert(explist[i-1]);
				}
			}
			return true;
		} else
			return false;
	}

	FOREACH(it_edge, edges) if (it_edge->first == curr_node)
		if ( edge_choices[*it_edge].count(explist[explist_id]) > 0 ) {
			int next_node = it_edge->second;
			path_nodes[explist_id+1] = next_node;
			if (mark_good_nodes_onpath_recursive(next_node, explist, explist_id+1, path_nodes))
				return true;
		}
	
	return false;
}

bool mark_good_nodes_onpath(int start, const vector<string> & explist)
{
	vector<int> path_nodes(explist.size() + 1);
	path_nodes[0] = start;

	return mark_good_nodes_onpath_recursive(start, explist, 0, path_nodes);
}

void mark_good_nodes()
{
	int init_label = node_label["init"];
	good.insert(init_label);

	FOREACH(it, min_exp_path[node_label["goal"]]) {
		bool found = mark_good_nodes_onpath(init_label, it->e_explist);

		FOREACH(it_edge, edges)
			if (it_edge->first == init_label && edge_choices[*it_edge].count("none") > 0)
				found = mark_good_nodes_onpath(it_edge->second, it->e_explist) || found;

		if (!found) {
			FOREACH(it_node, it->e_explist)
				cout << *it_node << "  ";
			cout << endl;
		}
		assert(found);
	}
}

void mark_reachable()
{
	bool changed;

	reachable.insert(node_label["goal"]);

	do {
		changed = false;
		FOREACH(it, edges) {
			int x = it->first;
			int y = it->second;
			if (reachable.count(y) > 0 && reachable.count(x) == 0) {
				changed = true;
				reachable.insert(x);
			}
		}
	} while (changed);
}

void cal_min_exp_path()
{
	bool changed;

	min_exp_path.clear();
	min_exp_path.resize(counter);
	min_exp_path[node_label["init"]].push_back(exppath_t());

	do {
		changed = false;
		FOREACH(it_edge, edges) FOREACH(it_choice, edge_choices[*it_edge]) {
			int x = it_edge->first;
			int y = it_edge->second;
			if (reachable.count(x) == 0 || reachable.count(y) == 0)
				continue;

			FOREACH(it_path, min_exp_path[x]) {
				exppath_t exppath = *it_path;
				if (*it_choice != "none") {
					exppath.e_expset.insert(*it_choice);
					exppath.e_explist.push_back(*it_choice);
				}
				if (can_improve_list(exppath, min_exp_path[y])) {
					changed = true;
					clean_list(exppath, min_exp_path[y]);
					min_exp_path[y].push_back(exppath);
				}
			}
		}
	} while (changed);
}

void output_min_exp_path()
{
	REP(i, counter) if (good.count(i) > 0 || node_name[i] == "goal") {
		fprintf(expFile, "%s\n", node_name[i].c_str());
		FOREACH(it_path, min_exp_path[i]) {
			fprintf(expFile, "\t[");
			FOREACH(it_elm, it_path->e_explist)
				fprintf(expFile, " %s ", it_elm->c_str());
			fprintf(expFile, "]\n");
		}
		fprintf(expFile, "\n");
	}
}

void add_goal_node()
{
	node_label["goal"] = counter;
	node_name[counter] = "goal";
	REP(i, counter)
		if (node_name[i].substr(0, 2) == "g_") {
			edges.insert(make_pair(i, counter));
			edge_choices[make_pair(i, counter)].insert("none");
		}
	++counter;
}

int main(int argc, char ** argv)
{
	if (argc != 4) {
		printf("usage: %s input_file output_file explist_file\n", argv[0]);
		return 0;
	}

	assert(inFile = fopen(argv[1], "r"));
	assert(outFile = fopen(argv[2], "w"));
	assert(expFile = fopen(argv[3], "w"));

	input();

	add_goal_node();
	mark_reachable();
	cal_min_exp_path();

	mark_good_nodes();

	output_dotfile();
	output_min_exp_path();

	fclose(inFile);
	fclose(outFile);
	fclose(expFile);

	return 0;
}

