/*	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 <QMenu>
#include <QMenuBar>
#include <QToolBar>
#include <QIcon>
#include <QStatusBar>
#include <QMessageBox>
#include <qevent.h>
#include <QHeaderView>

// RJL: added for exportBDDsd -  remove when bddsd
		//integrated with despot
#include <QFileInfo>
#include "MainForm.h"
// remove to here - RJL

// for debug
 #include <iostream>


#include "FlatProjectEditor.h"
#include "CommonDefinitions.h"
#include "FlatProjectWorkspace.h"
#include "DesFlatProject.h"
#include "AddDesToProjectDlg.h"
#include "Des.h"
#include "ProjStructureUiPart.h"
#include "FlatProjStructureUiPart.h"
#include "MeetAlgo.h"
#include "SyncAlgo.h"
#include "NonBlockingAlgo.h"
//#include "CtrlStdAlgo.h"
#include "DesEditor.h"
#include "OutputUiPart.h"
#include "FlatProjIntegrityAlgo.h"
#include "WaitCursor.h"
#include "CheckProjectDlg.h"
#include "NonBlockingAlgo.h"
#include "MultiCtrlAlgo.h"
#include "FlatProjectPropCheck.h"
#include "BddSdMain.h"

namespace DESpot
{

FlatProjectEditor::FlatProjectEditor(const QString& projName, MainForm* pMainForm) : ProjectEditor(pMainForm, eFlatProjectEditor)
{
	m_pProject = new DesFlatProject(projName.toStdWString());
	
	//create the workspace shown in form
	m_pWorkspace = new FlatProjectWorkspace(this, this->project());

	//set form attributes
	setAttribute(Qt::WA_DeleteOnClose);

	setupConnections();

	updateWindowTitle();
}

//_________________________________________________________________________________________________

FlatProjectEditor::FlatProjectEditor(DesProject* project, MainForm* pMainForm): ProjectEditor(project, pMainForm, eFlatProjectEditor)
{
	//create the workspace shown in form
	m_pWorkspace = new FlatProjectWorkspace(this, this->project());

	//set form attributes
	setAttribute(Qt::WA_DeleteOnClose);

	setupConnections();

	updateWindowTitle();
}

//_________________________________________________________________________________________________

FlatProjectEditor::~FlatProjectEditor(void)
{
}

//_________________________________________________________________________________________________

DesFlatProject* FlatProjectEditor::project()
{
	return dynamic_cast<DesFlatProject*>(m_pProject);
}

//_________________________________________________________________________________________________

FlatProjectWorkspace* FlatProjectEditor::workspace()
{
	return dynamic_cast<FlatProjectWorkspace*>(m_pWorkspace);
}

//_________________________________________________________________________________________________

void FlatProjectEditor::setupConnections()
{
	ProjectEditor::setupConnections();
}

//_________________________________________________________________________________________________

void FlatProjectEditor::onAddDes()
{
	try
	{
		AddDesToProjectDlg addDesDlg(*m_pProject, this);
		
		//initialize the dialog approriately depending on what is selected in the
		//project structure widget
		DesLevel desLevel;
		if (workspace()->projStructureUiPart().getCurrentDesLevel(desLevel))
		{
			//a DES type can be determined from whatever is selected in the 
			//project structure UI part so initialize the dialog to add the same type of DES
			addDesDlg.setDesLevel(desLevel);
		}
		
		if (addDesDlg.exec() == QDialog::Accepted)
		{
			if (addDesDlg.isNewDes())
			{
				//a new DES must be created with the name given by the user
				Des* pDes = new Des(addDesDlg.getNewDesName());			

				//add the DES to the project
				project()->addDes(pDes, addDesDlg.getDesLevel());
			}
			else
			{
				WaitCursor wait(this);
			
				Des* pDes = new Des();
				pDes->load(addDesDlg.getDesFileName());

				//add the DES to the project
				project()->addDes(pDes, addDesDlg.getDesLevel());
			}
		}
	}
	catch_display_ex()
}

//_________________________________________________________________________________________________

void FlatProjectEditor::onCheckProjectIntegrity()
{
	try
	{
		WaitCursor wait(this);
	
		FlatProjIntegrityAlgo integAlgo;
		
		//call the base class to do the check now that we've created the proper algorithm
		ProjectEditor::onCheckProjectIntegrity(integAlgo);
	}
	catch_display_ex()
}

//_________________________________________________________________________________________________

void FlatProjectEditor::onCheckProject()
{

	try
	{
		CheckProjectDlg checkProjDlg(eFlatProject, this);
		if (checkProjDlg.exec() == QDialog::Accepted)
		{
			WaitCursor wait(this);

			FlatProjectPropCheck projCheckAlgo(*project(), checkProjDlg.checkIncremental());
			
			projCheckAlgo.checkIntegrity(checkProjDlg.checkValid());
			projCheckAlgo.checkNonBlock(checkProjDlg.checkNonBlocking());
			projCheckAlgo.checkCtrl(checkProjDlg.checkCtrl());
			
			projCheckAlgo.runEx(NULL);
			//	projCheckAlgo.runEx(progressInterface());

			output().show(projCheckAlgo);
		}
	}
	catch(const std::wstring& e)
	{

		output().show(OutputUiPart::eProjectPropCheck, L"An error occurred while checking the project's properties", e);
	}
	catch_display_all()
}

//_________________________________________________________________________________________________

//Added by Adam for BDD Tools

#ifdef __ENABLE_BDD__

void FlatProjectEditor::onRunBddCheckAllTool()
{

  try
    {		
      
      WaitCursor wait(this);	

      int tmp;
      BDDSD::SD_ChkInfo  checkInfo("Project passes all BDDSD Checks");
      
      tmp = BddSdCheckSDAll(*m_pProject, checkInfo);
      
     //check only returns here if a pass/fail result is available
      // need to set appropriate flags
      if (checkInfo.m_chkPassed)
	{
	  // all passed so update all statuses.
	  project()->procBddNonBlockProp(checkInfo);
	  project()->procBddCtrlProp(checkInfo);
	  // would update remaining properties when added
	  // would need to add updates to the test failed section
	  // below as well

	  // now need to send output to various tabs
	  BDDSD::SD_NBChkInfo  checkInfoNB("Project passes Nonblocking Check");
	  checkInfoNB.m_chkPassed = true;
	  checkInfoNB.m_succStr = checkInfo.m_succStr;
	  output().show(checkInfoNB, OutputUiPart::eSetLastOutput, false /*no popup */);

	  BDDSD::SD_SDCtrlChkInfo  checkInfoSDCtrl("Project passes SD Controllability Check");
	  checkInfoSDCtrl.m_chkPassed = true;
	  checkInfoSDCtrl.m_succStr = checkInfo.m_succStr;
	  output().show(checkInfoSDCtrl, OutputUiPart::eAppendLastOutput, false /*no popup */);

	  BDDSD::SD_PTBChkInfo  checkInfoPTB("Project passes Proper Time Behavior Check");
	  checkInfoPTB.m_chkPassed = true;
	  checkInfoPTB.m_succStr = checkInfo.m_succStr;
	  output().show(checkInfoPTB, OutputUiPart::eAppendLastOutput, false /*no popup */);

	  BDDSD::SD_SSingPChkInfo  checkInfoSSingP("Project passes S-singular Prohibitable Behavior Check");
	  checkInfoSSingP.m_chkPassed = true;
	  checkInfoSSingP.m_succStr = checkInfo.m_succStr;
	  output().show(checkInfoSSingP, OutputUiPart::eAppendLastOutput, false /*no popup */);

	  BDDSD::SD_PCmpltChkInfo  checkInfoPCmplt("Project passes Plant Completeness Check");
	  checkInfoPCmplt.m_chkPassed = true;
	  checkInfoPCmplt.m_succStr = checkInfo.m_succStr;
	  output().show(checkInfoPCmplt, OutputUiPart::eAppendLastOutput, false /*no popup */);

	  BDDSD::SD_ALFChkInfo  checkInfoALF("Project passes Activity Loop Free Check");
	  checkInfoALF.m_chkPassed = true;
	  checkInfoALF.m_succStr = checkInfo.m_succStr;
	  output().show(checkInfoALF, OutputUiPart::eAppendLastOutput, false /*no popup */);

	  BDDSD::SD_CtrlChkInfo  checkInfoCtrl("Project passes all BDDSD Checks"); 
	  checkInfoCtrl.m_chkPassed = true;
	  checkInfoCtrl.m_succStr = checkInfo.m_succStr;
	  output().show(checkInfoCtrl, OutputUiPart::eAppendLastOutput, true);
	}
      else
	{
	  //  can only update and output for the failed property
	  if (checkInfo.m_NBChkFail)
	    {
	      project()->procBddNonBlockProp(checkInfo);
	      BDDSD::SD_NBChkInfo  checkInfoNB("Project passes Nonblocking Check");
	      checkInfoNB.m_chkPassed = false;
	      checkInfoNB.m_errStr = checkInfo.m_errStr;
	      output().show(checkInfoNB);
	    }
	  else if (checkInfo.m_CtrlChkFail)
	    {
	      project()->procBddCtrlProp(checkInfo);
	      BDDSD::SD_CtrlChkInfo  checkInfoCtrl("Project passes Untimed Controllability Check");
	      checkInfoCtrl.m_chkPassed = false;
	      checkInfoCtrl.m_errStr = checkInfo.m_errStr;
	      output().show(checkInfoCtrl);
	    }
	  else if (checkInfo.m_SDCtrlChkFail)
	    {
	      BDDSD::SD_SDCtrlChkInfo  checkInfoSDCtrl("Project passes SD Controllability Check");
	      checkInfoSDCtrl.m_chkPassed = false;
	      checkInfoSDCtrl.m_errStr = checkInfo.m_errStr;
	      output().show(checkInfoSDCtrl);
	    }
	  else if (checkInfo.m_PropTimedBChkFail)
	    {
	      BDDSD::SD_PTBChkInfo  checkInfoPTB("Project passes Proper Time Behavior Check");
    	      checkInfoPTB.m_chkPassed = false;
	      checkInfoPTB.m_errStr = checkInfo.m_errStr;
	      output().show(checkInfoPTB);
	    }
	  else if (checkInfo.m_SSingPhibBChkFail)
	    {
	      BDDSD::SD_SSingPChkInfo  checkInfoSSingP("Project passes S-singular Prohibitable Behavior Check");
    	      checkInfoSSingP.m_chkPassed = false;
	      // this is to ensure proper output as 
	      // currently sd cont and this test are combined.
	      checkInfoSSingP.m_SSingPhibBChkFail = true;
	      checkInfoSSingP.m_errStr = checkInfo.m_errStr;
	      output().show(checkInfoSSingP);
	    }
	  else if (checkInfo.m_PCompltChkFail)
	    {
	  BDDSD::SD_PCmpltChkInfo  checkInfoPCmplt("Project passes Plant Completeness Check");
    	      checkInfoPCmplt.m_chkPassed = false;
	      checkInfoPCmplt.m_errStr = checkInfo.m_errStr;
	      output().show(checkInfoPCmplt);
	    }
	  else if (checkInfo.m_ALFChkFail)
	    {
	  BDDSD::SD_ALFChkInfo  checkInfoALF("Project passes Activity Loop Free Check");
    	      checkInfoALF.m_chkPassed = false;
	      checkInfoALF.m_errStr = checkInfo.m_errStr;
	      output().show(checkInfoALF);
	    }
	}
    }
  catch_display_ex()

}

