/*	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 <QMessageBox>
#include <QFileInfo>
#include "MainForm.h"
#include "OutputUiPart.h"
#include "MultiNonBlockingAlgo.h"
//#include "CtrlStdAlgo.h"
#include "ProjIntegrityAlgo.h"
#include "MultiCtrlAlgo.h"
#include "DesProject.h"
#include "LdInterfaceCheckAlgo.h"
#include "IConsistAlgo.h"
#include "LwNonBlockingAlgo.h"
#include "LwCtrlAlgo.h"
#include "DesInterface.h"
#include "DesHierProject.h"
#include "IConsistAnsAcceptAlgo.h"
#include "LowSubsysIConsistAlgo.h"
#include "HighSubsysNonBlockAlgo.h"
#include "LowSubsysNonBlockAlgo.h"
#include "HighSubsysCtrlAlgo.h"
#include "LowSubsysCtrlAlgo.h"
#include "FlatProjectPropCheck.h"
#include "HierProjectPropCheck.h"
#include "MeetAlgo.h"
#include <assert.h>
#include <ctime>
#include <sstream>

#include "BddHiscMain.h"
#include "DummyProjCreation.h"

// for debug
//  #include <iostream>

namespace DESpot
{

const QString OutputUiPart::cProjIntegOutputTitle = "Project Integrity";
const QString OutputUiPart::cNonBlockOutputTitle = "Nonblocking";
const QString OutputUiPart::cCtrlOutputTitle = "Controllability";
const QString OutputUiPart::cSDCtrlOutputTitle = "SD Controllability";
const QString OutputUiPart::cPTBOutputTitle = "Proper Time Behavior";
const QString OutputUiPart::cSSingPOutputTitle = "S-Singular Prohibitable Behavior";
const QString OutputUiPart::cPCmpltOutputTitle = "Plant Completeness";
const QString OutputUiPart::cALFOutputTitle = "ALF";
const QString OutputUiPart::cSynthOutputTitle = "Synthesis";
const QString OutputUiPart::cMeasureOutputTitle = "System Measurements";
const QString OutputUiPart::cInterfConsistOutputTitle = "LD Interface Consistency";
const QString OutputUiPart::cLwNonBlockOutputTitle = "LD Level-Wise Nonblocking";
const QString OutputUiPart::cLwCtrlOutputTitle = "LD Level-Wise Controllable";
const QString OutputUiPart::cSubsysInterfConsistOutputTitle = "Subsystem LD I-Consistency";
const QString OutputUiPart::cSubsysNonBlockingOutputTitle = "Subsystem LD Nonblocking";
const QString OutputUiPart::cSubsysCtrlOutputTitle = "Subsystem LD Controllability";
const QString OutputUiPart::cLdInterfCheckTitle = "Interface LD Check";
const QString OutputUiPart::cLwSynthOutputTitle = "Level-Wise Synthesis";
const QString OutputUiPart::cSubsysSynthOutputTitle = "Subsystem Synthesis";
const QString OutputUiPart::cLastOutputTitle = "Last Output";



OutputUiPart::OutputUiPart(Ui::FlatProjectEditorUI* pUiContainer, DesProject* pProject) :
		m_project(pProject)
{
	initWidgets(pUiContainer);

	setupConnections();

	initOutputSelectionWidget();	
}

//_________________________________________________________________________________________________

OutputUiPart::OutputUiPart(Ui::HierProjectEditorUI* pUiContainer, DesProject* pProject):
		m_project(pProject)
{
	initWidgets(pUiContainer);

	setupConnections();

	initOutputSelectionWidget();
	
}

//_________________________________________________________________________________________________

OutputUiPart::~OutputUiPart()
{
}

//_________________________________________________________________________________________________

template<class T>
void OutputUiPart::initWidgets(T* pUiContainer)
{
	m_showOutputForWidg = pUiContainer->m_showOutputForWidg;
	m_copyBtn = pUiContainer->m_copyBtn;
	m_clearBtn = pUiContainer->m_clearBtn;
	m_wrapBtn = pUiContainer->m_wrapBtn;
	m_outputWidget = pUiContainer->m_outputWidg;

}

//_________________________________________________________________________________________________

void OutputUiPart::setupConnections()
{
	connect(m_showOutputForWidg, SIGNAL(currentIndexChanged(int)), this, SLOT(onShowOutputFor(int)));
	connect(m_clearBtn, SIGNAL(clicked()), m_outputWidget, SLOT(clear()));
	connect(m_outputWidget, SIGNAL(copyAvailable(bool)), m_copyBtn, SLOT(setEnabled(bool)));
	connect(m_copyBtn, SIGNAL(clicked()), m_outputWidget, SLOT(copy()));
	connect(m_wrapBtn, SIGNAL(clicked()), this, SLOT(onToggleWrap()));
}

//_________________________________________________________________________________________________

void OutputUiPart::initOutputSelectionWidget()
{
	m_showOutputForWidg->addItem(cLastOutputTitle);
	m_showOutputForWidg->addItem(cProjIntegOutputTitle, QString("Project integrity has not been checked in this session"));
	m_showOutputForWidg->addItem(cNonBlockOutputTitle, QString("Nonblocking has not been checked in this session"));
	m_showOutputForWidg->addItem(cCtrlOutputTitle, QString("Controllability has not been checked in this session"));
	m_showOutputForWidg->addItem(cSynthOutputTitle, QString("Synthesis has not been performed in this session"));
	if (m_project->getType() == eFlatProject)
	{
	m_showOutputForWidg->addItem(cSDCtrlOutputTitle, QString("SD Controllability has not been checked in this session"));
	m_showOutputForWidg->addItem(cPTBOutputTitle, QString("Proper Time Behavior has not been checked in this session"));
	m_showOutputForWidg->addItem(cSSingPOutputTitle, QString("S-Singular Prohibitable Behavior has not been checked in this session"));
	m_showOutputForWidg->addItem(cPCmpltOutputTitle, QString("Plant Completeness has not been checked in this session"));
	m_showOutputForWidg->addItem(cALFOutputTitle, QString("ALF has not been checked in this session"));
	}
	m_showOutputForWidg->addItem(cMeasureOutputTitle, QString("The size of the flat system is unknown and is not currently being calculated."));

	if (m_project->getType() == eHierProject)
	{
		m_showOutputForWidg->addItem(cInterfConsistOutputTitle, QString("LD-Interface consistency has not been checked in this session"));
		m_showOutputForWidg->addItem(cLwNonBlockOutputTitle, QString("LD Level-wise nonblocking has not been checked in this session"));
		m_showOutputForWidg->addItem(cLwCtrlOutputTitle, QString("LD Level-wise controllablility has not been checked in this session"));
		m_showOutputForWidg->addItem(cSubsysInterfConsistOutputTitle, QString("Selected a subsystem to check whether it is interface consistent or not."));
		m_showOutputForWidg->addItem(cLdInterfCheckTitle, QString("Select an interface to check if it is LD-interface"));
		m_showOutputForWidg->addItem(cSubsysNonBlockingOutputTitle, QString("Select an interface to check if it is nonblocking"));
		m_showOutputForWidg->addItem(cSubsysCtrlOutputTitle, QString("Select an interface to check if it is controllable"));
	m_showOutputForWidg->addItem(cLwSynthOutputTitle, QString("Level-wise Synthesis has not been performed in this session"));
	m_showOutputForWidg->addItem(cSubsysSynthOutputTitle, QString("Select a subsystem for synthesis"));
	}
}

//_________________________________________________________________________________________________

void OutputUiPart::setOwnerTabWidget(QTabWidget* tabWidget)
{
	m_tabWidget = tabWidget;
}

//_________________________________________________________________________________________________

void OutputUiPart::onShowOutputFor(int sourceIndex)
{
	QString output = m_showOutputForWidg->itemData(sourceIndex).toString();
	m_outputWidget->setHtml(output);
}

//_________________________________________________________________________________________________

void OutputUiPart::onToggleWrap()
{
	QTextEdit::LineWrapMode crtWrapMode = m_outputWidget->lineWrapMode();
	m_outputWidget->setLineWrapMode(crtWrapMode == QTextEdit::NoWrap ? QTextEdit::WidgetWidth : QTextEdit::NoWrap);
}

//_________________________________________________________________________________________________

void OutputUiPart::saveOutput()
{
	QString output = m_outputWidget->toHtml();
	m_showOutputForWidg->setItemData(m_showOutputForWidg->currentIndex(), output);
}

//_________________________________________________________________________________________________

void OutputUiPart::saveLastOutput(LastOutputOption copyToLastOutput)
{
	QString output = m_outputWidget->toHtml();

	int lastOutputIndex = m_showOutputForWidg->findText(cLastOutputTitle);
	QString lastOutput = m_showOutputForWidg->itemData(lastOutputIndex).toString();

	//set the output to show the Last Output section
	m_showOutputForWidg->setCurrentIndex(lastOutputIndex);

	if (copyToLastOutput == OutputUiPart::eSetLastOutput)
	{
		//we're supposed to set the last output so let's clear what's there
		clearLastOutput();

		m_outputWidget->write(output);

		m_showOutputForWidg->setItemData(lastOutputIndex, output);
	}
	else if (copyToLastOutput == OutputUiPart::eAppendLastOutput)
	{
		//the output widget already contains the "last output" so we just to write the new output
		m_outputWidget->write(output);

		//append current output to the last output if we were
		lastOutput += output;

		//save the new "last" output
		m_showOutputForWidg->setItemData(lastOutputIndex, lastOutput);
	}
}

//_________________________________________________________________________________________________

DesHierProject* OutputUiPart::hierProject()
{
	if (m_project->getType() == eHierProject)
	{
		return dynamic_cast<DesHierProject*>(m_project);
	}

	throw EX("Project not hierarhical");
}

//_________________________________________________________________________________________________

void OutputUiPart::show(ProjIntegrityAlgo& integAlgo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cProjIntegOutputTitle));
	m_outputWidget->clear();

	if (integAlgo.isValid())
	{
		if (integAlgo.getWarningCount() > 0)
		{
			QString out("<b>Project is valid - %1 warning(s)</b>");
			out = out.arg(integAlgo.getWarningCount());

			m_outputWidget->writeLine(out);

			if (showMsgBox)
			{
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", out);
			}

			m_outputWidget->writeLine("");

			//display all warnings
			const IntegrityAlgo::WarningList& warnList = integAlgo.getWarningList();
			for(IntegrityAlgo::WarnIt warnIt = warnList.begin(); warnIt != warnList.end(); ++warnIt)
			{
				m_outputWidget->writeLine(QString("Warning: ") + QString::fromStdWString(*warnIt));
			}
		}
		else
		{
			if (showMsgBox)
			{
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Project is valid");
			}

			QString out("Project is valid. Verified on %1");
			out = out.arg(QString::fromStdWString(m_project->getIntegrityStamp()));
			m_outputWidget->writeLine("<b>" + out + "</b>");
		}
	}
	else
	{
		QString out("Project is not valid - %1 error(s)");
		out = out.arg(integAlgo.getErrorCount());
		out += QString(", %1 warning(s)").arg(integAlgo.getWarningCount());

		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", out);
		}
		m_outputWidget->writeLine("<b>" + out + "</b>");


		//display all warnings
		m_outputWidget->writeLine("");const IntegrityAlgo::WarningList& warnList = integAlgo.getWarningList();
		for(IntegrityAlgo::WarnIt warnIt = warnList.begin(); warnIt != warnList.end(); ++warnIt)
		{
			m_outputWidget->writeLine(QString("Warning: ") + QString::fromStdWString(*warnIt));
		}

		//display all errors
        showErrors(integAlgo.getErrorList());
	}

	saveOutput();
}

//_________________________________________________________________________________________________

void OutputUiPart::show(ProjIntegrityAlgo& integAlgo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/,
						bool showMsgBox/* = true*/)
{
	show(integAlgo, showMsgBox);

	saveLastOutput(copyToLastOutput);
}
//_________________________________________________________________________________________________

void OutputUiPart::show(MultiNonBlockingAlgo& nonBlockAlgo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cNonBlockOutputTitle));

	m_outputWidget->clear();

	if (nonBlockAlgo.isNonBlocking())
	{
		QString message("System is nonblocking. Verified on %1");
		message = message.arg(QString::fromStdWString(m_project->getNonBlockingStamp()));
		if(!(m_project->getProjectChkFlag()))
		m_project->setDebugMode(DesProject::Reset);

		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","System is nonblocking ");
		}
		if(!(m_project->getProjectChkFlag()))
		m_project->setDebugMode(DesProject::Reset);
		m_outputWidget->writeLine("<b>" + message + "</b>");

	}
	else
	{
		m_outputWidget->writeLine("<b>System is blocking</b>");
		m_outputWidget->writeLine("The following states are blocking:");		

		//go through the blockign states and write them out in the output

     int errcount;
     QString message("System has %1 blocking state(s). See the output for the list of blocking states");
	
     if(nonBlockAlgo.getDesNum() >1)
	{
	  // for debug
	  //	  std::cout << "entering desNum > 1"  << "\n";

	  ErrorList errlst = nonBlockAlgo.getErrorList();
    	  errcount = errlst.size(); 	
		
	  QString blockingStateCount1 = QVariant(errcount).toString();

	  /**  Counter Example Genereation  **/	
	 if(nonBlockAlgo.getErrorAlgoFlag() && !(m_project->getProjectChkFlag()) && !(nonBlockAlgo.CE_tuplemap.empty()))
	{
		int DebugResponse=this->GetDebugResponse("System is blocking.");	  
		if(DebugResponse==QMessageBox::Yes)
		{			
			CounterExampleAlgo_FlatNB CEAlgo(nonBlockAlgo.CE_tuplemap,m_project->createDesIterator(), m_project->createProjEventIterator());		
			bool result=CEAlgo.runAlgo();
			DESpot::DummyProject temp(m_project,nonBlockAlgo.CE_tuplemap);
			m_project->setDummyProject(m_project);
			m_project->setSimulationErrorTuple(temp.getSimulationErrorTuple());
				if(result)
				{
					m_project->setCounterExample(CEAlgo.GetCounterExample());						
					m_project->setDebugMode(DesProject::CounterExample);
					QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
				}
				else
				{	
					m_project->setDebugMode(DesProject::ErrorTuple);
				}
		}
		else	  
	    {	
			DESpot::DummyProject temp(m_project,nonBlockAlgo.CE_tuplemap);
			m_project->setDummyProject(m_project);
			m_project->setSimulationErrorTuple(temp.getSimulationErrorTuple());	
			m_project->setDebugMode(DesProject::ErrorTuple);
			m_tabWidget->setCurrentIndex(2);
	    }		
						
	 }
	 /*else if(nonBlockAlgo.CE_tuplemap.empty())
	 {
		QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Either the project is not valid, or integrity \
		has not yet been checked.");
	 }*/

	  /***********************/

	  showErrors(errlst);
	  
	          
	}
      else
	{
	    // for debug
	  //	  std::cout << "entering desNum !> 1"  << "\n";

	  errcount=nonBlockAlgo.m_non_algo.getBlockingStateCount();
	  QString blockingStateCount2 = QVariant(errcount).toString();
	  
	  if (showMsgBox)
	    {
	      QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", message.arg(blockingStateCount2));
	    }


	  NonBlockingAlgo::StateIteratorPtr stateIt = nonBlockAlgo.m_non_algo.createBlockingStateIterator();

	  
	  for(stateIt->first(); stateIt->notDone(); stateIt->next())
	    {
	      const DesState* blockingState = stateIt->currentItem();
	      m_outputWidget->writeLine(QString(" &nbsp;&nbsp;&nbsp;&nbsp;%1").arg(QString::fromStdWString(blockingState->getName())));
	  

		  
	    }
	  errcount=nonBlockAlgo.m_non_algo.getBlockingStateCount();
	}

      m_outputWidget->writeLine("");// end is here

	  
	}

	//save the output in the output selection widget
	saveOutput();
}

