/*	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 "FlatProjectPropCheck.h"

// for debug
// #include <iostream>



namespace DESpot
{

const std::wstring FlatProjectPropCheck::cFlatProjectPropCheckAlgoDesc = L"Flat Project Properties Check Algorithm";

FlatProjectPropCheck::FlatProjectPropCheck(DesFlatProject& project, bool runIncremental /*= true*/):
		m_project(project),
		m_checkInteg(true),
		m_integAlgo(runIncremental),
		m_checkNonBlock(true),
		m_nonBlockAlgo(runIncremental),
		m_checkCtrl(true),
		m_ctrlAlgo(),
		m_runSuccessful(false)
{
	m_runIncremental = runIncremental;
	m_description = cFlatProjectPropCheckAlgoDesc;



}

//_________________________________________________________________________________________________

FlatProjectPropCheck::~FlatProjectPropCheck(void)
{
}

//_________________________________________________________________________________________________

void FlatProjectPropCheck::checkIntegrity(bool checkInteg /*= true*/)
{
	m_checkInteg = checkInteg;
}

//_________________________________________________________________________________________________

bool FlatProjectPropCheck::integrityChecked() const
{
	return m_checkInteg;
}

//_________________________________________________________________________________________________

FlatProjIntegrityAlgo& FlatProjectPropCheck::integAlgo()
{
	return m_integAlgo;
}

//_________________________________________________________________________________________________

void FlatProjectPropCheck::checkNonBlock(bool checkNonBlock /*= true*/)
{
	m_checkNonBlock = checkNonBlock;
}

//_________________________________________________________________________________________________

bool FlatProjectPropCheck::nonBlockChecked() const
{
	return m_checkNonBlock;
}


//_________________________________________________________________________________________________

MultiNonBlockingAlgo& FlatProjectPropCheck::nonBlockAlgo()
{
	return m_nonBlockAlgo;
}

//_________________________________________________________________________________________________

void FlatProjectPropCheck::checkCtrl(bool checkCtrl /*= true*/)
{
	m_checkCtrl = checkCtrl;
}

//_________________________________________________________________________________________________

bool FlatProjectPropCheck::ctrlChecked()
{
	return m_checkCtrl;
}

//_________________________________________________________________________________________________

MultiCtrlAlgo& FlatProjectPropCheck::ctrlAlgo()
{
	return m_ctrlAlgo;
}

//_________________________________________________________________________________________________

bool FlatProjectPropCheck::runSuccessful() const
{
	return m_runSuccessful;
}

//_________________________________________________________________________________________________

void FlatProjectPropCheck::prepareRun()
{

	if (m_runIncremental == false)
	{
		//this will reset all properties to "not verified" the validity of all
		//subsystems and interfaces to false and it will clean all pre-computed
		//sync products of all subsystems and interfaces
		m_project.clean();
	}

	//m_integAlgo.provideProgress(m_progress);
	
	//m_nonBlockAlgo.provideProgress(m_progress);


	// moved to after proj integrity has been run
	 	DesSubsystem::DesIteratorPtr hDesIt = m_project.createDesIterator();
	for(hDesIt->first(); hDesIt->notDone(); hDesIt->next())
	{
		const Des& hDes = hDesIt->currentItem();

		/*		if (hDes.getIntegrity() != eIntegYes)
		{
			throw EX("Either all DES are not valid, or integrity \
has not yet been checked.");
                } */
		m_nonBlockAlgo.addInputDes(&hDes);
	}

	



	m_ctrlAlgo.addInputPlantDes(m_project.createDesIterator(ePlantDes));
	m_ctrlAlgo.addInputSupDes(m_project.createDesIterator(eSupervisorDes));
//throw EX("controll algo");
}

//_________________________________________________________________________________________________

