/*	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
*/

#include "IConsistAlgo.h"
#include "LdInterfaceCheckAlgo.h"
#include "IConsistAnsAcceptAlgo.h"
#include "LowSubsysIConsistAlgo.h"
#include "InterfImplCheckAlgo.h"
#include "DesInterface.h"

namespace DESpot
{

const std::wstring IConsistAlgo::cIConsistAlgoDesc = L"Interface Consistency Algorithm";
const std::wstring IConsistAlgo::cIntegrityNotConfirmed = L"Project integrity has not been checked";
const std::wstring IConsistAlgo::cProjectInvalid = L"Project is not valid";
const std::wstring IConsistAlgo::cIntefNotLd = L"Interface '%ls' is not an LD interface";
//_________________________________________________________________________________________________

IConsistAlgo::IConsistAlgo(DesHierProject& project, bool runIncremental /*= true*/) : 
	m_project(project), 
	m_isInterfConsist(false)
{
	m_runIncremental = runIncremental;
	m_description = cIConsistAlgoDesc;
}

//_________________________________________________________________________________________________

IConsistAlgo::~IConsistAlgo(void)
{
	destroyLowSubsysAlgos();
}

//_________________________________________________________________________________________________

void IConsistAlgo::destroyLowSubsysAlgos()
{
	//destroy all the algorithms that were used to verify each low-level subsystem
	for(LowSubsysAlgoIt algoIt = m_lowSubsysAlgoMap.begin(); algoIt != m_lowSubsysAlgoMap.end(); algoIt++)
	{
		LowSubsysIConsistAlgo* subsysAlgo = algoIt->second;
		delete subsysAlgo;
		subsysAlgo = null;
	}
}

//_________________________________________________________________________________________________

bool IConsistAlgo::isInterfaceConsistent() const
{
	return m_isInterfConsist;
}

//_________________________________________________________________________________________________

void IConsistAlgo::overrideInterfConsist(bool iConsist)
{
	m_isInterfConsist = iConsist;
}

//_________________________________________________________________________________________________

//Step1: verify the project's integrity. This among other things checks that the event set
//is partioned correctly which takes care of Point 1 of the I-consist definition
bool IConsistAlgo::verifyProjectIntegrity()
{
	//updateProgress();

	if (m_project.getIntegrity() == eIntegNotVerified)
	{
		addError(cIntegrityNotConfirmed);
		return false;
	}
	else if (m_project.getIntegrity() == eIntegNo)
	{
		addError(cProjectInvalid);
		return false;
	}

	return true;
}

//_________________________________________________________________________________________________

//Step2: verify that all interfaces are LD-consistent
bool IConsistAlgo::verifyLdInterfaces()
{
	//updateProgress();

	DesHierProject::InterfIteratorPtr interfIt = m_project.createInterfIterator();
	for(interfIt->first(); interfIt->notDone(); interfIt->next())
	{
		const DesInterface& interf = interfIt->currentItem();
		
		if (interf.isInterfConsist() == false || !m_runIncremental)
		{
			LdInterfaceCheckAlgo interfCheckAlgo(interf);
			if (interfCheckAlgo.runEx(m_progress) == false)
			{
				addError(interfCheckAlgo.getErrorList());
				addError(errorMessage(cIntefNotLd, interf.getName()));
				this->isfirsterror=false;
				this->FailureType=DesAlgo::PointTwo;
				return false;
			}
		}

		//updateProgress();
	}

	return true;
}

//_________________________________________________________________________________________________

//Step3: verify that all answers enabled by interfaces are accepted by the high-level subsystem
bool IConsistAlgo::verifyHighLevelSubsysIConsist()
{
	//updateProgress();

	if (m_project.getRootSubsys().isInterfConsist() == false || !m_runIncremental)
	{
		IConsistAnsAcceptAlgo ansAcceptAlgo(m_project);
		if (ansAcceptAlgo.runEx(m_progress) == false)
		{
			
			if(IConsistAlgo::isfirsterror)
			{
				IConsistAlgo::setIFailureType(AnsAcptAlgo);
				IConsistAlgo::ErrorSubSystem=ansAcceptAlgo.getErrorSubsystem();
				this->CE_tuplemap=ansAcceptAlgo.CE_tuplemap;			
				IConsistAlgo::isfirsterror=false;
				IConsistAlgo::IsFirstErrorSubSystem=false;
			}
			addError(ansAcceptAlgo.getError());
			return false;
		}
	}

	return true;
}

//_________________________________________________________________________________________________

//Step 5 & 6: verify that each low-level subsystem implements its interface properly
bool IConsistAlgo::verifyLowLevelSubsysIConsist()
{
	//updateProgress();

	bool allSubsysICons = true;

	DesHierProject::SubsysIteratorPtr subsysIt = m_project.createSubsysIterator();
	for(subsysIt->first(); subsysIt->notDone(); subsysIt->next())
	{
		const DesSubsystem& subsys = subsysIt->currentItem();

		if (subsys.getLevel() > 0)
		{
			if (subsys.isInterfConsist() == false || !m_runIncremental)
			{
				//check that this low-level accepts all the request events dictated by its interface
				LowSubsysIConsistAlgo* lowSubsyIConsAlgo = new LowSubsysIConsistAlgo(subsys);
				
				//cache the algorith so we can inspect errors later
				m_lowSubsysAlgoMap[subsys.getName()] = lowSubsyIConsAlgo;

				if (lowSubsyIConsAlgo->runEx(m_progress) == false)
				{
					addError(lowSubsyIConsAlgo->getErrorList());
					allSubsysICons = false;
					//Added by zain for counter example generation
					if(IConsistAlgo::isfirsterror)
					{
						IConsistAlgo::setIFailureType(lowSubsyIConsAlgo->getIFailureType());
						IConsistAlgo::ErrorSubSystem=lowSubsyIConsAlgo->getErrorSubsystem();
						this->CE_tuplemap=lowSubsyIConsAlgo->CE_tuplemap;					
						IConsistAlgo::CE_tuplemap=lowSubsyIConsAlgo->CE_tuplemap;
						IConsistAlgo::isfirsterror=false;
						IConsistAlgo::IsFirstErrorSubSystem=false;
					}
				}
			}
		}
	}
	
	return allSubsysICons;
}

//_________________________________________________________________________________________________

void IConsistAlgo::prepareRun()
{
	m_isInterfConsist = false;
	m_errorList.clear();

	destroyLowSubsysAlgos();
}

//_________________________________________________________________________________________________

//Step2: verify that all interfaces are LD-consistent-----------(overloading for extraction project)
bool IConsistAlgo::verifyLdInterfaces(std::map<std::wstring,bool> &subsysIConsMap)
{
	//updateProgress();

	DesHierProject::InterfIteratorPtr interfIt = m_project.createInterfIterator();
	for(interfIt->first(); interfIt->notDone(); interfIt->next())
	{
		const DesInterface& interf = interfIt->currentItem();
		
		if (interf.isInterfConsist() == false || !m_runIncremental)
		{
			LdInterfaceCheckAlgo interfCheckAlgo(interf);
			if (interfCheckAlgo.runEx(m_progress) == false)
			{
				addError(interfCheckAlgo.getErrorList());
				addError(errorMessage(cIntefNotLd, interf.getName()));
				subsysIConsMap[interf.getName()]=false;
				return false;
			}
			subsysIConsMap[interf.getName()]=true;
		}

		//updateProgress();
	}

	return true;
}

//_________________________________________________________________________________________________

//Step3: verify that all answers enabled by interfaces are accepted by the high-level subsystem------(overloading for extraction project)
bool IConsistAlgo::verifyHighLevelSubsysIConsist(std::map<std::wstring,bool> &subsysIConsMap,DesHierProject* mainProject)
{
	//updateProgress();

	if (m_project.getRootSubsys().isInterfConsist() == false || !m_runIncremental)
	{
		IConsistAnsAcceptAlgo ansAcceptAlgo(m_project);
		if (ansAcceptAlgo.runEx(m_progress) == false)
		{
			addError(ansAcceptAlgo.getError());
			//if the susbsys is not iterface Consitant immediately set iConsistant property to false for mainProject
			DesHierProject::SubsysIteratorPtr subsysMainPrjIt = mainProject->createSubsysIterator();
			for(subsysMainPrjIt->first(); subsysMainPrjIt->notDone(); subsysMainPrjIt->next())
			{
				if (subsysMainPrjIt->currentItem().getName() == m_project.getRootSubsys().getName())
				{
					subsysMainPrjIt->currentItem().setInterfConsist(false);
				}

			}
			return false;
			
		}
		else
			//add it to map to use cache it which will be used to set iconsitant property for this stored subsys in map for main project
			subsysIConsMap[m_project.getRootSubsys().getName()]=true;
	}

	return true;
}

//_________________________________________________________________________________________________

//Step 5 & 6: verify that each low-level subsystem implements its interface properly---(overloading for extraction project)
bool IConsistAlgo::verifyLowLevelSubsysIConsist(std::map<std::wstring,bool> &subsysIConsMap,DesHierProject* mainProject)
{
	//updateProgress();

	bool allSubsysICons = true;

	DesHierProject::SubsysIteratorPtr subsysIt = m_project.createSubsysIterator();
	for(subsysIt->first(); subsysIt->notDone(); subsysIt->next())
	{
		const DesSubsystem& subsys = subsysIt->currentItem();

		if (subsys.getLevel() > 0)
		{
			if (subsys.isInterfConsist() == false || !m_runIncremental)
			{
				//check that this low-level accepts all the request events dictated by its interface
				LowSubsysIConsistAlgo* lowSubsyIConsAlgo = new LowSubsysIConsistAlgo(subsys);
				
				//cache the algorith so we can inspect errors later
				m_lowSubsysAlgoMap[subsys.getName()] = lowSubsyIConsAlgo;

				if (lowSubsyIConsAlgo->runEx(m_progress) == false)
				{
					addError(lowSubsyIConsAlgo->getErrorList());
					allSubsysICons = false;
					DesHierProject::SubsysIteratorPtr subsysMainPrjIt = mainProject->createSubsysIterator();
					for(subsysMainPrjIt->first(); subsysMainPrjIt->notDone(); subsysMainPrjIt->next())
					{
						if (subsysMainPrjIt->currentItem().getName() == subsys.getName())
						{
							subsysMainPrjIt->currentItem().setInterfConsist(false);
						}

					}
				}
				else
					subsysIConsMap[subsys.getName()]=true;
			}
		}
	}
	
	return allSubsysICons;
}


//_________________________________________________________________________________________________

bool IConsistAlgo::runAlgo()
{

try
  {

	ProgressUpdater updater(m_progress);
	
	

	//Step1: verify the project's integrity. This among other things checks that the event set
	//is partioned correctly which takes care of Point 1 of the I-consist definition
	if (verifyProjectIntegrity() == false)
	{
	  //		throw EX("Either project is not valid, or integrity \
	  //has not yet been checked.");
		return m_isInterfConsist = false; // = is intentional
	}


    prepareRun();


	//Step2: verify that all interfaces are LD-consistent
	if (verifyLdInterfaces() == false)
	{
		return m_isInterfConsist = false; // = is intentional
	}

	//Step3: verify that all answers enabled by interfaces are accepted by the high-level subsystem
	if (verifyHighLevelSubsysIConsist() == false)
	{				
		return m_isInterfConsist = false; // = is intentional
	}
	
	//Step 4, 5 & 6: verify that each low-level subsystem implements its interface properly
	if (verifyLowLevelSubsysIConsist() == false)
	{
		return m_isInterfConsist = false; // = is intentional
	}
	
	return m_isInterfConsist = true; // = is intentional	

 }
	catch(const std::wstring& e)
	{
	 addError(e);
	 return m_isInterfConsist = false; // '=' intended
	}
catch(...){
  //unkown exception occurred
  addError(L"Unknown exception occurred.");
  return  m_isInterfConsist = false;  // '=' intended
}

// Should never reach here. 

return  false;

}

//_________________________________________________________________________________________________

bool IConsistAlgo::runAlgo(std::map<std::wstring, bool> &subsysIConsMap,DesHierProject* mainProject)
{

try
  {

	ProgressUpdater updater(m_progress);
	
	

	//Step1: verify the project's integrity. This among other things checks that the event set
	//is partioned correctly which takes care of Point 1 of the I-consist definition
	if (verifyProjectIntegrity() == false)
	{
	  //		throw EX("Either project is not valid, or integrity \
	  //has not yet been checked.");
		return m_isInterfConsist = false; // = is intentional
	}


    prepareRun();


	//Step2: verify that all interfaces are LD-consistent
	if (verifyLdInterfaces(subsysIConsMap) == false)
	{
		return m_isInterfConsist = false; // = is intentional
	}

	//Step3: verify that all answers enabled by interfaces are accepted by the high-level subsystem
	if (verifyHighLevelSubsysIConsist(subsysIConsMap,mainProject) == false)
	{
		return m_isInterfConsist = false; // = is intentional
	}
	
	//Step 4, 5 & 6: verify that each low-level subsystem implements its interface properly
	if (verifyLowLevelSubsysIConsist(subsysIConsMap,mainProject) == false)
	{
		return m_isInterfConsist = false; // = is intentional
	}

	return m_isInterfConsist = true; // = is intentional	

 }
	catch(const std::wstring& e)
	{
	 addError(e);
	 return m_isInterfConsist = false; // '=' intended
	}
catch(...){
  //unkown exception occurred
  addError(L"Unknown exception occurred.");
  return  m_isInterfConsist = false;  // '=' intended
}

// Should never reach here. 

return  false;

}
//-----This method is only called when runnig checkProect( on Multi level project) to run I-consistent algo on each extraction system--------
bool IConsistAlgo::runAlgoOnExtractionSystem()
{
	
	if (verifyProjectIntegrity() == false)
	{
	  //		throw EX("Either project is not valid, or integrity \
	  //has not yet been checked.");
		return m_isInterfConsist = false; // = is intentional
	}
			std::map<std::wstring, bool> subsysIConstMap;
			std::map<std::wstring, bool>::iterator subsysIConstMapIt;
			DesHierProject::SubsysIteratorPtr subsysIt = m_project.createSubsysIterator();
			for(subsysIt->first(); subsysIt->notDone(); subsysIt->next())
			{
				bool nonLeaf = false;
				DesSubsystem::DependIteratorPtr depIt = subsysIt->currentItem().createDependsIterator();
					for(depIt->first(); depIt->notDone(); depIt->next())
					{
						nonLeaf = true;
					}
				//call extraction against non-leaf node only
					if(nonLeaf)
					{
						const DesSubsystem& subsysExtraction = subsysIt->currentItem();
						DesProject* desProj = m_project.extractionSystem(&subsysExtraction);
						DesHierProject* extractedProj = dynamic_cast<DesHierProject*>(desProj);
						DesHierProject* project = dynamic_cast<DesHierProject*>(&m_project);
						IConsistAlgo iConsAlgo(*extractedProj);	

						iConsAlgo.provideProgress(NULL);

						bool isIcons = extractedProj->checkIConsistProp(iConsAlgo,subsysIConstMap,project);
						if(isIcons == false)
						{
							DesHierProject::SubsysIteratorPtr subsysMainProjIt = m_project.createSubsysIterator();
							for(subsysMainProjIt->first(); subsysMainProjIt->notDone(); subsysMainProjIt->next())
							{
								const DesSubsystem& subMainProj = subsysMainProjIt->currentItem();
								subsysIConstMapIt = subsysIConstMap.find(subMainProj.getName());
								if (subsysIConstMapIt != subsysIConstMap.end())
								{
									bool isNonLeaf = false;
									DesSubsystem::DependIteratorPtr depSubIt = subMainProj.createDependsIterator();
									for(depSubIt->first(); depSubIt->notDone(); depSubIt->next())
									{
										isNonLeaf = true;
									}
									if(subMainProj.isRoot() || isNonLeaf==false)
										subMainProj.setInterfConsist(subsysIConstMapIt->second);
								}

							}
							DesHierProject::InterfIteratorPtr intrefAllIt = m_project.createInterfIterator();
							for(intrefAllIt->first(); intrefAllIt->notDone(); intrefAllIt->next())
							{
								const DesInterface& interfMainProj = intrefAllIt->currentItem();
								DesInterface& interfNc= const_cast<DesInterface &>(interfMainProj);
								
								subsysIConstMapIt = subsysIConstMap.find(interfMainProj.getName());
								if (subsysIConstMapIt != subsysIConstMap.end())
									interfNc.setInterfConsist(subsysIConstMapIt->second);
							}
							addError(iConsAlgo.getErrorList());
							return m_isInterfConsist = false;
						}
					}
			}
			DesHierProject::SubsysIteratorPtr subsysAllIt = m_project.createSubsysIterator();
			for(subsysAllIt->first(); subsysAllIt->notDone(); subsysAllIt->next())
			{
				const DesSubsystem& subsysMainProj = subsysAllIt->currentItem();
				DesSubsystem& subsysNc= const_cast<DesSubsystem &>(subsysMainProj);
				subsysNc.setInterfConsist(true);
			}
			DesHierProject::InterfIteratorPtr intrefAllIt = m_project.createInterfIterator();
			for(intrefAllIt->first(); intrefAllIt->notDone(); intrefAllIt->next())
			{
				const DesInterface& interfMainProj = intrefAllIt->currentItem();
				DesInterface& interfNc= const_cast<DesInterface &>(interfMainProj);
				interfNc.setInterfConsist(true);
			}

			return m_isInterfConsist = true;
	}


	
	

void IConsistAlgo::run()
{
	if(m_project.isBilevel())
	runAlgo();
	else
	runAlgoOnExtractionSystem();
}
} //end of namespace DESpot
