/*************************************************************************
  FILE:  BddHiscLowSub3.cpp
  DESCR: Verification and synthesis for low-levels
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#include "BddHiscLowSub.h"
#include "BddHiscSub.h"
#include "BddHiscPubfunc.h"
#include "BddHiscType.h"
#include <fdd.h>
#include "BddHiscProject.h"
#include "BddHiscErrmsg.h"
#include <string>
#include <math.h>
#ifdef _WIN32
#include <winsock.h>
#include <time.h>
#include <sys/types.h>
#include <sys/timeb.h>
#else
#include <sys/time.h>
#endif

//#include "BddGetTime.h"

using namespace std;


namespace BDDHISC
{

#ifdef _WIN32
extern void gettimeofday(struct timeval* t,void* timezone);
#endif

extern CProject *pPrj;

/**
 * DESCR:   Verify whether a high level is level-wise controllable, 
 *          nonblocking and  p4, p5 and p6 satisfied or not.
 * PARA:    showtrace:show a trace to a bad state or not(not implemented)(input)
 *          superinfo: returned verification info (see BddHisc.h)(output)   
 *          savetype: save syn-product or not (See BddHisc.h)(input)
 *          savepath: where to save syn-product(input)
 *          testType: specifies which tests should be run on low-level
 * RETURN:  0: sucess <0: fail
 * ACCESS:  public
 */
int CLowSub::VeriSub(const HISC_TRACETYPE showtrace, HISC_SUPERINFO & superinfo, 
		     const HISC_SAVEPRODUCTTYPE savetype, const
		     string& savepath, const HISC_TESTTYPE testType,Hisc_ChkInfo& checkInfo)
{
	int iRet = 0;
	int iErr = 0;
	//Initialize the BDD data members
	CSub::InitBddFields();
	InitBddFields();
	bdd bddReach = bddfalse;
	string sErr;
	
	#ifdef DEBUG_TIME
	timeval tv1, tv2;
	#endif
	
	try
	{
		//Make transition bdds
		if (MakeBdd() < 0)
			throw -1;

		if ((testType == HISC_DOICONSIS) || (testType ==
		  HISC_DOINTFCHK) || (testType == HISC_DOALL))
		  {

		    //Check command pair interface
		    if (CheckIntf() < 0)
		      throw -1;
		  }


		// if just checking intf, doing the bddreach is not
		// efficient.  Remove in future including the
		// saveproduct stuff.

		
		bdd bddConBad = bddfalse;
		bdd bddP4Bad = bddfalse;
		bdd bddP5 = bddfalse;
		bdd bddP6 = bddfalse;
		
		bdd bddCoreach = bddfalse;
		
		//compute bddReach	
		#ifdef DEBUG_TIME
		cout << endl << "Computing reachable subpredicate..." << endl;
		gettimeofday(&tv1, NULL);
		#endif

		bddReach = r(bddtrue, iErr);
		if (iErr < 0)
			throw -1;

		#ifdef DEBUG_TIME
		gettimeofday(&tv2, NULL);
		cout << "R: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
		cout << "bddReach states:" 
			<< bdd_satcount(bddReach)/pow((double)2, double(m_iNumofBddNormVar)) 
			<< endl;
		cout << "bddReach Nodes:" << bdd_nodecount(bddReach) << endl << endl;
		#endif
			
		m_bddMarking &= bddReach;
		
		if ((testType == HISC_DOLWCONT) || (testType == HISC_DOALL))
		  {
		    // check lw-cont
		    //Initialize controllable bddBad

#ifdef DEBUG_TIME
		    cout << "Verifying controllablity..." << endl;
		    gettimeofday(&tv1, NULL);
#endif

		    bddConBad = bddfalse;
		    if (VeriConBad(bddConBad, bddReach, sErr) < 0)
		      throw -1;

#ifdef DEBUG_TIME
		    gettimeofday(&tv2, NULL);
		    cout << "VERI_CON: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
#endif

		    //check if any reachable states belong to bad states
		    if (bddConBad != bddfalse)
		      {
			BadStateInfo(bddConBad, HISC_VERI_LOW_UNCON, showtrace,checkInfo, sErr);
			throw -2;
		      }
		  }

		if ((testType == HISC_DOICONSIS) || (testType == HISC_DOALL))
		  {
		    // verify iconsist property 4

#ifdef DEBUG_TIME
		    cout << "Verifying Point 4..." << endl;
		    gettimeofday(&tv1, NULL);
#endif
		    
		    //Initialize P4 bddBad
		    if (VeriP4Bad(bddP4Bad, bddReach, sErr) < 0)
		      throw -1;

#ifdef DEBUG_TIME
		    gettimeofday(&tv2, NULL);
		    cout << "VERI_P4: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
#endif
		    
		    //check if any reachable states belong to bad states
		    if (bddP4Bad != bddfalse)
		      {
			BadStateInfo(bddP4Bad, HISC_VERI_LOW_P4FAILED, showtrace,checkInfo, sErr);
			throw -3;
		      }
		  }


                if (((testType == HISC_DOLWNONBLK) || (testType == HISC_DOALL)) &&
                    (!extractionSystemSkipTest()))
		  {
		    // verify lw-nonblk

		    //Computing CR()
#ifdef DEBUG_TIME
		    cout << "Verifying Nonblocking..." << endl;
		    gettimeofday(&tv1, NULL);
#endif

		    bddCoreach = cr(m_bddMarking, bddReach, ALL_EVENT, iErr);
		    if (iErr != 0)
		      throw -1;

#ifdef DEBUG_TIME
		    gettimeofday(&tv2, NULL);
		    cout << "VERI_NONBLOCKING: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
#endif

		    //check if the system is nonblocking
		    if (bddReach != bddCoreach)
		      {
			BadStateInfo(bddReach - bddCoreach, HISC_VERI_LOW_BLOCKING, showtrace,checkInfo, sErr);
			throw -4;
		      }
		  }
                else if (((testType == HISC_DOLWNONBLK) || (testType == HISC_DOALL)) &&
                    (extractionSystemSkipTest()))
                {
                    cout << "SKIPPED LOW-LEVEL LW NONBLK TEST" << endl;
                }

		if ((testType == HISC_DOICONSIS) || (testType == HISC_DOALL))
		  {
		    //verify iconsist properties 5-6

		    //Computing P6()
#ifdef DEBUG_TIME
		    cout << "Verifying Point 6..." << endl;
		    gettimeofday(&tv1, NULL);
#endif

		    bddP6 = p6(bddReach, iErr);
		    if (iErr != 0)
		      throw -1;

#ifdef DEBUG_TIME
		    gettimeofday(&tv2, NULL);
		    cout << "VERI_P6: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
#endif

		    if (bddP6 != bddReach)
		      {
			BadStateInfo(bddReach - bddP6, HISC_VERI_LOW_P6FAILED, showtrace,checkInfo, sErr );
			throw -5;
		      }

		
		    //Computing P5()
#ifdef DEBUG_TIME
		    cout << "Verifying Point 5..." << endl;
		    gettimeofday(&tv1, NULL);
#endif

		    bddP5 = p5(bddReach, iErr);

#ifdef DEBUG_TIME
		    gettimeofday(&tv2, NULL);
		    cout << "VERI_P5: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
#endif

		    if (iErr != 0)
		      throw -1;
		    if (bddP5 != bddReach)
		      {
			BadStateInfo(bddReach - bddP5, HISC_VERI_LOW_P5FAILED, showtrace,checkInfo);
			throw -6;
		      }
		  }

		//always execute remaining portion of function
		//final synchronous product;
		m_bddSuper = bddReach;
		
		//save supervisor
		superinfo.statesize = bdd_satcount(m_bddSuper)/pow((double)2, double(m_iNumofBddNormVar));
		superinfo.nodesize =  bdd_nodecount(m_bddSuper);
		if (savetype != HISC_NOTSAVEPRODUCT)
		{
			if (SaveSuper(m_bddSuper, HISC_SAVESUPER_AUTOMATA, savepath) < 0) 
				throw -1;
		}
	}
	catch (int iResult)
	{
		if (iResult < -1)
		{
			superinfo.statesize = bdd_satcount(bddReach)/pow((double)2, double(m_iNumofBddNormVar));
			superinfo.nodesize =  bdd_nodecount(bddReach);
			if (savetype != HISC_NOTSAVEPRODUCT)
				SaveSuper(bddReach, HISC_SAVESUPER_AUTOMATA, savepath);
		}

		iRet = -1;
	}
	ClearBddFields();
	CSub::ClearBddFields();
	bdd_done();		
	return iRet;
}