//_________________________________________________________________________________________________

int OutputUiPart::GetDebugResponse(QString errormsg)
{
	QMessageBox msgBox;
	errormsg += "<HR>Do you want to generate a counter example? Depending on the system, it may take a long time.";
	msgBox.setText(errormsg);
	msgBox.setIcon(QMessageBox::Critical );
	msgBox.setWindowTitle("DESpot");
	msgBox.addButton(QMessageBox::Yes);
	msgBox.addButton(QMessageBox::No);
	int reply=msgBox.exec();
	return reply;		
}

//==================================================================================================

void OutputUiPart::show(MultiNonBlockingAlgo& nonBlockAlgo, LastOutputOption copyToLastOutput/* = eSetLastOutput*/,
						bool showMsgBox/* = true*/)
{
	show(nonBlockAlgo, showMsgBox);

	saveLastOutput(copyToLastOutput);
}
//_________________________________________________________________________________________________


/*
void OutputUiPart::show(CtrlStdAlgo& ctrlAlgo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cCtrlOutputTitle));
	m_outputWidget->clear();

	if (ctrlAlgo.isControllable())
	{
		QString message("System is controllable. Verified on %1");
		message = message.arg(QString::fromStdWString(m_project->getCtrlStamp()));

		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","The system is controllable");
		}

		m_outputWidget->writeLine("<b>" + message + "</b>");
	}
	else
	{
		m_outputWidget->writeLine("<b>The system is not controllable</b>");
		QString messageTempl = "The system is uncontrollable at state (%1, %2) for event %3.";
		QString plantStateName = QString::fromStdWString(ctrlAlgo.getUnctrlBehaviour().plantState->getName());
		QString supStateName = QString::fromStdWString(ctrlAlgo.getUnctrlBehaviour().supState->getName());
		QString blockEventName = QString::fromStdWString(ctrlAlgo.getUnctrlBehaviour().event->getName());
		QString message = messageTempl.arg(plantStateName, supStateName, blockEventName);

		m_outputWidget->writeLine(message);
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine("Trace to uncontrollable behaviour:");

		const CtrlStdAlgo::CounterExample& counterExample = ctrlAlgo.getCounterExample();
		for(CtrlStdAlgo::BehavIt it = counterExample.begin(); it != counterExample.end(); it++)
		{
			const CtrlStdAlgo::CtrlBehaviour& behav = *it;

			QString plantStateName = QString::fromStdWString(behav.plantState->getName());
			QString supStateName = QString::fromStdWString(behav.supState->getName());
			QString eventName = QString::fromStdWString(behav.event->getName());

			m_outputWidget->writeLine(QString("&nbsp;&nbsp;&nbsp;(%1, %2)&nbsp;&nbsp;-->&nbsp;&nbsp;%3").arg(plantStateName, supStateName, eventName));
		}

		if (m_tabWidget->currentIndex() == 2)
		{
			message += "\nSee the output for a detailed counter example.";
			if (showMsgBox)
			{
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESPOT", message);
			}
		}
		else
		{
			message += "\nWould you like to see a detailed counter example?";
			if (showMsgBox)
			{
				if (QMessageBox::information(m_outputWidget->topLevelWidget(), "DESPOT", message, QMessageBox::Yes|QMessageBox::No) == QMessageBox::Yes)
				{
					m_tabWidget->setCurrentIndex(2);
				}
			}
		}
	}

	//save the output in the output selection widget
	saveOutput();
}

void OutputUiPart::show(CtrlStdAlgo& ctrlAlgo, LastOutputOption copyToLastOutput ,
						bool showMsgBox )
{
	show(ctrlAlgo, showMsgBox);

	saveLastOutput(copyToLastOutput);
}



*/
//_________________________________________________________________________________________________

void OutputUiPart::show(MultiCtrlAlgo& ctrlAlgo, bool showMsgBox /*= true*/)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cCtrlOutputTitle));
	m_outputWidget->clear();

	if (ctrlAlgo.isControllable())
	{
		QString message("<b>System is controllable. Verified on %1</b>");
		message = message.arg(QString::fromStdWString(m_project->getCtrlStamp()));
		m_outputWidget->writeLine(message);
		if(!(m_project->getProjectChkFlag()))
		m_project->setDebugMode(DesProject::Reset);
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","The system is controllable");
		}
	}
	else
	{
		m_outputWidget->writeLine("<b>System is not controllable</b>");
		QString messageTempl = "The system is uncontrollable at state:&nbsp;&nbsp;(%1)<br>for event:&nbsp;&nbsp;'%2'.<br><br> State '%3' of DES '%4' is blocking the event.";

		// Creates list of DEs for project so can be matched
		// to state names
		MeetAlgo::DesSet&  inDesSet = ctrlAlgo.getInDesSet();

		//Create the closed state name
        QString closedStateName;
		for(unsigned int iSrcState = 0; iSrcState < ctrlAlgo.getUnctrlBehaviour().closedState.size(); iSrcState++)
		{

       		       // get DES that matches state
		       const Des*  blockingDes = inDesSet[iSrcState];

			if (iSrcState > 0)
			{
				closedStateName += ", ";
			}

			// prepend state by DES name so we can
			// distinguish which DES the state name
			// belongs to 
			closedStateName += QString::fromStdWString(blockingDes->getName()) + "/";

			closedStateName += QString::fromStdWString(ctrlAlgo.getUnctrlBehaviour().closedState[iSrcState]->getName());
		}





		QString blockEventName = QString::fromStdWString(ctrlAlgo.getUnctrlBehaviour().exitEvent->getName());
		QString blockingStateName = QString::fromStdWString(ctrlAlgo.getUnctrlBehaviour().blockingState->getName());
		QString blockingDesName = QString::fromStdWString(ctrlAlgo.getUnctrlBehaviour().blockingDes->getName());

		QString message = messageTempl.arg(closedStateName, blockEventName, blockingStateName, blockingDesName);
		m_outputWidget->writeLine(message);
		m_outputWidget->writeLine("");

		
		/**Counter example generation  **/
	   m_tabWidget->setCurrentIndex(2);
	 if(ctrlAlgo.getErrorAlgoFlag() && !(m_project->getProjectChkFlag()) && !(ctrlAlgo.CE_tuplemap.empty())) 
	{
		
		DesProject::DesIteratorPtr desptr=m_project->createDesIterator();
		CounterExampleAlgo::CEStateTuple FinalState(ctrlAlgo.getUnctrlBehaviour().closedState.size());				
		for(unsigned int i = 0; i < ctrlAlgo.getUnctrlBehaviour().closedState.size(); i++)
		{
			const unsigned long long itmp=ctrlAlgo.getUnctrlBehaviour().closedState[i]->getId().id();			
            unsigned long long tmp=itmp;
			FinalState[i]=(short)tmp;		
		} 

	    int DebugResponse=this->GetDebugResponse("System is Uncontrollable.");

		if(DebugResponse==QMessageBox::Yes)
		{	
			m_project->setDummyProject(m_project);
			CounterExampleAlgo_FlatCntr CEAlgo(ctrlAlgo.CE_tuplemap,m_project,m_project->createProjEventIterator());
			bool result=CEAlgo.runAlgo();
			if(result)
			{
				m_project->setCounterExample(CEAlgo.GetCounterExample());				
				m_project->setDebugMode(DesProject::CounterExample);
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
			}
			else	  
			{					
			m_project->setDebugMode(DesProject::ErrorTuple);
			m_tabWidget->setCurrentIndex(2);
			DESpot::DummyProject temp(m_project,ctrlAlgo.CE_tuplemap);
			m_project->setSimulationErrorTuple(temp.getSimulationErrorTuple());			
			}
			
				
	   }
	   	else	  
		{					
			m_project->setDebugMode(DesProject::ErrorTuple);
			m_tabWidget->setCurrentIndex(2);
			m_project->setDummyProject(m_project);
			DESpot::DummyProject temp(m_project,ctrlAlgo.CE_tuplemap);
			m_project->setSimulationErrorTuple(temp.getSimulationErrorTuple());			
	    }

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

	}

	//save the output in the output selection widget

	saveOutput();
}

//_________________________________________________________________________________________________

void OutputUiPart::show(MultiCtrlAlgo& ctrlAlgo, LastOutputOption copyToLastOutput /*= OutputUiPart::eSetLastOutput*/,
						bool showMsgBox /*= true*/)
{
	show(ctrlAlgo, showMsgBox);

	saveLastOutput(copyToLastOutput);
}
//_________________________________________________________________________________________________

void OutputUiPart::showMeasurements(const Des* flatSystem)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cMeasureOutputTitle));
	m_outputWidget->clear();

	m_outputWidget->writeLine("<b>Flat System Size:</b>");
	m_outputWidget->write(QString("&nbsp;&nbsp;&nbsp;%1 state(s)").arg(flatSystem->getStateCount()));
	m_outputWidget->writeLine(QString(" with %2 marked").arg(flatSystem->getMarkedStateCount()));
	m_outputWidget->writeLine(QString("&nbsp;&nbsp;&nbsp;%1 event(s)").arg(flatSystem->getEventCount()));
	m_outputWidget->writeLine(QString("&nbsp;&nbsp;&nbsp;%1 transitions(s)").arg(flatSystem->getTransCount()));

	saveOutput();
}

//_________________________________________________________________________________________________

void OutputUiPart::show(LdInterfaceCheckAlgo& ldInterfCheckAlgo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cLdInterfCheckTitle));

	m_outputWidget->clear();

	if (ldInterfCheckAlgo.isLdInterface())
	{
		if (showMsgBox)
		{
			QString message("'%1' is an LD-interface");
			message = message.arg(QString::fromStdWString(ldInterfCheckAlgo.getInputInterface()->getName()));
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot",message);
		}

		QString out("<b>Interface '%1' is an LD-interface. Verified on %2.</b>");
		out = out.arg(QString::fromStdWString(ldInterfCheckAlgo.getInputInterface()->getName()),
							  QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);

	}
	else
	{
		if (showMsgBox)
		{
			QString message("'%1' is not an LD-interface.");
			message = message.arg(QString::fromStdWString(ldInterfCheckAlgo.getInputInterface()->getName()));
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot",message);
		}

		QString out("<b>Interface '%1' is not LD-interface.</b> <br><br><I>Error:</I> &nbsp;&nbsp;%2.");
		out = out.arg(QString::fromStdWString(ldInterfCheckAlgo.getInputInterface()->getName()),
					  QString::fromStdWString(ldInterfCheckAlgo.getCounterExample().errMessage));
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine("");

	}

	saveOutput();
}

//_________________________________________________________________________________________________

void OutputUiPart::show(LdInterfaceCheckAlgo& ldInterfCheckAlgo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/,
						bool showMsgBox /*= true*/)
{
	show(ldInterfCheckAlgo, showMsgBox);

	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________

void OutputUiPart::show(IConsistAnsAcceptAlgo& ansAcceptAlgo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysInterfConsistOutputTitle));

	m_outputWidget->clear();

	if (ansAcceptAlgo.allAnsEventsAccepted())
	{
		if (showMsgBox)
		{
			QString msg("The high-level subsystem '%1' is interface consistent");
			msg = msg.arg(QString::fromStdWString(hierProject()->getRootSubsys().getName()));
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot",msg);
		}
		if(!(m_project->getProjectChkFlag()))
		m_project->setDebugMode(DesProject::Reset);
		QString out("<b>The high-level subsystem '%1' is interface consistent. Verified on %2.</b>");
		out = out.arg(QString::fromStdWString(hierProject()->getRootSubsys().getName()),
							  QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine("<b>" + out + "</b>");

	}
	
	else
	{
		QString out("The high-level subsystem '%1' fails to accept all answer events.");
		out = out.arg(QString::fromStdWString(hierProject()->getRootSubsys().getName()));

		/*if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot",out);
		}*/
		m_outputWidget->writeLine("<b>" + out + "</b>");
		m_outputWidget->writeLine("");

		QString errOut("<I>Error:</I> %1");
		errOut = out.arg(QString::fromStdWString(ansAcceptAlgo.getError()));
		m_outputWidget->writeLine(errOut);
		m_outputWidget->writeLine("");

		/** Counter Example **/
m_tabWidget->setCurrentIndex(2);
if(ansAcceptAlgo.getIFailureType()==DesAlgo::AnsAcptAlgo && !( ansAcceptAlgo.CE_tuplemap.empty()))
{
		int DebugResponse=this->GetDebugResponse("The high-level subsystem fails to accept all answer events.");
		if(DebugResponse==QMessageBox::Yes)
		{
			DESpot::DummyProject m_dummyproj(ansAcceptAlgo.getErrorSubsystem(),(DesHierProject*)m_project,ansAcceptAlgo.CE_tuplemap);			
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			CounterExampleAlgo_IAnsAcpt CEAlgo(ansAcceptAlgo.CE_tuplemap, (DesHierProject*)m_project,m_project->getDummyProject()->createProjEventIterator());	
			bool result=CEAlgo.runAlgo();
			if(result)
			{
				m_project->setDebugMode(DesProject::CounterExample);				
				m_project->setCounterExample( CEAlgo.GetCounterExample());
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
			}
			else	  
			{					
				m_project->setDebugMode(DesProject::ErrorTuple);				
				m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}
		}
		else	  
			{	
				m_project->setDebugMode(DesProject::ErrorTuple);
				DESpot::DummyProject m_dummyproj(ansAcceptAlgo.getErrorSubsystem(),(DesHierProject*)m_project,ansAcceptAlgo.CE_tuplemap);				
				m_project->setDummyProject(m_dummyproj.GetDummyProject());
				m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}
}
	  /**************************/

	}

	saveOutput();
}