//_________________________________________________________________________________________________

void FlatProjectEditor::onRunBddNonblockingTool()
{

  try
    {		
      
      WaitCursor wait(this);	

      int tmp;
      BDDSD::SD_NBChkInfo  checkInfo("Project passes Nonblocking Check");
      
      tmp = BddSdCheckNB(*m_pProject, checkInfo);

      //check only returns here if a pass/fail result is available
      // need to set appropriate flags
      project()->procBddNonBlockProp(checkInfo);
      
      output().show(checkInfo);

    }
  catch_display_ex()


}

//_________________________________________________________________________________________________

void FlatProjectEditor::onRunBddTDESControllabilityTool()
{
	try
	{		
		QMessageBox::information(this, "DESpot","Feature not implemented yet.");
	}
	catch_display_ex()
}


//_________________________________________________________________________________________________

void FlatProjectEditor::onRunBddControllabilityTool()
{

  try
    {		
      
      WaitCursor wait(this);	

      int tmp;
      BDDSD::SD_CtrlChkInfo  checkInfo("Project passes Untimed Controllability Check");

      //std::cout << "entering onRunBddControllabilityTool.\n";
      
      tmp = BddSdCheckCtrl(*m_pProject, checkInfo);
      

      //check only returns here if a pass/fail result is available
      // need to set appropriate flags
      project()->procBddCtrlProp(checkInfo);

      output().show(checkInfo);

    }
  catch_display_ex()


}

