/*	Author: Magdin Stoica
	Supervisor: Dr. Ryan Leduc
	
	Project created in conformity with the requirements for the Degree of Master of Engineering in Software Engineering, 
	Computing and Software Department, 
	McMaster University
	2003 - 2007
*/

#pragma once

#include <string>
#include "CommonDefinitions.h"
#include "ProgressUpdate.h"
#include "DesSubsystem.h"

namespace DESpot
{
	using namespace std;
	class DesAlgo
	{
		//types
		public:
			typedef std::list<std::wstring> WarningList;
			typedef WarningList::const_iterator WarnIt;

			typedef std::list<std::wstring> ErrorList;
			typedef ErrorList::const_iterator ErrIt;

			typedef std::vector<short> CounterExampleStateTuple;


		public:
			DesAlgo(UpdateProgressInterface* progress, const std::wstring& desc = std::wstring());
			DesAlgo(const std::wstring& desc = std::wstring());
			virtual ~DesAlgo(void);

		public:
			bool runEx(UpdateProgressInterface* progress);
			virtual bool runAlgo() = 0;

		public:
			void provideProgress(UpdateProgressInterface* progress);
			
			const std::wstring& getDescription() const;
			
			//returns the error list. Algorithms may override this method to be provide the error list
			//as it is requested as opposed to while the algorithm is running
			virtual const ErrorList& getErrorList();
			
			//returns the number of errors encountered
			virtual int getErrorCount() const;

			//returns the error list. Algorithms may override this method to be provide the error list
			//as it is requested as opposed to while the algorithm is running
			virtual const WarningList& getWarningList();
			
			//returns the number of errors encountered
			virtual int getWarningCount() const;

		protected:
			void startAlgo();
			void updateProgress();
			void finish();

			void addError(const std::wstring& error);

		public:
			//void addError(const std::wstring& errorFormat, const std::wstring& data);
			void addError(const ErrorList& errorList);
		
		protected:
			void addWarning(const std::wstring& warn);
			//void addWarning(const std::wstring& warnFormat, const std::wstring& data);
			void addWarning(const WarningList& warnList);


			std::wstring errorMessage(const std::wstring& format, const std::wstring& arg1);
			std::wstring errorMessage(const std::wstring& format, const std::wstring& arg1, const std::wstring& arg2);
			std::wstring errorMessage(const std::wstring& format, const std::wstring& arg1, const std::wstring& arg2, const std::wstring& arg3);
			std::wstring errorMessage(const std::wstring& format, const std::wstring& arg1, const std::wstring& arg2, const std::wstring& arg3, const std::wstring& arg4);
			std::wstring errorMessage(const std::wstring& format, const std::wstring& arg1, const std::wstring& arg2, const std::wstring& arg3, const std::wstring& arg4, const std::wstring& arg5);
			std::wstring errorMessage(const std::wstring& format, const std::wstring& arg1, const std::wstring& arg2, const std::wstring& arg3, const std::wstring& arg4, const std::wstring& arg5, const std::wstring& arg6);
			std::wstring errorMessage(const std::wstring& format, const std::wstring& arg1, const std::wstring& arg2, const std::wstring& arg3, const std::wstring& arg4, const std::wstring& arg5, const std::wstring& arg6, const std::wstring& arg7);

		protected:
			UpdateProgressInterface* m_progress;

			//tells the algorithm to run incremental meaning if there is any cached information
			//to take advantage of it. Not all algorithms support incremental and non-incremental
			//execution. Those that do have to have a way to set this to true as this is not provided
			//in general
			bool m_runIncremental;

			std::wstring m_description;

			//the list of warnings issued by the algorithm
			WarningList m_warningList;

			//the list of errors detected by an algorithm
			ErrorList m_errorList;

			//buffer used in formatting error messages
			// If state name cut off, need to increase
			// size here and in DesAlgo.cpp
			static wchar_t s_buffer[10000];

			// Added by zain for counter example generation
	public:
		enum IConstSubAlgos
			{
				AnsAcptAlgo,
				ReqAcptAlgo,
				IntrfImplAlgo,
				PointTwo
			};
	protected:
		bool isfirsterror;
		bool IsFirstErrorSubSystem;
		bool isFirstErrorAlgo;					
		const DesSubsystem* ErrorSubSystem;		
		IConstSubAlgos FailureType;	
		std::wstring ErrorSubSystemName;
	public: 		
		map<std::wstring,short> CE_tuplemap;
		inline bool getErrorFlag(){return isfirsterror;}
		inline void setErrorFlag(bool in_value){isfirsterror=in_value;}

		inline const DesSubsystem* getErrorSubsystem(){return ErrorSubSystem;}

		inline void setErrorAlgoFlag(bool in_flag){isFirstErrorAlgo=in_flag;}
		inline bool getErrorAlgoFlag(){return isFirstErrorAlgo;}		
		
		inline IConstSubAlgos getIFailureType(){return FailureType;}
		void setIFailureType(IConstSubAlgos in_type);

		inline std::wstring getErrorSubsystemName(){return ErrorSubSystemName;}
		inline void setErrorSubSystemName(std::wstring in_name){ErrorSubSystemName=in_name;}
		
		
	};

} //namespace DESpot