//_________________________________________________________________________________________________

void OutputUiPart::show(IConsistAnsAcceptAlgo& ansAcceptAlgo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/,
						bool showMsgBox /*= true*/)
{
	show(ansAcceptAlgo, showMsgBox);

	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________

void OutputUiPart::show(LowSubsysIConsistAlgo& lowSubsysIConsAlgo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysInterfConsistOutputTitle));

	m_outputWidget->clear();

	if (lowSubsysIConsAlgo.isSubsysInterfConsist())
	{
		if (showMsgBox)
		{
			QString msg("The low-level subsystem '%1' is LD interface consistent");
			msg = msg.arg(QString::fromStdWString(lowSubsysIConsAlgo.getInputSubsystem().getName()));
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot",msg);
		}
		
		if(!(m_project->getProjectChkFlag()))
		m_project->setDebugMode(DesProject::Reset);
		QString out("<b>The low-level subsystem '%1' is LD interface consistent. Verified on %2.</b>");
		out = out.arg(QString::fromStdWString(lowSubsysIConsAlgo.getInputSubsystem().getName()),
							  QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);

	}
	else
	{
		QString out("The low-level subsystem '%1' is not LD interface consistent - %2 error(s).");
		out = out.arg(QString::fromStdWString(lowSubsysIConsAlgo.getInputSubsystem().getName()),
					  QString("%1").arg(lowSubsysIConsAlgo.getErrorCount()));

		/*if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot",out);
		}
		*/
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
        showErrors(lowSubsysIConsAlgo.getErrorList());
		m_outputWidget->writeLine("");

		/** Counter Example **/				 
m_tabWidget->setCurrentIndex(2);
if((lowSubsysIConsAlgo.getIFailureType()==DesAlgo::ReqAcptAlgo || lowSubsysIConsAlgo.getIFailureType()==DesAlgo::IntrfImplAlgo)
	&& !(lowSubsysIConsAlgo.CE_tuplemap.empty()))
{
			
		int DebugResponse=this->GetDebugResponse("The low-level subsystem is not LD interface consistent.");
		if(DebugResponse==QMessageBox::Yes)
	{
			if(lowSubsysIConsAlgo.getIFailureType()==DesAlgo::ReqAcptAlgo ) 
			{
			DESpot::DummyProject m_dummyproj(lowSubsysIConsAlgo.getErrorSubsystem(),lowSubsysIConsAlgo.CE_tuplemap,lowSubsysIConsAlgo.get_proj());
			m_project->setDummyProject( m_dummyproj.GetDummyProject());
			CounterExampleAlgo_IReqAcpt CEAlgo(lowSubsysIConsAlgo.CE_tuplemap,
											 *(lowSubsysIConsAlgo.getErrorSubsystem()), 
											   m_project->getDummyProject()->createProjEventIterator());
			bool result=CEAlgo.runAlgo();
				if(result)
				{
					m_project->setDebugMode(DesProject::CounterExample);
					m_project->setCounterExample( CEAlgo.GetCounterExample());
					QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
				}
				else
				{
					m_project->setDebugMode(DesProject::ErrorTuple);				
					m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
			}

			if(lowSubsysIConsAlgo.getIFailureType()==DesAlgo::IntrfImplAlgo ) 
			{
			DESpot::DummyProject m_dummyproj(lowSubsysIConsAlgo.getErrorSubsystem(),lowSubsysIConsAlgo.CE_tuplemap,lowSubsysIConsAlgo.get_proj());
			m_project->setDummyProject( m_dummyproj.GetDummyProject());			
			CounterExampleAlgo_IntfImpAlgo CEAlgo((DesHierProject*)m_project,
												  lowSubsysIConsAlgo.getErrorSubsystem(),
												  m_project->getDummyProject()->createProjEventIterator(),
												  lowSubsysIConsAlgo.CE_tuplemap
												  );
			bool result=CEAlgo.runAlgo();
			if(result)
			{
				m_project->setDebugMode(DesProject::CounterExample);
				m_project->setCounterExample( CEAlgo.GetCounterExample());
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
			}
			else
			{
				m_project->setDebugMode(DesProject::ErrorTuple);				
				m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}
			}
		}
			else	  
			{					
				m_tabWidget->setCurrentIndex(2);
				m_project->setDebugMode(DesProject::ErrorTuple);
				DESpot::DummyProject m_dummyproj(lowSubsysIConsAlgo.getErrorSubsystem(),lowSubsysIConsAlgo.CE_tuplemap,lowSubsysIConsAlgo.get_proj());			
				m_project->setDummyProject(m_dummyproj.GetDummyProject());
				m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}

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

	}

	saveOutput();
}

void OutputUiPart::show(std::wstring subsysName, bool showMsgBox)
{

			m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysInterfConsistOutputTitle));

			m_outputWidget->clear();


			if (showMsgBox)
			{
				QString msg("The high-level/low-level subsystem '%1' is LD interface consistent");
				msg = msg.arg(QString::fromStdWString(subsysName));
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot",msg);
			}

			QString out("<b>The high-level/low-level subsystem '%1' is LD interface consistent. Verified on %2.</b>");
			out = out.arg(QString::fromStdWString(subsysName),
				QDateTime::currentDateTime().toString());
			m_outputWidget->writeLine(out);
		
	
	saveOutput();
}

//_________________________________________________________________________________________________

void OutputUiPart::show(LowSubsysIConsistAlgo& lowSubsysIConsAlgo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/,
						bool showMsgBox /*= true*/)
{
	show(lowSubsysIConsAlgo, showMsgBox);

	saveLastOutput(copyToLastOutput);
}
//_________________________________________________________________________________________________

void OutputUiPart::show(std::wstring subsysName, LastOutputOption copyToLastOutput /*= eSetLastOutput*/,
						bool showMsgBox /*= true*/)
{
	show(subsysName, showMsgBox);

	saveLastOutput(copyToLastOutput);
}
//_________________________________________________________________________________________________