/**
 * DESCR:   Synthesize a supervisor for this low-level. The superivsor states is
 *          saved in m_bddSuper.
 * PARA:    computemethod: first compute reachable states or not (See BddHisc.h)
 *                         (input)
 *          superinfo: returned synthesis info (see BddHisc.h)(output)  
 *          savetype: how to save synthesized supervisor (See BddHisc.h)(input)
 *          savepath: where to save syn-product(input)
 * RETURN:  0: sucess <0: fail
 * ACCESS:  public
 */
int CLowSub::SynSuper(const HISC_COMPUTEMETHOD computemethod, 
                      HISC_SUPERINFO &superinfo, 
                      const HISC_SAVESUPERTYPE savetype, 
                      const string& savepath)
{
	bdd bddSuper = bddfalse;
	
	bool bFirstLoop = true;
	bdd bddK = bddfalse;
	bdd bddReach = bddfalse;
	int iRet = 0;
	int iErr = 0;
	//Initialize the BDD data memebers
	CSub::InitBddFields();
	InitBddFields();

	#ifdef DEBUG_TIME
	int iCount = 0;
	timeval tv1, tv2;
	#endif

	try
	{
		iRet = 0;
                //Make transition bdds (already includes LD events)
		if (MakeBdd() < 0)
			throw -1;
			
                //Check command pair interface (also includes LD checks)
		if (CheckIntf() < 0)
			throw -1;
			
		//Initialize bddBad
		bdd bddBad = bddfalse;
		if (GenConBad(bddBad) < 0)
			throw -1;
		if (GenP4Bad(bddBad) < 0)
			throw -1;
			
		if (computemethod == HISC_ONREACHABLE)
		{

			#ifdef DEBUG_TIME
			cout << endl << "Computing initial reachable subpredicate..." << endl;
			gettimeofday(&tv1, NULL);
			#endif

			bddReach = r(bddtrue, iErr);
			if (iErr < 0)
				throw -1;
			//bdd_reorder(BDD_REORDER_WIN2ITE);
			
			#ifdef DEBUG_TIME
			gettimeofday(&tv2, NULL);
			cout << "r: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
			cout << "bddReach states:" 
				<< bdd_satcount(bddReach)/pow((double)2, double(m_iNumofBddNormVar)) 
				<< endl;
			cout << "bddReach Nodes:" << bdd_nodecount(bddReach) << endl;
			#endif
			
			bddBad &= bddReach;

			#ifdef DEBUG_TIME
			cout << endl << "Initial bddBad subpredicate:"
				<< bdd_satcount(bddBad)/pow((double)2, double(m_iNumofBddNormVar))<< endl;
			cout << "Initial bddBad Nodes:" << bdd_nodecount(bddBad) << endl;
			#endif

			do
			{
				bddK = bddBad;
				
				//controllable, p4, nonblocking
				#ifdef DEBUG_TIME
				cout << endl << "{{{{{{{{{{{{{{{{{external loops:" << ++iCount << "}}}}}}}}}}}}}}}}}" << endl;
				cout << "Computing the fixpoint of controllability, P4 and nonblocking..." << endl;
				gettimeofday(&tv1, NULL);
				#endif
				
				if (SynPartSuper(computemethod, bddReach, bddBad) < 0)
					throw -1;
				bddBad &= bddReach;

				#ifdef DEBUG_TIME
				gettimeofday(&tv2, NULL);
				cout << "SYN_PART: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
				cout << "bddBad states:" 
					<< bdd_satcount(bddBad)/pow((double)2, double(m_iNumofBddNormVar)) 
					<< endl;
				cout << "bddBad Nodes:" << bdd_nodecount(bddBad) << endl << endl;
				#endif

				//p6
				#ifdef DEBUG_TIME
				cout << endl << "Computing P6 satisfied subpredicate..." << endl;
				gettimeofday(&tv1, NULL);
				#endif
				
				bddBad = bdd_not(p6(bddReach - bddBad, iErr));
				if (iErr < 0)
					throw -1;
				bddBad &= bddReach;
					
				#ifdef DEBUG_TIME
				gettimeofday(&tv2, NULL);
				cout << "P6: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
				cout << "bddBad states:" 
					<< bdd_satcount(bddBad)/pow((double)2, double(m_iNumofBddNormVar)) 
					<< endl;
				cout << "bddBad Nodes:" << bdd_nodecount(bddBad) << endl;
				#endif
	
				//p5
				#ifdef DEBUG_TIME
				cout << endl << "Computing P5 satisfied subpredicate..." << endl;
				gettimeofday(&tv1, NULL);
				#endif

				bddBad = bdd_not(p5(bddReach - bddBad, iErr));
				if (iErr < 0)
					throw -1;
				bddBad &= bddReach;

				#ifdef DEBUG_TIME
				gettimeofday(&tv2, NULL);
				cout << "P5: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
				cout << "bddBad states:" 
					<< bdd_satcount(bddBad)/pow((double)2, double(m_iNumofBddNormVar)) 
					<< endl;
				cout << "bddBad Nodes:" << bdd_nodecount(bddBad) << endl;
				#endif
				
				bFirstLoop = false;
	
			} while (bddBad != bddK);

			#ifdef DEBUG_TIME
			cout << endl << "Computing the last time of reachable subpredicate..." << endl;
			gettimeofday(&tv1, NULL);
			#endif

			m_bddSuper = r(bddReach - bddBad, iErr);
			if (iErr < 0)
				throw -1;

			#ifdef DEBUG_TIME
			gettimeofday(&tv2, NULL);
			cout << "last r: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
			cout << "#########################################################" << endl << endl;
			#endif
		}
		else
		{
			#ifdef DEBUG_TIME
			cout << endl << "Initial bddBad subpredicate:"
				<< bdd_satcount(bddBad)/pow((double)2, double(m_iNumofBddNormVar))<< endl;
			cout << "Initial bddBad Nodes:" << bdd_nodecount(bddBad) << endl;
			#endif
			//synthesis
			do
			{
				bddK = bddBad;
				
				//controllable, p4, nonblocking
				#ifdef DEBUG_TIME
				cout << endl << "{{{{{{{{{{{{{{{{{external loops:" << ++iCount << "}}}}}}}}}}}}}}}}}" << endl;
				cout << "Computing the fixpoint of controllability, P4 and nonblocking..." << endl;
				gettimeofday(&tv1, NULL);
				#endif
				
				//controllable, p4, nonblocking
				if (SynPartSuper(computemethod, bddBad, bddBad) < 0)
					throw -1;

				#ifdef DEBUG_TIME
				gettimeofday(&tv2, NULL);
				cout << "SYN_PART: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
				cout << "bddBad states:" 
					<< bdd_satcount(bddBad)/pow((double)2, double(m_iNumofBddNormVar)) 
					<< endl;
				cout << "bddBad Nodes:" << bdd_nodecount(bddBad) << endl << endl;
				#endif
				
				//p6
				#ifdef DEBUG_TIME
				cout << endl << "Computing P6 satisfied subpredicate..." << endl;
				gettimeofday(&tv1, NULL);
				#endif

				bddBad = bdd_not(p6(bdd_not(bddBad), iErr));
				if (iErr < 0)
					throw -1;
	
				#ifdef DEBUG_TIME
				gettimeofday(&tv2, NULL);
				cout << "P6: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
				cout << "bddBad states:" 
					<< bdd_satcount(bddBad)/pow((double)2, double(m_iNumofBddNormVar)) 
					<< endl;
				cout << "bddBad Nodes:" << bdd_nodecount(bddBad) << endl;
				#endif

				//p5
				#ifdef DEBUG_TIME
				cout << endl << "Computing P5 satisfied subpredicate..." << endl;
				gettimeofday(&tv1, NULL);
				#endif

				bddBad = bdd_not(p5(bdd_not(bddBad), iErr));
				if (iErr < 0)
					throw -1;
				
				#ifdef DEBUG_TIME
				gettimeofday(&tv2, NULL);
				cout << "P5: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
				cout << "bddBad states:" 
					<< bdd_satcount(bddBad)/pow((double)2, double(m_iNumofBddNormVar)) 
					<< endl;
				cout << "bddBad Nodes:" << bdd_nodecount(bddBad) << endl;
				#endif

				bFirstLoop = false;
	
			} while (bddBad != bddK);
			
			#ifdef DEBUG_TIME
			cout << endl << "Computing the last time of reachable subpredicate..." << endl;
			gettimeofday(&tv1, NULL);
			#endif

			m_bddSuper = r(bdd_not(bddBad), iErr);

			#ifdef DEBUG_TIME
			gettimeofday(&tv2, NULL);
			cout << "last r: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
			cout << "#########################################################" << endl << endl;
			#endif
		}
		m_bddMarking &= m_bddSuper;
		m_bddInit &= m_bddSuper;
		
		//save supervisor
		superinfo.statesize = bdd_satcount(m_bddSuper)/pow((double)2, double(m_iNumofBddNormVar));
		superinfo.nodesize =  bdd_nodecount(m_bddSuper);
		if (savetype != HISC_SAVESUPER_NONE)
		{
			if (SaveSuper(m_bddSuper, savetype, savepath) < 0) 
				throw -1;
		}
	}
	catch( int iErr)
	{
		iRet = -1;
	}
	ClearBddFields();
	CSub::ClearBddFields();
	bdd_done();		
	return iRet;
}

