/*************************************************************************
  FILE:  BddSdSub2.cpp
  DESCR: Save synthesized automata-based supervisor, or synthesized local
         control predicates, or the syn-product of a verified system.
         For the high-level or one low-level.
  AUTH:  Raoguang Song, Yu Wang
  DATE:  (C) Jan, 2006, 2008
*************************************************************************/
#include "BddSdLowSub.h"
#include "BddSdSub.h"
#include "BddSdSub.h"
#include "BddSdPubfunc.h"
#include "BddSdType.h"
#include "fdd.h"
#include "BddSdErrmsg.h"
#include <string>
#include <cassert>
#include <cstdlib>

using namespace std;

namespace BDDSD
{

extern CSub *pSub;

void CSub::PrintStateSet2(const bdd & bddStateSet)
{
    bdd bddStates = bddStateSet;
    int *piStateSet = fdd_scanallvar(bddStates);

    int count = 0;

    while (piStateSet != NULL && count < 3)
    {
        bdd bddVisitedState = bddtrue;

        cout << "<";
        for (int i = 0; i < this->GetNumofDES(); i++)
        {
            int iState = piStateSet[m_piDESPosArr[i] * 2];
            cout << m_pDESArr[m_piDESPosArr[i]]->GetDESName() + ":";
            cout << m_pDESArr[m_piDESPosArr[i]]->GetStateName(iState);
            if (i < this->GetNumofDES() -1)
            {
                cout << ", ";
            }
            bddVisitedState &= fdd_ithvar(m_piDESPosArr[i] * 2, iState);
        }
        cout << "> ";
        free(piStateSet);

        bddStates = bddStates - bddVisitedState;
        piStateSet = fdd_scanallvar(bddStates);

        count++;
    }

    if (count == 3)
    {
        cout << "...";
    }
}

bdd CSub::GetOneState(const bdd & bddStates)
{
    int *piStateSet = fdd_scanallvar(bddStates);
    bdd bddState = bddtrue;

    if (piStateSet != NULL)
    {
        for (int i = 0; i < this->GetNumofDES(); i++)
        {
            int iState = piStateSet[m_piDESPosArr[i] * 2];
            bddState &= fdd_ithvar(m_piDESPosArr[i] * 2, iState);
        }
        free(piStateSet);
        return bddState;
    }
    return bddfalse;
}

int CSub::CountStates(const bdd & bddStateSet)
{
    int count = 0;
    bdd bddStates = bddStateSet;
    int *piStateSet = fdd_scanallvar(bddStates);

    while (piStateSet != NULL)
    {
        count++;

        bdd bddVisitedState = bddtrue;

        for (int i = 0; i < this->GetNumofDES(); i++)
        {
            int iState = piStateSet[m_piDESPosArr[i] * 2];
            bddVisitedState &= fdd_ithvar(m_piDESPosArr[i] * 2, iState);
        }
        free(piStateSet);

        bddStates = bddStates - bddVisitedState;
        piStateSet = fdd_scanallvar(bddStates);
    }
    return count;
}

/*
 * DESCR:   Print all the state vectors using state names
 * PARA:    bddStateSet: BDD respresentation of the state set (input)
 *          viSetFlat: 0: Initial state  1: All states 2: Marking States (input)
 * RETURN:  0: sucess -1: fail
 * ACCESS:  protected
 */
int CSub::PrintStateSet(const bdd & bddStateSet, int viSetFlag)
{
    int *statevec = NULL;
    int iStateIndex = 0;

    STATES statesMap;

    try
    {
        string sLine;
        bdd bddTemp = bddfalse;
        bdd bddNormStateSet = bddtrue;
        string sInitState;
        bool bInitState = false;

        //restrict the prime variable to 0
        for (int i = 0; i < this->GetNumofDES(); i++)
            bddNormStateSet &= fdd_ithvar(i * 2 + 1, 0);
        bddNormStateSet &= bddStateSet;

        //save number of states
        if (viSetFlag != 0)
            cout << bdd_satcount(bddNormStateSet) << endl;

        //Initial state
        STATES::const_iterator csmi = statesMap.begin();
        if (csmi != statesMap.end())
            sInitState = csmi->first;
        else
            sInitState.clear();
        //print all the vectors
        statevec = fdd_scanallvar(bddNormStateSet);
        while ( statevec!= NULL)
        {
            sLine.clear();
            sLine = "<";
            for (int i = 0; i < this->GetNumofDES(); i++)
            {
                sLine += m_pDESArr[m_piDESPosArr[i]]->GetStateName(
                                    statevec[m_piDESPosArr[i] * 2]) + ",";
            }
            sLine = sLine.substr(0, sLine.length() - 1);
            sLine += ">";
            iStateIndex++;

            //state index for initial state should be 0
            if (viSetFlag == 0)
            {
                iStateIndex = 0;
                statesMap[sLine] = iStateIndex;
            }
            else
            {
                //for marking states, should show the corresponding state index
                if (viSetFlag == 2)
                    cout << statesMap[sLine] << " #" << sLine << endl;
                else  //all the states
                {
                    if (bInitState)  //initial state alredy been printed
                    {
                        statesMap[sLine] = iStateIndex;
                        cout << iStateIndex << " #" << sLine << endl;
                    }
                    else
                    {
                        if (sLine != sInitState)
                        {
                            statesMap[sLine] = iStateIndex;
                            cout << iStateIndex << " #" << sLine << endl;
                        }
                        else
                        {
                            iStateIndex--;
                            bInitState = true;
                            cout << "0" << " #" << sLine << endl;
                        }
                    }
                }
            }

            //remove the outputed state
            bddTemp = bddtrue;
            for (int i = 0; i < this->GetNumofDES(); i++)
                bddTemp &= fdd_ithvar(i * 2, statevec[i * 2]);
            bddNormStateSet = bddNormStateSet - bddTemp;
            free(statevec);
            statevec = NULL;

            statevec = fdd_scanallvar(bddNormStateSet);
        }
    }
    catch(...)
    {
        delete[] statevec;
        statevec = NULL;
        return -1;
    }
    return 0;
}

/*
 * DESCR:   Print all events from the pPrj->m_InvAllEventsMap
 * PARA:    fout: file stream (input)
 * RETURN:  0: sucess -1: fail
 * ACCESS:  protected
 */
int CSub::PrintEvents(ofstream & fout)
{
    char cSub = '\0';
    char cCon = '\0';
    string sLine;

    try
    {
        INVEVENTS::const_iterator ci = pSub->GetInvAllEventsMap().begin();
        for (; ci != pSub->GetInvAllEventsMap().end(); ++ci)
        {
            if ((ci->first & 0x0FFF0000) >> 16 == 1)
            {
                cCon = ci->first % 2 == 0 ? 'N':'Y';
                sLine = ci->second + "\t\t";
                sLine += cCon;
                sLine += "\t\t";
                sLine += cSub;
                fout << sLine << endl;
            }
        }
    }
    catch (...)
    {
        return -1;
    }
    return 0;
}

/*
 * DESCR:   Print all the transitions one by one
 * PARA:    fout: file stream (input)
 *          bddController: not simplified bdd control predicate for sEventName
 *          EventSub: 'H'/'R'/'A'/L'
 *          usiLocalIndex: local index (in this sub)
 *          bddReach: BDD respresentation of reachable states in
 *                    synthesized automata-based supervisor or syn-product of
 *                    the verified system.
 *          sEventName: Event Name
 *          statesMap: state name and index map (index is for the output file)
 * RETURN:  0: sucess -1: fail
 * ACCESS:  protected
 */
int CSub::PrintTextTrans(ofstream & fout, bdd & bddController,
                        unsigned short usiLocalIndex,
                         const bdd & bddReach, string sEventName,
                         STATES & statesMap)
{
    int *statevec1 = NULL;
    int *statevec2 = NULL;
    try
    {
        string sExit;
        string sEnt;
        bdd bddTemp = bddfalse;
        bdd bddNext = bddfalse;

        //extract each state from bddController
        statevec1 = fdd_scanallvar(bddController);
        while ( statevec1!= NULL)
        {
            sExit.clear();
            sExit = "<";
            for (int i = 0; i < this->GetNumofDES(); i++)
                sExit += m_pDESArr[m_piDESPosArr[i]]->GetStateName(
                                    statevec1[m_piDESPosArr[i] * 2]) + ",";
            sExit = sExit.substr(0, sExit.length() - 1);
            sExit += ">";

            bddTemp = bddtrue;
            for (int i = 0; i < this->GetNumofDES(); i++)
                bddTemp &= fdd_ithvar(i * 2, statevec1[i * 2]);
            bddController = bddController - bddTemp;
            free(statevec1);
            statevec1 = NULL;
            statevec1 = fdd_scanallvar(bddController);

            //Get the target state
            if (usiLocalIndex % 2 == 0)
                bddNext =
                    bdd_replace(
                        bdd_relprod(
                           m_pbdd_UnConTrans[(usiLocalIndex - 2) / 2],
                           bddTemp,
                           m_pbdd_UnConVar[(usiLocalIndex - 2) / 2]),
                        m_pPair_UnConPrim[(usiLocalIndex - 2) / 2]) &
                    bddReach;
            else
                bddNext =
                    bdd_replace(
                        bdd_relprod(
                            m_pbdd_ConTrans[(usiLocalIndex - 1) / 2],
                            bddTemp,
                            m_pbdd_ConVar[(usiLocalIndex - 1) / 2]),
                        m_pPair_ConPrim[(usiLocalIndex - 1) / 2]) &
                    bddReach;

            statevec2 = fdd_scanallvar(bddNext);
            if (statevec2 == NULL)
                throw -1;
            sEnt = "<";
            for (int i = 0; i < this->GetNumofDES(); i++)
                sEnt += m_pDESArr[m_piDESPosArr[i]]->GetStateName(
                                        statevec2[m_piDESPosArr[i] * 2]) + ",";
            sEnt = sEnt.substr(0, sEnt.length() - 1);
            sEnt += ">";
            free(statevec2);
            statevec2 = NULL;

            //print the transition
            fout << statesMap[sExit] << " <" << sEventName << "> " <<
                statesMap[sEnt] << endl;
        }
    }
    catch(...)
    {
        free(statevec1);
        statevec1 = NULL;
        free(statevec2);
        statevec2 = NULL;
        return -1;
    }
    return 0;
}

/*
 * DESCR:   Compute triple-prime simplified BDD control predicate for an event
 * PARA:    fout: file stream (input)
 *          bddController: BDD control predicate for event usiIndex
 *          EventSub: 'H'/'R'/'A'/L'
 *          usiIndex: local index (in this sub)
 * RETURN:  triple-prime simplified BDD control predicate
 * ACCESS:  protected
 */
bdd CSub::SimplifyController(const bdd & bddController,
                             const unsigned short usiIndex)
{
    //event should be controllable
    assert(usiIndex % 2 == 1);

    bdd bddElig = bddfalse;
    bdd bddSpecElig = bddfalse;

    //\dHs'
    bddElig = bdd_exist(m_pbdd_ConTrans[(usiIndex - 1) / 2],
                            m_pbdd_ConVarPrim[(usiIndex - 1) / 2]);
    //spec part
    bddSpecElig = bdd_exist(bddElig,
                            m_pbdd_ConPhysicVar[(usiIndex - 1) / 2]);

    return bddSpecElig & bdd_simplify(bddController, m_bddSuper & bddElig);
}

} //end of namespace BDDSD
