/*************************************************************************
  FILE:  BddSdLowSub3.cpp
  DESCR: Verification and synthesis for low-levels
  AUTH:  Raoguang Song, Yu Wang
  DATE:  (C) Jan, 2006, 2009
*************************************************************************/
#include "BddSdLowSub.h"
#include "BddSdErrmsg.h"
#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"


namespace BDDSD
{

  // do I need the lines below? or should I use the 
  // #include "BddGetTime.h"

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


extern CSub *pSub;

/**
 * DESCR:   Verify the SD controllable properties.
 * PARA:    showtrace:show a trace to a bad state or not(not implemented)(input)
 *          superinfo: returned verification info (see BddSd.h)(output)
 *          savetype: save syn-product or not (See BddSd.h)(input)
 *          savepath: where to save syn-product(input)
 * RETURN:  0: sucess <0: fail
 * ACCESS:  public
 */
  int CLowSub::VeriSub(const HISC_TRACETYPE showtrace, HISC_SUPERINFO
  & superinfo, SD_TESTTYPE testType)
{
  int iRet = 0;
  int iErr = 0;
  //Initialize the BDD data memebers
  CSub::InitBddFields();
  InitBddFields();
  bdd bddReach = bddfalse;
  string sErr;

#ifdef DEBUG_TIME
  timeval tv1, tv2;
#endif
  
  try
    {
      //Make transition bdds
      if (MakeBdd() < 0)
	throw -1;
      
      bdd bddConBad = bddfalse;
      bdd bddBalemiBad = bddfalse;
      bdd bddCoreach = bddfalse;
      bdd bddNBBad = bddfalse;
      bdd bddALFBad = bddfalse;
      bdd bddPTBBad = bddfalse;
      bdd bddSDBad = 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 == SD_DOCONT) || (testType == SD_DONBandCONT) ||
	  (testType == SD_DOSDCONT) || (testType == SD_DOALL)) 
	{

#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, sErr);
	      throw -2;
	    }
	}

      if ((testType == SD_DONONBLK) || (testType == SD_DONBandCONT) ||
	  (testType == SD_DOALL)) 
	{

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

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

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

	  bddNBBad = bddReach & !bddCoreach;
	  if (bddfalse != bddNBBad)
	    {
	      BadStateInfo(bddNBBad, HISC_VERI_LOW_BLOCKING, showtrace);
	      throw -4;
	    }

	}

      if ((testType == SD_DOPCOMPL) || (testType == SD_DOALL)) 
	{

#ifdef DEBUG_TIME
	  cout << "Checking Plant Completeness Condition..." << endl;
	  gettimeofday(&tv1, NULL);
#endif

	  bddBalemiBad = bddfalse;
	  if (VeriBalemiBad(bddBalemiBad, bddReach, sErr) < 0)
            throw -1;

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

	  //check if any reachable states belong to Balemi bad states
	  if (bddBalemiBad != bddfalse)
	    {
	      //	      BadStateInfo(bddBalemiBad, HISC_VERI_LOW_CON, showtrace, sErr);
	      BadStateInfo(bddBalemiBad, HISC_VERI_LOW_PCOMPLT, showtrace, sErr);
		throw -2;
	    }

	}

      if ((testType == SD_DOALF) || (testType == SD_DOALL)) 
	{

	  // Checking if the system is ALF
#ifdef DEBUG_TIME
	  cout << "Verifying Activity Loop Free..." << endl;
	  gettimeofday(&tv1, NULL);
#endif

	  bddALFBad = bddfalse;
	  if (VeriALF(bddALFBad, bddReach, sErr) < 0)
            throw -1;

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

	  if (bddALFBad != bddfalse)
	    {
	      BadStateInfo(bddALFBad, HISC_VERI_LOW_ALF, showtrace, sErr);
	      throw -2;
	    }

	}

      if ((testType == SD_DOPTB) || (testType == SD_DOALL)) 
	{

	  // Checking if the system has proper timed behavior
#ifdef DEBUG_TIME
	  cout << "Verifying Proper Timed Behavior..." << endl;
	  gettimeofday(&tv1, NULL);
#endif

	  bddPTBBad = bddfalse;
	  if (VeriProperTimedBehavior(bddPTBBad, bddReach, sErr) < 0)
            throw -1;

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

	  if (bddPTBBad != bddfalse)
	    {
	      BadStateInfo(bddPTBBad, HISC_VERI_LOW_PTB, showtrace, sErr);
	      throw -2;
	    }
	}

      // RJL: I don't see an S-Singular specific function to separate
      //      out here.  I'm assuming that it is checked within
      //  Sd cont function. Will leave for Hamid to separate out.
      if ((testType == SD_DOSDCONT) || (testType == SD_DOALL) ||
	  (testType == SD_DOSSPROHIBB))
	{

	  // Checking SD Controllability
#ifdef DEBUG_TIME
	  cout << "Checking SD Controllability" << endl;
	  gettimeofday(&tv1, NULL);
#endif

	  int ret = CheckSDControllability(bddSDBad, bddReach, sErr);
	  if (-1 == ret)
            throw -1;

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

	  if (bddSDBad != bddfalse)
	    {
	      BadStateInfo(bddSDBad, ret, showtrace, sErr);
	      throw -2;
	    }

	}

		//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);
	}
	catch (int iResult)
	{
		if (iResult < -1)
		{
			superinfo.statesize = bdd_satcount(bddReach)/pow((double)2, double(m_iNumofBddNormVar));
			superinfo.nodesize =  bdd_nodecount(bddReach);
		}

		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, 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), 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})(uncontorlalble 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;

            for (int i = 0; i < m_usiMaxUnCon/ 2; i++)
            {
                //Compute illegal state predicate for each uncontrollable event
                bddConBad |= bdd_exist(m_pbdd_UnConPlantTrans[i],
                                        m_pbdd_UnConPlantVarPrim[i]) &
                             bdd_not(bdd_exist(m_pbdd_UnConSupTrans[i],
                                        bdd_exist(m_pbdd_UnConVarPrim[i],
                                        m_pbdd_UnConPlantVarPrim[i])));
            }
    }
    catch(...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error during generating controllable bad states.";
        pSub->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
    {
        int iErr = 0;

            for (int i = 0; i < m_usiMaxUnCon/ 2; i++)
            {
                //Compute illegal state predicate for each uncontrollable event
                bddConBad |= bdd_exist(m_pbdd_UnConPlantTrans[i],
                                        m_pbdd_UnConPlantVarPrim[i]) &
                             bdd_not(bdd_exist(m_pbdd_UnConSupTrans[i],
                                     bdd_exist(m_pbdd_UnConVarPrim[i],
                                     m_pbdd_UnConPlantVarPrim[i])));
                bddConBad &= bddReach;

                if (iErr < 0)
                {
                    throw -1;
                }

                if (bddConBad != bddfalse)
                {
                    vsErr = "Blocked uncontrollable event: ";
                    vsErr += SearchEventName((i + 1) * 2);
                    throw -1;
                }
            }

    }
    catch(int)
    {
    }
    catch(...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error during generating controllable bad states.";
        pSub->SetErr(sErr, HISC_LOWERR_GENCONBAD);
        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;

    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];

                        iIndex = iEvent & 0x0000FFFF;
                        if ( iEvent % 2 == 0)
                        {
                            iIndex = (iIndex - 2) / 2;
                            bddP |=
                                bdd_appex(m_pbdd_UnConTrans[iIndex],
                                         bdd_replace(bddK2,
                                               m_pPair_UnCon[iIndex]),
                                         bddop_and,
                                         m_pbdd_UnConVarPrim[iIndex]);
                        }
                    }
                }
            }
        }
    }
    catch (...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error during computing PLPC(P).";
        pSub->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, int & iErr)
{
	try
	{
		bdd bddK = bddP & bddPStart;
		bdd bddK1 = bddfalse;
		bdd bddK2 = bddfalse;
		bdd bddKNew = bddfalse;
		int iEvent = 0;
		int iIndex = 0;

		#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];

							iIndex = iEvent & 0x0000FFFF;
							if (iEvent % 2 == 0)
							{
								iIndex = (iIndex - 2) / 2;
								bddK |= bdd_appex(m_pbdd_UnConTrans[iIndex],
									bdd_replace(bddKNew, m_pPair_UnCon[iIndex]),
									bddop_and, m_pbdd_UnConVarPrim[iIndex])
									& bddP;
							}
							else
							{
								iIndex = (iIndex - 1) / 2;
								bddK |= bdd_appex(m_pbdd_ConTrans[iIndex],
									bdd_replace(bddKNew, m_pPair_Con[iIndex]),
									bddop_and, m_pbdd_ConVarPrim[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.";
		pSub->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;

		#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];

						iIndex = iEvent & 0x0000FFFF;
						if (iEvent % 2 == 0)
						{
							iIndex = (iIndex - 2) / 2;
							bddK |= bdd_replace(
								bdd_appex(m_pbdd_UnConTrans[iIndex], bddKNew, bddop_and,
                                    m_pbdd_UnConVar[iIndex]),
								m_pPair_UnConPrim[iIndex]) & bddP;
						}
						else
						{
							iIndex = (iIndex - 1) / 2;
							bddK |= bdd_replace(
								bdd_appex(m_pbdd_ConTrans[iIndex], bddKNew, bddop_and,
                                    m_pbdd_ConVar[iIndex]),
								m_pPair_ConPrim[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.";
		pSub->SetErr(sErr, HISC_LOWERR_REACH);
		iErr = -1;
		return bddfalse;
	}
}

} //end of namespace BDDSD