/**
 * DESCR:   Does part of the sythesis work, i.e. controllable, p4, nonblocking
 * PARA:    computemethod: first compute reachable states or not (See BddHisc.h)
 *                         (input)
 *          bddReach: All the current reachable legal states
 *          bddBad: All the current bad states
 * RETURN:  0: sucess <0: fail
 * ACCESS:  private
 */
int CLowSub::SynPartSuper(const HISC_COMPUTEMETHOD computemethod, 
                          bdd & bddReach, bdd & bddBad)
{
	bool bFirstLoop = true;
	bdd bddK = bddtrue;
	int iErr = 0;

	#ifdef DEBUG_TIME
	int iCount = 0;
	timeval tv1, tv2;
	#endif

	try
	{
		if (computemethod == HISC_ONREACHABLE)
		{
			//compute controllable, p4, nonblocking fixpoint
			do
			{
				bddK = bddBad;
				
				//Computing [bddBad]
				#ifdef DEBUG_TIME
				cout << endl << "------------internal_loops:" << ++iCount << "----------------" << endl;
				cout << "Computing supremal controllable & P4 subpredicate..." << endl;
				gettimeofday(&tv1, NULL);
				#endif

				if (supcp(bddBad) < 0)
					throw -1;
				bddBad &= bddReach;

				#ifdef DEBUG_TIME
				gettimeofday(&tv2, NULL);
				cout << "supcp: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
				cout << "bddBad states:" 
					<< bdd_satcount(bddBad)/pow((double)2, double(m_iNumofBddNormVar)) 
					<< endl;
				cout << "bddBad Nodes:" << bdd_nodecount(bddBad) << endl;
				#endif

				if (bddK == bddBad && bFirstLoop == false)
					break;
					
				//Computing CR(not(bddBad))
				bdd bddTemp = bddReach - bddBad;

				#ifdef DEBUG_TIME
				cout << endl << "bddGood states:" 
					<< bdd_satcount(bddTemp)/pow((double)2, double(m_iNumofBddNormVar)) 
					<< endl;
				cout << "bddGood Nodes:" << bdd_nodecount(bddTemp) << endl;
				cout << endl << "Computing coreachable subpredicate..." << endl;
				gettimeofday(&tv1, NULL);
				#endif

				bddBad = bdd_not(cr(m_bddMarking, bddTemp, ALL_EVENT, iErr));
				if (iErr != 0)
					throw -1;
				bddBad &= bddReach;
				bFirstLoop = false;

				#ifdef DEBUG_TIME
				gettimeofday(&tv2, NULL);
				cout << "cr: " << (tv2.tv_sec - tv1.tv_sec) << "seconds." << endl;
				cout << "bddBad states:" 
					<< bdd_satcount(bddBad)/pow((double)2, double(m_iNumofBddNormVar)) 
					<< endl;
				cout << "bddBad Nodes:" << bdd_nodecount(bddBad) << endl;
				#endif
			} while (bddBad != bddK);
		}
		else
		{
			//compute controllable, p4, nonblocking fixpoint
			do
			{
				bddK = bddBad;
				
				//Computing [bddBad]
				if (supcp(bddBad) < 0)
					throw -1;
				
				if (bddK == bddBad && bFirstLoop == false)
					break;
					
				//Computing CR(not(bddBad))
				bddBad = bdd_not(cr(m_bddMarking, bdd_not(bddBad), ALL_EVENT, iErr));
				if (iErr != 0)
					throw -1;
				
				bFirstLoop = false;
		
			} while (bddBad != bddK);
		}
	}
	catch (int)
	{
		return -1;
	}
	return 0;
}

