// -----------------------------------------------------------------------------
// - Mikhailishin Alexei, group 420 - CMC MSU, Model Checking task 1, (c) 2010 -
// -----------------------------------------------------------------------------
#include <iostream>
#include <fstream>
#include <string>
#include <set>

using namespace std;

// переменные a и b в обоих функциях не меняются и не используются вообще
// объявим их дефайном
#define a_f 1
#define b_f 2
#define a_g 3
#define b_g 4

//#define ABSTRACTION_MODE 1

#ifdef ABSTRACTION_MODE
string f_string[2] = { "h = b;", "" };
#else
string f_string[11] = { "x = 6;", "y = 2;", "h = b;", "(x < 9)", "y = 4;", "y = 4;", "!(y < 4)", "", "", "", "" };
#endif
string g_string[18] = { "x = 9;", "y = 8;", "h = 3;", "!(x < 3)", "", "", "", "", "", "", "(x > 5)", "(h > 0)", "break;", "", "", "", "", "" };

// класс состояния, набор переменных и счетчики команд
class State
{
	// переменные, отвечающие за то, определено ли уже значение переменной
	// или оно еще undefined т.е. равно #
	int h_initialized;
	int x_f_initialized, y_f_initialized;
	int x_g_initialized, y_g_initialized;

	// переменные
	int h;
	int x_f, y_f;
	int x_g, y_g;

	// счетчики команд
	int c_f, c_g;

	string IntToStr(int);

public:
	State();
	void print(ofstream &);
	void print_label();
	void print_arc_to(State, bool);
	string hash();
	bool f();
	bool g();

	// оператор сравнения на меньше, нужен для хранения состояний с set
	// сравниваем в лексикографическом порядке
	bool operator <(const State &state) const
	{
		if(c_f != state.c_f) return c_f < state.c_f; else
		if(c_g != state.c_g) return c_g < state.c_g; else
		if(h_initialized != state.h_initialized) return h_initialized < state.h_initialized; else
		if(x_f_initialized != state.x_f_initialized) return x_f_initialized < state.x_f_initialized; else
		if(y_f_initialized != state.y_f_initialized) return y_f_initialized < state.y_f_initialized; else
		if(x_g_initialized != state.x_g_initialized) return x_g_initialized < state.x_g_initialized; else
		if(y_g_initialized != state.y_g_initialized) return y_g_initialized < state.y_g_initialized; else
		if(x_f != state.x_f) return x_f < state.x_f; else
		if(y_f != state.y_f) return y_f < state.y_f; else
		if(x_g != state.x_g) return x_g < state.x_g; else
		if(y_g != state.y_g) return y_g < state.y_g; else
		if(h != state.h) return h < state.h; else return false;
	}
};

// множество состояний - результат работы программы
set<State> result;

bool lts_mode = false;
ofstream lts;

// конструктор - задаем счетчикам команд начальные значения и
// делаем переменные неинициализированными
State::State()
{
	h = x_f = y_f = x_g = y_g = c_f = c_g = 0;
	h_initialized = x_f_initialized = y_f_initialized = x_g_initialized = y_g_initialized = 0;
}

// вывод состояния в нужном формате в файл
void State::print(ofstream &file)
{
	// если глобальная переменная инициализирована, то выводим ее значение
	if(h_initialized)
		file << c_f << ", " << c_g << ", " << h << ", " << a_f << ", " << b_f << ", " << a_g << ", " << b_g << endl;
	// иначе знак #
	else
		file << c_f << ", " << c_g << ", #, " << a_f << ", " << b_f << ", " << a_g << ", " << b_g << endl;
}

string State::IntToStr(int value)
{
	char buf[256];
	sprintf_s(buf, "%d", value);
	return string(buf);
}

string State::hash()
{
#define DELIM + "0" +
	return IntToStr(c_f) DELIM IntToStr(c_g) DELIM IntToStr(h_initialized) DELIM IntToStr(x_f_initialized) DELIM
		IntToStr(y_f_initialized) DELIM IntToStr(x_g_initialized) DELIM IntToStr(y_g_initialized) DELIM
		IntToStr(x_f) DELIM IntToStr(y_f) DELIM IntToStr(x_g) DELIM IntToStr(y_g) DELIM IntToStr(h);
}

void State::print_label()
{
  #define W(A, B) ", " << (A ? IntToStr(B) : "#")
	lts << hash() << " [label = \"" << IntToStr(c_f) << ", " << IntToStr(c_g);
	lts << W(h_initialized, h);
	lts << W(x_f_initialized, x_f);
	lts << W(y_f_initialized, y_f);
	lts << W(x_g_initialized, x_g);
	lts << W(y_g_initialized, y_g);
	lts << "\"];" << endl;
}

