/*************************************************************************
  FILE:  BddHiscHighSub2.cpp
  DESCR: Verification and synthesis for high-level
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#include <fdd.h>
#include <string>
#include <iostream>
#include "BddHiscErrmsg.h"
#include "BddHiscProject.h"
#include "BddHiscHighSub.h"
#include "BddHiscSub.h"
#include "BddHiscLowSub.h"
#include "BddHiscDES.h"
#include "BddHiscType.h"
#include "BddHiscPubfunc.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"

using namespace std;

namespace BDDHISC
{
    extern CProject *pPrj;

    /**
     * DESCR:   Verify whether a high level is level-wise controllable,
     *          nonblocking and p3 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 high-level
     * RETURN:  0: sucess <0: fail
     * ACCESS:  public
     */
    int CHighSub::VeriSub(const HISC_TRACETYPE showtrace,
                          HISC_SUPERINFO & superinfo,
                          const HISC_SAVEPRODUCTTYPE savetype,
                          const string& savepath,
                          const HISC_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
                //updated to support LD Events --H.I.
                if (MakeBdd() < 0)
                        throw -1;

                bdd bddBad = bddfalse;
                bdd bddCoreach = bddfalse;
                bdd bddBlocking = bddfalse;

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

                //Compute reachable events transition predicate
                //Updated to support LD Events --H.I.
                bddReach = r(bddtrue, iErr);
                if (iErr < 0)
                        throw -1;

                #ifdef DEBUG_TIME
                cout << "bddReach Nodes:" << bdd_nodecount(bddReach) << endl << endl;
                #endif

                #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

                //Marking and reachable state predicate --H.I.
                m_bddMarking &= bddReach;

                if ((testType == HISC_DOLWCONT) || (testType == HISC_DOALL))
                {
                    //test for lw-cont

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

                    //Updated to support LD Events --H.I.
                    bddBad = bddfalse;
                    if (VeriConBad(bddBad, 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
                    //Updated to look at LD event transitions --H.I.
                    if (bddBad != bddfalse)
                    {
                            BadStateInfo(bddBad, HISC_VERI_HIGH_UNCON, showtrace, sErr);
                            throw -2;
                    }
                }

                // always execute next line
                bddBad = bddfalse;

                if ((testType == HISC_DOICONSIS) || (testType == HISC_DOALL))
                {
                    //test Intf con point 3
                    //Initialize P3 bddBad

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

                    if (VeriP3Bad(bddBad, bddReach, sErr) < 0)
                            throw -1;

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

                    //check if any reachable states belong to bad states
                    if (bddBad != bddfalse)
                    {
                            BadStateInfo(bddBad, HISC_VERI_HIGH_P3FAILED, showtrace, sErr);
                            throw -3;
                    }
                }

                // always execute next line
                bddBad = bddfalse;


                if ((testType == HISC_DOLWNONBLK) || (testType == HISC_DOALL))
                {
                    // check lw-nonblk

                    //Computing CR(not(bddBad))
                    //now supports LD events --H.I.
                    #ifdef DEBUG_TIME
                    cout << "Verifying Nonblocking..." << endl;
                    gettimeofday(&tv1, NULL);
                    #endif

                    bddCoreach = cr(m_bddMarking, bddReach, ALL_EVENT_EXCEPT_LD, 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
                    bddBlocking = bddReach - bddCoreach;

                    if (bddBlocking != bddfalse)
                    {
                            BadStateInfo(bddBlocking, HISC_VERI_HIGH_BLOCKING, showtrace);
                            throw -4;
                    }
                }

                //always execute rest 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 high-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 CHighSub::SynSuper(const HISC_COMPUTEMETHOD computemethod,
                            HISC_SUPERINFO &superinfo,
                            const HISC_SAVESUPERTYPE savetype,
                            const string& savepath)
    {
            bool bFirstLoop = true;
            bdd bddK = bddfalse;
            bdd bddReach = bddfalse;
            bdd bddDead = bddfalse;
            int iRet = 0;
            int iErr = 0;

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

            //Initialize the BDD data memebers
            CSub::InitBddFields();
            InitBddFields();
            try
            {
                    iRet = 0;
                    //Make transition bdds
                    if (MakeBdd() < 0)
                            throw -1;

                    //Initialize bddBad
                    bdd bddBad = bddfalse;
                    if (GenConBad(bddBad) < 0)
                            throw -1;
                    if (GenP3Bad(bddBad) < 0)
                            throw -1;

                    if (computemethod == HISC_ONREACHABLE)  //always compute on reachable states
                    {
                            #ifdef DEBUG_TIME
                            cout << endl << "Computing initial 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;
                            #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

                            //compute controllable, p3, nonblocking fixpoint
                            do
                            {

                                    bddK = bddBad;

                                    #ifdef DEBUG_TIME
                                    cout << endl << "------------loops:" << ++iCount << "----------------" << endl;
                                    cout << "Computing supremal controllable & P3 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()
                                    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_EXCEPT_LD, 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);

                            #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  //first compute on coreachable states, then do reachable operation
                    {
                            #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

                            //compute controllable, p3, nonblocking fixpoint
                            do
                            {
                                    bddK = bddBad;

                                    #ifdef DEBUG_TIME
                                    cout << endl << "------------loops:" << ++iCount << "----------------" << endl;
                                    cout << "Computing supremal controllable & P3 subpredicate..." << endl;
                                    gettimeofday(&tv1, NULL);
                                    #endif

                                    if (supcp(bddBad) < 0)
                                            throw -1;

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

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

                                    //Computing CR(not(bddBad))
                                    bddBad = bdd_not(cr(m_bddMarking, bdd_not(bddBad), ALL_EVENT_EXCEPT_LD, iErr));
                                    if (iErr != 0)
                                            throw -1;

                                    #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

                                    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);
                            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
                    }

                    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:   Compute the initial bad states(Bad_H)(uncontorlalble event part)
     * PARA:    bddConBad: BDD containing all the bad states (output)
     * RETURN:  0: sucess -1: fail
     * ACCESS:  private
     */
    int CHighSub::GenConBad(bdd &bddConBad)
    {
        try
        {
            bdd bddPlantTrans = bddfalse;
            bdd bddSpecTrans = bddfalse;

            for (int k = 0; k < 4; 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_HIGHERR_GENCONBAD);
            return -1;
        }
        return 0;
    }

    /**
     * DESCR:   Test if there are any bad states in the reachable states
     *          (Uncontrollable event part of Bad_H)
     * PARA:    bddConBad: BDD containing tested bad states(output).
     *                     Initially, bddBad should be bddfalse.
     *          bddReach: BDD containing all reachable states in high-level (input)
     *          vsErr: returned errmsg(output)
     * RETURN:  0: sucess -1: fail
     * ACCESS:  private
     */
    int CHighSub::VeriConBad(bdd &bddConBad, const bdd &bddReach, string & vsErr)
    {
        vsErr.clear();
        try
        {
            bdd bddPlantTrans = bddfalse;
            bdd bddSpecTrans = bddfalse;

            for (int k = 0; k < 5; k++)
            {
                //Updated to include transitions resulting from low data events
                //--H.I.
                if (k != 3)
                {
                    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 = "Causing 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_HIGHERR_GENCONBAD);
            return -1;
        }
        return 0;
    }

    /**
     * DESCR:   Compute the initial bad states(Bad_H)(answer event part)
     * PARA:    bddConBad: BDD containing all the bad states (output)
     * RETURN:  0: sucess -1: fail
     * ACCESS:  private
     */
    int CHighSub::GenP3Bad(bdd &bddP3Bad)
    {
        try
        {
            bdd bddHighTrans = bddfalse;

            EVENTSUB EventSub;
            int iSub = 0;
            unsigned short usiLocalIndex = 0;
            int iIndex = 0;

            for (int iDES = 0, iIntf = 0; iDES < this->GetNumofDES(); iDES++)
            {
                if (m_pDESArr[iDES]->GetDESType() == INTERFACE_DES)
                {
                    for (int i = 0; i < m_pDESArr[iDES]->GetNumofEvents(); i++)
                    {
                        pPrj->GenEventInfo((m_pDESArr[iDES]->GetEventsArr())[i],
                                            EventSub, iSub, usiLocalIndex);
                        if (EventSub == A_EVENT)
                        {
                            if (usiLocalIndex % 2 == 0)
                            {
                                usiLocalIndex = (usiLocalIndex - 2) / 2;
                                iIndex = usiLocalIndex +
                                            m_piUArr[EventSub - 1][iSub - 1];
                                bddHighTrans = bdd_exist(
                                                m_pbdd_UnConTrans[A_EVENT][iIndex],
                                                m_pbdd_IVar[iIntf]);
                                bddHighTrans = bdd_exist(bddHighTrans,
                                                            m_pbdd_IVarPrim[iIntf]);

                                //Compute illegal predicate for each answer event
                                bddP3Bad |=
                                    bdd_exist(m_pbdd_UnConATrans[iIndex],
                                              m_pbdd_IVarPrim[iIntf]) &
                                    bdd_not(
                                        bdd_exist(bddHighTrans,
                                          bdd_exist(
                                            m_pbdd_UnConVarPrim[A_EVENT][iIndex],
                                            m_pbdd_IVarPrim[iIntf])));
                            }
                            else
                            {
                                usiLocalIndex = (usiLocalIndex - 1) / 2;
                                iIndex = usiLocalIndex +
                                                m_piCArr[EventSub - 1][iSub - 1];

                                bddHighTrans = bdd_exist(
                                                m_pbdd_ConTrans[A_EVENT][iIndex],
                                                m_pbdd_IVar[iIntf]);
                                bddHighTrans = bdd_exist(bddHighTrans,
                                                m_pbdd_IVarPrim[iIntf]);

                                //Compute illegal predicate for each answer event
                                bddP3Bad |=
                                    bdd_exist(m_pbdd_ConATrans[iIndex],
                                              m_pbdd_IVarPrim[iIntf]) &
                                    bdd_not(bdd_exist(bddHighTrans,
                                                bdd_exist(
                                                 m_pbdd_ConVarPrim[A_EVENT][iIndex],
                                                 m_pbdd_IVarPrim[iIntf])));
                            }
                        }
                    }
                    iIntf++;
                }
            }
        }
        catch(...)
        {
            string sErr = this->GetSubName();
            sErr += ": Error during generating point 3 bad states.";
            pPrj->SetErr(sErr, HISC_HIGHERR_GENP3BAD);
            return -1;
        }
        return 0;
    }

    /**
     * DESCR:   Test if there are any bad states in the reachable states
     *          (answer and low-data event part of Bad_H)
     *          updated to support LD Events --H.I.
     * PARA:    bddP3Bad: BDD containing tested bad states(output).
     *                     Initially, bddBad should be bddfalse.
     *          bddReach: BDD containing all reachable states in high-level (input)
     *          vsErr: returned errmsg(output)
     * RETURN:  0: sucess -1: fail
     * ACCESS:  private
     */
    int CHighSub::VeriP3Bad(bdd &bddP3Bad, const bdd &bddReach, string &vsErr)
    {
        vsErr.clear();
        try
        {
            bdd bddHighTrans = bddfalse;

            EVENTSUB EventSub;
            int iSub = 0;
            unsigned short usiLocalIndex = 0;
            int iIndex = 0;

            for (int iDES = 0, iIntf = 0; iDES < this->GetNumofDES(); iDES++)
            {
                if (m_pDESArr[iDES]->GetDESType() == INTERFACE_DES)
                {
                    for (int i = 0; i < m_pDESArr[iDES]->GetNumofEvents(); i++)
                    {
                        pPrj->GenEventInfo((m_pDESArr[iDES]->GetEventsArr())[i],
                                            EventSub, iSub, usiLocalIndex);
                        if (EventSub == A_EVENT)
                        {
                            if (usiLocalIndex % 2 == 0)
                            {
                                iIndex = (usiLocalIndex - 2) / 2 +
                                                m_piUArr[EventSub - 1][iSub - 1];

                                bddHighTrans = bdd_exist(
                                    m_pbdd_UnConTrans[A_EVENT][iIndex],
                                    m_pbdd_IVar[iIntf]);
                                bddHighTrans = bdd_exist(bddHighTrans,
                                                            m_pbdd_IVarPrim[iIntf]);

                                //Compute illegal predicate for each anwer event
                                bddP3Bad |=
                                    bdd_exist(m_pbdd_UnConATrans[iIndex],
                                              m_pbdd_IVarPrim[iIntf]) &
                                    bdd_not(bdd_exist(bddHighTrans,bdd_exist(
                                            m_pbdd_UnConVarPrim[A_EVENT][iIndex],
                                            m_pbdd_IVarPrim[iIntf])));
                                bddP3Bad &= bddReach;

                                if (bddP3Bad != bddfalse)
                                {
                                    vsErr = "Causing answer event:";
                                    vsErr += SearchEventName(A_EVENT,
                                              usiLocalIndex +
                                              m_piUArr[EventSub - 1][iSub - 1] * 2);
                                    return 0;
                                }
                            }
                            else
                            {
                                iIndex = (usiLocalIndex - 1) / 2 +
                                                m_piCArr[EventSub - 1][iSub - 1];

                                bddHighTrans = bdd_exist(
                                                m_pbdd_ConTrans[A_EVENT][iIndex],
                                                m_pbdd_IVar[iIntf]);
                                bddHighTrans = bdd_exist(bddHighTrans,
                                                m_pbdd_IVarPrim[iIntf]);

                                //Compute illegal predicate for each answer event
                                bddP3Bad |= bdd_exist(m_pbdd_ConATrans[iIndex],
                                                      m_pbdd_IVarPrim[iIntf]) &
                                            bdd_not(bdd_exist(bddHighTrans,
                                                bdd_exist(
                                                 m_pbdd_ConVarPrim[A_EVENT][iIndex],
                                                 m_pbdd_IVarPrim[iIntf])));
                                bddP3Bad &= bddReach;

                                if (bddP3Bad != bddfalse)
                                {
                                    vsErr = "Blocking answer event:";
                                    vsErr += SearchEventName(A_EVENT,
                                             usiLocalIndex +
                                             m_piCArr[EventSub - 1][iSub - 1] * 2);
                                    throw -1;
                                }
                            }
                        }

                        else if (EventSub == LD_EVENT)
                        {

                            if (usiLocalIndex % 2 == 0)
                            {
                                iIndex = (usiLocalIndex - 1) / 2 +
                                                m_piUArr[EventSub - 1][iSub - 1];

                                bddHighTrans = bdd_exist(
                                    m_pbdd_UnConTrans[LD_EVENT][iIndex],
                                    m_pbdd_IVar[iIntf]);
                                bddHighTrans = bdd_exist(bddHighTrans,
                                                            m_pbdd_IVarPrim[iIntf]);

                                //Compute illegal predicate for each low data event
                                bddP3Bad |=
                                    bdd_exist(m_pbdd_UnConLDTrans[iIndex],
                                              m_pbdd_IVarPrim[iIntf]) &
                                    bdd_not(bdd_exist(bddHighTrans,bdd_exist(
                                            m_pbdd_UnConVarPrim[LD_EVENT][iIndex],
                                            m_pbdd_IVarPrim[iIntf])));
                                bddP3Bad &= bddReach;

                                if (bddP3Bad != bddfalse)
                                {
                                    vsErr = "Causing low data event:";
                                    vsErr += SearchEventName(LD_EVENT,
                                              usiLocalIndex +
                                              m_piUArr[EventSub - 1][iSub - 1] * 2);
                                    return 0;
                                }
                            }
                            else
                            {
                                iIndex = (usiLocalIndex - 1) / 2 +
                                                m_piCArr[EventSub - 1][iSub - 1];

                                bddHighTrans = bdd_exist(
                                                m_pbdd_ConTrans[LD_EVENT][iIndex],
                                                m_pbdd_IVar[iIntf]);
                                bddHighTrans = bdd_exist(bddHighTrans,
                                                m_pbdd_IVarPrim[iIntf]);

                                //Compute illegal predicate for each low data event
                                bddP3Bad |= bdd_exist(m_pbdd_ConLDTrans[iIndex],
                                                      m_pbdd_IVarPrim[iIntf]) &
                                            bdd_not(bdd_exist(bddHighTrans,
                                                bdd_exist(
                                                 m_pbdd_ConVarPrim[LD_EVENT][iIndex],
                                                 m_pbdd_IVarPrim[iIntf])));
                                bddP3Bad &= bddReach;

                                if (bddP3Bad != bddfalse)
                                {
                                    vsErr = "Blocking low data event:";
                                    vsErr += SearchEventName(LD_EVENT,
                                             usiLocalIndex +
                                             m_piCArr[EventSub - 1][iSub - 1] * 2);
                                    throw -1;
                                }
                            }
                        }
                    }
                    iIntf++;
                }
            }
        }
        catch(int)
        {
        }
        catch(...)
        {
            string sErr = this->GetSubName();
            sErr += ": Error during generating point 3 bad states.";
            pPrj->SetErr(sErr, HISC_HIGHERR_GENP3BAD);
            return -1;
        }
        return 0;
    }

    /**
     * DESCR:   compute PHIC(P)
     * PARA:    bddP : BDD for predicate P. (input and output(=PHIC(P)))
     * RETURN:  0: sucess -1: fail
     * ACCESS:  private
     */
    int CHighSub::supcp(bdd & bddP)
    {
        bdd bddK1 = bddfalse;
        bdd bddK2 = bddfalse;
        int iEvent = 0;
        unsigned short usiIndex = 0;
        int iSub = 0;
        EVENTSUB EventSub;
        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];
                            pPrj->GenEventInfo(iEvent, EventSub, iSub, usiIndex);

                            if ( iEvent % 2 == 0) //Uncontrollable events
                            {
                                usiIndex = (usiIndex - 2) / 2;
                                if (EventSub == R_EVENT || EventSub == A_EVENT)
                                    iIndex = usiIndex +
                                            m_piUArr[(int)EventSub - 1][iSub - 1];
                                else
                                    iIndex = usiIndex;

                                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 == A_EVENT )//should be controllable
                            {
                                usiIndex = (usiIndex - 1) / 2;
                                iIndex = usiIndex +
                                        m_piCArr[(int)EventSub - 1][iSub - 1];
                                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 low-level PHIC(P).";
            pPrj->SetErr(sErr, HISC_HIGHERR_SUPCP);
            return -1;
        }
        return 0;
    }

    /**
     * DESCR:   compute CR(G_H, P', \Sigma', P)
     *          updated to support LD Events --H.I.
     * 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_H, P', \Sigma', P)
     * ACCESS:  private
     */
    bdd CHighSub::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;
            unsigned short usiIndex = 0;
            int iIndex = 0;
            EVENTSUB EventSub;
            int iSub = 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];
                            pPrj->GenEventInfo(iEvent, EventSub, iSub, usiIndex);
                            if (viEventSub == ALL_EVENT || ((viEventSub == ALL_EVENT_EXCEPT_LD) && (EventSub != (int) LD_EVENT)) || viEventSub == (int)EventSub)
                            {
                                if (iEvent % 2 == 0) //Uncontrollable
                                {
                                    //Compute index
                                    usiIndex = (usiIndex - 2) / 2;
                                    if (EventSub == R_EVENT || EventSub == A_EVENT || EventSub == LD_EVENT)
                                            iIndex = usiIndex + m_piUArr[(int)EventSub - 1][iSub - 1];
                                    else
                                            iIndex = usiIndex;

                                    //Compute bddK
                                    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
                                {
                                    //Compute Index
                                    usiIndex = (usiIndex - 1) / 2;
                                    if (EventSub == R_EVENT || EventSub == A_EVENT || EventSub == LD_EVENT)
                                        iIndex = usiIndex + m_piCArr[(int)EventSub - 1][iSub - 1];

                                    else
                                        iIndex = usiIndex;

                                    //Compute bddK
                                    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_HIGHERR_COREACH);
                iErr = -1;
                return bddfalse;
            }
    }


    /**
     * DESCR:   compute R(G_H, P)
     *          updated to support LD Events --H.I.
     * PARA:    bddP: P (input)
     *          iErr: returned Errcode (0: success <0: fail)(output)
     * RETURN:  BDD for R(G_H, P)
     * ACCESS:  private
     */
    bdd CHighSub::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;
                    unsigned short usiIndex = 0;
                    int iSub = 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];
                                                    pPrj->GenEventInfo(iEvent, EventSub, iSub, usiIndex);
                                                    if (iEvent % 2 == 0)
                                                    {
                                                            //Compute index
                                                            usiIndex = (usiIndex - 2) / 2;
                                                            if (EventSub == R_EVENT || EventSub == A_EVENT || EventSub == LD_EVENT)
                                                                    iIndex = usiIndex + m_piUArr[(int)EventSub - 1][iSub - 1];
                                                            else
                                                                    iIndex = usiIndex;

                                                            //Compute bddK
                                                            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
                                                    {
                                                            //Compute Index
                                                            usiIndex = (usiIndex - 1) / 2;
                                                            if (EventSub == R_EVENT || EventSub == A_EVENT || EventSub == LD_EVENT)
                                                                    iIndex = usiIndex + m_piCArr[(int)EventSub - 1][iSub - 1];
                                                            else
                                                                    iIndex = usiIndex;

                                                            //Compute bddK
                                                            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_HIGHERR_REACH);
                    iErr = -1;
                    return bddfalse;
            }
    }
} //end of namespace BDDHISC