/**
 * DESCR:   Compute the initial bad states(Bad_{L_j})(uncontrollable event part)
 * PARA:    bddConBad: BDD containing all the bad states (output)
 * RETURN:  0: sucess -1: fail
 * ACCESS:  private
 */
int CLowSub::GenConBad(bdd &bddConBad)
{
    try
    {
        bdd bddPlantTrans = bddfalse;
        bdd bddSpecTrans = bddfalse;
        
        for (int k = R_EVENT; k < NUMBER_OF_EVENTS; k++)
        {
            for (int i = 0; i < m_usiMaxUnCon[k]/ 2; i++)
            {
                //Get spec transition predicate
                bddSpecTrans = bdd_exist(m_pbdd_UnConTrans[k][i], 
                                    m_pbdd_UnConPlantVar[k][i]);
                bddSpecTrans = bdd_exist(bddSpecTrans, 
                                    m_pbdd_UnConPlantVarPrim[k][i]);
                
                //Compute illegal state predicate for each uncontrollable event
                bddConBad |= bdd_exist(m_pbdd_UnConPlantTrans[k][i], 
                                        m_pbdd_UnConPlantVarPrim[k][i]) & 
                             bdd_not(bdd_exist(bddSpecTrans, 
                                        bdd_exist(m_pbdd_UnConVarPrim[k][i], 
                                        m_pbdd_UnConPlantVarPrim[k][i])));
            }
        }
    }
    catch(...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error during generating controllable bad states.";
        pPrj->SetErr(sErr, HISC_LOWERR_GENCONBAD);
        return -1;
    }
    return 0;
}

