/*	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 "HierProjectPropCheck.h"
#include "DummyProjCreation.h"
#include "CounterExampleAlgo_IAnsAccept.h"
#include "CounterExampleAlgo_IReqAcpt.h"
#include "CounterExampleAlgo_LwCntr.h"
#include "CounterExampleAlgo_LwNB.h"

// for debug
// #include <iostream>

namespace DESpot
{

const std::wstring HierProjectPropCheck::cHierProjectPropCheckAlgoDesc = L"HISC Project Properties Check Algorithm";

HierProjectPropCheck::HierProjectPropCheck(DesHierProject& project, bool runIncremental /*= true*/):
		m_project(project),
		m_checkInteg(true),
		m_integAlgo(runIncremental),
		m_checkIConsist(true),
		m_iConsAlgo(project, runIncremental),
		m_checkLwNonBlock(true),
		m_lwNonBlockAlgo(project, runIncremental),
		m_checkLwCtrl(true),
		m_lwCtrlAlgo(project, runIncremental),
		m_runSuccessful(false)
{
	m_runIncremental = runIncremental;
	m_description = cHierProjectPropCheckAlgoDesc;
}

//_________________________________________________________________________________________________

HierProjectPropCheck::~HierProjectPropCheck(void)
{
}

//_________________________________________________________________________________________________

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

//_________________________________________________________________________________________________

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

//_________________________________________________________________________________________________

HierProjIntegrityAlgo& HierProjectPropCheck::integAlgo()
{
	return m_integAlgo;
}

//_________________________________________________________________________________________________

void HierProjectPropCheck::checkInterfConsist(bool checkIConsist /*= true*/)
{
	m_checkIConsist = checkIConsist;
}

//_________________________________________________________________________________________________

bool HierProjectPropCheck::iConsistChecked() const
{
	return m_checkIConsist;
}

//_________________________________________________________________________________________________

IConsistAlgo& HierProjectPropCheck::interfConsistAlgo()
{
	return m_iConsAlgo;
}

//_________________________________________________________________________________________________

void HierProjectPropCheck::checkLwNonBlock(bool checkLwNonBlock /*= true*/)
{
	m_checkLwNonBlock = checkLwNonBlock;
}

//_________________________________________________________________________________________________

bool HierProjectPropCheck::lwNonBlockChecked() const
{
	return m_checkLwNonBlock;
}

//_________________________________________________________________________________________________

LwNonBlockingAlgo& HierProjectPropCheck::levelWiseNonBlockAlgo()
{
	return m_lwNonBlockAlgo;
}

//_________________________________________________________________________________________________

void HierProjectPropCheck::checkLwCtrl(bool checkLwCtrl /*= true*/)
{
	m_checkLwCtrl = checkLwCtrl;
}

//_________________________________________________________________________________________________

bool HierProjectPropCheck::lwCtrlChecked()
{
	return m_checkLwCtrl;
}

//_________________________________________________________________________________________________

LwCtrlAlgo& HierProjectPropCheck::levelWiseCtrlAlgo()
{
	return m_lwCtrlAlgo;
}

//_________________________________________________________________________________________________

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

//_________________________________________________________________________________________________

void HierProjectPropCheck::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_iConsAlgo.provideProgress(m_progress);
	m_lwNonBlockAlgo.provideProgress(m_progress);
	m_lwCtrlAlgo.provideProgress(m_progress);
}

//_________________________________________________________________________________________________

