/*************************************************************************
  FILE:  BddHiscLowSub2.cpp
  DESCR: Verify this low-level interface (Command-pair) 
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/

#include "BddHiscLowSub.h"
#include "BddHiscSub.h"
#include "BddHiscPubfunc.h"
#include "BddHiscType.h"
#include <fdd.h>
#include "BddHiscProject.h"
#include "BddHiscErrmsg.h"
#include <string>

using namespace std;

namespace BDDHISC
{
    extern CProject *pPrj;

    /*
     * DESCR:   Verify if this low-level interface is an LD interface
     * PARA:    None
     * RETURN:  0: This low-level interface is an LD interface
     *          < 0: Not a command-pair interface
     * ACCESS: private
     *
     * Updated to Check for an LD Interface instead (backwards compatible
     * with command-pair definitions.) --H.I.
     */
    int CLowSub::CheckIntf()
    {
        int iRet = 0;
        string sErr = "Interface for low level ";
        sErr += this->GetSubName();
        sErr += ": ";
        bddPair *pPair = bdd_newpair();
        SetBddPairs(pPair, m_bddIVarPrim, m_bddIVar);
        bdd P_Ij = bddfalse;
        bdd P_Ijm = bddfalse;

        bdd P_Ijnm = bddfalse;  //All the reachable states that are non-marking --H.I.
        bdd P_IjmLD = bddfalse;
        bdd P_IjmA = bddfalse;
        bdd P_IjnmA = bddfalse;
        bdd P_IjnmR = bddfalse;

        try
        {

            cout <<"Testing PT1 of LD Interface Requirements"<<endl;

            if (m_bddIntfInit == bddfalse)
            {
                pPrj->SetErr(sErr + "No reachable states.", HISC_BAD_INTERFACE);
                throw -1;
            }

            //Compute all the reachable states --H.I.
            P_Ij = intf_r(bddtrue, iRet);
            if (iRet < 0)
                throw -1;

            //Compute all the states that are both reachable AND marking --H.I.
            P_Ijm = m_bddIntfMarking & P_Ij;

            //Compute all the states that are both reachable AND non-marking --H.I.
            P_Ijnm = P_Ij - P_Ijm;

            //---------------PT2 of the LD Interface Requirements-------------------------

            cout <<"Testing PT2 of LD Interface Requirements"<<endl;

            // Compute the predicate that includes all the reachable states that are
            //the target states of low data event transitions with source states satisfying
            //P_Ijm (the predicate consisting of reachable, marked states)
            for (int i = 1; i <= (unsigned short)(m_usiMaxCon[LD_EVENT] + 1); i += 2)
                P_IjmLD |= bdd_exist(m_pbdd_LDTrans[1][(i - 1)/2] & P_Ijm, m_bddIVar);
            for (int i = 2; i <= (unsigned short)(m_usiMaxUnCon[LD_EVENT] + 1); i += 2)
                P_IjmLD |= bdd_exist(m_pbdd_LDTrans[0][(i - 2)/2] & P_Ijm, m_bddIVar);
            for (int i = 1; i <= (unsigned short)(m_usiMaxCon[CHILD_LD_EVENT] + 1); i += 2)
                P_IjmLD |= bdd_exist(m_pbdd_CLDTrans[1][(i - 1)/2] & P_Ijm, m_bddIVar);
            for (int i = 2; i <= (unsigned short)(m_usiMaxUnCon[CHILD_LD_EVENT] + 1); i += 2)
                P_IjmLD |= bdd_exist(m_pbdd_CLDTrans[0][(i - 2)/2] & P_Ijm, m_bddIVar);

            P_IjmLD = bdd_replace(P_IjmLD, pPair);
            P_IjmLD |= P_Ijm;

            // Compute the predicate that includes the reachable states that are the
            //target states of answer event transitions with source states satisfying
            //P_Ijm (the predicate consisting of reachable, marked states)
            for (int i = 1; i <= (unsigned short)(m_usiMaxCon[A_EVENT] + 1); i += 2)
                P_IjmA |= bdd_exist(m_pbdd_ATrans[1][(i - 1)/2] & P_Ijm, m_bddIVar);
            for (int i = 2; i <= (unsigned short)(m_usiMaxUnCon[A_EVENT] + 1); i += 2)
                P_IjmA |= bdd_exist(m_pbdd_ATrans[0][(i - 2)/2] & P_Ijm, m_bddIVar);

            P_IjmA = bdd_replace(P_IjmA, pPair);

            //---------------PT3 of the LD Interface Requirements-------------------------

            cout <<"Testing PT3 of LD Interface Requirements"<<endl;

            // Compute the predicate that includes all the reachable states that are
            //the target states of answer event transitions with source states satisfying
            //P_Ijnm (the predicate consisting of reachable, non-marked states)
            for (int i = 1; i <= (unsigned short)(m_usiMaxCon[A_EVENT] + 1); i += 2)
                P_IjnmA |= bdd_exist(m_pbdd_ATrans[1][(i - 1)/2] & P_Ijnm, m_bddIVar);

            for (int i = 2; i <= (unsigned short)(m_usiMaxUnCon[A_EVENT] + 1); i += 2)
                P_IjnmA |= bdd_exist(m_pbdd_ATrans[0][(i - 2)/2] & P_Ijnm, m_bddIVar);

            P_IjnmA = bdd_replace(P_IjnmA, pPair);
            P_IjnmA |= P_Ijm;

            // Compute the predicate that includes the reachable states that are the
            //target states of request event transitions with source states satisfying
            //P_Ijnm (the predicate consisting of reachable, non-marked states)
            for (int i = 1; i <= (unsigned short)(m_usiMaxCon[R_EVENT] + 1); i += 2)
                P_IjnmR |= bdd_exist(m_pbdd_RTrans[1][(i - 1)/2] & P_Ijnm, m_bddIVar);

            for (int i = 2; i <= (unsigned short)(m_usiMaxUnCon[R_EVENT] + 1); i += 2)
                P_IjnmR |= bdd_exist(m_pbdd_RTrans[0][(i - 2)/2] & P_Ijnm, m_bddIVar);

            P_IjnmR = bdd_replace(P_IjnmR, pPair);

            if ((m_bddIntfInit & P_Ijm) == bddfalse)
            {
                pPrj->SetErr(sErr + "Not an LD interface. Fails Pt. 1", HISC_BAD_INTERFACE);
            }

            if (P_IjmA != bddfalse || P_IjmLD != P_Ijm)
            {
                pPrj->SetErr(sErr + "Not an LD interface. Fails Pt. 2", HISC_BAD_INTERFACE);
                throw -1;
            }

            if (P_IjnmR != bddfalse || P_IjnmA != P_Ijm)
            {
                pPrj->SetErr(sErr + "Not an LD interface. Fails Pt. 3", HISC_BAD_INTERFACE);
                throw -1;
            }

        }
        catch(int iErr)
        {
            iRet = iErr;
        }
        bdd_freepair(pPair);
        pPair = NULL;
        return iRet;
    }


    /*
     * DESCR:   Compute R(GIj, P)
     * PARA:    bddP: P (input)
                iErr: returned error code
     * RETURN:  R(GIj, P)
     * ACCESS: private
     */
    bdd CLowSub::intf_r(const bdd &bddP, int &iErr)
    {
        bdd bddK = bddP & m_bddIntfInit;
        bdd bddK1 = bddfalse;
        bdd bddKStep = bddfalse;
        bddPair *pPair = bdd_newpair();
        SetBddPairs(pPair, m_bddIVarPrim, m_bddIVar);
        iErr = 0;

        try
        {
            while (bddK != bddK1)
            {
                bddK1 = bddK;
                for (int i = 1; i <= (unsigned short)(m_usiMaxCon[R_EVENT] + 1); i += 2)
                {
                    bddKStep = bdd_exist(m_pbdd_RTrans[1][(i - 1)/2] & bddK1, m_bddIVar);
                    bddKStep = bdd_replace(bddKStep, pPair);
                    bddK |= bddKStep;
                }
                for (int i = 2; i <= (unsigned short)(m_usiMaxUnCon[R_EVENT]); i += 2)
                {
                    bddKStep = bdd_exist(m_pbdd_RTrans[0][(i - 2)/2] & bddK1, m_bddIVar);
                    bddKStep = bdd_replace(bddKStep, pPair);
                    bddK |= bddKStep;
                }
                for (int i = 1; i <= (unsigned short)(m_usiMaxCon[A_EVENT] + 1); i += 2)
                {
                    bddKStep = bdd_exist(m_pbdd_ATrans[1][(i - 1)/2] & bddK1, m_bddIVar);
                    bddKStep = bdd_replace(bddKStep, pPair);
                    bddK |= bddKStep;
                }
                for (int i = 2; i <= (unsigned short)(m_usiMaxUnCon[A_EVENT] + 1); i += 2)
                {
                    bddKStep = bdd_exist(m_pbdd_ATrans[0][(i - 2)/2] & bddK1, m_bddIVar);
                    bddKStep = bdd_replace(bddKStep, pPair);
                    bddK |= bddKStep;
                }
                for (int i = 1; i <= (unsigned short)(m_usiMaxCon[LD_EVENT] + 1); i += 2)
                {
                    bddKStep = bdd_exist(m_pbdd_LDTrans[1][(i - 1)/2] & bddK1, m_bddIVar);
                    bddKStep = bdd_replace(bddKStep, pPair);
                    bddK |= bddKStep;
                }
                for (int i = 2; i <= (unsigned short)(m_usiMaxUnCon[LD_EVENT] + 1); i += 2)
                {
                    bddKStep = bdd_exist(m_pbdd_LDTrans[0][(i - 2)/2] & bddK1, m_bddIVar);
                    bddKStep = bdd_replace(bddKStep, pPair);
                    bddK |= bddKStep;
                }
                for (int i = 1; i <= (unsigned short)(m_usiMaxCon[CHILD_LD_EVENT] + 1); i += 2)
                {
                    bddKStep = bdd_exist(m_pbdd_CLDTrans[1][(i - 1)/2] & bddK1, m_bddIVar);
                    bddKStep = bdd_replace(bddKStep, pPair);
                    bddK |= bddKStep;
                }
                for (int i = 2; i <= (unsigned short)(m_usiMaxUnCon[CHILD_LD_EVENT] + 1); i += 2)
                {
                    bddKStep = bdd_exist(m_pbdd_CLDTrans[0][(i - 2)/2] & bddK1, m_bddIVar);
                    bddKStep = bdd_replace(bddKStep, pPair);
                    bddK |= bddKStep;
                }
            }
        }
        catch(int)
        {
            string sErr = "Interface for low level ";
            sErr += this->GetSubName();
            sErr += ": Error during computing interface reachable states.";
            pPrj->SetErr(sErr, HISC_LOWERR_REACH);
            iErr = -1;
            bdd_freepair(pPair);
            pPair = NULL;
            return bddfalse;
        }
        bdd_freepair(pPair);
        pPair = NULL;
        return bddK;
    }
} //end of namespace BDDHISC