/** 
 * DESCR:   Test if there are any bad states in the reachable states
 *          (Uncontorllable event part of Bad_{L_j})
 * PARA:    bddConBad: BDD containing tested bad states(output). 
 *                     Initially, bddBad should be bddfalse.
 *          bddReach: BDD containing all reachable states 
 *                    in this low-level(input)
 *          vsErr: returned errmsg(output)
 * RETURN:  0: sucess -1: fail
 * ACCESS:  private
 */
int CLowSub::VeriConBad(bdd &bddConBad, const bdd &bddReach, string & vsErr)
{
    try
    {
        bdd bddSpecTrans = bddfalse;
        
        for (int k = R_EVENT; k < NUMBER_OF_EVENTS; k++)
        {
            for (int i = 0; i < m_usiMaxUnCon[k]/ 2; i++)
            {
                //Get spec transition predicate
                bddSpecTrans = bdd_exist(m_pbdd_UnConTrans[k][i], 
                                    m_pbdd_UnConPlantVar[k][i]);
                bddSpecTrans = bdd_exist(bddSpecTrans, 
                                    m_pbdd_UnConPlantVarPrim[k][i]);
                
                //Compute illegal state predicate for each uncontrollable event
                bddConBad |= bdd_exist(m_pbdd_UnConPlantTrans[k][i], 
                                        m_pbdd_UnConPlantVarPrim[k][i]) & 
                             bdd_not(bdd_exist(bddSpecTrans, 
                                     bdd_exist(m_pbdd_UnConVarPrim[k][i], 
                                     m_pbdd_UnConPlantVarPrim[k][i])));
                bddConBad &= bddReach;
                if (bddConBad != bddfalse)
                {
                    vsErr = "Blocking uncontrollable event: ";
                    vsErr += SearchEventName((EVENTSUB)k, (i + 1) * 2);
                    throw -1;
                }
            }
        }
    }
    catch(int)
    {
    }
    catch(...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error during generating controllable bad states.";
        pPrj->SetErr(sErr, HISC_LOWERR_GENCONBAD);
        return -1;
    }
    return 0;
}

/**
 * DESCR:   Compute the initial bad states(Bad_{L_j})(request event part)
 * PARA:    bddConBad: BDD containing all the bad states (output)
 * RETURN:  0: sucess -1: fail
 * ACCESS:  private
 */
int CLowSub::GenP4Bad(bdd &bddP4Bad)
{
    try
    {
        bdd bddLowTrans = bddfalse;
        
        for (int i = 0; i < m_usiMaxUnCon[R_EVENT]/ 2; i++)
        {
            //Get low level sub transition predicate
            bddLowTrans = bdd_exist(m_pbdd_UnConTrans[R_EVENT][i], m_bddIVar); 
            bddLowTrans = bdd_exist(bddLowTrans, m_bddIVarPrim);
            
            //Compute the illegal state predicate for each uncontrollable event
            bddP4Bad |= bdd_exist(m_pbdd_RTrans[0][i], m_bddIVarPrim) & 
                        bdd_not(bdd_exist(bddLowTrans, 
                            bdd_exist(m_pbdd_UnConVarPrim[R_EVENT][i], 
                            m_bddIVarPrim)));
        }
        for (int i = 0; i < ((unsigned short)(m_usiMaxCon[R_EVENT] + 1))/ 2;i++)
        {
            //Get low level sub transition predicate
            bddLowTrans = bdd_exist(m_pbdd_ConTrans[R_EVENT][i], m_bddIVar); 
            bddLowTrans = bdd_exist(bddLowTrans, m_bddIVarPrim);
            
            //Compute the illegal state predicate for each uncontrollable event
            bddP4Bad |= bdd_exist(m_pbdd_RTrans[1][i], m_bddIVarPrim) & 
                        bdd_not(bdd_exist(bddLowTrans, 
                            bdd_exist(m_pbdd_ConVarPrim[R_EVENT][i], 
                            m_bddIVarPrim)));
        }
    }
    catch(...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error during generating point 4 bad states.";
        pPrj->SetErr(sErr, HISC_LOWERR_GENP4BAD);
        return -1;
    }
    return 0;
}

/** 
 * DESCR:   Test if there are any bad states in the reachable states
 *          (answer event part of Bad_{L_j})
 * PARA:    bddP4Bad: BDD containing tested bad states(output). 
 *                     Initially, bddBad should be bddfalse.
 *          bddReach: BDD containing all reachable states 
 *                    in this low-level (input)
 *          vsErr: returned errmsg(output)
 * RETURN:  0: sucess -1: fail
 * ACCESS:  private
 */