void OutputUiPart::show(IConsistAlgo& iConsAlgo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cInterfConsistOutputTitle));

	m_outputWidget->clear();

	if (iConsAlgo.isInterfaceConsistent())
	{
		if (showMsgBox)
		{
			QString message("Project is LD interface consistent");
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", message);
		}
		if(!(m_project->getProjectChkFlag()))
		m_project->setDebugMode(DesProject::Reset);
		QString out("<b>Project is LD interface consistent. Verified on %1.</b>");
		out = out.arg(QString::fromStdWString(hierProject()->getIConsistStamp()));
		m_outputWidget->writeLine(out);
	}
	else
	{

		QString out("<b>Project is not LD interface consistent - %1 error(s)</b>");
		out = out.arg(iConsAlgo.getErrorCount());

		m_outputWidget->writeLine("<b> " + out + "</b>");

		//output all errors
		showErrors(iConsAlgo.getErrorList());

		m_outputWidget->writeLine("");

		
		/** Counter Example **/
m_tabWidget->setCurrentIndex(2);
if(!(m_project->getProjectChkFlag()) && !(iConsAlgo.CE_tuplemap.empty()))
{
	m_tabWidget->setCurrentIndex(2);
	if(iConsAlgo.getIFailureType()==DesAlgo::ReqAcptAlgo || iConsAlgo.getIFailureType()==DesAlgo::IntrfImplAlgo ||iConsAlgo.getIFailureType()==DesAlgo::AnsAcptAlgo )
	{
		int DebugResponse=this->GetDebugResponse("Project is not LD interface consistent.");

		if(iConsAlgo.getIFailureType()==DesAlgo::AnsAcptAlgo)
		{			
			if(DebugResponse==QMessageBox::Yes)
			{
			DESpot::DummyProject m_dummyproj(iConsAlgo.getErrorSubsystem(),(DesHierProject*)m_project,iConsAlgo.CE_tuplemap);
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			CounterExampleAlgo_IAnsAcpt CEAlgo(iConsAlgo.CE_tuplemap, (DesHierProject*)m_project,m_project->getDummyProject()->createProjEventIterator());	
			bool result=CEAlgo.runAlgo();
				if(result)
				{
					m_project->setDebugMode(DesProject::CounterExample);
					m_project->setCounterExample(CEAlgo.GetCounterExample());
					QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
				}
				else
				{
					m_project->setDebugMode(DesProject::ErrorTuple);							
					m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
			}
			else	  
			{	
				DESpot::DummyProject m_dummyproj(iConsAlgo.getErrorSubsystem(),(DesHierProject*)m_project,iConsAlgo.CE_tuplemap);				
				m_tabWidget->setCurrentIndex(2);
				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(iConsAlgo.getErrorSubsystem(),iConsAlgo.CE_tuplemap,iConsAlgo.getProject());
			m_project->setDummyProject( m_dummyproj.GetDummyProject());

			if(iConsAlgo.getIFailureType()==DesAlgo::ReqAcptAlgo) 
			{		
			CounterExampleAlgo_IReqAcpt CEAlgo(iConsAlgo.CE_tuplemap,*(iConsAlgo.getErrorSubsystem()), m_project->getDummyProject()->createProjEventIterator());
			bool result=CEAlgo.runAlgo();
				if(result)
				{
					m_project->setDebugMode(DesProject::CounterExample);
					m_project->setCounterExample( CEAlgo.GetCounterExample());	
					QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
				}	
				else
				{
					m_project->setDebugMode(DesProject::ErrorTuple);
					m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
			}		

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

	
}
	saveOutput();
}


//_________________________________________________________________________________________________

void OutputUiPart::show(IConsistAlgo& iConsAlgo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/,
						bool showMsgBox /*= true*/)
{
	show(iConsAlgo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________

void OutputUiPart::show(LwNonBlockingAlgo& lwNonBlockAlgo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cLwNonBlockOutputTitle));

	m_outputWidget->clear();

	if (lwNonBlockAlgo.isLwNonBlocking())
	{
		if (showMsgBox)
		{
			QString message("Project is LD level-wise nonblocking.");
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", message);
		}
		if(!(m_project->getProjectChkFlag()))
		m_project->setDebugMode(DesProject::Reset);
		QString out("<b>Project is LD level-wise nonblocking. Verified on %1.</b>");
		out = out.arg(QString::fromStdWString(hierProject()->getLwNonBlockStamp()));
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine("");
	}
	else
	{
		QString out("Project is not LD level-wise nonblocking - %1 error(s)");
		out = out.arg(lwNonBlockAlgo.getErrorCount());
		
		m_outputWidget->writeLine("<b>" + out + "</b>");

		/** Counter example **/
m_tabWidget->setCurrentIndex(2);
if(!(m_project->getProjectChkFlag()) && !(lwNonBlockAlgo.CE_tuplemap.empty()))
{
		int DebugResponse=this->GetDebugResponse("Project is not LD level-wise nonblocking.");
		if(lwNonBlockAlgo.getErrorSubsystem()->getLevel()==0 )
		{	
			// for high level subsystem
			if(DebugResponse==QMessageBox::Yes)
			{		
			DESpot::DummyProject m_dummyproj(lwNonBlockAlgo.getErrorSubsystem(),&lwNonBlockAlgo.getProject(),lwNonBlockAlgo.CE_tuplemap);
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			m_project->setDummyProject( m_dummyproj.GetDummyProject());
			CounterExampleAlgo_LwNB counterexpalgo(&lwNonBlockAlgo.getProject(),
											  lwNonBlockAlgo.getErrorSubsystem(),
											  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(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
				}
				else
				{
					m_project->setDebugMode(DesProject::ErrorTuple);
				}
			}
			else
			{	
				DESpot::DummyProject m_dummyproj(lwNonBlockAlgo.getErrorSubsystem(),&lwNonBlockAlgo.getProject(),lwNonBlockAlgo.CE_tuplemap);	
				m_tabWidget->setCurrentIndex(2);
				m_project->setDebugMode(DesProject::ErrorTuple);
				m_project->setDummyProject(m_dummyproj.GetDummyProject());
				m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}	
		}
		else
		{  
			//for low level subsystem
				if(DebugResponse==QMessageBox::Yes)
				{
				DESpot::DummyProject m_dummyproj(lwNonBlockAlgo.getErrorSubsystem(),lwNonBlockAlgo.CE_tuplemap,&lwNonBlockAlgo.getProject());
				m_project->setDummyProject( m_dummyproj.GetDummyProject());
				CounterExampleAlgo_LwNB counterexpalgo(lwNonBlockAlgo.getErrorSubsystem(),
											  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(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
					}
					else
					{
						m_project->setDebugMode(DesProject::ErrorTuple);
						m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
					}
				}
				else
				{	
				DESpot::DummyProject m_dummyproj(lwNonBlockAlgo.getErrorSubsystem(),lwNonBlockAlgo.CE_tuplemap,&lwNonBlockAlgo.getProject());	
				m_tabWidget->setCurrentIndex(2);
				m_project->setDebugMode(DesProject::ErrorTuple);				
				m_project->setDummyProject(m_dummyproj.GetDummyProject());
				m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
			}
}		
	
		/*************************************************/

		//output all errors
		showErrors(lwNonBlockAlgo.getErrorList());
		
		// remove next two  lines
		//		m_outputWidget->writeLine("Verification of low-level<br>line 2<br> line 3");
		//		m_outputWidget->writeLine("line 4.");
	}

	saveOutput();
}


//_________________________________________________________________________________________________

void OutputUiPart::show(LwNonBlockingAlgo& lwNonBlockAlgo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/,
						bool showMsgBox /*= true*/)
{
	show(lwNonBlockAlgo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________

void OutputUiPart::show(AlgoType algoType,bool showMsgBox)
{
	switch(algoType)
	{
	case eLwNonBlock:
		{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cLwNonBlockOutputTitle));

	m_outputWidget->clear();

	if (showMsgBox)
		{
			QString message("Project is LD level-wise nonblocking.");
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", message);
		}

		QString out("<b>Project is LD level-wise nonblocking. Verified on %1.</b>");
		out = out.arg(QString::fromStdWString(hierProject()->getLwNonBlockStamp()));
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine("");
		}
		break;
	case eLwIConst:
		{
		m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cInterfConsistOutputTitle));

	m_outputWidget->clear();

	if (showMsgBox)
		{
			QString message("Project is LD interface consistent");
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", message);
		}

		QString out("<b>Project is LD interface consistent. Verified on %1.</b>");
		out = out.arg(QString::fromStdWString(hierProject()->getIConsistStamp()));
		m_outputWidget->writeLine(out);
	}
	break;
	case eLwCtrl:
		{
			m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cLwCtrlOutputTitle));

	m_outputWidget->clear();

	if (showMsgBox)
		{
			QString message("Project is LD level-wise controllable.");
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", message);
		}

		QString out("<b>Project is LD level-wise controllable. Verified on %1.<b>");
		out = out.arg(QString::fromStdWString(hierProject()->getLwCtrlStamp()));
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine("");
	}
		break;
	}



	saveOutput();
}

//_________________________________________________________________________________________________

void OutputUiPart::show(AlgoType algoType,LastOutputOption copyToLastOutput /*= eSetLastOutput*/,
						bool showMsgBox /*= true*/)
{
	show(algoType,showMsgBox);
	saveLastOutput(copyToLastOutput);
}
//_________________________________________________________________________________________________

void OutputUiPart::show(LwCtrlAlgo& lwCtrlAlgo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cLwCtrlOutputTitle));

	m_outputWidget->clear();

	if (lwCtrlAlgo.isLwControllable())
	{
		if (showMsgBox)
		{
			QString message("Project is LD level-wise controllable.");
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", message);
		}
		if(!(m_project->getProjectChkFlag()))
		m_project->setDebugMode(DesProject::Reset);
		QString out("<b>Project is LD level-wise controllable. Verified on %1.<b>");
		out = out.arg(QString::fromStdWString(hierProject()->getLwCtrlStamp()));
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine("");
	}
	else
	{
		QString out("Project is not LD level-wise controllable - %1 error(s)");
		out = out.arg(lwCtrlAlgo.getErrorCount());
		/*if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", out);
		}*/
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		showErrors(lwCtrlAlgo.getErrorList());

		/** Counter example **/
m_tabWidget->setCurrentIndex(2);
if(!(m_project->getProjectChkFlag())&& !(lwCtrlAlgo.CE_tuplemap.empty()))
{
		if(lwCtrlAlgo.getErrorSubsystem()->getLevel()==0)
		{	
			int
			DebugResponse=this->GetDebugResponse("System is not controllable.");
			if(DebugResponse==QMessageBox::Yes)
			{
			DESpot::DummyProject m_dummyproj(lwCtrlAlgo.getErrorSubsystem(),&lwCtrlAlgo.getProject(),lwCtrlAlgo.CE_tuplemap);
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			CounterExampleAlgo_LwCntr counterexalgo(&lwCtrlAlgo.getProject(),
												     lwCtrlAlgo.getErrorSubsystem(),
													 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(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
				}
				else
				{
					m_project->setDebugMode(DesProject::ErrorTuple);	
					m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}

			}
			else
			{	
			DESpot::DummyProject m_dummyproj(lwCtrlAlgo.getErrorSubsystem(),&lwCtrlAlgo.getProject(),lwCtrlAlgo.CE_tuplemap);	
			m_tabWidget->setCurrentIndex(2);
			m_project->setDebugMode(DesProject::ErrorTuple);	
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}
		}
		else
		{
			int DebugResponse=this->GetDebugResponse("System is not controllable.");
			if(DebugResponse==QMessageBox::Yes)
			{
			DESpot::DummyProject m_dummyproj(lwCtrlAlgo.getErrorSubsystem(),lwCtrlAlgo.CE_tuplemap,&lwCtrlAlgo.getProject());
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			CounterExampleAlgo_LwCntr counterexalgo(lwCtrlAlgo.getErrorSubsystem(),
													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(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
				}
				else
				{
					m_project->setDebugMode(DesProject::ErrorTuple);	
					m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
			}
			else
			{	
			DESpot::DummyProject m_dummyproj(lwCtrlAlgo.getErrorSubsystem(),lwCtrlAlgo.CE_tuplemap,&lwCtrlAlgo.getProject());	
			m_tabWidget->setCurrentIndex(2);
			m_project->setDebugMode(DesProject::ErrorTuple);	
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}
		}

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

		m_outputWidget->writeLine("");
	}

	saveOutput();
}


//_________________________________________________________________________________________________

void OutputUiPart::show(LwCtrlAlgo& lwCtrlAlgo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/,
						bool showMsgBox /*= true*/)
{
	show(lwCtrlAlgo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________

void OutputUiPart::show(HighSubsysNonBlockAlgo& hSubsysNonBlockAlgo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysNonBlockingOutputTitle));

	m_outputWidget->clear();

	if (hSubsysNonBlockAlgo.isNonBlocking())
	{
		/*if (showMsgBox)
		{
			QString msg("The high-level subsystem is nonblocking.");
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot",msg);
		}
		if(!(m_project->getProjectChkFlag()))
		m_project->setDebugMode(DesProject::Reset);
		QString out("<b>The high-level subsystem is nonblocking. Verified on %1.</b>");
		out = out.arg(QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);*/

		if (showMsgBox)
		{
			QString msg("The high-level subsystem '%1' is nonblocking");
			msg = msg.arg(QString::fromStdWString(hSubsysNonBlockAlgo.getInputProject().getRootSubsys().getName()));
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot",msg);
		}

		QString out("<b>The high-level subsystem '%1' is nonblocking. Verified on %2.</b>");
		out = out.arg(QString::fromStdWString(hSubsysNonBlockAlgo.getInputProject().getRootSubsys().getName()),
							  QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);

	}
	else
	{
		QString out("The high-level subsystem '%1' is blocking - %2 error(s).");

		const DesAlgo::ErrorList& errList = hSubsysNonBlockAlgo.getErrorList();
		// for some reason, getErrorCount() returns wrong value
		//		only for the subsystem nonblocking algs

		out = out.arg(QString::fromStdWString(hSubsysNonBlockAlgo.getInputProject().getRootSubsys().getName()),
			      QString("%1").arg(errList.size()));
	
		//		out = out.arg(hSubsysNonBlockAlgo.getErrorCount());
		/*if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot",out);
		}*/
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		showErrors(errList);
		//		showErrors(hSubsysNonBlockAlgo.getErrorList());

		m_outputWidget->writeLine("");

		/** Counter example **/	
m_tabWidget->setCurrentIndex(2);
if(!(hSubsysNonBlockAlgo.CE_tuplemap.empty()))
{
	int DebugResponse=this->GetDebugResponse("The high-level subsystem is blocking.");
	if(DebugResponse==QMessageBox::Yes)
	{
		DESpot::DummyProject m_dummyproj(hSubsysNonBlockAlgo.getErrorSubsystem(),&(hSubsysNonBlockAlgo.getInputProject()),hSubsysNonBlockAlgo.CE_tuplemap);
		m_project->setDummyProject( m_dummyproj.GetDummyProject());
		CounterExampleAlgo_LwNB m_cntrexpalgo(&(hSubsysNonBlockAlgo.getInputProject()),
											  hSubsysNonBlockAlgo.getErrorSubsystem(),
											  hSubsysNonBlockAlgo.CE_tuplemap,
											  m_project->getDummyProject()->createProjEventIterator());
		bool result=m_cntrexpalgo.runAlgo();
			if(result)
			{
				m_project->setDebugMode(DesProject::CounterExample);
				m_project->setCounterExample( m_cntrexpalgo.GetCounterExample());
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
			}
			else
			{
				m_project->setDebugMode(DesProject::ErrorTuple);	
				m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			}
	}
	else
	{	
		DESpot::DummyProject m_dummyproj(hSubsysNonBlockAlgo.getErrorSubsystem(),&(hSubsysNonBlockAlgo.getInputProject()),hSubsysNonBlockAlgo.CE_tuplemap);
		m_tabWidget->setCurrentIndex(2);
		m_project->setDebugMode(DesProject::ErrorTuple);	
		m_project->setDummyProject(m_dummyproj.GetDummyProject());
		m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
	}
}
	  /***************************************************/

}

	saveOutput();
}


//_________________________________________________________________________________________________

void OutputUiPart::show(HighSubsysNonBlockAlgo& hSubsysNonBlockAlgo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/,
						bool showMsgBox /*= true*/)
{
	show(hSubsysNonBlockAlgo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________

void OutputUiPart::show(LowSubsysNonBlockAlgo& lowSubsysNonBlockAlgo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysNonBlockingOutputTitle));

	m_outputWidget->clear();

	if (lowSubsysNonBlockAlgo.isNonBlocking())
	{
		if (showMsgBox)
		{
			QString msg("The low-level subsystem '%1' is nonblocking");
			msg = msg.arg(QString::fromStdWString(lowSubsysNonBlockAlgo.getInputSubsystem().getName()));
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot",msg);
		}
		if(!(m_project->getProjectChkFlag()))
		m_project->setDebugMode(DesProject::Reset);
		QString out("<b>The low-level subsystem '%1' is nonblocking. Verified on %2.</b>");
		out = out.arg(QString::fromStdWString(lowSubsysNonBlockAlgo.getInputSubsystem().getName()),
							  QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);

	}
	else
	{
		QString out("The low-level subsystem '%1' is blocking - %2 error(s).");

		const DesAlgo::ErrorList& errList = lowSubsysNonBlockAlgo.getErrorList();
		// for some reason, getErrorCount() returns wrong value
		// only for the subsystem nonblocking algs

		out = out.arg(QString::fromStdWString(lowSubsysNonBlockAlgo.getInputSubsystem().getName()),
			      QString("%1").arg(errList.size()));

		/*		out = out.arg(QString::fromStdWString(lowSubsysNonBlockAlgo.getInputSubsystem().getName()),
				QString("%1").arg(lowSubsysNonBlockAlgo.getErrorCount()));  */
		
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		showErrors(errList);
		//		showErrors(lowSubsysNonBlockAlgo.getErrorList());

		m_outputWidget->writeLine("");


		/** Counter example **/
		m_tabWidget->setCurrentIndex(2);

if( !(lowSubsysNonBlockAlgo.CE_tuplemap.empty()))
{
		int DebugResponse=this->GetDebugResponse("The low-level subsystem is blocking");
		if(DebugResponse==QMessageBox::Yes)
		{
			DESpot::DummyProject m_dummyproj(lowSubsysNonBlockAlgo.getErrorSubsystem(),lowSubsysNonBlockAlgo.CE_tuplemap,lowSubsysNonBlockAlgo.get_proj());
			m_project->setDummyProject( m_dummyproj.GetDummyProject());
			CounterExampleAlgo_LwNB counterexpalgo(lowSubsysNonBlockAlgo.getErrorSubsystem(),
											  lowSubsysNonBlockAlgo.CE_tuplemap,
											  m_project->getDummyProject()->createProjEventIterator());
			bool result=counterexpalgo.runAlgo();
				if(result)
				{
					m_project->setDebugMode(DesProject::CounterExample);
					m_project->setCounterExample( counterexpalgo.GetCounterExample());
					QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
				}
				else
				{
					m_project->setDebugMode(DesProject::ErrorTuple);	
					m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
		}
		else
		{	
			DESpot::DummyProject m_dummyproj(lowSubsysNonBlockAlgo.getErrorSubsystem(),lowSubsysNonBlockAlgo.CE_tuplemap,lowSubsysNonBlockAlgo.get_proj());	
			m_tabWidget->setCurrentIndex(2);
			m_project->setDebugMode(DesProject::ErrorTuple);	
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
		}
}	
	  /********************************/

	}

	saveOutput();
}


//_________________________________________________________________________________________________

void OutputUiPart::show(LowSubsysNonBlockAlgo& lowSubsysNonBlockAlgo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/,
						bool showMsgBox /*= true*/)
{
	show(lowSubsysNonBlockAlgo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________

void OutputUiPart::show(HighSubsysCtrlAlgo& hSubsysCtrlAlgo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysCtrlOutputTitle));

	m_outputWidget->clear();

	if (hSubsysCtrlAlgo.isControllable())
	{
		if (showMsgBox)
		{
			QString msg("The high-level subsystem '%1' is controllable");
			msg = msg.arg(QString::fromStdWString(hierProject()->getRootSubsys().getName()));
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot",msg);
		}
		if(!(m_project->getProjectChkFlag()))
		m_project->setDebugMode(DesProject::Reset);
		QString out("<b>The high-level subsystem '%1' is controllable. Verified on %2.</b>");
		out = out.arg(QString::fromStdWString(hierProject()->getRootSubsys().getName()),
							  QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);

	}
	else
	{
		QString out("The high-level subsystem '%1' is not controllable - %2 error(s).");
		out = out.arg(QString::fromStdWString(hierProject()->getRootSubsys().getName()),
					  QString("%1").arg(hSubsysCtrlAlgo.getErrorCount()));
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		showErrors(hSubsysCtrlAlgo.getErrorList());

		m_outputWidget->writeLine("");

		/** Counter Example **/
m_tabWidget->setCurrentIndex(2);

if(!(hSubsysCtrlAlgo.CE_tuplemap.empty()))
{
		
			int DebugResponse=this->GetDebugResponse("The high-level subsystem is not controllable.");
			if(DebugResponse==QMessageBox::Yes)
			{	
			DESpot::DummyProject m_dummyproj(hSubsysCtrlAlgo.getErrorSubsystem(),&(hSubsysCtrlAlgo.getInputProject()),hSubsysCtrlAlgo.CE_tuplemap);
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			CounterExampleAlgo_LwCntr counterexalgo(&hSubsysCtrlAlgo.getInputProject(),
												     hSubsysCtrlAlgo.getErrorSubsystem(),
													 hSubsysCtrlAlgo.CE_tuplemap,
													 m_project->getDummyProject()->createProjEventIterator());
			bool result=counterexalgo.runAlgo();
				if(result)
				{
					m_project->setDebugMode(DesProject::CounterExample);
					m_project->setCounterExample(counterexalgo.GetCounterExample());
					QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
				}
				else
				{
					m_project->setDebugMode(DesProject::ErrorTuple);
					m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
			}
			else
			{
				DESpot::DummyProject m_dummyproj(hSubsysCtrlAlgo.getErrorSubsystem(),&(hSubsysCtrlAlgo.getInputProject()),hSubsysCtrlAlgo.CE_tuplemap);	
				m_tabWidget->setCurrentIndex(2);
				m_project->setDebugMode(DesProject::ErrorTuple);	
				m_project->setDummyProject(m_dummyproj.GetDummyProject());
				m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());

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

	saveOutput();
}


//_________________________________________________________________________________________________

void OutputUiPart::show(HighSubsysCtrlAlgo& hSubsysCtrlAlgo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/,
						bool showMsgBox /*= true*/)
{
	show(hSubsysCtrlAlgo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________

void OutputUiPart::show(LowSubsysCtrlAlgo& lowSubsysCtrlAlgo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysCtrlOutputTitle));

	m_outputWidget->clear();

	if (lowSubsysCtrlAlgo.isControllable())
	{
		if (showMsgBox)
		{
			QString msg("The low-level subsystem '%1' is controllable");
			msg = msg.arg(QString::fromStdWString(lowSubsysCtrlAlgo.getInputSubsystem().getName()));
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot",msg);
		}
		if(!(m_project->getProjectChkFlag()))
		m_project->setDebugMode(DesProject::Reset);
		QString out("<b>The low-level subsystem '%1' is controllable. Verified on %2.</b>");
		out = out.arg(QString::fromStdWString(lowSubsysCtrlAlgo.getInputSubsystem().getName()),
							  QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);

	}
	else
	{
		QString out("The low-level subsystem '%1' is not controllable - %2 error(s).");
		out = out.arg(QString::fromStdWString(lowSubsysCtrlAlgo.getInputSubsystem().getName()),
					  QString("%1").arg(lowSubsysCtrlAlgo.getErrorCount()));
		
		m_outputWidget->writeLine("<b>" + out + "</b>");
		//output all errors
		showErrors(lowSubsysCtrlAlgo.getErrorList());
		m_outputWidget->writeLine("");
		
		
m_tabWidget->setCurrentIndex(2);

if(!(lowSubsysCtrlAlgo.CE_tuplemap.empty()))
{
		int DebugResponse=this->GetDebugResponse("The low-level subsystem is not controllable");
		if(DebugResponse==QMessageBox::Yes)
		{	
			DESpot::DummyProject m_dummyproj(lowSubsysCtrlAlgo.getErrorSubsystem(),lowSubsysCtrlAlgo.CE_tuplemap,lowSubsysCtrlAlgo.get_proj());
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			CounterExampleAlgo_LwCntr counterexalgo(lowSubsysCtrlAlgo.getErrorSubsystem(),
													lowSubsysCtrlAlgo.CE_tuplemap,
													m_project->getDummyProject()->createProjEventIterator());
			bool result=counterexalgo.runAlgo();
				if(result)
				{
					m_project->setDebugMode(DesProject::CounterExample);	
					m_project->setCounterExample(counterexalgo.GetCounterExample());
					QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
				}
				else
				{
					m_project->setDebugMode(DesProject::ErrorTuple);	
					m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				}
		}
		else
		{
			DESpot::DummyProject m_dummyproj(lowSubsysCtrlAlgo.getErrorSubsystem(),lowSubsysCtrlAlgo.CE_tuplemap,lowSubsysCtrlAlgo.get_proj());
			m_tabWidget->setCurrentIndex(2);
			m_project->setDebugMode(DesProject::ErrorTuple);	
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
		}	

	}
}

	saveOutput();
}


//_________________________________________________________________________________________________

void OutputUiPart::show(LowSubsysCtrlAlgo& lowSubsysCtrlAlgo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/,
						bool showMsgBox /*= true*/)
{
	show(lowSubsysCtrlAlgo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________
void OutputUiPart::show(OutputSource source, std::wstring heading, std::wstring error, LastOutputOption copyToLastOutput, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(getOutputIndexForSource(source));

	m_outputWidget->clear();

	m_outputWidget->writeLine("<b>" + QString::fromStdWString(heading) + ":</b>");
	m_outputWidget->writeLine(QString::fromStdWString(error));

	if (showMsgBox)
	{
		QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", QString::fromStdWString(error));
	}

	//save the output in the output selection widget
	saveOutput();

	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________

#ifdef __ENABLE_BDD__

//_________________________________________________________________________________________________

void OutputUiPart::show(BDDSD::SD_NBChkInfo& checkInfo, bool showMsgBox)
{
  m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cNonBlockOutputTitle));

  m_outputWidget->clear();
  
  if (checkInfo.m_chkPassed)
    {
      if (showMsgBox)
	{
	  QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
	}
      m_project->setDebugMode(DesProject::Reset);
      QString out("<b>Project is nonblocking. Verified on %1.</b>");
      out = out.arg(QString::fromStdWString(m_project->getNonBlockingStamp()));
      m_outputWidget->writeLine(out);
      m_outputWidget->writeLine(checkInfo.m_succStr);
      m_outputWidget->writeLine("");
    }
  else
    {
      QString out("Project is blocking.");      
      m_outputWidget->writeLine("<b>" + out + "</b>");      
      m_outputWidget->writeLine("");
      m_outputWidget->writeLine(checkInfo.m_errStr);
      m_outputWidget->writeLine("");

	  
		m_tabWidget->setCurrentIndex(2);
		if( !(checkInfo.CE_tuplemap.empty()))
		{
		int DebugResponse=this->GetDebugResponse("Project is blocking.");
		DESpot::DummyProject_BDD m_dummyproj(m_project,checkInfo);
		m_project->setDummyProject(m_dummyproj.GetDummyProject());
		m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());

		if(DebugResponse==QMessageBox::Yes)
		{			
			CounterExampleAlgo_BDDFNB CEAlgo(m_project, m_project->createProjEventIterator(),checkInfo);
			bool result=CEAlgo.runAlgo();
			if(result)
			{
				m_project->setDebugMode(DesProject::CounterExample);
				m_project->setCounterExample(CEAlgo.GetCounterExample());
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
			}
			else
			{
				m_project->setDebugMode(DesProject::ErrorTuple);
			}
		}
		else
		{
			m_tabWidget->setCurrentIndex(2);
			m_project->setDebugMode(DesProject::ErrorTuple);
		}
		}

  }

  saveOutput();
}

void OutputUiPart::show(BDDSD::SD_NBChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________

void OutputUiPart::GenerateCounterExample(BDDSD::SD_ChkInfo& checkinfo,QString errormsg)
{ 
	m_tabWidget->setCurrentIndex(2);
if( !(checkinfo.CE_tuplemap.empty()))
{
	int DebugResponse=this->GetDebugResponse(errormsg);
		DESpot::DummyProject_BDD m_dummyproj(m_project,checkinfo);
		m_project->setDummyProject(m_dummyproj.GetDummyProject());
		m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
		if(DebugResponse==QMessageBox::Yes)
		{
			m_project->setDummyProject(m_project);
			CounterExampleAlgo_BDDTimedCheck CEAlgo(m_project, m_project->createProjEventIterator(),checkinfo);
			bool result=CEAlgo.runAlgo();
			if(result)
			{
				m_project->setDebugMode(DesProject::CounterExample);
				m_project->setCounterExample(CEAlgo.GetCounterExample());
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
			}
			else
			{				
				m_project->setDebugMode(DesProject::ErrorTuple);
			}
			
		}
		else
		{
			m_tabWidget->setCurrentIndex(2);
			m_project->setDebugMode(DesProject::ErrorTuple);
		}	
}
}

//=================================================================================================
void OutputUiPart::show(BDDSD::SD_CtrlChkInfo& checkInfo, bool showMsgBox)
{

  m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cCtrlOutputTitle));


  m_outputWidget->clear();

  if (checkInfo.m_chkPassed)
    {
      if (showMsgBox)
	{
	  QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
	}
      m_project->setDebugMode(DesProject::Reset);
      QString out("<b>Project is controllable. Verified on %1.</b>");
      out = out.arg(QString::fromStdWString(m_project->getCtrlStamp()));
      m_outputWidget->writeLine(out);
      m_outputWidget->writeLine(checkInfo.m_succStr);
      m_outputWidget->writeLine("");
    }
  else
    {
      QString out("Project is not controllable.");      
      m_outputWidget->writeLine("<b>" + out + "</b>");
      
      //output all errors
      m_outputWidget->writeLine("");
      m_outputWidget->writeLine(checkInfo.m_errStr);
      m_outputWidget->writeLine("");

	  /******* Counter example  ********************/
		m_tabWidget->setCurrentIndex(2);
		if( !(checkInfo.CE_tuplemap.empty()))
		{
		int DebugResponse=this->GetDebugResponse("Project is not controllable.");
		DESpot::DummyProject_BDD m_dummyproj(m_project,checkInfo);
		m_project->setDummyProject(m_dummyproj.GetDummyProject());
		m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
		if(DebugResponse==QMessageBox::Yes)
		{
		CounterExampleAlgo_BDDFCntr CEAlgo(m_project, m_project->createProjEventIterator(),checkInfo);
		bool result=CEAlgo.runAlgo();
		if(result)
		{
			m_project->setDebugMode(DesProject::CounterExample);	
			m_project->setCounterExample(CEAlgo.GetCounterExample());
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
		}
		else
			{
				m_project->setDebugMode(DesProject::ErrorTuple);
			}
		}
		else
		{
			m_tabWidget->setCurrentIndex(2);
			m_project->setDebugMode(DesProject::ErrorTuple);
		}		
		}
		/*********************************************************************/
    }
  
  saveOutput();
}

void OutputUiPart::show(BDDSD::SD_CtrlChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}


//_________________________________________________________________________________________________

void OutputUiPart::show(BDDSD::SD_SDCtrlChkInfo& checkInfo, bool showMsgBox)
{

  m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSDCtrlOutputTitle));


  m_outputWidget->clear();

  if (checkInfo.m_chkPassed)
    {
      if (showMsgBox)
	{
	  QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
	}
      
      //      QString out("<b>Project is SD controllable. Verified on %1.</b>");
      //out = out.arg(QString::fromStdWString(m_project->getCtrlStamp()));
	  m_project->setDebugMode(DesProject::Reset);
      QString out("<b>Project is SD controllable.</b>");
      m_outputWidget->writeLine(out);
      m_outputWidget->writeLine(checkInfo.m_succStr);
      m_outputWidget->writeLine("");
    }
  else
    {
      // at momement, sd cont and S-Sing behavior checked are
      //combined.  Need to make sure the other check did not cause the
      //failure 
      if (!(checkInfo.m_SSingPhibBChkFail) && !(checkInfo.CE_tuplemap.empty()))
	{

	  
	  QString out("Project is not SD controllable.");	  
	  GenerateCounterExample(checkInfo,"Project is not SD controllable.");
	  m_outputWidget->writeLine("<b>" + out + "</b>");
	  
	  //output all errors
	  m_outputWidget->writeLine("");
	  m_outputWidget->writeLine(checkInfo.m_errStr);
	  m_outputWidget->writeLine("");
	}
      else {
	QString out("SD controllable test indeterminate as currently\
 combined with S-singular Prohibitable Behavior check which failed\
 before test could complete.");
	
	/*
	GenerateCounterExample(checkInfo,"SD controllable test indeterminate as currently\
 combined with S-singular Prohibitable Behavior check which failed\
 before test could complete.");*/
	m_outputWidget->writeLine("<b>" + out + "</b>");
	m_outputWidget->writeLine("");
      }    
}

  saveOutput();
}

void OutputUiPart::show(BDDSD::SD_SDCtrlChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}


//_________________________________________________________________________________________________

void OutputUiPart::show(BDDSD::SD_PTBChkInfo& checkInfo, bool showMsgBox)
{

  m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cPTBOutputTitle));


  m_outputWidget->clear();

  if (checkInfo.m_chkPassed)
    {
      if (showMsgBox)
	{
	  QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
	}
      
      //      QString out("<b>Project is SD controllable. Verified on %1.</b>");
      //out = out.arg(QString::fromStdWString(m_project->getCtrlStamp()));
      QString out("<b>Project has Proper Time Behavior.</b>");
      m_outputWidget->writeLine(out);
      m_outputWidget->writeLine(checkInfo.m_succStr);
      m_outputWidget->writeLine("");
	  m_project->setDebugMode(DesProject::Reset);
    }
  else
    {
      QString out("Project does not have Proper Time Behavior.");     
      m_outputWidget->writeLine("<b>" + out + "</b>");
	 
	  GenerateCounterExample(checkInfo,"Project does not have Proper Time Behavior.");
      
      //output all errors
      m_outputWidget->writeLine("");
      m_outputWidget->writeLine(checkInfo.m_errStr);
      m_outputWidget->writeLine("");
    }

  saveOutput();
}

void OutputUiPart::show(BDDSD::SD_PTBChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________

void OutputUiPart::show(BDDSD::SD_SSingPChkInfo& checkInfo, bool showMsgBox)
{

  m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSSingPOutputTitle));


  m_outputWidget->clear();

  if (checkInfo.m_chkPassed)
    {
      if (showMsgBox)
	{
	  QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
	}
      
      //      QString out("<b>Project is SD controllable. Verified on %1.</b>");
      //out = out.arg(QString::fromStdWString(m_project->getCtrlStamp()));
      QString out("<b>Project has S-singular Prohibitable Behavior.</b>");
      m_outputWidget->writeLine(out);
      m_outputWidget->writeLine(checkInfo.m_succStr);
      m_outputWidget->writeLine("");
	  m_project->setDebugMode(DesProject::Reset);
    }
  else
    {
      // at momement, sd cont and S-Sing behavior checked are
      //combined.  Need to make sure the other check did not cause the
      //failure 
      if (checkInfo.m_SSingPhibBChkFail)
	{
	  QString out("Project does not have S-singular Prohibitable Behavior.");	  
	  m_outputWidget->writeLine("<b>" + out + "</b>");
	  GenerateCounterExample(checkInfo,"Project does not have S-singular Prohibitable Behavior.");
	  //output all errors
	  m_outputWidget->writeLine("");
	  m_outputWidget->writeLine(checkInfo.m_errStr);
	  m_outputWidget->writeLine("");
	}
      else {
	QString out("S-singular Prohibitable Behavior check\
 indeterminate as currently combined with SD controllable check which\
 failed before test could complete.");	
	
	// not generating a counter example as one can't be sure if the error tuple was obtained.
	/*GenerateCounterExample(checkInfo,"S-singular Prohibitable Behavior check\
 indeterminate as currently combined with SD controllable check which\
 failed before test could complete.");*/
	m_outputWidget->writeLine("<b>" + out + "</b>");
	m_outputWidget->writeLine("");
      }
    }

  saveOutput();
}

void OutputUiPart::show(BDDSD::SD_SSingPChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________

void OutputUiPart::show(BDDSD::SD_PCmpltChkInfo& checkInfo, bool showMsgBox)
{

  m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cPCmpltOutputTitle));


  m_outputWidget->clear();

  if (checkInfo.m_chkPassed)
    {
      if (showMsgBox)
	{
	  QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
	}
      
      //      QString out("<b>Project is SD controllable. Verified on %1.</b>");
      //out = out.arg(QString::fromStdWString(m_project->getCtrlStamp()));
      QString out("<b>Project passes Plant Completeness check.</b>");
      m_outputWidget->writeLine(out);
      m_outputWidget->writeLine(checkInfo.m_succStr);
      m_outputWidget->writeLine("");
	  m_project->setDebugMode(DesProject::Reset);
    }
  else
    {
      QString out("Project fails Plant Completeness check.");     
      GenerateCounterExample(checkInfo,"Project fails Plant Completeness check.");
	  m_outputWidget->writeLine("<b>" + out + "</b>");
      
      //output all errors
      m_outputWidget->writeLine("");
      m_outputWidget->writeLine(checkInfo.m_errStr);
      m_outputWidget->writeLine("");
    }

  saveOutput();
}

void OutputUiPart::show(BDDSD::SD_PCmpltChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}


//_________________________________________________________________________________________________

void OutputUiPart::show(BDDSD::SD_ALFChkInfo& checkInfo, bool showMsgBox)
{

  m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cALFOutputTitle));


  m_outputWidget->clear();

  if (checkInfo.m_chkPassed)
    {
      if (showMsgBox)
	{
	  QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
	}
      
      //      QString out("<b>Project is SD controllable. Verified on %1.</b>");
      //out = out.arg(QString::fromStdWString(m_project->getCtrlStamp()));
      QString out("<b>Project is Activity Loop Free.</b>");
      m_outputWidget->writeLine(out);
      m_outputWidget->writeLine(checkInfo.m_succStr);
      m_outputWidget->writeLine("");
	  m_project->setDebugMode(DesProject::Reset);
    }
  else
    {
      QString out("Project is not Activity Loop Free.");
	  GenerateCounterExample(checkInfo,"Project is not Activity Loop Free.");
      m_outputWidget->writeLine("<b>" + out + "</b>");
      
      //output all errors
      m_outputWidget->writeLine("");
      m_outputWidget->writeLine(checkInfo.m_errStr);
      m_outputWidget->writeLine("");
    }

  saveOutput();
}

void OutputUiPart::show(BDDSD::SD_ALFChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}





//_________________________________________________________________________________________________


void OutputUiPart::show(BDDHISC::Hisc_LWNBChkInfo& checkInfo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cLwNonBlockOutputTitle));

	m_outputWidget->clear();

	if (checkInfo.m_chkPassed)
	{
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
		}

		QString out("<b>Project is LD level-wise nonblocking. Verified on %1.</b>");
		out = out.arg(QString::fromStdWString(hierProject()->getLwNonBlockStamp()));
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		m_project->setDebugMode(DesProject::Reset);
	}
	else
	{
	        QString out("Project is not LD level-wise nonblocking.");
		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");

	  /** Counter Example **/
		 m_tabWidget->setCurrentIndex(2);
if( !(checkInfo.CE_tuplemap.empty()))
{
		const DesHierProject* errproj=(DesHierProject*)m_project;
		const DesSubsystem* errSubSys=&errproj->getSubsystem(checkInfo.getErrorSubsystemName());
		if(errSubSys->getLevel()==0)
		{
			DESpot::DummyProject_BDD m_dummyproj(errSubSys,errproj,checkInfo);
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
		}
		if(errSubSys->getLevel()>0)
		{
			DESpot::DummyProject_BDD m_dummyproj(errSubSys,checkInfo,m_project);
			m_project->setDummyProject( m_dummyproj.GetDummyProject());
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
		}
		int DebugResponse=this->GetDebugResponse("Project is not LD level-wise nonblocking.");		
		if(DebugResponse==QMessageBox::Yes)
		{
		CounterExampleAlgo_BDDLwNB CEAlgo((DesHierProject*)m_project, m_project->getDummyProject()->createProjEventIterator(),checkInfo);
		bool result=CEAlgo.runAlgo();
			if(result)
			{
				m_project->setDebugMode(DesProject::CounterExample);	
				m_project->setCounterExample(CEAlgo.GetCounterExample());
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
			}
			else
			{
				m_project->setDebugMode(DesProject::ErrorTuple);
			}
		}
		else
		{
				m_tabWidget->setCurrentIndex(2);
				m_project->setDebugMode(DesProject::ErrorTuple);		
		}
}

	  /******************************************************/

	}

	saveOutput();
}