bool HierProjectPropCheck::runAlgo()
{
	prepareRun();

	m_runSuccessful = 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 con=false;
	bool non=false;
	bool intf=false;
	bool CounterExampleGenerated=false;
	m_project.setProjectChkFlag(true);

	if (m_checkIConsist)
	{
	  if (m_project.getIConsistProp() != eIConsYes || !m_runIncremental)
	    {
	      intf=true;
		   m_iConsAlgo.start();
		  
	    }
	  else
	    {
	      m_iConsAlgo.overrideInterfConsist(true);
	    }
	}

	if (m_checkLwNonBlock)
	{
	  if (m_project.getLwNonBlockProp() != eLwNonBlockYes || !m_runIncremental)
	    {
	      non=true;		  
	      m_lwNonBlockAlgo.start();		  
	    }
	  else
	    {
	      m_lwNonBlockAlgo.overrideLwNonBlocking(true);
	    }
	}
	
	if (m_checkLwCtrl)
	{
	  if (m_project.getLwCtrlProp() != eLwCtrlYes || !m_runIncremental)
	    {
	      con=true;
	      m_lwCtrlAlgo.start();		  
	    }
	  else
	    {
	      m_lwCtrlAlgo.overrideLwControllable(true);
	    }
	}	
	
	
	if(intf==true)
	{
		m_iConsAlgo.wait();
		bool IConstchkResult = m_project.checkIConsistProp(m_iConsAlgo,true);
       // m_runSuccessful &= m_project.checkIConsistProp(m_iConsAlgo,true);
		m_runSuccessful &=IConstchkResult;

		  /****Counter example generation ****/

if(!IConstchkResult && !(m_iConsAlgo.CE_tuplemap.empty()))
{
	if(m_iConsAlgo.getIFailureType()==DesAlgo::ReqAcptAlgo || m_iConsAlgo.getIFailureType()==DesAlgo::IntrfImplAlgo ||m_iConsAlgo.getIFailureType()==DesAlgo::AnsAcptAlgo )
{
		   CounterExampleGenerated=true;		  
			QMessageBox msgBox;	
			msgBox.setText("The project is not Interface Consistent.<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)
		{
		  if(m_iConsAlgo.getIFailureType()==DesAlgo::AnsAcptAlgo )
			{	
				DESpot::DummyProject m_dummyproj(m_iConsAlgo.getErrorSubsystem(),&m_project,m_iConsAlgo.CE_tuplemap);
				m_project.setDummyProject(m_dummyproj.GetDummyProject());
				CounterExampleAlgo_IAnsAcpt CEAlgo(m_iConsAlgo.CE_tuplemap,&m_project,m_project.getDummyProject()->createProjEventIterator());	
				bool result=CEAlgo.runAlgo();
				if(result)
				{
					m_project.setDebugMode(DesProject::CounterExample);
					m_project.setCounterExample( CEAlgo.GetCounterExample());
					QMessageBox::information(NULL, "DESpot","Counter example generated successfully.");
				}
				else
				{	
					m_project.setDebugMode(DesProject::ErrorTuple);					
					m_project.setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
			 }			
		  else if(m_iConsAlgo.getIFailureType()==DesAlgo::ReqAcptAlgo) 
			{
				DESpot::DummyProject m_dummyproj(m_iConsAlgo.getErrorSubsystem(),m_iConsAlgo.CE_tuplemap,&m_project);
				m_project.setDummyProject(m_dummyproj.GetDummyProject());
				CounterExampleAlgo_IReqAcpt CEAlgo(m_iConsAlgo.CE_tuplemap,*(m_iConsAlgo.getErrorSubsystem()),m_project.getDummyProject()->createProjEventIterator());
				bool result=CEAlgo.runAlgo();
				if(result)
				{
					m_project.setDebugMode(DesProject::CounterExample);
					m_project.setCounterExample( CEAlgo.GetCounterExample());	
					QMessageBox::information(NULL, "DESpot","Counter example generated successfully.");
				}
				else
				{	
					m_project.setDebugMode(DesProject::ErrorTuple);					
					m_project.setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
			
			}

		  else if(m_iConsAlgo.getIFailureType()==DesAlgo::IntrfImplAlgo ) 
			{
				DESpot::DummyProject m_dummyproj(m_iConsAlgo.getErrorSubsystem(),m_iConsAlgo.CE_tuplemap,&m_project);
				m_project.setDummyProject(m_dummyproj.GetDummyProject());
				CounterExampleAlgo_IntfImpAlgo CEAlgo(m_iConsAlgo.getProject(),m_iConsAlgo.getErrorSubsystem(),
												  m_project.getDummyProject()->createProjEventIterator(),
												  m_iConsAlgo.CE_tuplemap);
				bool result=CEAlgo.runAlgo();
				if(result)
				{
					m_project.setDebugMode(DesProject::CounterExample);
					m_project.setCounterExample( CEAlgo.GetCounterExample());
					QMessageBox::information(NULL, "DESpot","Counter example generated successfully.");
				}
				else
				{	
					m_project.setDebugMode(DesProject::ErrorTuple);					
					m_project.setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
		    }	 
		}

	 else // for response NO
		{	
			if(m_iConsAlgo.getErrorSubsystem()->getLevel()==0)
			{
				//for high level
				DESpot::DummyProject m_dummyproj(m_iConsAlgo.getErrorSubsystem(),&m_project,m_iConsAlgo.CE_tuplemap);		
				m_project.setDebugMode(DesProject::ErrorTuple);
				m_project.setDummyProject(m_dummyproj.GetDummyProject());
				m_project.setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}
			else
			{
				//for low level
				DESpot::DummyProject m_dummyproj(m_iConsAlgo.getErrorSubsystem(),m_iConsAlgo.CE_tuplemap,&m_project);		
				m_project.setDebugMode(DesProject::ErrorTuple);
				m_project.setDummyProject(m_dummyproj.GetDummyProject());
				m_project.setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}
		}
	}
			/************************************************/
}
	}

	if(non==true)
	{
		m_lwNonBlockAlgo.wait();
		bool NBAlgoResult = m_project.checkLwNonBlockProp(m_lwNonBlockAlgo,true);
        //m_runSuccessful &= m_project.checkLwNonBlockProp(m_lwNonBlockAlgo,true);
		m_runSuccessful &=NBAlgoResult;

		/**** Counter example generation ****/		
if(!CounterExampleGenerated && !(NBAlgoResult) && !(m_lwNonBlockAlgo.CE_tuplemap.empty()))
{
			 CounterExampleGenerated=true;
			 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(m_lwNonBlockAlgo.getErrorSubsystem()->getLevel()==0)
	{	
			if(DebugResponse==QMessageBox::Yes)
			{
			DESpot::DummyProject m_dummyproj(m_lwNonBlockAlgo.getErrorSubsystem(),&m_lwNonBlockAlgo.getProject(),m_lwNonBlockAlgo.CE_tuplemap);			
			m_project.setDummyProject(m_dummyproj.GetDummyProject());
			CounterExampleAlgo_LwNB counterexpalgo(&m_lwNonBlockAlgo.getProject(),
											  m_lwNonBlockAlgo.getErrorSubsystem(),
											  m_lwNonBlockAlgo.CE_tuplemap,
											  m_project.getDummyProject()->createProjEventIterator());
			bool result=counterexpalgo.runAlgo();
				if(result)
				{
					m_project.setDebugMode(DesProject::CounterExample);
					m_project.setCounterExample( counterexpalgo.GetCounterExample());
					QMessageBox::information(NULL, "DESpot","Counter example generated successfully.");
				}
				else
				{	
					m_project.setDebugMode(DesProject::ErrorTuple);					
					m_project.setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
			}
			else
			{
				DESpot::DummyProject m_dummyproj(m_lwNonBlockAlgo.getErrorSubsystem(),&m_lwNonBlockAlgo.getProject(),m_lwNonBlockAlgo.CE_tuplemap);	
				m_project.setDebugMode(DesProject::ErrorTuple);
				m_project.setDummyProject(m_dummyproj.GetDummyProject());
				m_project.setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}
	}
	else
			if(DebugResponse==QMessageBox::Yes)
			{  
				DESpot::DummyProject m_dummyproj(m_lwNonBlockAlgo.getErrorSubsystem(),m_lwNonBlockAlgo.CE_tuplemap,&m_project);
				m_project.setDummyProject(m_dummyproj.GetDummyProject());
				CounterExampleAlgo_LwNB counterexpalgo(m_lwNonBlockAlgo.getErrorSubsystem(),
											  m_lwNonBlockAlgo.CE_tuplemap,
											  m_project.getDummyProject()->createProjEventIterator());
				bool result=counterexpalgo.runAlgo();
				if(result)
				{
					m_project.setDebugMode(DesProject::CounterExample);
					m_project.setCounterExample( counterexpalgo.GetCounterExample());
					QMessageBox::information(NULL, "DESpot","Counter example generated successfully.");
				}
				else
				{	
					m_project.setDebugMode(DesProject::ErrorTuple);					
					m_project.setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
			}		
			else
			{
				DESpot::DummyProject m_dummyproj(m_lwNonBlockAlgo.getErrorSubsystem(),m_lwNonBlockAlgo.CE_tuplemap,&m_project);	
				m_project.setDebugMode(DesProject::ErrorTuple);
				m_project.setDummyProject(m_dummyproj.GetDummyProject());
				m_project.setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}

}
		/**********************************************/
	}

    if(con==true)

	{
		m_lwCtrlAlgo.wait();
		bool isControllable = m_project.checkLwCtrlProp(m_lwCtrlAlgo,true);
		//m_runSuccessful &= m_project.checkLwCtrlProp(m_lwCtrlAlgo,true);
		m_runSuccessful &=isControllable;

		/********* Counter example generation ****************/		
if(!CounterExampleGenerated && !(isControllable)&& !(m_lwCtrlAlgo.CE_tuplemap.empty()))
{
			 CounterExampleGenerated=true;
			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(m_lwCtrlAlgo.getErrorSubsystem()->getLevel()==0  )
	{
			if(DebugResponse==QMessageBox::Yes)
			{
			DESpot::DummyProject m_dummyproj(m_lwCtrlAlgo.getErrorSubsystem(),&m_lwCtrlAlgo.getProject(),m_lwCtrlAlgo.CE_tuplemap);
			m_project.setDummyProject(m_dummyproj.GetDummyProject());
			CounterExampleAlgo_LwCntr counterexalgo(&m_lwCtrlAlgo.getProject(),
												     m_lwCtrlAlgo.getErrorSubsystem(),
													 m_lwCtrlAlgo.CE_tuplemap,
													 m_project.getDummyProject()->createProjEventIterator());
			bool result=counterexalgo.runAlgo();
			if(result)
				{
					m_project.setDebugMode(DesProject::CounterExample);
					m_project.setCounterExample(counterexalgo.GetCounterExample());
					QMessageBox::information(NULL, "DESpot","Counter example generated successfully.");
				}
				else
				{	
					m_project.setDebugMode(DesProject::ErrorTuple);					
					m_project.setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
				
			}
			else
			{DESpot::DummyProject m_dummyproj(m_lwCtrlAlgo.getErrorSubsystem(),&m_lwCtrlAlgo.getProject(),m_lwCtrlAlgo.CE_tuplemap);	
			m_project.setDebugMode(DesProject::ErrorTuple);
			m_project.setDummyProject(m_dummyproj.GetDummyProject());
			m_project.setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}
	}
	else
			if(DebugResponse==QMessageBox::Yes)
			{  
			DESpot::DummyProject m_dummyproj(m_lwCtrlAlgo.getErrorSubsystem(),m_lwCtrlAlgo.CE_tuplemap,&m_project);
			m_project.setDummyProject(m_dummyproj.GetDummyProject());
			CounterExampleAlgo_LwCntr counterexalgo(m_lwCtrlAlgo.getErrorSubsystem(),
													m_lwCtrlAlgo.CE_tuplemap,
												    m_project.getDummyProject()->createProjEventIterator());
			bool result=counterexalgo.runAlgo();
			if(result)
				{
					m_project.setDebugMode(DesProject::CounterExample);
					m_project.setCounterExample(counterexalgo.GetCounterExample());
					QMessageBox::information(NULL, "DESpot","Counter example generated successfully.");
				}
				else
				{	
					m_project.setDebugMode(DesProject::ErrorTuple);					
					m_project.setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
			}
			else
			{DESpot::DummyProject m_dummyproj(m_lwCtrlAlgo.getErrorSubsystem(),m_lwCtrlAlgo.CE_tuplemap,(DesHierProject*)&m_project);	
			m_project.setDebugMode(DesProject::ErrorTuple);
			m_project.setDummyProject(m_dummyproj.GetDummyProject());
			m_project.setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}
}
		/************************************/
	}

	

	return m_runSuccessful;
}

} //end of namespace DESpot