int CLowSub::VeriP4Bad(bdd &bddP4Bad, const bdd &bddReach, string &vsErr)
{
    try
    {
        bdd bddLowTrans = bddfalse;
        
        for (int i = 0; i < m_usiMaxUnCon[R_EVENT]/ 2; i++)
        {
            //Get low level sub transition predicate
            bddLowTrans = bdd_exist(m_pbdd_UnConTrans[R_EVENT][i], m_bddIVar); 
            bddLowTrans = bdd_exist(bddLowTrans, m_bddIVarPrim);
            
            //Compute the illegal state predicate for each uncontrollable event
            bddP4Bad |= bdd_exist(m_pbdd_RTrans[0][i], m_bddIVarPrim) & 
                        bdd_not(bdd_exist(bddLowTrans, 
                            bdd_exist(m_pbdd_UnConVarPrim[R_EVENT][i], 
                            m_bddIVarPrim)));
            bddP4Bad &= bddReach;
            
            if (bddP4Bad != bddfalse)
            {
                vsErr = "Blocking request event: ";
                vsErr += SearchEventName(R_EVENT, (i + 1) * 2);
                return 0;
            }
        }
        for (int i = 0; i < ((unsigned short)(m_usiMaxCon[R_EVENT] + 1))/ 2;i++)
        {
            //Get low level sub transition predicate
            bddLowTrans = bdd_exist(m_pbdd_ConTrans[R_EVENT][i], m_bddIVar); 
            bddLowTrans = bdd_exist(bddLowTrans, m_bddIVarPrim);
            
            //Compute the illegal state predicate for each uncontrollable event
            bddP4Bad |= bdd_exist(m_pbdd_RTrans[1][i], m_bddIVarPrim) & 
                        bdd_not(bdd_exist(bddLowTrans, 
                            bdd_exist(m_pbdd_ConVarPrim[R_EVENT][i], 
                            m_bddIVarPrim)));
            bddP4Bad &= bddReach;
            
            if (bddP4Bad != bddfalse)
            {
                vsErr = "Blocking request event: ";
                vsErr += SearchEventName(R_EVENT, i * 2 + 1);
                return 0;
            }
        }
    }
    catch(...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error during generating point 4 bad states.";
        pPrj->SetErr(sErr, HISC_LOWERR_GENP4BAD);
        return -1;
    }
    return 0;
}


/**
 * DESCR:   compute PLPC(P)
 * PARA:    bddP : BDD for predicate P. (input and output(=PHIC(P)))
 * RETURN:  0: sucess -1: fail
 * ACCESS:  private
 */
int CLowSub::supcp(bdd & bddP) 
{
    bdd bddK1 = bddfalse;
    bdd bddK2 = bddfalse;
    int iEvent = 0;
    int iIndex = 0;
    EVENTSUB EventSub;
    
    try
    {
        while (bddP != bddK1)
        {
            bddK1 = bddP;
            for (int i = 0; i < this->GetNumofDES(); i++)
            {
                bddK2 = bddfalse;
                while (bddP != bddK2)
                {
                    bddK2 = bddP;
                    for (int j = 0; j < m_pDESArr[i]->GetNumofEvents(); j++)
                    {
                        iEvent = (m_pDESArr[i]->GetEventsArr())[j];
                        EventSub = (EVENTSUB)(iEvent >> 28);
                        iIndex = iEvent & 0x0000FFFF;
                        if ( iEvent % 2 == 0)
                        {
                            iIndex = (iIndex - 2) / 2;
                            bddP |= 
                                bdd_appex(m_pbdd_UnConTrans[EventSub][iIndex], 
                                         bdd_replace(bddK2, 
                                               m_pPair_UnCon[EventSub][iIndex]), 
                                         bddop_and, 
                                         m_pbdd_UnConVarPrim[EventSub][iIndex]);
                        }
                        else if ( EventSub == R_EVENT )
                        {
                            iIndex = (iIndex - 1) / 2;
                            bddP |= 
                                bdd_appex(m_pbdd_ConTrans[EventSub][iIndex], 
                                          bdd_replace(bddK2, 
                                                m_pPair_Con[EventSub][iIndex]), 
                                          bddop_and, 
                                          m_pbdd_ConVarPrim[EventSub][iIndex]);
                        }
                    }
                }
            }
        }
    }
    catch (...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error during computing PLPC(P).";
        pPrj->SetErr(sErr, HISC_LOWERR_SUPCP);
        return -1;
    }
    return 0;
}

/**
 * DESCR:   compute CR(G_{L_j}, P', \Sigma', P)
 * PARA:    bddPStart: P' (input)
 *          bddP: P (input)
 *          viEventSub: \Sigma' (input) (0,1,2,3) <-> (H,R,A,L) ALL_EVENT<->All
 *          iErr: returned Errcode (0: success <0: fail)(output)
 * RETURN:  BDD for CR(G_{L_j}, P', \Sigma', P)
 * ACCESS:  private
 */
