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

#include "BddSdLowSub.h"
#include "BddSdErrmsg.h"
#include "BddSdPubfunc.h"

namespace BDDSD
{

extern CSub *pSub;

int CLowSub::VeriProperTimedBehavior(bdd &bddPTBBad, bdd bddReach, string & vsErr)
{
    const char * DEBUG = "CLowSub::VeriProperTimedBehavior():";

    try
    {
        bdd bddP1 = bddfalse;
        bdd bddTemp = bddfalse;

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

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

            cout << "Tick not found." << endl;
            return 0;
        }

        for (int i = 0; i < m_usiMaxUnCon / 2; i++)
        {
            // Get all the states left by uncontrollable event i.
            bddTemp = bdd_exist(m_pbdd_UnConPlantTrans[i], m_pbdd_UnConPlantVarPrim[i]);
            bddP1 |= bddTemp;
        }

        // Get all states left by tick event
        bddTemp = bdd_exist(m_pbdd_ConPlantTrans[iTick], m_pbdd_ConPhysicVarPrim[iTick]);

        bddP1 |= bddTemp;

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

        bddPTBBad = bddReach - bddP1;

        if(bddPTBBad != bddfalse)
        {
            VERBOSE(2)
            {
                PRINT_DEBUG << "bddPTBBad: ";
                PrintStateSet2(bddPTBBad);
                cout << endl;
            }

            vsErr = "Not proper timed behavior.";
            throw -1;
        }
    }
    catch(int)
    {
    }
    catch(...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error when checking proper timed behavior.";
        pSub->SetErr(sErr, HISC_LOWERR_PTB);
        return -1;
    }
    return 0;
}

int CLowSub::VeriALF(bdd &bddALFBad, bdd bddReach, string & vsErr)
{
    const char * DEBUG = "CLowSub::VeriALF():";

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

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

        cout << "Tick not found." << endl;
        return 0;
    }

    bdd bddChk = bddReach;
    bdd bddTemp = bddfalse;

    try
    {
        while (bddfalse != bddChk)
        {
            VERBOSE(2)
            {
                PRINT_DEBUG << "bddChk: ";
                PrintStateSet2(bddChk);
                cout << endl;
            }

            bdd bddQ = GetOneState(bddChk);

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

            bdd bddVisit = bddfalse;

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

                bddTemp = bdd_relprod(m_pbdd_ConTrans[i], bddQ, m_pbdd_ConVar[i]);
                bddVisit |= bdd_replace(bddTemp, m_pPair_ConPrim[i]);
            }

            for (int i = 0; i < (m_usiMaxUnCon / 2); i++)
            {
                bddTemp = bdd_relprod(m_pbdd_UnConTrans[i], bddQ, m_pbdd_UnConVar[i]);
                bddVisit |= bdd_replace(bddTemp, m_pPair_UnConPrim[i]);
            }

            bddVisit &= bddChk;

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

            bool overlap = false;

            bdd bddNext = bddfalse;

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

                bddTemp = bdd_relprod(m_pbdd_ConTrans[i], bddVisit, m_pbdd_ConVar[i]);
                bddNext |= bdd_replace(bddTemp, m_pPair_ConPrim[i]);
            }

            for (int i = 0; i < (m_usiMaxUnCon / 2); i++)
            {
                bddTemp = bdd_relprod(m_pbdd_UnConTrans[i], bddVisit, m_pbdd_UnConVar[i]);
                bddNext |= bdd_replace(bddTemp, m_pPair_UnConPrim[i]);
            }

            bddNext &= bddChk;

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

            bdd bddOldVisit = bddfalse;
            do
            {
                bddOldVisit = bddVisit;

                if (bddfalse != (bddVisit & bddNext))
                {
                    overlap = true;
                }

                bddVisit |= bddNext;

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

                bddALFBad = bddQ & bddVisit;
                if (bddfalse != bddALFBad)
                {
                    VERBOSE(2)
                    {
                        PRINT_DEBUG << "bddALFBad: ";
                        PrintStateSet2(bddALFBad);
                        cout << endl;
                    }

                    vsErr = "Not ALF.";
                    throw -1;
                }

                bdd bddNewNext = bddfalse;

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

                    bddTemp = bdd_relprod(m_pbdd_ConTrans[i], bddNext, m_pbdd_ConVar[i]);
                    bddNewNext |= bdd_replace(bddTemp, m_pPair_ConPrim[i]);
                }

                for (int i = 0; i < (m_usiMaxUnCon / 2); i++)
                {
                    bddTemp = bdd_relprod(m_pbdd_UnConTrans[i], bddNext, m_pbdd_UnConVar[i]);
                    bddNewNext |= bdd_replace(bddTemp, m_pPair_UnConPrim[i]);
                }

                bddNext = bddNewNext & bddChk;

                VERBOSE(2)
                {
                    PRINT_DEBUG << "bddNext: ";
                    PrintStateSet2(bddNext);
                    cout << endl;
                }
            }
            while (bddVisit != bddOldVisit);

            VERBOSE(1) { PRINT_DEBUG << "overlap: " << (overlap ? "true" : "false") << endl; }

            bddChk -= bddQ;
            if (!overlap)
            {
                bddChk -= bddVisit;
            }
        }
    }
    catch(int)
    {
    }
    catch(...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error when checking ALF.";
        pSub->SetErr(sErr, HISC_LOWERR_ALF);
        return -1;
    }
    return 0;
}