void OutputUiPart::show(BDDHISC::Hisc_LWNBChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}


//_________________________________________________________________________________________________

void OutputUiPart::show(BDDHISC::Hisc_SubLWNBChkInfo& checkInfo, bool showMsgBox)
{
        m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysNonBlockingOutputTitle));

	m_outputWidget->clear();

	if (checkInfo.m_chkPassed)
	{
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
		}

		QString out("<b>Subsystem '" + checkInfo.m_subsystName + "' is LD nonblocking. Verified on %1.</b>");
		out = out.arg(QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		m_project->setDebugMode(DesProject::Reset);
	}
	else
	{
	        QString out("Subsystem '" + checkInfo.m_subsystName + 
			    "' is not LD nonblocking.");
		
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");

		/** Counter example **/
 m_tabWidget->setCurrentIndex(2);
if( !(checkInfo.CE_tuplemap.empty()))
{
		const DesHierProject* errproj=(DesHierProject*)m_project;
		const DesSubsystem* errSubSys=&errproj->getSubsystem(checkInfo.getErrorSubsystemName());
		if(errSubSys->getLevel()==0)
		{
			DESpot::DummyProject_BDD m_dummyproj(errSubSys,errproj,checkInfo);
			m_project->setDummyProject(m_dummyproj.GetDummyProject());		
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
		}
		else if(errSubSys->getLevel()>0)
		{
			DESpot::DummyProject_BDD m_dummyproj(errSubSys,checkInfo,m_project);
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
		}
		int DebugResponse=this->GetDebugResponse(out);
		if(DebugResponse==QMessageBox::Yes)
		{									   
			CounterExampleAlgo_BDDLwNB CEAlgo((DesHierProject*)m_project, m_project->getDummyProject()->createProjEventIterator(),checkInfo);
			bool result=CEAlgo.runAlgo();
				if(result)
					{
						m_project->setDebugMode(DesProject::CounterExample);
						m_project->setCounterExample(CEAlgo.GetCounterExample());
						QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
					}
				else
					{
						m_project->setDebugMode(DesProject::ErrorTuple);
					}
		}
		else
		{
			m_tabWidget->setCurrentIndex(2);
			m_project->setDebugMode(DesProject::ErrorTuple);
		}
}
		
	  /*******************************************************/

	}

	saveOutput();
}
//_________________________________________________________________________________________________