bdd CLowSub::cr(const bdd & bddPStart, const bdd & bddP, 
                const int viEventSub, int & iErr)
{
	try
	{
		bdd bddK = bddP & bddPStart;
		bdd bddK1 = bddfalse;
		bdd bddK2 = bddfalse;
		bdd bddKNew = bddfalse;
		int iEvent = 0;
		int iIndex = 0;
		EVENTSUB EventSub;
		
		#ifdef DEBUG_TIME
		int iLoopCount = 0;
		timeval tv1, tv2;
		#endif
		
		while (bddK != bddK1)
		{
			#ifdef DEBUG_TIME
			gettimeofday(&tv1, NULL);
			#endif

			bddK1 = bddK;
			
			for (int i = 0; i < this->GetNumofDES(); i++)
			{
				bddK2 = bddfalse;
				while (bddK != bddK2)
				{
					bddKNew = bddK - bddK2;
					bddK2 = bddK;
					for (int j = 0; j < m_pDESArr[i]->GetNumofEvents(); j++)
					{
						iEvent = (m_pDESArr[i]->GetEventsArr())[j];
						EventSub = (EVENTSUB)(iEvent >> 28);
						if (viEventSub == ALL_EVENT || viEventSub == (int)EventSub)
						{
							iIndex = iEvent & 0x0000FFFF;
							if (iEvent % 2 == 0)
							{
								iIndex = (iIndex - 2) / 2;
								bddK |= bdd_appex(m_pbdd_UnConTrans[EventSub][iIndex], 
									bdd_replace(bddKNew, m_pPair_UnCon[EventSub][iIndex]), 
									bddop_and, m_pbdd_UnConVarPrim[EventSub][iIndex])
									& bddP;
							}
							else
							{
								iIndex = (iIndex - 1) / 2;
								bddK |= bdd_appex(m_pbdd_ConTrans[EventSub][iIndex], 
									bdd_replace(bddKNew, m_pPair_Con[EventSub][iIndex]), 
									bddop_and, m_pbdd_ConVarPrim[EventSub][iIndex])
									& bddP;
							}
						}
					}
				}
			}
			#ifdef DEBUG_TIME
			gettimeofday(&tv2, NULL);
			cout << "CR: Iteration_" << ++iLoopCount << " nodes: " << bdd_nodecount(bddK);
			cout << "\t time: " << ((tv2.tv_sec - tv1.tv_sec) * 1000000.0 + (tv2.tv_usec - tv1.tv_usec))/1000000.0 << " s";
			cout << "\t states: " << bdd_satcount(bddK)/pow((double)2, double(m_iNumofBddNormVar)) << endl;
			#endif
		}
		return bddK;
	}
	catch (...)
	{
		string sErr = this->GetSubName();
		sErr += ": Error during computing coreachable.";
		pPrj->SetErr(sErr, HISC_LOWERR_COREACH);
		iErr = -1;
		return bddfalse;
	}
}


/**
 * DESCR:   compute R(G_{L_j}, P)
 * PARA:    bddP: P (input)
 *          iErr: returned Errcode (0: success <0: fail)(output)
 * RETURN:  BDD for R(G_{L_j}, P)
 * ACCESS:  private
 */
bdd CLowSub::r(const bdd &bddP, int &iErr)
{
	try
	{
		bdd bddK = bddP & m_bddInit;
		bdd bddK1 = bddfalse;
		bdd bddK2 = bddfalse;
		bdd bddKNew = bddfalse;
		int iEvent = 0;
		int iIndex = 0;
		EVENTSUB EventSub;
		
		#ifdef DEBUG_TIME
		int iLoopCount = 0;
		timeval tv1, tv2;
		#endif

		while (bddK != bddK1)
		{
			#ifdef DEBUG_TIME
			gettimeofday(&tv1, NULL);
			#endif

			bddK1 = bddK;
			
			for (int i = 0; i < this->GetNumofDES(); i++)
			{
				bddK2 = bddfalse;
				while (bddK != bddK2)
				{
					bddKNew = bddK-bddK2;
					bddK2 = bddK;
					
					for (int j = 0; j < m_pDESArr[i]->GetNumofEvents(); j++)
					{
						iEvent = (m_pDESArr[i]->GetEventsArr())[j];
						EventSub = (EVENTSUB)(iEvent >> 28);
						iIndex = iEvent & 0x0000FFFF;
						if (iEvent % 2 == 0)
						{
							iIndex = (iIndex - 2) / 2;
							bddK |= bdd_replace(
								bdd_appex(m_pbdd_UnConTrans[EventSub][iIndex], 
								bddKNew, bddop_and, m_pbdd_UnConVar[EventSub][iIndex]),
								m_pPair_UnConPrim[EventSub][iIndex]) & bddP;
						}
						else
						{
							iIndex = (iIndex - 1) / 2;
							bddK |= bdd_replace(
								bdd_appex(m_pbdd_ConTrans[EventSub][iIndex], 
								bddKNew, bddop_and, m_pbdd_ConVar[EventSub][iIndex]),
								m_pPair_ConPrim[EventSub][iIndex]) & bddP;
						}
					}
				}
			}
			#ifdef DEBUG_TIME
			gettimeofday(&tv2, NULL);
			cout << "R: Iteration_" << ++iLoopCount << " nodes: " << bdd_nodecount(bddK);
			cout << "\t time: " << ((tv2.tv_sec - tv1.tv_sec) * 1000000.0 + (tv2.tv_usec - tv1.tv_usec))/1000000.0 << " s";
			cout << "\t states: " << bdd_satcount(bddK)/pow((double)2, double(m_iNumofBddNormVar)) << endl;
			#endif
		}
		return bddK;
	}
	catch (...)
	{
		string sErr = this->GetSubName();
		sErr += ": Error during computing coreachable.";
		pPrj->SetErr(sErr, HISC_LOWERR_REACH);
		iErr = -1;
		return bddfalse;
	}
}

/**
 * DESCR:   Compute interface consistent condition 5 operator \Gamma_{p5_j}(P).
 * PARA:    bddGood: P (input)
 *          iErr: returned Errcode (0: success <0: fail)(output)
 * RETURN:  BDD for predicate \Gamma_{p5_j}(P)
 * ACCESS:  private
 */