//_________________________________________________________________________________________________

void FlatProjectEditor::onRunBddNBControllabilityTool()
{

  try
    {		
      
      WaitCursor wait(this);	

      int tmp;
      BDDSD::SD_ChkInfo  checkInfo("Project is Nonblocking and passes Untimed Controllability Check");
      
      tmp = BddSdCheckNBCtrl(*m_pProject, checkInfo);
      
      std::cout << "entering contNNB test.\n";

      //check only returns here if a pass/fail result is available
      // need to set appropriate flags
      if (checkInfo.m_chkPassed)
	{
	  // all passed so update all statuses.
	  project()->procBddNonBlockProp(checkInfo);
	  project()->procBddCtrlProp(checkInfo);

	  // now need to send output to various tabs
	  BDDSD::SD_NBChkInfo  checkInfoNB("Project passes Nonblocking Check");
	  checkInfoNB.m_chkPassed = true;
	  checkInfoNB.m_succStr = checkInfo.m_succStr;
	  output().show(checkInfoNB, OutputUiPart::eSetLastOutput, false /*no popup */);

	  BDDSD::SD_CtrlChkInfo  checkInfoCtrl("Project  is Nonblocking and passes Untimed Controllability Check");
	  checkInfoCtrl.m_chkPassed = true;
	  checkInfoCtrl.m_succStr = checkInfo.m_succStr;
	  output().show(checkInfoCtrl, OutputUiPart::eAppendLastOutput, true);
	}
      else
	{

      std::cout << "entering contNNB test failed section.\n";

	  //  can only update and output for the failed property
	  if (checkInfo.m_NBChkFail)
	    {
	      project()->procBddNonBlockProp(checkInfo);
	      BDDSD::SD_NBChkInfo  checkInfoNB("Project passes Nonblocking Check");
	      checkInfoNB.m_chkPassed = false;
	      checkInfoNB.m_errStr = checkInfo.m_errStr;
	      output().show(checkInfoNB);
	    }
	  else if (checkInfo.m_CtrlChkFail)
	    {
	      std::cout << "entering contNNB test failed cont section.\n";
	      project()->procBddCtrlProp(checkInfo);
	      BDDSD::SD_CtrlChkInfo  checkInfoCtrl("Project passes Untimed Controllability Check");
	      checkInfoCtrl.m_chkPassed = false;
	      checkInfoCtrl.m_errStr = checkInfo.m_errStr;
	      output().show(checkInfoCtrl);
	      std::cout << "exiting contNNB test failed cont section.\n";
	    }
	}
    }
  catch_display_ex()
}