void OutputUiPart::show(BDDHISC::Hisc_SubLWNBChkInfo& checkInfo,bool isHigh, bool showMsgBox)
{
        m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysNonBlockingOutputTitle));

	m_outputWidget->clear();

	if (checkInfo.m_chkPassed)
	{
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
		}
		if(isHigh)
		{
		QString out("<b>High level subsystem '" + checkInfo.m_subsystName + "' is LD nonblocking. Verified on %1.</b>");
		out = out.arg(QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		}
		else
		{
		QString out("<b>Low level subsystem '" + checkInfo.m_subsystName + "' is LD nonblocking. Verified on %1.</b>");
		out = out.arg(QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		}
	}
	else
	{
		if(isHigh)
		{
	        QString out("High level subsystem '" + checkInfo.m_subsystName + 
			    "' is not LD nonblocking.");
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", out);
		}
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");
		}
		else
		{
			 QString out("Low level subsystem '" + checkInfo.m_subsystName + 
			    "' is not LD nonblocking.");
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", out);
		}
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");
		}
	}

	saveOutput();
}
void OutputUiPart::show(BDDHISC::Hisc_SubLWNBChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

void OutputUiPart::show( bool isHigh,BDDHISC::Hisc_SubLWNBChkInfo& checkInfo,LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo,isHigh, showMsgBox);
	saveLastOutput(copyToLastOutput);
}
//_________________________________________________________________________________________________

void OutputUiPart::show(BDDHISC::Hisc_LWContChkInfo& checkInfo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cLwCtrlOutputTitle));

	m_outputWidget->clear();

	if (checkInfo.m_chkPassed)
	{
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
		}

		QString out("<b>Project is LD level-wise controllable. Verified on %1.</b>");
		out = out.arg(QString::fromStdWString(hierProject()->getLwCtrlStamp()));
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		m_project->setDebugMode(DesProject::Reset);
	}
	else
	{
	        QString out("Project is not LD level-wise controllable.");
		
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");

		/** Counter example **/
 m_tabWidget->setCurrentIndex(2);
if( !(checkInfo.CE_tuplemap.empty()))
{
		const DesHierProject* errproj=(DesHierProject*)m_project;
		const DesSubsystem* errSubSys=&errproj->getSubsystem(checkInfo.getErrorSubsystemName());
		if(errSubSys->getLevel()==0)
		{
			DESpot::DummyProject_BDD m_dummyproj(errSubSys,errproj,checkInfo);
			m_project->setDummyProject( m_dummyproj.GetDummyProject());
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
		}
		else if(errSubSys->getLevel()>0)
		{
			DESpot::DummyProject_BDD m_dummyproj(errSubSys,checkInfo,m_project);
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
		}

		int DebugResponse=this->GetDebugResponse("Project is not LD level-wise controllable.");	
		if(DebugResponse==QMessageBox::Yes)
		{
		CounterExampleAlgo_BDDLwCntr testalgo2((DesHierProject*)m_project,m_project->getDummyProject()->createProjEventIterator(),checkInfo);
		bool result=testalgo2.runAlgo();
		if(result)
			{
				m_project->setDebugMode(DesProject::CounterExample);
				m_project->setCounterExample(testalgo2.GetCounterExample());
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
			}
			else
			{
				m_project->setDebugMode(DesProject::ErrorTuple);
			}
		}
		else
		{
			m_tabWidget->setCurrentIndex(2);
			m_project->setDebugMode(DesProject::ErrorTuple);
		}

		/* for debugging
		ProjectEventSet::iterator it = OutputUiPart::CEEventSet.begin();
		QString str="Event Sequence for BDD Level-Wise Controllability ";
		for (;it != OutputUiPart::CEEventSet.end(); ++it) 
		{
			ProjectEvent *ev = const_cast<ProjectEvent*>(it.value());
			 str += QString::fromStdWString(ev->getName());
			 str+=" ";
        }
		m_outputWidget->writeLine(str);
		*/
}
	  /*****************************************/


	}

	saveOutput();
}

void OutputUiPart::show(BDDHISC::Hisc_LWContChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}


//_________________________________________________________________________________________________

void OutputUiPart::show(BDDHISC::Hisc_SubLWContChkInfo& checkInfo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysCtrlOutputTitle));

	m_outputWidget->clear();

	if (checkInfo.m_chkPassed)
	{
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
		}

		QString out("<b>Subsystem '" + checkInfo.m_subsystName + "' is LD controllable. Verified on %1.</b>");
		out = out.arg(QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		m_project->setDebugMode(DesProject::Reset);
	}
	else
	{
	        QString out("Subsystem '" + checkInfo.m_subsystName + 
			    "' is not LD controllable.");
		
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");

		/** Counter example **/
m_tabWidget->setCurrentIndex(2);
if( !(checkInfo.CE_tuplemap.empty()))
{		
		const DesHierProject* errproj=(DesHierProject*)m_project;
		const DesSubsystem* errSubSys=&errproj->getSubsystem(checkInfo.getErrorSubsystemName());
		if(errSubSys->getLevel()==0)
		{
			DESpot::DummyProject_BDD m_dummyproj(errSubSys,errproj,checkInfo);
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
		}
		else if(errSubSys->getLevel()>0)
		{
			DESpot::DummyProject_BDD m_dummyproj(errSubSys,checkInfo,m_project);
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
		}

		int DebugResponse=this->GetDebugResponse(out);
		if(DebugResponse==QMessageBox::Yes)
		{
		CounterExampleAlgo_BDDLwCntr CEAlgo((DesHierProject*)m_project, m_project->getDummyProject()->createProjEventIterator(),checkInfo);
		bool result=CEAlgo.runAlgo();
		if(result)
			{
			m_project->setDebugMode(DesProject::CounterExample);	
			m_project->setCounterExample(CEAlgo.GetCounterExample());
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
			}
			else
			{
				m_project->setDebugMode(DesProject::ErrorTuple);
			}
		}
		else
		{
			m_tabWidget->setCurrentIndex(2);
			m_project->setDebugMode(DesProject::ErrorTuple);
		}
		/*
		ProjectEventSet::iterator it = OutputUiPart::CEEventSet.begin();
		QString str="Event Sequence for BDD subsystem Controllability Algo: ";
		for (;it != OutputUiPart::CEEventSet.end(); ++it) 
		{
			ProjectEvent *ev = const_cast<ProjectEvent*>(it.value());
			 str += QString::fromStdWString(ev->getName());
			 str+=" ";
        }
		m_outputWidget->writeLine(str);
		*/
}		
	  /*********************************************/
	}

	saveOutput();
}

void OutputUiPart::show(BDDHISC::Hisc_SubLWContChkInfo& checkInfo, bool isHigh, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysCtrlOutputTitle));

	m_outputWidget->clear();

	if (checkInfo.m_chkPassed)
	{
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
		}
		if(isHigh)
		{
		QString out("<b>High level subsystem '" + checkInfo.m_subsystName + "' is LD controllable. Verified on %1.</b>");
		out = out.arg(QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		}
		else
		{
			QString out("<b>Low level subsystem '" + checkInfo.m_subsystName + "' is LD controllable. Verified on %1.</b>");
		out = out.arg(QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		}
	}
	else
	{
		if(isHigh)
		{
	        QString out("High level subsystem '" + checkInfo.m_subsystName + 
			    "' is not LD controllable.");
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", out);
		}
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");
		}
		else
		{
			 QString out("Low level subsystem '" + checkInfo.m_subsystName + 
			    "' is not LD controllable.");
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", out);
		}
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");
		}
	}

	saveOutput();
}
void OutputUiPart::show(BDDHISC::Hisc_SubLWContChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

void OutputUiPart::show(bool isHigh,BDDHISC::Hisc_SubLWContChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo,isHigh, showMsgBox);
	saveLastOutput(copyToLastOutput);
}
//_________________________________________________________________________________________________