void State::print_arc_to(State dest, bool is_f)
{
	lts << hash() << " -> " << dest.hash() << " [label = \"";
	lts << (is_f ? f_string[c_f] : g_string[c_g]);
	lts << "\"];" << endl;
}

// эмуляция выполнения одной команды функции f
bool State::f()
{
	// выбор действия в зависимости от счетчика команд
	switch(c_f)
	{
	#ifdef ABSTRACTION_MODE
	case 0: 
		h = b_f;
		h_initialized = 1; 
		break;
	case 1:
		// это финальный оператор
		return false;
	#else
	case 0: 
		x_f = 6;
		x_f_initialized = 1; 
		break;
	case 1:
		y_f = 2;
		y_f_initialized = 1;
		break;
	case 2:
		h = b_f;
		h_initialized = 1;
		break;
	case 4: case 5:
		y_f = 4;
		y_f_initialized = 1;
		break;
	case 6:
		c_f = 10;
		return true;		
		break;
	case 10:
		// это финальный оператор
		return false;
	#endif
	}

	// увеличиваем счетчик команд, он указывает на следующую команду, а это выполнена
	c_f++;
	return true;
}

// эмуляция выполнения одной команды функции g
bool State::g()
{
	// выбор действия в зависимости от счетчика команд
	switch(c_g)
	{
	case 0: 
		x_g = 9;
		x_g_initialized = 1;
		break;
	case 1:
		y_g = 8;
		y_g_initialized = 1;
		break;
	case 2:
		h = 3;
		h_initialized = 1;
		break;
	case 3:
		c_g = 10;
		return true;
	case 12:
		c_g = 17;
		return true;
	case 17:
		// это финальный оператор
		return false;	
	}

	// увеличиваем счетчик команд
	c_g++;
	return true;
}

// основная функция, инициализирующая все вычисления
// рекурсивно строится дерево, где левая ветвь - переход по f, правая - по g
// таким образом переберуться все возможные варианты
void recursion(State _state)
{
	if(result.find(_state) != result.end())
		return;

	// добавляем текущее состояние в множество результатов
	result.insert(_state);

	int final_state_count = 0;

	// локальная копия состояния
	State state = _state;
	// выполняем один оператор функции f и если он не последний входим глубже в рекурсию
	if(state.f())
	{
		if(lts_mode) _state.print_arc_to(state, true);
		recursion(state);
	} else
	{
		final_state_count++;
	}
	
	// восстановили состояние
	state = _state;
	// выполняем один оператор функции g и если он не последний входим глубже в рекурсию
	if(state.g())
	{
		if(lts_mode) _state.print_arc_to(state, false);
		recursion(state);
	} else
	{
		final_state_count++;
	}

	if(final_state_count == 2 && lts_mode)
	{
		_state.print_arc_to(_state, false);
	}
}

// точка входа
int main(int argc, char* argv[])
{
	// если параметров не задано, выводим информацию
	if(argc < 2)
	{
		cout << "CMC MSU, Model Checking course, first task" << endl;
		cout << "Author: Mikhailishin Alexei, 420 group (c) 2010" << endl;
		cout << "Usage:" << endl;
		cout << "  " << argv[0] << " [-count] [-file file_name]";
	}

	// начальные значения переменных
	string s, fname = "states.txt", ltsfname = "";
	bool count = false;

	// цикл по параметрамы
	for (int i = 1; i < argc; i++)
	{
		s = argv[i];
		if (s == "-count") count = true; // выводить число состояний в stdout
		if (s == "-file") // переназначение файла для записи состояний
		{
			if((i + 1) < argc) // если имя файла задано
				fname = argv[i + 1];
		}
		if (s == "-lts") 
		{
			if((i + 1) < argc) // если имя файла задано
				ltsfname = argv[i + 1];
		}
	}

	if(lts_mode = ltsfname != "")
	{
		lts.open(ltsfname.c_str(), ios_base::trunc);
		lts << "digraph F\n{" << endl;
	}

	// запускаем рекурсию
	recursion(State());

	// вывод числа состояний, если требуется
	if(count)	cout << result.size();
	
	// пытаемся открыть файл для записи
	ofstream file(fname.c_str());
	if(file.fail())
	{
		cerr << "invalid filename";
		return 1;
	}

	// вывод заголовка (формата) выходных данных
	file << "c_f, c_g, h, f.a, f.b, g.a, g.b" << endl;
	// цикл по множеству
	for(set<State>::iterator i = result.begin(); i != result.end(); i++)
	{
		i->print(file); // печатаем результат
		if(lts_mode) i->print_label();
	}
	file.close();

	if(lts_mode)
	{
		lts << "}" << endl;
		lts.close();
	}

	// ansi c++ =)
	return 0;
}