//_________________________________________________________________________________________________

void FlatProjectEditor::onRunBddSDControllabilityTool()
{
  try
    {		
      
      WaitCursor wait(this);	

      int tmp;
      // these are from BddHiscCheckLWNonBlk
      //      QString succMessage = "";

      // set to process all susbsytems
      //      QString subSysName =  "all!";
      // isHigh will be ignored
      // bool isHigh = false;

      //      BDDHISC::Hisc_LWNBChkInfo checkInfo("Project is LD
      //      level-wise nonblocking.");
      // replace this with the sd cont version
      BDDSD::SD_SDCtrlChkInfo  checkInfo("Project passes SD Controllability Check");
      
      tmp = BddSdCheckSDCtrl(*m_pProject, checkInfo);
      
      //check only returns here if a pass/fail result is available
      // need to set appropriate flags
      
      // When flags added for this property, need to add
      // function like  one below to set them
      //      project()->procBddNonBlockProp(checkInfo);

      output().show(checkInfo);

	}
	catch_display_ex()
}

//_________________________________________________________________________________________________

void FlatProjectEditor::onRunBddProperTimebehaviorTool()
{

  try
    {		
      
      WaitCursor wait(this);	

      int tmp;
      BDDSD::SD_PTBChkInfo  checkInfo("Project passes Proper Time Behavior Check");
      
      tmp = BddSdCheckPTB(*m_pProject, checkInfo);
      
      output().show(checkInfo);

    }
  catch_display_ex()

}