void OutputUiPart::show(BDDHISC::Hisc_IConsisChkInfo& checkInfo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cInterfConsistOutputTitle));

	m_outputWidget->clear();

	if (checkInfo.m_chkPassed)
	{
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
		}

		QString out("<b>Project is LD interface consistent. Verified on %1.</b>");
		out = out.arg(QString::fromStdWString(hierProject()->getIConsistStamp()));
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		m_project->setDebugMode(DesProject::Reset);
	}
	else
	{
	        QString out("Project is not LD interface consistent.");
		
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");

		/** Counter Example **/
m_tabWidget->setCurrentIndex(2);
if( !(checkInfo.CE_tuplemap.empty()))
{
if(checkInfo.getIFailureType()==DesAlgo::ReqAcptAlgo || checkInfo.getIFailureType()==DesAlgo::IntrfImplAlgo ||checkInfo.getIFailureType()==DesAlgo::AnsAcptAlgo )
{
		const DesHierProject* errproj=(DesHierProject*)m_project;
		const DesSubsystem* errSubSys=&errproj->getSubsystem(checkInfo.getErrorSubsystemName());		
		if(checkInfo.getIFailureType()==DesAlgo::AnsAcptAlgo)
		{
			int DebugResponse=this->GetDebugResponse("Project is not LD interface consistent. The high level does not accept all answer events.");
			DESpot::DummyProject_BDD m_dummyproj(errSubSys,errproj,checkInfo);
			m_project->setDummyProject(m_dummyproj.GetDummyProject());
			m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			if(DebugResponse==QMessageBox::Yes)
				{
					CounterExampleAlgo_BDDAnsAcpt CEAlgo( (DesHierProject*)m_project,
													m_project->getDummyProject()->createProjEventIterator(),
													checkInfo);	
					bool result=CEAlgo.runAlgo();
					if(result)
						{
							m_project->setDebugMode(DesProject::CounterExample);	
							m_project->setCounterExample(CEAlgo.GetCounterExample());	
							QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
						}
						else
						{
							m_project->setDebugMode(DesProject::ErrorTuple);
						}
				}
			else
				{
					m_tabWidget->setCurrentIndex(2);
					m_project->setDebugMode(DesProject::ErrorTuple);
				}
		}
		else if(checkInfo.getIFailureType()==DesAlgo::ReqAcptAlgo || checkInfo.getIFailureType()==DesAlgo::IntrfImplAlgo) 
		{
		int DebugResponse=this->GetDebugResponse("Project is not LD interface consistent.");
		DESpot::DummyProject_BDD m_dummyproj(errSubSys,checkInfo,m_project);
		m_project->setDummyProject(m_dummyproj.GetDummyProject());
		m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
			if(DebugResponse==QMessageBox::Yes)
			{			
				CounterExampleAlgo_BDDIReqAcpt CEAlgo( (DesHierProject*)m_project,
													m_project->getDummyProject()->createProjEventIterator(),
													checkInfo);	
				bool result=CEAlgo.runAlgo();
					if(result)
					{
						m_project->setDebugMode(DesProject::CounterExample);
						m_project->setCounterExample(CEAlgo.GetCounterExample());
						QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
					}
					else
					{
						m_project->setDebugMode(DesProject::ErrorTuple);
					}
						
			}
			else
			{
				m_tabWidget->setCurrentIndex(2);
				m_project->setDebugMode(DesProject::ErrorTuple);
			}
		}
}
			/*
			ProjectEventSet::iterator it = OutputUiPart::CEEventSet.begin();
			QString str="Event Sequence for Request Accept algo:    ";
				for (;it != OutputUiPart::CEEventSet.end(); ++it) 
				{
				ProjectEvent *ev = const_cast<ProjectEvent*>(it.value());
				 str += QString::fromStdWString(ev->getName());
				 str+=" ";
		        }
			m_outputWidget->writeLine(str);
			*/
		/***********************************************************/

	}
}
	saveOutput();	
}

void OutputUiPart::show(BDDHISC::Hisc_IConsisChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}


//_________________________________________________________________________________________________

void OutputUiPart::show(BDDHISC::Hisc_SubIConsisChkInfo& checkInfo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysInterfConsistOutputTitle));

	m_outputWidget->clear();

	if (checkInfo.m_chkPassed)
	{
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
		}

		QString out("<b>Subsystem '" + checkInfo.m_subsystName + "' is LD interface consistent. Verified on %1.</b>");
		out = out.arg(QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		m_project->setDebugMode(DesProject::Reset);
	}
	else
	{
	        QString out("Subsystem '" + checkInfo.m_subsystName + 
			    "' is not LD interface consistent.");
		
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");

		/**** Counter Example ****/
m_tabWidget->setCurrentIndex(2);
if( !(checkInfo.CE_tuplemap.empty()))
{
if(checkInfo.getIFailureType()==DesAlgo::ReqAcptAlgo || checkInfo.getIFailureType()==DesAlgo::IntrfImplAlgo ||checkInfo.getIFailureType()==DesAlgo::AnsAcptAlgo )
{

		const DesHierProject* errproj=(DesHierProject*)m_project;
		const DesSubsystem* errSubSys=&errproj->getSubsystem(checkInfo.getErrorSubsystemName());
		int DebugResponse=this->GetDebugResponse(out);
		if(DebugResponse==QMessageBox::Yes)
		{		
			if(checkInfo.getIFailureType()==DesAlgo::AnsAcptAlgo)
			{				
				DESpot::DummyProject_BDD m_dummyproj(errSubSys,errproj,checkInfo);
				m_project->setDummyProject(m_dummyproj.GetDummyProject());
				m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				
				CounterExampleAlgo_BDDAnsAcpt CEAlgo( (DesHierProject*)m_project,
													m_project->getDummyProject()->createProjEventIterator(),
													checkInfo);	
				bool result=CEAlgo.runAlgo();
					if(result)
					{
						m_project->setDebugMode(DesProject::CounterExample);
						m_project->setCounterExample(CEAlgo.GetCounterExample());
						QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
					}
					else
					{
						m_project->setDebugMode(DesProject::ErrorTuple);
					}
			}

			if(checkInfo.getIFailureType()==DesAlgo::ReqAcptAlgo || checkInfo.getIFailureType()==DesAlgo::IntrfImplAlgo) 
			{
				DESpot::DummyProject_BDD m_dummyproj(errSubSys,checkInfo,m_project);
				m_project->setDummyProject(m_dummyproj.GetDummyProject());
				m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				CounterExampleAlgo_BDDIReqAcpt CEAlgo( (DesHierProject*)m_project,
													m_project->getDummyProject()->createProjEventIterator(),
													checkInfo);				
				bool result=CEAlgo.runAlgo();
					if(result)
					{
						m_project->setDebugMode(DesProject::CounterExample);
						m_project->setCounterExample(CEAlgo.GetCounterExample());
						QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot","Counter example generated successfully.");
					}
					else
					{
						m_project->setDebugMode(DesProject::ErrorTuple);
					}
			
			}
		}
		if(DebugResponse==QMessageBox::No)
		{
			m_tabWidget->setCurrentIndex(2);
			if(checkInfo.getIFailureType()==DesAlgo::AnsAcptAlgo)
			{				
				DESpot::DummyProject_BDD m_dummyproj(errSubSys,errproj,checkInfo);
				m_project->setDummyProject(m_dummyproj.GetDummyProject());
				m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				m_project->setDebugMode(DesProject::ErrorTuple);
			}
			else
			{
				DESpot::DummyProject_BDD m_dummyproj(errSubSys,checkInfo,m_project);
				m_project->setDummyProject(m_dummyproj.GetDummyProject());
				m_project->setSimulationErrorTuple(m_dummyproj.getSimulationErrorTuple());
				m_project->setDebugMode(DesProject::ErrorTuple);
			}
		}
			/*
			ProjectEventSet::iterator it = OutputUiPart::CEEventSet.begin();
			QString str="Event Sequence for Request Accept algo:    ";
				for (;it != OutputUiPart::CEEventSet.end(); ++it) 
				{
				ProjectEvent *ev = const_cast<ProjectEvent*>(it.value());
				 str += QString::fromStdWString(ev->getName());
				 str+=" ";
		        }
			m_outputWidget->writeLine(str);
			*/
}
}
		/***********************************************/


	}

	saveOutput();
}

void OutputUiPart::show(BDDHISC::Hisc_SubIConsisChkInfo& checkInfo, bool isHigh, bool isMiddle, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysInterfConsistOutputTitle));

	m_outputWidget->clear();

	if (checkInfo.m_chkPassed)
	{
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
		}
		if(isHigh)
		{
		QString out("<b>High level subsystem '" + checkInfo.m_subsystName + "' is LD interface consistent. Verified on %1.</b>");
		out = out.arg(QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		}
		else if(isMiddle)
		{
		QString out("<b>High/Low level subsystem '" + checkInfo.m_subsystName + "' is LD interface consistent. Verified on %1.</b>");
		out = out.arg(QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		}
		else
		{
		QString out("<b>Low level subsystem '" + checkInfo.m_subsystName + "' is LD interface consistent. Verified on %1.</b>");
		out = out.arg(QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);
		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		}
	}
	else
	{
		if(isHigh)
		{
	        QString out("High LEvel subsystem '" + checkInfo.m_subsystName + 
			    "' is not LD interface consistent.");
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", out);
		}
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");
		}
		if(isMiddle)
		{
	        QString out("High/Low Level subsystem '" + checkInfo.m_subsystName + 
			    "' is not LD interface consistent.");
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", out);
		}
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");
		}
		else
		{
	        QString out("Low Level subsystem '" + checkInfo.m_subsystName + 
			    "' is not LD interface consistent.");
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", out);
		}
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");
		}
	}

	saveOutput();
}
void OutputUiPart::show(BDDHISC::Hisc_SubIConsisChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

void OutputUiPart::show(bool isHigh,bool isMiddle,BDDHISC::Hisc_SubIConsisChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo,isHigh,isMiddle, showMsgBox);
	saveLastOutput(copyToLastOutput);
}
//_________________________________________________________________________________________________

void OutputUiPart::show(BDDHISC::Hisc_LDIntfChkInfo& checkInfo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cLdInterfCheckTitle));

	m_outputWidget->clear();

	if (checkInfo.m_chkPassed)
	{
		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
		}

		QString out("<b>Interface '" + checkInfo.m_theIntfName
		+ "' is an LD interface. Verified on %1.</b>");
		out = out.arg(QDateTime::currentDateTime().toString());
		m_outputWidget->writeLine(out);
		//		m_outputWidget->writeLine("");
		//		m_outputWidget->writeLine(checkInfo.m_succStr);
		m_outputWidget->writeLine("");
		m_project->setDebugMode(DesProject::Reset);
	}
	else
	{
	        QString out("Interface '" + checkInfo.m_theIntfName
			    + "' is not an LD interface.");

		if (showMsgBox)
		{
			QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", out);
		}
		m_outputWidget->writeLine("<b>" + out + "</b>");

		//output all errors
		m_outputWidget->writeLine("");
		m_outputWidget->writeLine(checkInfo.m_errStr);
		m_outputWidget->writeLine("");
	}

	saveOutput();

}

void OutputUiPart::show(BDDHISC::Hisc_LDIntfChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}


//_________________________________________________________________________________________________

void OutputUiPart::show(BDDHISC::Hisc_SubLWSynthChkInfo& checkInfo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cSubsysSynthOutputTitle));

	m_outputWidget->clear();

	if (showMsgBox)
	  {
	    QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
	  }
	
	QString out("<b>" + checkInfo.m_headerStr + "</b>");
	m_outputWidget->writeLine(out);
	m_outputWidget->writeLine("");
	m_outputWidget->writeLine(checkInfo.m_succStr);
	m_outputWidget->writeLine("");

	saveOutput();
}

