/* about the algorithm used here see also:
http://lackingrhoticity.blogspot.com/2009/08/how-to-do-model-checking-of-python-code.html
*/

#pragma once

#include <vector>
#include <set>
#include <deque>
#include <string>
#include <memory>
#include <exception>

using namespace std;

class ChooserException: public exception
{
	virtual const char* what() const throw()
	{
		return "Program is not deterministic";
	}
} chooser_exc;

class ModelCheckEscape: public exception
{
	virtual const char* what() const throw()
	{
		return "";
	}
} modelcheck_exc;


class AbstractObject{
public:
	AbstractObject(){}
	virtual ~AbstractObject(){}
};

// cute pattern which enables quasi heterogeneous lists
template <typename T>
class Object : public AbstractObject
{
private:
	T value;
public:	
	T get()
	{
		return value;
	}

	void set(T value)
	{
		this->value = value;
	}

	Object(T value)
	{
		this->value = value;
	}
	virtual ~Object(){;}
};

// Wrapper of vector<T> object. Used to store the current
// position of iteration. 
struct Chosen
{
	Chosen(){}
	virtual ~Chosen()
	{
		delete container;
	}
	Chosen(vector<AbstractObject*>* container)
	{
		this->container = container;
		this->idx = 0;
	}

	AbstractObject* element(unsigned int i)
	{
		return (*container)[i];
	}

	AbstractObject* current()
	{
		return element(idx);
	}

	vector<AbstractObject*>* container;
	unsigned int idx;
};

typedef deque< Chosen* > Queue;

class Chooser  
{
private:	
	Chosen* chosen;		
	vector<AbstractObject*> elements;
	Queue* queue;		
public:
	Chooser(){;}
	virtual ~Chooser(){}				

	Chooser(Chosen* chosen, Queue* queue)
	{		
		this->chosen = chosen;		
		this->queue  = queue;				
	}

	template <typename Container>
	Container* pull(string resource)
	{
		return null;
	}

	vector<AbstractObject*>* getElements()
	{
		return &elements;
	}

	template <typename T>
	T choose(T choices[], int cnt)
	{		
		vector<T> C;
		for(int i=0; i<cnt; i++)
			C.push_back(choices[i]);
		return choose< vector<T> >(C);
	}	

	int choose(int choices)
	{		
		vector<int> C;
		for(int i=0; i<choices; i++)
			C.push_back(i);
		return choose< vector<int> >(C);
	}	

	template <typename Container>
	typename Container::value_type choose(Container& choices)
	{		
		Container::iterator p;

		typedef typename Container::value_type ElemType;				
		if(chosen->idx<chosen->container->size())		
		{									
			ElemType choice = ((Object<ElemType>*)chosen->current())->get();		
			chosen->idx++;

			p = choices.begin();
			bool found = false;
			while(p!=choices.end())
			{
				if(*p == choice)
				{
					found = true;
					break;
				}
				p++;
			}
			if(!found)
				throw chooser_exc;			
			Object<ElemType>* e = new Object<ElemType>(choice);			
			elements.push_back(e);
			return choice;
		}
		else
		{
			p = choices.begin();
			while(p!=choices.end())
			{				
				vector<AbstractObject*>* clone = new vector<AbstractObject*>(elements);					
				Object<ElemType>* e = new Object<ElemType>(*p);
				clone->insert(clone->end(), e);	
				Chosen* c = new Chosen(clone);
				queue->push_back(c);
				p++;
			}
			throw modelcheck_exc;
		}
	}
};

// tiny garbage collector
class GC 
{
private:
	set<AbstractObject*> collector;
public:
	GC(){}
	virtual ~GC(){}

	void collect(vector<AbstractObject*>* container)
	{
		vector<AbstractObject*>::iterator iter = container->begin();
		while(iter!=container->end())
		{
			collector.insert(*iter);
			iter++;
		}
	}

	void cleanup()
	{
		set<AbstractObject*>::iterator iter = collector.begin();
		while(iter!=collector.end())
		{				
			delete *iter;		
			iter++;
		}
	}
};

// main checking function. evaluates Functor in a loop, determined
// by Chooser objects.

template <typename Functor>
void check(Functor& functor) {	
	GC gc;
	Queue* queue = new Queue();			

	vector<AbstractObject*>* v0 = new vector<AbstractObject*>();	
	queue->push_back(new Chosen(v0));	
	while(queue->size()>0)
	{
		Chosen* chosen = queue->front();
		queue->pop_front();		
		try {
			gc.collect(chosen->container);

			Chooser chooser(chosen, queue);
			functor(chooser);

			gc.collect(chooser.getElements());
		}
		catch(ModelCheckEscape exc)
		{
		}		
		delete chosen;				
	}
	gc.cleanup();
	delete queue;
}
// 
class ChooserMixin {
protected:
	Chooser chooser;
public:
	virtual void test() = 0;
	void check() {
		GC gc;
		Queue* queue = new Queue();			

		vector<AbstractObject*>* v0 = new vector<AbstractObject*>();	
		queue->push_back(new Chosen(v0));	
		while(queue->size()>0)
		{
			Chosen* chosen = queue->front();
			queue->pop_front();		
			try {
				gc.collect(chosen->container);

				this->chooser = Chooser(chosen, queue);
				test();

				gc.collect(chooser.getElements());
			}
			catch(ModelCheckEscape exc)
			{
			}		
			delete chosen;				
		}
		gc.cleanup();
		delete queue;
	}
};