//_________________________________________________________________________________________________

void FlatProjectEditor::onRunBddSSingularProhibitableBehaviorTool()
{

  try
    {		
      
      WaitCursor wait(this);	

      int tmp;
      BDDSD::SD_SSingPChkInfo  checkInfo("Project passes S-singular Prohibitable Behavior Check");
      
      tmp = BddSdCheckSSingP(*m_pProject, checkInfo);
      
      output().show(checkInfo);

    }
  catch_display_ex()


}

//_________________________________________________________________________________________________

void FlatProjectEditor::onRunBddPlantCompletenessTool()
{

  try
    {		
      
      WaitCursor wait(this);	

      int tmp;
      BDDSD::SD_PCmpltChkInfo  checkInfo("Project passes Plant Completeness Check");
      
      tmp = BddSdCheckPCmplt(*m_pProject, checkInfo);
      
      output().show(checkInfo);

    }
  catch_display_ex()

}

//_________________________________________________________________________________________________

void FlatProjectEditor::onRunBddALFTool()
{

  try
    {		
      
      WaitCursor wait(this);	

      int tmp;
      BDDSD::SD_ALFChkInfo  checkInfo("Project passes Activity Loop Free Check");
      
      tmp = BddSdCheckALF(*m_pProject, checkInfo);
      
      output().show(checkInfo);

    }
  catch_display_ex()

}

#endif

//_________________________________________________________________________________________________

//Added by Adam for bddExport  remove when bddhisc
// integrated with despot  (see other places where changes made and
// remove as well). See svn revision 220 for details. 218 as well.
void FlatProjectEditor::onExportToBDDsd()
{
	try
	{
	  attemptExportToBDDsd();
	}
	catch_display_xml_ex()
	catch_display_ex()
}

// remove to here - Adam

// added by RJL - remove when bddsd
// integrated with despot 
bool FlatProjectEditor::attemptExportToBDDsd()
{


  if (!m_pProject->isValid()) 
    {
       throw EX("Project integrity test must pass before exporting allowed.");
    }


  QString warning = "WARNING: exporting to BDDsd format will create\
  a number of files (*.sub for projects and *.hsc for DES).  If any file\
 already exists, it will be overwritten without warning.\n\nDo you\
  want to continue?"; 


  if (QMessageBox::question(this, STR_DESPOT_WARNING, warning, QMessageBox::Yes|QMessageBox::No) == QMessageBox::No)
    {
			return false;
    }


	QString absoluteFileName = m_pProject->isNew()? QString::fromStdWString(m_pProject->getName()) : QString::fromStdWString(m_pProject->getFileName()); 

        if (absoluteFileName.endsWith(".desp",Qt::CaseInsensitive)) 
	  {
	    absoluteFileName.replace((absoluteFileName.length()-4), 4,"sub");
	  }

      
	if (MainForm::getSaveFileName(this, tr("Export to BDDsd format"), tr("BDDsd Project Files (*.sub)"), absoluteFileName) == false)
	{
		//user canceled the save as
		return false;
	}

	//getSaveFileName  is adding the despot extension, so we need
        // to remove that
        if (absoluteFileName.endsWith(".desp",Qt::CaseInsensitive)) 
	  {
	    absoluteFileName.remove((absoluteFileName.length()-5), 5);
	  }


	// we now need to check to make sure name ends in ".sub"
        if (!absoluteFileName.endsWith(".sub",Qt::CaseInsensitive)) 
	  {
	    absoluteFileName += ".sub";
	  }

	NameValidator fileNameValidator(new AlphaNumValidator(new WordSepValidator(new DotValidator())));
	std::wstring fileName = QFileInfo(absoluteFileName).fileName().toStdWString();
	if (fileNameValidator.validate(fileName) == false)							  
	{
		std::wstring message = L"Invalid project file name (";
		message += fileName;
		message += L"). Use an alpha-numeric string (a-z;A-Z;0-9;.-_)";
		throw message;
	}

	m_pProject->exportToBDDsd(absoluteFileName.toStdWString());

	return true;
}

// remove to here - RJL

} //end of namespace DESpot