void OutputUiPart::show(BDDHISC::Hisc_SubLWSynthChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

//_________________________________________________________________________________________________

void OutputUiPart::show(BDDHISC::Hisc_LWSynthChkInfo& checkInfo, bool showMsgBox)
{
	m_showOutputForWidg->setCurrentIndex(m_showOutputForWidg->findText(cLwSynthOutputTitle));

	m_outputWidget->clear();


	if (showMsgBox)
	  {
	    QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", checkInfo.m_headerStr);
	  }
	
	QString out("<b>Level-wise synthesis successful.</b>");
	m_outputWidget->writeLine(out);
	m_outputWidget->writeLine("");
	m_outputWidget->writeLine(checkInfo.m_succStr);
	m_outputWidget->writeLine("");

	saveOutput();	

}

void OutputUiPart::show(BDDHISC::Hisc_LWSynthChkInfo& checkInfo, LastOutputOption copyToLastOutput /*= eSetLastOutput*/, bool showMsgBox /*= true*/)
{
	show(checkInfo, showMsgBox);
	saveLastOutput(copyToLastOutput);
}

#endif

//_________________________________________________________________________________________________

int OutputUiPart::getOutputIndexForSource(OutputSource source)
{
	switch(source)
	{
		case eProjectIntegrityCheck:
			return m_showOutputForWidg->findText(cProjIntegOutputTitle);

		case eNonBlockingCheck:
			return m_showOutputForWidg->findText(cNonBlockOutputTitle);

		case eControllabilityCheck:
			return m_showOutputForWidg->findText(cCtrlOutputTitle);

		case eInterfConsistCheck:
			return m_showOutputForWidg->findText(cInterfConsistOutputTitle);

		case eLwNonblockingCheck:
			return m_showOutputForWidg->findText(cLwNonBlockOutputTitle);

		case eLwCtrlCheck:
			return m_showOutputForWidg->findText(cLwCtrlOutputTitle);

		case eSubsysInterfConsistCheck:
			return m_showOutputForWidg->findText(cSubsysInterfConsistOutputTitle);

		case eLdInterfCheck:
			return m_showOutputForWidg->findText(cLdInterfCheckTitle);

		case eSubsysNonblockingCheck:
			return m_showOutputForWidg->findText(cSubsysNonBlockingOutputTitle);

		case eSubsysCtrlCheck:
			return m_showOutputForWidg->findText(cSubsysCtrlOutputTitle);

		default:
			return m_showOutputForWidg->findText(cLastOutputTitle);
	}

}

//_________________________________________________________________________________________________

void OutputUiPart::clearLastOutput()
{
	int lastOutIndex = m_showOutputForWidg->findText(cLastOutputTitle);

	if (m_showOutputForWidg->currentIndex() == lastOutIndex)
	{
		//we're displaying the last output so we must clear the output widget
		m_outputWidget->clear();
	}

	//erase the data stored for the last output itme
	m_showOutputForWidg->setItemData(lastOutIndex, "");
}

//_________________________________________________________________________________________________

void OutputUiPart::show(FlatProjectPropCheck& projCheckAlgo)
{
	clearLastOutput();

	if (projCheckAlgo.runSuccessful())
	{
		m_project->setDebugMode(DesProject::Reset);
	}
	
	if (projCheckAlgo.integrityChecked())
	{
		show(projCheckAlgo.integAlgo(), OutputUiPart::eSetLastOutput, false);
	}

	if (projCheckAlgo.nonBlockChecked())
	{
		showMeasurements(&m_project->getFlatSystemDes());
		show(projCheckAlgo.nonBlockAlgo(), OutputUiPart::eAppendLastOutput, false);	
		if(!(projCheckAlgo.nonBlockAlgo().isnonblocked))
			{				
				m_project->setProjectChkFlag(true);
			}
	}

	if (projCheckAlgo.ctrlChecked())
	{
		show(projCheckAlgo.ctrlAlgo(), OutputUiPart::eAppendLastOutput, false);
	}
	m_project->setProjectChkFlag(false);
}

//_________________________________________________________________________________________________

void OutputUiPart::show(HierProjectPropCheck& projCheckAlgo)
{
	clearLastOutput();

	if (projCheckAlgo.runSuccessful())
	{
		m_project->setDebugMode(DesProject::Reset);
	}
	
	if (projCheckAlgo.integrityChecked())
	{
		show(projCheckAlgo.integAlgo(), OutputUiPart::eSetLastOutput, false);
	}

	if (projCheckAlgo.iConsistChecked())
	{
		show(projCheckAlgo.interfConsistAlgo(), OutputUiPart::eAppendLastOutput, false);
		if(!projCheckAlgo.interfConsistAlgo().isInterfaceConsistent())
		{
			projCheckAlgo.levelWiseNonBlockAlgo().setErrorFlag(false);
			projCheckAlgo.levelWiseCtrlAlgo().setErrorFlag(false);
		}
		
	}
	if (projCheckAlgo.lwNonBlockChecked())
	{
		show(projCheckAlgo.levelWiseNonBlockAlgo(), OutputUiPart::eAppendLastOutput, false);
		if(!projCheckAlgo.levelWiseNonBlockAlgo().isLwNonBlocking())
		{
			projCheckAlgo.levelWiseCtrlAlgo().setErrorFlag(false);
		}
	}

	if (projCheckAlgo.lwCtrlChecked())
	{
		show(projCheckAlgo.levelWiseCtrlAlgo(), OutputUiPart::eAppendLastOutput, false);
	}

	m_project->setProjectChkFlag(false);
}

//_________________________________________________________________________________________________
//Show the errors in the algorithm, paging them in case the number of errors is too large
void OutputUiPart::showErrors(const DesAlgo::ErrorList& errList)
{
	m_outputWidget->writeLine("");

	const short errorPagingSize = 10;
	long errorsRemaining = errList.size();

	//for debug
	// std::cout << "entering showErrors. Size" << errorsRemaining << "\n";

	bool pageErrors = true;
	long crtPageErrCount = 0;
	for(DesAlgo::ErrIt errIt = errList.begin(); errIt != errList.end(); ++errIt)
	{
		m_outputWidget->writeLine(QString("<I>Error:</I> ") + QString::fromStdWString(*errIt));
		crtPageErrCount++;
		errorsRemaining--;

		if (pageErrors && (crtPageErrCount == errorPagingSize) && errorsRemaining > 0)
		{
		  QString msg("Do you want to show the next %1 errors?<BR><BR>Selecting 'Yes To All'  will  save all errors to a file.");
			msg = msg.arg(errorPagingSize);
			int userAnswer = QMessageBox::question(m_outputWidget->topLevelWidget(), STR_DESPOT_WARNING, msg, 
															  QMessageBox::Yes | QMessageBox::YesToAll | 
	 														  QMessageBox::No, 
															  QMessageBox::Yes);

			if (userAnswer == QMessageBox::Yes)
			{
				//the user wants to see the next page of errors; reset the error counter for the new page
				crtPageErrCount = 0;
				continue;
			}
			else if (userAnswer == QMessageBox::YesToAll)
			{

			  m_outputWidget->writeLine((errorsRemaining == 1) ? 
			     QString("1 error has not been displayed.") : 
			     QString("%1 errors have not been displayed.").arg(errorsRemaining));

			  // The user wants to save all errors to a file
			  saveErrors(errList);

			  // old version that sent remaining errors to
			  // output tab but this usually caused things
			  // to freeze.
			  // pageErrors = false;
			  // continue;


			  break;
			}
			else if (userAnswer == QMessageBox::No)
			{
				//the user doesn't want to see anymore errors
				m_outputWidget->writeLine(
					(errorsRemaining == 1) ? 
						QString("1 error has not been displayed.") : 
						QString("%1 errors have not been displayed.").arg(errorsRemaining));
				break;
			}
			else
			{
				assert(false);
				//assume the user doesn't want to see anymore errors
				m_outputWidget->writeLine(
					(errorsRemaining == 1) ? 
						QString("1 error has not been displayed.") : 
						QString("%1 errors have not been displayed.").arg(errorsRemaining));
				break;
			}
		}

	}

	m_outputWidget->writeLine("");
}


//_________________________________________________________________________________________________
//Save all errors to a file
void OutputUiPart::saveErrors(const DesAlgo::ErrorList& errList)
{

	// for debug
       //  std::cout << "entering saveErrors.\n";

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

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

      
	if (MainForm::getSaveFileName(m_outputWidget, tr("Save errors to file."), tr("Text file (*.txt)"), absoluteFileName) == false)
	{
		//user canceled the save as
		return;
	}

	//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 ".txt"
        if (!absoluteFileName.endsWith(".txt",Qt::CaseInsensitive)) 
	  {
	    absoluteFileName += ".txt";
	  }


	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 file name (";
		message += fileName;
		message += L"). Use an alpha-numeric string (a-z;A-Z;0-9;.-_)";
		throw message;
	}

	m_outputWidget->writeLine("");
	m_outputWidget->writeLine(QString("Writing all errors to file: ")
           + absoluteFileName);
	m_outputWidget->writeLine("");

	//open the error file with the given file name
	QFile errFile(absoluteFileName);
	if (errFile.open(QIODevice::WriteOnly|QIODevice::Text) == false) {
	  throw EX("Cannot open file in write-only mode. Cannot save errors.");
	}

	//write out project file
	QTextStream errOut(&errFile);

	//   errOut << "[SYSTEM]\n";  



	for(DesAlgo::ErrIt errIt = errList.begin(); errIt != errList.end(); ++errIt)
	  {
	    errOut << QString("Error: ") + QString::fromStdWString(*errIt) +QString("\n");
	  }
}

#ifdef __ENABLE_DIST__
//_________________________________________________________________________________________________

	void OutputUiPart::showFlat(resultStruct results, int time)
	{
		clearLastOutput();
		m_project->setDebugMode(DesProject::Reset);
		bool success = true;
		if (results.ctrlChecked)
			success &= results.controllable;
		if (results.NBChecked)
			success &= results.nonBlocking;

		if (success)
		{
			QMessageBox::question(m_outputWidget->topLevelWidget(), "DESpot", STR_PROJ_PROP_CHECKED_OK, QMessageBox::Ok);

			// indicate that each property succeeded
			if (results.NBChecked)
				m_outputWidget->writeLine(QString::fromStdString("<b>System is nonblocking. Verified on ") + QDateTime::currentDateTime().toString() + QString::fromStdString("</b><br />"));

			if (results.ctrlChecked)
				m_outputWidget->writeLine(QString::fromStdString("<b>System is controllable. Verified on ") + QDateTime::currentDateTime().toString() + QString::fromStdString("</b>"));

			showMessage(results.SucList);
		}
		else
		{
			if (m_tabWidget->currentIndex() == 2)
			{
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", STR_PROJ_PROP_CHECKED_FAIL_STM);
			}
			else
			{
				bool showOutput = (QMessageBox::question(m_outputWidget->topLevelWidget(), "DESpot", STR_PROJ_PROP_CHECKED_FAIL, QMessageBox::Yes | QMessageBox::No)
														 == QMessageBox::Yes);
				if (showOutput)
				{
					m_tabWidget->setCurrentIndex(2);
				}
			}

			// indicate which properties succeeded and which failed
			if (results.NBChecked)
				if (results.nonBlocking == eLwNonBlockYes)
				{
					m_outputWidget->writeLine(QString::fromStdString("<b>System is nonblocking. Verified on ") + QDateTime::currentDateTime().toString() + QString::fromStdString("</b><br />"));
				}
				else if (results.nonBlocking == eLwNonBlockNo)
				{					
					showMessage(results.NBList);
				}

			if (results.ctrlChecked)
				if (results.controllable == eLwCtrlYes)
				{
					m_outputWidget->writeLine(QString::fromStdString("<br/><b>System is controllable. Verified on ") + QDateTime::currentDateTime().toString() + QString::fromStdString("</b><br />"));
				}
				else if (results.controllable == eLwCtrlNo)
				{					
					showMessage(results.CtrlList);
				}	
		}
		
		showTime(time);
	}

//_________________________________________________________________________________________________

	void OutputUiPart::show(resultStruct results, int time)
	{
		clearLastOutput();
		m_project->setDebugMode(DesProject::Reset);
		bool success = true;
		if (results.ctrlChecked)
			success &= results.controllable;
		if (results.NBChecked)
			success &= results.nonBlocking;
		if (results.iConsistChecked)
			success &= results.iConsistent;

		if (success)
		{
			QMessageBox::question(m_outputWidget->topLevelWidget(), "DESpot", STR_PROJ_PROP_CHECKED_OK, QMessageBox::Ok);

			// indicate that each property succeeded
			if (results.NBChecked)
				m_outputWidget->writeLine(QString::fromStdString("<b>Project is LD level-wise nonblocking. Verified on ") + QDateTime::currentDateTime().toString() + QString::fromStdString("</b><br />"));

			if (results.ctrlChecked)
				m_outputWidget->writeLine(QString::fromStdString("<b>Project is LD level-wise controllable. Verified on ") + QDateTime::currentDateTime().toString() + QString::fromStdString("</b><br />"));

			if (results.iConsistChecked)
				m_outputWidget->writeLine(QString::fromStdString("<b>Project is LD interface consistent. Verified on ") + QDateTime::currentDateTime().toString() + QString::fromStdString("</b>"));

			showMessage(results.SucList);
		}
		else
		{
			if (m_tabWidget->currentIndex() == 2)
			{
				QMessageBox::information(m_outputWidget->topLevelWidget(), "DESpot", STR_PROJ_PROP_CHECKED_FAIL_STM);
			}
			else
			{
				bool showOutput = (QMessageBox::question(m_outputWidget->topLevelWidget(), "DESpot", STR_PROJ_PROP_CHECKED_FAIL, QMessageBox::Yes | QMessageBox::No)
														 == QMessageBox::Yes);
				if (showOutput)
				{
					m_tabWidget->setCurrentIndex(2);
				}
			}

			// indicate which properties succeeded and which failed
			if (results.NBChecked)
				if (results.nonBlocking == eLwNonBlockYes)
				{
					m_outputWidget->writeLine(QString::fromStdString("<b>Project is LD level-wise nonblocking. Verified on ") + QDateTime::currentDateTime().toString() + QString::fromStdString("</b><br />"));
				}
				else if (results.nonBlocking == eLwNonBlockNo)
				{
					stringstream ss;
					ss << "<b>Project is not LD level-wise nonblocking - " << results.NBList.size() << " error(s)</b><br/>";
					m_outputWidget->writeLine(QString::fromStdString(ss.str()));

					showErrors(results.NBList);
				}

			if (results.ctrlChecked)
				if (results.controllable == eLwCtrlYes)
				{
					m_outputWidget->writeLine(QString::fromStdString("<br/><b>Project is LD level-wise controllable. Verified on ") + QDateTime::currentDateTime().toString() + QString::fromStdString("</b><br />"));
				}
				else if (results.controllable == eLwCtrlNo)
				{
					stringstream ss;
					ss << "<br/><b>Project is not LD level-wise controllable - " << results.CtrlList.size() << " error(s)</b><br/>";
					m_outputWidget->writeLine(QString::fromStdString(ss.str()));

					showErrors(results.CtrlList);
				}

			if (results.iConsistChecked)
				if (results.iConsistent == eIConsYes)
				{
					m_outputWidget->writeLine(QString::fromStdString("<br/><b>Project is LD interface consistent. Verified on ") + QDateTime::currentDateTime().toString() + QString::fromStdString("</b><br />"));
				}
				else if (results.iConsistent == eIConsNo)
				{
					stringstream ss;
					ss << "<br/><b>Project is not LD interface consistent - " << results.iConsList.size() << " error(s)</b><br/>";
					m_outputWidget->writeLine(QString::fromStdString(ss.str()));

					showErrors(results.iConsList);
				}
		}
		
		showTime(time);
	}

//_________________________________________________________________________________________________

// Copied from showErrors, but with the 'Error' before each line
void OutputUiPart::showMessage(const DesAlgo::ErrorList& msglist)
{
	const short errorPagingSize = 10;
	long errorsRemaining = msglist.size();

	bool pageErrors = true;
	long crtPageErrCount = 0;
	m_project->setDebugMode(DesProject::Reset);
	for(DesAlgo::ErrIt errIt = msglist.begin(); errIt != msglist.end(); ++errIt)
	{
		m_outputWidget->writeLine(QString::fromStdWString(*errIt));
		crtPageErrCount++;
		errorsRemaining--;

		if (pageErrors && (crtPageErrCount == errorPagingSize) && errorsRemaining > 0)
		{
			QString msg("Do you want to show the next %1 messages?");
			msg = msg.arg(errorPagingSize);
			int userAnswer = QMessageBox::question(m_outputWidget->topLevelWidget(), STR_DESPOT_WARNING, msg, 
															  QMessageBox::Yes | QMessageBox::YesToAll | 
															  QMessageBox::No, 
															  QMessageBox::Yes);

			if (userAnswer == QMessageBox::Yes)
			{
				//the user wants to see the next page of errors; reset the error counter for the new page
				crtPageErrCount = 0;
				continue;
			}
			else if (userAnswer == QMessageBox::YesToAll)
			{
				pageErrors = false;							
				continue;
			}
			else if (userAnswer == QMessageBox::No)
			{
				//the user doesn't want to see anymore errors
				m_outputWidget->writeLine(
					(errorsRemaining == 1) ? 
						QString("1 message has not been displayed.") : 
						QString("%1 messages have not been displayed.").arg(errorsRemaining));
				break;
			}
			else
			{
				assert(false);
				//assume the user doesn't want to see anymore errors
				m_outputWidget->writeLine(
					(errorsRemaining == 1) ? 
						QString("1 message has not been displayed.") : 
						QString("%1 messages have not been displayed.").arg(errorsRemaining));
				break;
			}
		}

	}

	m_outputWidget->writeLine("");
}

#endif

void OutputUiPart::showTime(int time)
{
	stringstream ss;
	ss << "Total computing time: " << time << " second(s)";

	m_outputWidget->writeLine(QString::fromStdString(ss.str()));
}

}