bdd CLowSub::p5(const bdd& bddGood, int &iErr)
{
    int iLocalErr = 0;
    
    try
    {
        bdd bddPBad5 = bddfalse;
        bdd bddPalpha = bddfalse;
        bdd bddPCRalpha = bddfalse;
        bdd bddPrho = bddfalse;
        
        bddPair *pPair = bdd_newpair();
        SetBddPairs(pPair, m_bddIVar, m_bddIVarPrim);
        
        //Uncontrollable answer events
        for (int i = 0; i < m_usiMaxUnCon[A_EVENT] / 2; i++)
        {
            bddPalpha =  bdd_relprod(m_pbdd_UnConTrans[A_EVENT][i], 
                            bdd_replace(bddGood, m_pPair_UnCon[A_EVENT][i]),
                            m_pbdd_UnConVarPrim[A_EVENT][i]);
            bddPCRalpha = cr(bddPalpha, bddGood, (int)L_EVENT, iLocalErr);
            if (iLocalErr < 0)
                throw -1;

            for (int j = 0; 
                 j < ((unsigned short)(m_usiMaxCon[R_EVENT] + 1)) / 2; j++)
            {
                bddPrho = bdd_relprod(m_pbdd_ConTrans[R_EVENT][j],
                                        bdd_replace(bdd_not(bddPCRalpha), 
                                        m_pPair_Con[R_EVENT][j]),
                                        m_pbdd_ConVarPrim[R_EVENT][j]);
                
                bddPrho &= bdd_relprod(m_pbdd_ConTrans[R_EVENT][j], 
                                   bdd_replace(bdd_exist(m_pbdd_ATrans[0][i], 
                                   m_bddIVarPrim), pPair), 
                                   m_pbdd_ConVarPrim[R_EVENT][j]);
                bddPBad5 |= bddPrho;
            }

            for (int j = 0; j < m_usiMaxUnCon[R_EVENT] / 2; j++)
            {
                bddPrho = bdd_relprod(m_pbdd_UnConTrans[R_EVENT][j],
                                        bdd_replace(bdd_not(bddPCRalpha), 
                                        m_pPair_UnCon[R_EVENT][j]),
                                        m_pbdd_UnConVarPrim[R_EVENT][j]);
                
                bddPrho &= bdd_relprod(m_pbdd_UnConTrans[R_EVENT][j], 
                                   bdd_replace(bdd_exist(m_pbdd_ATrans[0][i], 
                                   m_bddIVarPrim), pPair), 
                                   m_pbdd_UnConVarPrim[R_EVENT][j]);
                bddPBad5 |= bddPrho;
            }
        }

        //Controllable answer events
        for (int i = 0; 
             i < ((unsigned short)(m_usiMaxCon[A_EVENT] + 1)) / 2; i++)
        {

            bddPalpha =  bdd_relprod(m_pbdd_ConTrans[A_EVENT][i], 
                            bdd_replace(bddGood, m_pPair_Con[A_EVENT][i]),
                            m_pbdd_ConVarPrim[A_EVENT][i]);
            bddPCRalpha = cr(bddPalpha, bddGood, (int)L_EVENT, iLocalErr);
            if (iLocalErr < 0)
                throw -1;

            for (int j = 0; 
                 j < ((unsigned short)(m_usiMaxCon[R_EVENT] + 1)) / 2; j++)
            {
                bddPrho = bdd_relprod(m_pbdd_ConTrans[R_EVENT][j],
                                        bdd_replace(bdd_not(bddPCRalpha), 
                                        m_pPair_Con[R_EVENT][j]),
                                        m_pbdd_ConVarPrim[R_EVENT][j]);
                
                bddPrho &= bdd_relprod(m_pbdd_ConTrans[R_EVENT][j], 
                                   bdd_replace(bdd_exist(m_pbdd_ATrans[1][i], 
                                   m_bddIVarPrim), pPair), 
                                   m_pbdd_ConVarPrim[R_EVENT][j]);
                bddPBad5 |= bddPrho;
            }

            for (int j = 0; j < m_usiMaxUnCon[R_EVENT] / 2; j++)
            {
                bddPrho = bdd_relprod(m_pbdd_UnConTrans[R_EVENT][j],
                                        bdd_replace(bdd_not(bddPCRalpha), 
                                        m_pPair_UnCon[R_EVENT][j]),
                                        m_pbdd_UnConVarPrim[R_EVENT][j]);
                
                bddPrho &= bdd_relprod(m_pbdd_UnConTrans[R_EVENT][j], 
                                   bdd_replace(bdd_exist(m_pbdd_ATrans[1][i], 
                                   m_bddIVarPrim), pPair), 
                                   m_pbdd_UnConVarPrim[R_EVENT][j]);
                bddPBad5 |= bddPrho;
            }
        }
        bdd_freepair(pPair);
        pPair = NULL;

        return bddGood - bddPBad5; 
    }
    catch (...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error during computing Gamma_{p5_j}(P).";
        pPrj->SetErr(sErr, HISC_LOWERR_P5);
        iErr = -1;
        return bddfalse;
    }
}

/**
 * DESCR:   Compute interface consistent condition P6 operator \Gamma_{p6_j}(P).
 * PARA:    bddGood: P (input)
 *          iErr: returned Errcode (0: success <0: fail)(output)
 * RETURN:  BDD for predicate \Gamma_{p6_j}(P)
 * ACCESS:  private
 */
bdd CLowSub::p6(const bdd& bddP, int &iErr)
{
    try
    {
        int iErr = 0;
        bdd bddPBad6 = bddfalse;
        
        bddPBad6 = (m_bddIntfMarking & bddP) - cr(m_bddMarking, bddP, (int)L_EVENT, iErr);
        if (iErr < 0)
            throw -1;
            
        return bddP - bddPBad6;
    }
    catch (...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error during computing Gamma_{p6_j}(P).";
        pPrj->SetErr(sErr, HISC_LOWERR_P6);
        iErr = -1;
        return bddfalse;
    }
}


} //end of namespace BDDHISC