/**
 * DESCR:   Compute the Balemi bad states
 * PARA:    bddBalemiBad: BDD containing all the bad states (output)
 * RETURN:  0: sucess -1: fail
 * ACCESS:  private
 */
int CLowSub::GenBalemiBad(bdd &bddBalemiBad)
{
    const char * DEBUG = "CLowSub::VeriBalemiBad():";

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

    try
    {
        bdd bddPlantTrans = bddfalse;

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

            //Compute illegal state predicate for each uncontrollable event
            bddBalemiBad |= bdd_not(bdd_exist(m_pbdd_ConPlantTrans[i],
                                        m_pbdd_ConPhysicVarPrim[i])) &
                                        bdd_exist(m_pbdd_ConSupTrans[i],
                                        bdd_exist(m_pbdd_ConVarPrim[i],
                                        m_pbdd_ConPhysicVarPrim[i]));
        }
    }
    catch(...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error during generating Plant Completeness bad states.";
        pSub->SetErr(sErr, HISC_LOWERR_GENBALEMIBAD);
        return -1;
    }
    return 0;
}

/**
 * DESCR:   Test if there are any Balemi bad states in the reachable states
 * PARA:    bddBalemiBad: 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::VeriBalemiBad(bdd &bddBalemiBad, const bdd &bddReach, string & vsErr)
{
    const char * DEBUG = "CLowSub::VeriBalemiBad():";

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

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

        cout << "Tick not found." << endl;
        return 0;
    }

    try
    {
        int iErr = 0;

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

                //Compute illegal state predicate for each uncontrollable event
                bddBalemiBad |= bdd_not(bdd_exist(m_pbdd_ConPlantTrans[i],
                                        m_pbdd_ConPhysicVarPrim[i])) &
                             bdd_exist(m_pbdd_ConSupTrans[i],
                                     bdd_exist(m_pbdd_ConVarPrim[i],
                                     m_pbdd_ConPhysicVarPrim[i]));
                bddBalemiBad &= bddReach;
                //bddBalemiBad = r(bddBalemiBad, iErr);
                if (iErr < 0)
                {
                    throw -1;
                }

                if (bddBalemiBad != bddfalse)
                {
                    vsErr = "Blocked controllable event: ";
                    vsErr += SearchEventName((i * 2) + 1);
                    throw -1;
                }
            }
    }
    catch(int)
    {
    }
    catch(...)
    {
        string sErr = this->GetSubName();
        sErr += ": Error during generating Plant Completeness bad states.";
        pSub->SetErr(sErr, HISC_LOWERR_GENBALEMIBAD);
        return -1;
    }
    return 0;
}

} //end of namespace BDDSD
