/*************************************************************************
  FILE:  BddSdLowSub5.cpp
  DESCR: Verification and synthesis for low-levels
  AUTH:  Yu Wang
  DATE:  (C) Jan 2009
*************************************************************************/


#include <stack>
#include "BddSdLowSub.h"
#include "BddSdErrmsg.h"
#include "BddSdPubfunc.h"

namespace BDDSD
{

extern CSub *pSub;

int CLowSub::CheckSDControllability(bdd & bddSDBad, const bdd & bddreach, string & vsErr)
{
    const char * DEBUG = "CLowSub::CheckSDControllability():";

    int ret = 0;

    try
    {
        ret = CheckTimedControllability(bddSDBad, bddreach);
        if (ret < 0)
        {
            VERBOSE(1) { PRINT_DEBUG << "CheckTimedControllability()\t= " << ret << endl; }

            throw HISC_VERI_LOW_SD_II;
        }

        bdd bddSF = m_bddInit;

        stack<bdd> stack_bddSP;
        stack_bddSP.push(m_bddInit);

        list< list<bdd> > list_NerFail;

        int iSubTick = SearchSubEvent(sTick);
        VERBOSE(1) { PRINT_DEBUG << "iSubTick = " << iSubTick << endl; }

        //If tick does not exist
        if (iSubTick < 0)
        {
            string sErr = this->GetSubName();
            sErr += ": Tick event is not found.";
            pSub->SetErr(sErr, HISC_TICK_NOT_FOUND);

            VERBOSE(1) { PRINT_DEBUG << "Tick not found." << endl; }
            return 0;
        }

        int r;
        while (!stack_bddSP.empty())
        {
            bdd bddSS = stack_bddSP.top();
            stack_bddSP.pop();

            r = AnalyseSampledState(bddSDBad, bddreach, bddSS, list_NerFail, bddSF, stack_bddSP, vsErr);
            if (r < 0)
            {
                VERBOSE(1) { PRINT_DEBUG << "AnalyseSampledState() < 0" << endl; }

		// the line below is shareed with S-singular and sd
		// iii.1 error  but doesn't work for both
		//               vsErr = "AnalyseSampledState() Failed: " + vsErr;

		//RJL: customize for each error type
		if ( r == HISC_VERI_LOW_SD_III_1) {
		  vsErr = "Above state(s) were reached from a sampled\
 state by an activity event only string that caused\
 condition to fail.\n" + vsErr;
		} 

                throw r;
            }
        }

        if (!list_NerFail.empty())
        {
            VERBOSE(1) { PRINT_DEBUG << "list_NerFail is not empty." << endl; }
            if (!RecheckNerodeCells(bddSDBad, bddreach, list_NerFail))
            {
                VERBOSE(1) { PRINT_DEBUG << "RecheckNerodeCells() < 0" << endl; }
		//RJL: message below not informative enough.
		//                vsErr = "list_NerFail is not empty and RecheckNerodeCells() Failed.";
		                vsErr = "States listed were all\
 reached from the same sampled state but by different\
 concurrent strings that had the same occurrence image.";
                throw HISC_VERI_LOW_SD_III_2;
            }
        }

	//  cout  << "about to check sd IV.\n";

        CheckSDiv(bddSDBad, bddreach);

	//  cout  << "finished check sd IV.\n";

        if (bddSDBad != bddfalse)
        {

  cout  << "failed check sd IV.\n";
            VERBOSE(1) { PRINT_DEBUG << "(m_bddMarking - bddTemp) != m_bddInit" << endl; }
            vsErr = "There is a reachable marked state reached by a non-tick event.";
            throw HISC_VERI_LOW_SD_IV;
        }
    }
    catch(int failureCode)
    {
        ret = failureCode;
    }
    catch(...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error when checking SD Controllability.";
        pSub->SetErr(sErr, HISC_LOWERR_SD);
        return -1;
    }
    return ret;
}

// Algorithm 6.12
int CLowSub::AnalyseSampledState(bdd & bddSSBad, const bdd & bddreach, const bdd & bddSS,
    list< list<bdd> > & list_NerFail, bdd & bddSF, stack<bdd> & stack_bddSP, string & vsErr)
{
    const char * DEBUG = "CLowSub::AnalyseSampledState():";

    VERBOSE(2)
    {
        cout << endl;
        PRINT_DEBUG << "Analysing Sample State: ";
        PrintStateSet2(bddSS);
        cout << endl;
    }

    map<int, bdd> B_map;

    // Line 1
    B_map[0] = bddSS;

    // Line 2
    map<int, bdd> B_conc;

    stack<int> B_p;

    // Line 3
    B_p.push(0);

    // Line 4
    int intNextFreeLabel = 1;

    // Line 5
    map<int, EVENTSET> B_occu;

    // Line 6
    EVENTSET eventsElig;

    int iSubTick = SearchSubEvent(sTick);
    int iTick = (iSubTick - 1) / 2;
    VERBOSE(1) { PRINT_DEBUG << "iTick\t= " << iTick << endl; }

    // Line 7
    while (!B_p.empty())
    {
        VERBOSE(1)
        {
            cout << endl;
            PRINT_DEBUG << "B_p.size()\t= " << B_p.size() << endl;
        }

        // Line 8
        int b = B_p.top();
        B_p.pop();

        // Line 9
        bdd bddZ = B_map[b];

        VERBOSE(2) { PRINT_DEBUG << "bddZ : "; PrintStateSet2(bddZ); cout << endl; }

        bdd bddtemp = bddfalse;

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

        // Line 10
        EVENTSET eventsA;

        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP START : m_SubPlantEvents" << endl; }

        // Line 11
        for (EVENTSET::iterator i = m_SubPlantEvents.begin(); i != m_SubPlantEvents.end(); i++)
        {
            int iIndex, event = *i;
            if (event < 1)
            {
                VERBOSE(1) { PRINT_DEBUG << "ERROR - Found a Sub-level event index lower than 1" << endl; }
                return HISC_INTERNAL_ERR_SUBEVENT;
            }

            VERBOSE(1) { PRINT_DEBUG << "event\t= " << m_InvSubEventsMap[event] << endl; }
            if (1 == event % 2) //Controllable
            {
                iIndex = (event - 1) / 2;
                bddtemp = bdd_relprod(m_pbdd_ConPlantTrans[iIndex], bddZ, m_pbdd_ConVar[iIndex]);
                bddtemp = bdd_replace(bddtemp, m_pPair_ConPrim[iIndex]);
            }
            else //Uncontrollable
            {
                iIndex = (event / 2) - 1;
                bddtemp = bdd_relprod(m_pbdd_UnConPlantTrans[iIndex], bddZ, m_pbdd_UnConVar[iIndex]);
                bddtemp = bdd_replace(bddtemp, m_pPair_UnConPrim[iIndex]);
            }

            bddtemp &= bddreach;
            VERBOSE(2) { PRINT_DEBUG << "bddtemp\t= "; PrintStateSet2(bddtemp); cout << endl; }

            // Line 12
            if (bddtemp != bddfalse)
            {
                VERBOSE(1) { PRINT_DEBUG << "bddtemp != bddfalse" << endl; }

                // Line 13
                eventsA.insert(event);
                VERBOSE(1) { PRINT_DEBUG << "eventsA.size()\t= " << eventsA.size() << endl; }

            // Line 14
            }

        // Line 15
        }
        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP END   : m_SubPlantEvents" << endl; }

        // Line 16
        EVENTSET eventsD;

        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP START : m_SubSupervisorEvents" << endl; }

        // Line 17
        for (EVENTSET::iterator i = m_SubSupervisorEvents.begin(); i != m_SubSupervisorEvents.end(); i++)
        {
            bdd bddSupervisorTrans = bddfalse;
            int iIndex, event = *i;
            if (event < 1)
            {
                VERBOSE(1) { PRINT_DEBUG << "ERROR - Found a Sub-level event index lower than 1" << endl; }
                return HISC_INTERNAL_ERR_SUBEVENT;
            }

            if (1 == event % 2) //Controllable
            {
                iIndex = (event - 1) / 2;
                //Get supervisor transition predicate
                bddSupervisorTrans = bdd_exist(m_pbdd_ConTrans[iIndex], m_pbdd_ConPhysicVar[iIndex]);
                bddSupervisorTrans = bdd_exist(bddSupervisorTrans, m_pbdd_ConPhysicVarPrim[iIndex]);

                bddtemp = bdd_relprod(bddSupervisorTrans, bddZ, m_pbdd_ConVar[iIndex]);
                bddtemp = bdd_replace(bddtemp, m_pPair_ConPrim[iIndex]);
            }
            else //Uncontrollable
            {
                iIndex = (event / 2) - 1;
                //Get supervisor transition predicate
                bddSupervisorTrans = bdd_exist(m_pbdd_UnConTrans[iIndex], m_pbdd_UnConPlantVar[iIndex]);
                bddSupervisorTrans = bdd_exist(bddSupervisorTrans, m_pbdd_UnConPlantVarPrim[iIndex]);

                bddtemp = bdd_relprod(bddSupervisorTrans, bddZ, m_pbdd_UnConVar[iIndex]);
                bddtemp = bdd_replace(bddtemp, m_pPair_UnConPrim[iIndex]);
            }

            bddtemp &= bddreach;

            // Line 18
            if (bddtemp != bddfalse)
            {
                VERBOSE(1) { PRINT_DEBUG << "bddtemp != bddfalse" << endl; }

                // Line 19
                eventsD.insert(event);
                VERBOSE(1) { PRINT_DEBUG << "eventsD.size()\t= " << eventsD.size() << endl; }

            // Line 20
            }

        // Line 21
        }
        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP END   : m_SubSupervisorEvents" << endl; }

        EVENTSET eventsPoss;
        EVENTSET eventsDis = eventsA;
        for (EVENTSET::iterator i = eventsA.begin(); i != eventsA.end(); i++)
        {
            if (eventsD.end() != eventsD.find(*i))
            {
                // Line 22
                eventsPoss.insert(*i);
                eventsDis.erase(*i);
            }
        }

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

        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP START : eventsPoss" << endl; }
        for (EVENTSET::iterator i = eventsPoss.begin(); i != eventsPoss.end(); i++)
        {
            if ((*i) < 1)
            {
                VERBOSE(1) { PRINT_DEBUG << "ERROR - Found a Sub-level event index lower than 1" << endl; }
                return HISC_INTERNAL_ERR_SUBEVENT;
            }
            VERBOSE(1) { PRINT_DEBUG << "eventsPoss : " << m_InvSubEventsMap[(*i)] << endl; }
        }
        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP END   : eventsPoss" << endl; }

        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP START : eventsDis" << endl; }
        for (EVENTSET::iterator i = eventsDis.begin(); i != eventsDis.end(); i++)
        {

            if ((*i) < 1)
            {
                VERBOSE(1) { PRINT_DEBUG << "ERROR - Found a Sub-level event index lower than 1" << endl; }
                return HISC_INTERNAL_ERR_SUBEVENT;
            }
            VERBOSE(1) { PRINT_DEBUG << "eventsDis : " << m_InvSubEventsMap[(*i)] << endl; }
        }
        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP END   : eventsDis" << endl; }

        // Line 23
        if (bddZ == bddSS)
        {
            VERBOSE(1) { PRINT_DEBUG << "bddZ == bddSS" << endl; }
            eventsElig = eventsPoss;

            // Line 24
            // Remove uncontrollable events
            for (int i = 0; i < m_usiMaxUnCon / 2; i++)
            {
                eventsElig.erase((i + 1) * 2);
            }
            // Remove tick event
            eventsElig.erase(iSubTick);

        // Line 25
        }

        VERBOSE(1) { PRINT_DEBUG << "eventsElig.size() :" << eventsElig.size() << endl; }
        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP START : eventsElig" << endl; }
        for (EVENTSET::iterator i = eventsElig.begin(); i != eventsElig.end(); i++)
        {

            if ((*i) < 1)
            {
                VERBOSE(1) { PRINT_DEBUG << "ERROR - Found a Sub-level event index lower than 1" << endl; }
                return HISC_INTERNAL_ERR_SUBEVENT;
            }
            VERBOSE(1) { PRINT_DEBUG << "eventsElig : " << m_InvSubEventsMap[(*i)] << endl; }
        }
        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP END   : eventsElig" << endl; }

        EVENTSET eventsTemp = eventsPoss;
        eventsTemp.insert(B_occu[b].begin(), B_occu[b].end());

        // Remove uncontrollable events
        for (int i = 0; i < m_usiMaxUnCon / 2; i++)
        {
            eventsTemp.erase((i + 1) * 2);
        }
        // Remove tick event
        eventsTemp.erase(iSubTick);

        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP START : eventsTemp" << endl; }
        for (EVENTSET::iterator i = eventsTemp.begin(); i != eventsTemp.end(); i++)
        {
            if ((*i) < 1)
            {
                VERBOSE(1) { PRINT_DEBUG << "ERROR - Found a Sub-level event index lower than 1" << endl; }
                return HISC_INTERNAL_ERR_SUBEVENT;
            }
            VERBOSE(1) { PRINT_DEBUG << "eventsTemp = (eventsPoss V B_occu[" << b << "]) ^ <P_hib> : " << m_InvSubEventsMap[(*i)] << endl; }
        }
        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP END   : eventsTemp" << endl; }

        // Line 26
        if ((eventsTemp < eventsElig) || (eventsTemp > eventsElig) )
        {
            bddSSBad = bddZ;
            VERBOSE(1) { PRINT_DEBUG << "eventsTemp <> eventsElig" << endl; }

            VERBOSE(1) { PRINT_DEBUG << "eventsTemp.size() :" << eventsTemp.size() << endl; }

            // Line 27
            return HISC_VERI_LOW_SD_III_1;

        // Line 28
        }

        // Line 29
        if (-1 == DetermineNextState(bddSSBad, eventsPoss, bddZ, bddreach, b, intNextFreeLabel, B_map, B_p,
            bddSF, stack_bddSP, B_occu, B_conc, vsErr))
        {
            // Line 30
            return HISC_VERI_LOW_ZERO_LB;
        // Line 31
        }

    // Line 32
    }

    // Line 33
    CheckNerodeCells(B_conc, B_occu, list_NerFail);
    return 0;
}

void CLowSub::CheckNerodeCells(map<int, bdd> & B_conc, map<int, EVENTSET> & B_occu,
    list< list<bdd> > & list_NerFail)
{
    const char * DEBUG = "CLowSub::CheckNerodeCells():";

    VERBOSE(1) { PRINT_DEBUG << "WHILE-LOOP START : !B_conc.empty()" << endl; }

    // Line 2
    while (!B_conc.empty())
    {
        map<int, bdd>::iterator i = B_conc.begin();

        // Line 3
        int b = (*i).first;
        bdd bddZ = (*i).second;
        B_conc.erase(i);

        VERBOSE(2)
        {
            PRINT_DEBUG << "(b, bddZ) = (" << b << ", ";
            PrintStateSet2(bddZ);
            cout << ")" << endl;
        }

        // Line 3
        list<bdd> Zeqv;

        // Line 4
        Zeqv.push_back(bddZ);

        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP START : B_conc" << endl; }

        // Work around: C++ doesn't allow a map collection (i.e. B_Conc) to be modified in a loop
        //              by collection iterator. Need to first save B_Conc iterators in a list,
        //              and then read the iterators from the list in the loop from // Line 5.
        list<map<int, bdd>::iterator> iteratorList_B_Conc;
        for (map<int, bdd>::iterator k = B_conc.begin(); B_conc.end() != k; k++)
        {
            iteratorList_B_Conc.push_back(k);
        }

        // Line 5
        bool sameCell = true;

        // Line 6
        for (list<map<int, bdd>::iterator>::iterator j = iteratorList_B_Conc.begin(); iteratorList_B_Conc.end() != j; j++)
        {
            int bprime = (*(*j)).first;
            VERBOSE(1) { PRINT_DEBUG << "bprime : " << bprime << endl; }

            bdd bddZprime = (*(*j)).second;

            VERBOSE(2)
            {
                PRINT_DEBUG << "bddZprime : ";
                PrintStateSet2(bddZprime);
                cout << endl;
            }
            // Line 7
            if (B_occu[b] == B_occu[bprime])
            {
                VERBOSE(1) { PRINT_DEBUG << "B_occu[b:" << b << "] == B_occu[bprime:" << bprime << "]" << endl; }

                // Line 8
                Zeqv.push_back(bddZprime);

                // Line 9
                B_conc.erase(*j);

                // Line 10
                if (bddZ != bddZprime)
                {
                    VERBOSE(1) { PRINT_DEBUG << "bddZ != bddZprime" << endl; }

                    // Line 11
                    sameCell = false;

                // Line 12
                }
            // Line 13
            }
        // Line 14
        }
        VERBOSE(1) { PRINT_DEBUG << "FOR-LOOP END   : B_conc" << endl; }

        // Line 15
        if (!sameCell)
        {
            VERBOSE(1) { PRINT_DEBUG << "sameCell : false" << endl; }
            // Line 16
            list_NerFail.push_back(Zeqv);

        // Line 17
        }

    // Line 18
    }
    VERBOSE(1) { PRINT_DEBUG << "WHILE-LOOP END   : !B_conc.empty()" << endl; }

    // Line 19
    return;
}

int CLowSub::DetermineNextState(bdd & bddLBBad, const EVENTSET & eventsPoss, const bdd & bddZ, const bdd & bddreach,
    const int & intB, int & intNextFreeLabel, map<int, bdd> & B_map, stack<int> & B_p,
    bdd & bddSF, stack<bdd> & stack_bddSP,
    map<int, EVENTSET> & B_occu, map<int, bdd> & B_conc, string & vsErr)
{
    const char * DEBUG = "CLowSub::DetermineNextState():";

    // Line 1
    if (eventsPoss.empty())
    {
        VERBOSE(1) { PRINT_DEBUG << "eventsPoss is empty" << endl; }

        // Line 2
        return 0;
    } //Line 3

    int iSubTick = SearchSubEvent(sTick);
    int iTick = (iSubTick - 1) / 2;

    VERBOSE(1) { PRINT_DEBUG << "iSubTick = " << iSubTick << endl; }
    VERBOSE(1) { PRINT_DEBUG << "iTick = " << iTick << endl; }

    // Line 4
    if (eventsPoss.end() != eventsPoss.find(iSubTick))
    {
        VERBOSE(1) { PRINT_DEBUG << "Found tick in eventsPoss." << endl; }

        // Line 5
        bdd bddZprime = bdd_relprod(m_pbdd_ConTrans[iTick], bddZ, m_pbdd_ConVar[iTick]);
        bddZprime = bdd_replace(bddZprime, m_pPair_ConPrim[iTick]);
        bddZprime &= bddreach;

        VERBOSE(2)
        {
            PRINT_DEBUG << "bddZprime = ";
            PrintStateSet2(bddZprime);
            cout << endl;
        }

            // Line 7
            B_conc.insert(make_pair(intB, bddZprime));

            // Line 8
            if ((bddZprime & bddSF) == bddfalse)
            {
                // Line 9
                bddSF |= bddZprime;

                // Line 10
                stack_bddSP.push(bddZprime);

            // Line 11
            }

            VERBOSE(1) { PRINT_DEBUG << "eventsPoss.size() = " << eventsPoss.size() << endl; }

            // If tick is the only event in eventsPoss, then no need to run anything after Line 14.
            if (1 == eventsPoss.size())
            {
                VERBOSE(1) { PRINT_DEBUG << "eventsPoss only has a tick." << endl; }
                return 0;
            }


    // Line 13
    }

    // Line 14
    for (EVENTSET::iterator i = eventsPoss.begin(); i != eventsPoss.end(); i++)
    {
        int event, iSubEvent = *i;

        if (iSubEvent < 1)
        {
            VERBOSE(1) { PRINT_DEBUG << "ERROR - Found a Sub-level event index lower than 1" << endl; }
            return HISC_INTERNAL_ERR_SUBEVENT;
        }

        VERBOSE(1) { PRINT_DEBUG << "iSubEvent = " << m_InvSubEventsMap[iSubEvent] << endl; }

        if (iSubEvent == iSubTick)
        {
            continue;
        }

        // Line 15
        bdd bddZprime;

        if (1 == iSubEvent % 2) //Controllable
        {
            event = (iSubEvent - 1) / 2;
            VERBOSE(1) { PRINT_DEBUG << "Controllable event = " << m_InvSubEventsMap[iSubEvent] << endl; }
            bddZprime = bdd_relprod(m_pbdd_ConTrans[event], bddZ, m_pbdd_ConVar[event]);
            bddZprime = bdd_replace(bddZprime, m_pPair_ConPrim[event]);
        }
        else //Uncontrollable
        {
            event = (iSubEvent / 2) - 1;
            VERBOSE(1) { PRINT_DEBUG << "Uncontrollable event = " << m_InvSubEventsMap[iSubEvent] << endl; }
            bddZprime = bdd_relprod(m_pbdd_UnConTrans[event], bddZ, m_pbdd_UnConVar[event]);
            bddZprime = bdd_replace(bddZprime, m_pPair_UnConPrim[event]);
        }

        bddZprime &= bddreach;

        VERBOSE(2)
        {
            PRINT_DEBUG << "bddZprime = "; PrintStateSet2(bddZprime); cout << endl;
        }

        EVENTSET eventsTemp = B_occu[intB];

        // Line 17
        if ((1 == iSubEvent % 2) && (eventsTemp.end() != eventsTemp.find(iSubEvent)))
        {
            bddLBBad = B_map[intB];
            vsErr = "Event " + SearchEventName(iSubEvent) + " is found to occur more than once in this sampling period.";

            // Line 18
            return -1;

        // Line 19
        }

        // Line 20
        int intBprime = intNextFreeLabel;

        VERBOSE(1) { PRINT_DEBUG << "intBprime = " << intBprime << endl; }

        // Line 21
        intNextFreeLabel++;

        // Line 22
        B_map.insert(make_pair(intBprime, bddZprime));

        VERBOSE(1) { PRINT_DEBUG << "B_map.size() = " << B_map.size() << endl; }

        // Line 23
        B_p.push(intBprime);

        VERBOSE(1) { PRINT_DEBUG << "B_p.size() = " << B_p.size() << endl; }

        eventsTemp.insert(iSubEvent);

        VERBOSE(1) { PRINT_DEBUG << "eventsTemp.size() = " << eventsTemp.size() << endl; }

        // Line 24
        B_occu.insert(make_pair(intBprime, eventsTemp));

        VERBOSE(1) { PRINT_DEBUG << "B_occu.size() = " << B_occu.size() << endl; }

        for (EVENTSET::iterator i = B_occu[intB].begin(); i != B_occu[intB].end(); i++)
        {
            VERBOSE(1) { PRINT_DEBUG << "B_occu[intB = " << intB << "]: " << m_InvSubEventsMap[(*i)] << endl; }
        }

        for (EVENTSET::iterator i = B_occu[intBprime].begin(); i != B_occu[intBprime].end(); i++)
        {
            VERBOSE(1) { PRINT_DEBUG << "B_occu[intBprime = " << intBprime << "]: " << m_InvSubEventsMap[(*i)] << endl; }
        }
    // Line 26
    }

    // Line 27
    return 0;
}

int CLowSub::CheckTimedControllability(bdd & bddTCBad, const bdd & bddreach)
{
    bdd bddZhib = bddfalse;

    int iTick = (SearchSubEvent(sTick) - 1) / 2;

    for (int i = 0; i < (m_usiMaxCon + 1) / 2; i++)
    {
        if (iTick == i) continue;

        bddZhib |= bdd_exist(m_pbdd_ConTrans[i], m_pbdd_ConVarPrim[i]);
    }

    bddTCBad = bdd_exist(m_pbdd_ConTrans[iTick], m_pbdd_ConVarPrim[iTick]) & bddZhib & bddreach;

    if (bddfalse != bddTCBad)
    {
        return -3;
    }

    bddTCBad = bdd_exist(m_pbdd_ConPlantTrans[iTick], m_pbdd_ConPhysicVarPrim[iTick])
        & (!bdd_exist(m_pbdd_ConSupTrans[iTick], m_pbdd_ConSupVarPrim[iTick]))
        & (!bddZhib) & bddreach;

    if (bddfalse != bddTCBad)
    {
        return -2;
    }

    return 0;
}


int CLowSub::CheckTimedControllability(const EVENTSET & eventsDis, const EVENTSET & eventsPoss)
{
    //Uncontrollable events
    cout << "CLowSub::CheckTimedControllability() : FOR-LOOP START : eventsDis" << endl;
    for (EVENTSET::iterator i = eventsDis.begin(); i != eventsDis.end(); i++)
    {
        if (0 == (*i) % 2)
        {
            cout << "CLowSub::CheckTimedControllability() : Uncontrollable event found in eventsDis : " << m_InvSubEventsMap[(*i)] << endl;
            return -1;
        }
    }
    cout << "CLowSub::CheckTimedControllability() : FOR-LOOP END   : eventsDis" << endl;

    int iSubTick = SearchSubEvent(sTick);

    // Prohibitable events intersect with Poss events
    bool bool_Poss_and_Hib = false;

    cout << "CLowSub::CheckTimedControllability() : FOR-LOOP START : eventsPoss" << endl;
    for (EVENTSET::iterator i = eventsPoss.begin(); i != eventsPoss.end(); i++)
    {
        if (iSubTick == (*i)) continue;
        if (1 == (*i) % 2)
        {
            cout << "CLowSub::CheckTimedControllability() : Prohibitable event found in eventsPoss : " << m_InvSubEventsMap[(*i)] << endl;
            bool_Poss_and_Hib = true;
        }
    }
    cout << "CLowSub::CheckTimedControllability() : FOR-LOOP END   : eventsPoss" << endl;

    if (!bool_Poss_and_Hib && (eventsDis.end() != eventsDis.find(iSubTick)))
    {
        return -2;
    }

    if (bool_Poss_and_Hib && (eventsPoss.end() != eventsPoss.find(iSubTick)))
    {
        return -3;
    }

    return 0;
}

bool CLowSub::RecheckNerodeCells(bdd & bddNCBad, const bdd & bddreach, list< list<bdd> > & list_NerFail)
{
    // Line 1
    if (list_NerFail.empty())
    {
        // Line 2
        return true;
    // Line 3
    }

    // Line 4
    list< pair<bdd, bdd> > listVisited;

    // Line 5
    for (list< list<bdd> >::iterator i = list_NerFail.begin(); i != list_NerFail.end(); i++)
    {
        // Line 6
        list<bdd> Zeqv = *i;

        // Line 7
        if (!RecheckNerodeCell(bddNCBad, bddreach, Zeqv, listVisited))
        {
	  //            if (bddfalse == bddNCBad)
	  //            {
	  // RJL: I think test should always report Zeqv info

	  // also added next line.
	  bddNCBad = bddfalse;

                for (list<bdd>::iterator j = Zeqv.begin(); j != Zeqv.end(); j++)
                {
                    bddNCBad |= *j;
                }
		//            }
            // Line 8;
            return false;
        // Line 9
        }
    // Line 10
    }

    // Line 11
    return true;
}

bool CLowSub::RecheckNerodeCell(bdd & bddNCBad, const bdd & bddreach, const list<bdd> & Zeqv, list< pair<bdd, bdd> > & listVisited)
{
    const char * DEBUG = "CLowSub::RecheckNerodeCell():";

    // Line 1
    list<bdd>::const_iterator z1 = Zeqv.begin();

    if (Zeqv.end() == z1)
    {
        return true;
    }

    // Line 2
    list < pair<bdd, bdd> > listPending;

    list<bdd>::const_iterator z2 = Zeqv.begin();
    z2++;

    // Line 3, 4
    while(Zeqv.end() != z2)
    {
        // Line 5
        listPending.push_back(make_pair(*z1, *z2));
        z2++;
    // Line 6
    }

    // Line 7
    while (!listPending.empty())
    {
        // Line 8
        list< pair<bdd, bdd> >::iterator itr_Pending = listPending.begin();
        bdd bddz1 = itr_Pending->first;
        bdd bddz2 = itr_Pending->second;
        listPending.erase(itr_Pending);

        // Line 9
        bdd bddP = bddz1 | bddz2;

        // Line 10
        if ((bddfalse != (bddP & m_bddMarking)) && (bddP != (bddP & m_bddMarking)))
        {
            bddNCBad = bddP;
            VERBOSE(1) { PRINT_DEBUG << "Neither all states in Zeqv are marked nor non of them are marked." << endl; }

            // Line 11
            return false;

        // Line 12
        }

        // Line 13
        for (EVENTSET::iterator itr_event = m_SubPlantEvents.begin(); itr_event != m_SubPlantEvents.end(); itr_event++)
        {
            int event, iSubEvent = *itr_event;
            VERBOSE(1) { PRINT_DEBUG << "iSubEvent : " << m_InvSubEventsMap[iSubEvent] << " (index: " << iSubEvent << ")" << endl; }

            if (iSubEvent < 1)
            {
                VERBOSE(1) { PRINT_DEBUG << "ERROR - Found a Sub-level event index lower than 1" << endl; }
                return HISC_INTERNAL_ERR_SUBEVENT;
            }

            bdd bddPprime = bddfalse;
            bdd bddz1prime = bddfalse;
            bdd bddz2prime = bddfalse;

            bdd bddTemp = bddfalse;

            if (1 == iSubEvent % 2) //Controllable
            {
                event = (iSubEvent - 1) / 2;

                bddTemp = bdd_relprod(m_pbdd_ConTrans[event], bddP, m_pbdd_ConVar[event]);
                bddPprime |= bdd_replace(bddTemp, m_pPair_ConPrim[event]);

                bddTemp = bdd_relprod(m_pbdd_ConTrans[event], bddz1, m_pbdd_ConVar[event]);
                bddz1prime |= bdd_replace(bddTemp, m_pPair_ConPrim[event]);

                bddTemp = bdd_relprod(m_pbdd_ConTrans[event], bddz2, m_pbdd_ConVar[event]);
                bddz2prime |= bdd_replace(bddTemp, m_pPair_ConPrim[event]);
            }
            else //Uncontrollable
            {
                event = (iSubEvent / 2) - 1;

                bddTemp = bdd_relprod(m_pbdd_UnConTrans[event], bddP, m_pbdd_UnConVar[event]);
                bddPprime |= bdd_replace(bddTemp, m_pPair_UnConPrim[event]);

                bddTemp = bdd_relprod(m_pbdd_UnConTrans[event], bddz1, m_pbdd_UnConVar[event]);
                bddz1prime |= bdd_replace(bddTemp, m_pPair_UnConPrim[event]);

                bddTemp = bdd_relprod(m_pbdd_UnConTrans[event], bddz2, m_pbdd_UnConVar[event]);
                bddz2prime |= bdd_replace(bddTemp, m_pPair_UnConPrim[event]);
            }

            // Line 14
            bddPprime &= bddreach;

            // Line 15
            bddz1prime &= bddreach;

            // Line 16
            bddz2prime &= bddreach;

            VERBOSE(2)
            {
                PRINT_DEBUG << "bddPprime : ";
                PrintStateSet2(bddPprime);
                cout << endl;
                PRINT_DEBUG << "bddz1prime : ";
                PrintStateSet2(bddz1prime);
                cout << endl;
                PRINT_DEBUG << "bddz2prime : ";
                PrintStateSet2(bddz2prime);
                cout << endl;
            }

            // Line 17
            if (bddfalse != bddPprime)
            {
                // Line 18
                if ((bddfalse != (bddz1prime & bddPprime)) && (bddfalse != (bddz2prime & bddPprime)))
                {
                    // Line 19
                    if (bddz1prime != bddz2prime)
                    {
                        // Need to manually search for the pair, since bdd::operator< returns bdd
                        // instead of bool, which makes all STL containers with ability to search
                        // malfunctional.
                        bool found = false;
                        for (list< pair<bdd, bdd> >::iterator itr = listVisited.begin();
                            itr != listVisited.end(); itr++)
                        {
                            if ((itr->first == bddz1prime) && (itr->second == bddz2prime))
                            {
                                found = true;
                            }
                        }

                        if (!found)
                        {
                            // Line 20
                            listVisited.push_back(make_pair(bddz1prime, bddz2prime));
                            // Line 21
                            listVisited.push_back(make_pair(bddz2prime, bddz1prime));
                            // Line 22
                            listPending.push_back(make_pair(bddz1prime, bddz2prime));
                        }
                    // Line 23
                    }
                }
                // Line 24
                else
                {
		  // RJL: I don't think this is really the error info
		  // that should be reported. This is the states that
		  // the lambda test failed, not the  Zeqv.
                    bddNCBad = bddP;
                    // Line 25
                    return false;
                // Line 26
                }
            // Line 27
            }
        // Line 28
        }
    // Line 29
    }

    // Line 30
    return true;
}

int CLowSub::CheckSDiv(bdd & bddSDivBad, const bdd & bddReach)
{
    int iTick = (SearchSubEvent(sTick) - 1) / 2;

    // Line 1: Get all states entered by non-tick event from a reachable state.
    bdd bddTemp = bddfalse;

    for (int i = 0; i < (m_usiMaxCon + 1) / 2; i++)
    {
        if (iTick == i) continue;

        bddTemp |= bdd_replace(
                        bdd_exist(m_pbdd_ConTrans[i] & bddReach, m_pbdd_ConVar[i]),
                    m_pPair_ConPrim[i]);
    }

    for (int i = 0; i < m_usiMaxUnCon / 2; i++)
    {
      //        bddTemp = bdd_replace(
      // change appears to fix sd IV error
        bddTemp |= bdd_replace(
                        bdd_exist(m_pbdd_UnConTrans[i] & bddReach, m_pbdd_UnConVar[i]),
                    m_pPair_UnConPrim[i]);
    }

    // Line 2 - 4: Each reachable marking states must not be reached by a non-tick event from a reachable state.
    bddSDivBad = (m_bddMarking & bddReach) & bddTemp;

    return 0;
}

EVENTSET CLowSub::GetTransitionEvents(const bdd & bddleave, const bdd & bddenter)
{
    EVENTSET events;
    events.clear();

    if ((bddleave == bddfalse) || (bddenter == bddfalse))
    {
        cout << "CLowSub::GetTransitionEvents() : bddleave is empty or bddfalse is empty." << endl;
        return events;
    }

    //Controllable events
    for (int i = 0; i < (m_usiMaxCon + 1) / 2; i++)
    {
        bdd bddtrans = bddleave & bdd_replace(bddenter, m_pPair_Con[i]);
        if ((bddtrans & m_pbdd_ConTrans[i]) != bddfalse)
        {
            events.insert((i * 2) + 1);
        }
    }

    //Uncontrollable events
    for (int i = 0; i < m_usiMaxUnCon / 2; i++)
    {
        bdd bddtrans = bddleave & bdd_replace(bddenter, m_pPair_UnCon[i]);
        if ((bddtrans & m_pbdd_UnConTrans[i]) != bddfalse)
        {
            events.insert((i + 1) * 2);
        }
    }

    return events;
}

} //end of namespace BDDSD