bool FlatProjectPropCheck::runAlgo()
{
	

	//throw EX("controll algo");
	prepareRun();


	m_runSuccessful = true;
	m_project.setProjectChkFlag(true);
	if (m_checkInteg || !m_runIncremental)
	{
	  if (m_project.getIntegrity() != eIntegYes || !m_runIncremental)
	    {
	      m_runSuccessful &= m_project.checkIntegrity(m_integAlgo);
	    }
	  else
	    {
	      m_integAlgo.overrideIsValid();
	    }
	}
	bool NonBlockingResult=true;
	if (m_checkNonBlock)
	{
	  if (m_project.getNonBlockingProp() != eNonBlockYes || !m_runIncremental)
	    {
			NonBlockingResult= m_project.checkNonBlocking(m_nonBlockAlgo);
			m_runSuccessful &= NonBlockingResult;
			if(!NonBlockingResult && !(m_nonBlockAlgo.CE_tuplemap.empty()))
			{
				m_ctrlAlgo.setErrorAlgoFlag(false);
				QMessageBox msgBox;	
				msgBox.setText("The project is blocking.<HR> Do you want to generate a counter example? Depending on the system, it may take a long time. ");
				msgBox.setIcon(QMessageBox::Critical );
				msgBox.setWindowTitle("DESpot");
				msgBox.addButton(QMessageBox::Yes);
				msgBox.addButton(QMessageBox::No);
				int DebugResponse=msgBox.exec();
					  
					if(DebugResponse==QMessageBox::Yes)
						{		
							m_project.setDebugMode(DesProject::CounterExample);
							CounterExampleAlgo_FlatNB CEAlgo(m_nonBlockAlgo.CE_tuplemap,m_project.createDesIterator(), m_project.createProjEventIterator());		
							bool result=CEAlgo.runAlgo();
							DESpot::DummyProject temp(&m_project,m_nonBlockAlgo.CE_tuplemap);
							m_project.setSimulationErrorTuple(temp.getSimulationErrorTuple());
								if(result)
									{
										m_project.setCounterExample(CEAlgo.GetCounterExample());			
										m_project.setDummyProject(&m_project);	
										QMessageBox::information(NULL, "DESpot","Counter example generated successfully.");
									}		
						}
						else	  
						 {	
							DESpot::DummyProject temp(&m_project,m_nonBlockAlgo.CE_tuplemap);
							m_project.setSimulationErrorTuple(temp.getSimulationErrorTuple());	
							m_project.setDebugMode(DesProject::ErrorTuple);	
							m_project.setDummyProject(&m_project);
						  }				
			}
			
	    }
	  else
	    {
	      //this project is nonblocking and we're running the algorithm incrementally so 
	      //override the result of the algorithm without actually running the algorithm.
	      //this is needed because the algorithm is used to output information to the user
	      m_nonBlockAlgo.overrideNonBlocking(true);
	    }
	}

if (m_checkCtrl)
{	
	  if (m_project.getControllableProp() != eCtrlYes || !m_runIncremental)
	    {		
	      m_runSuccessful &= m_project.checkControllable(m_ctrlAlgo);
		  if (m_project.getNonBlockingProp() != eNonBlockYes || !m_runIncremental)
			 {
			bool CntrResult =m_project.checkControllable(m_ctrlAlgo);	     
			m_runSuccessful &= CntrResult;
			if(NonBlockingResult &&!CntrResult && !(m_ctrlAlgo.CE_tuplemap.empty()))
			{
				m_ctrlAlgo.setErrorAlgoFlag(false);				
				QMessageBox msgBox;	
				msgBox.setText("The project is not Controllable.<HR> Do you want to generate a counter example? Depending on the system, it may take a long time. ");
				msgBox.setIcon(QMessageBox::Critical );
				msgBox.setWindowTitle("DESpot");
				msgBox.addButton(QMessageBox::Yes);
				msgBox.addButton(QMessageBox::No);
				int DebugResponse=msgBox.exec();

				if(DebugResponse==QMessageBox::Yes)
				{								
					CounterExampleAlgo_FlatCntr CEAlgo(m_ctrlAlgo.CE_tuplemap,&m_project,m_project.createProjEventIterator());
					bool result=CEAlgo.runAlgo();
					if(result)
					{
						m_project.setCounterExample(CEAlgo.GetCounterExample());			
						m_project.setDummyProject(&m_project);	
						m_project.setDebugMode(DesProject::CounterExample);
						QMessageBox::information(NULL, "DESpot","Counter example generated successfully.");
					}
				}
	   		else	  
			{				
				m_project.setDebugMode(DesProject::ErrorTuple);				
				DESpot::DummyProject temp(&m_project,m_ctrlAlgo.CE_tuplemap);
				m_project.setDummyProject((DesProject*)&m_project);
				m_project.setSimulationErrorTuple(temp.getSimulationErrorTuple());			
		    }
			}

	    }
	  
	 }
	  else
	    {
			 //this project is controllable and we're running the algorithm incrementally so 
			 //override the result of the algorithm without actually running the algorithm.
			 //this is needed because the algorithm is used to output information to the user
			 m_ctrlAlgo.overrideControllable(true);
			 
		}
}
	//m_project.setProjectChkFlag(false);
	return m_runSuccessful; // = is intentional
}

} //end of namespace DESpot
