/*************************************************************************
  FILE:  BddHiscSub2.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
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#include "BddHiscLowSub.h"
#include "BddHiscHighSub.h"
#include "BddHiscSub.h"
#include "BddHiscSub.h"
#include "BddHiscPubfunc.h"
#include "BddHiscType.h"
#include <fdd.h>
#include "BddHiscProject.h"
#include "BddHiscErrmsg.h"
#include <string>
#include <cstring>
#include <cassert>
#include <cstdlib>

using namespace std;

namespace BDDHISC
{
    extern CProject *pPrj;

    /*
     * DESCR:   Save synthesized automata-based supervisor, or synthesized local
     *          control predicates, or the syn-product of a verified system.
     * PARA:    bddReach:   BDD including all the reachable states (input)
     *          savetype: which format to save (see type.h) (input)
     *          savepath: where to save the result (input)
     * RETURN:  0: sucess -1: fail
     * ACCESS:  protected
     */
    int CSub::SaveSuper(const bdd & bddReach, const HISC_SAVESUPERTYPE savetype,
                        const string & savepath)
    {
        string sEventName;
        bdd bddController = bddfalse;
        bdd bddSimController = bddfalse;
        string sCurFile;
        ofstream fout;
        string sLine;
        string sSavePath;
        char scFileName[MAX_PATH2];
        STATES statesMap;
        string sInitState;
        //save bdd variable file
        try
        {
            sSavePath = savepath;
            if (sSavePath.length() > 0)
            {
                if (sSavePath[sSavePath.length() - 1] != '/')
                    sSavePath += "/";
            }
            //bdd Controller
            if (savetype == HISC_SAVESUPER_BDD || savetype == HISC_SAVESUPER_BOTH)
            {
                sCurFile = sSavePath + m_sSubName + "_var.txt";
                fout.open(sCurFile.data());
                if (!fout)
                    throw -1;
                for (int i = 0; i < this->GetNumofDES(); i++)
                {
                    sLine = m_pDESArr[i]->GetDESName() + " : ";
                    int ivarnum = fdd_varnum(i * 2);
                    for (int j = 0; j < ivarnum; j++)
                    {
                        sLine += str_itos(fdd_vars(i * 2)[j]);
                        sLine += " ";
                    }
                    fout << sLine << endl;

                    sLine.clear();
                    for (int j = 0; j < m_pDESArr[i]->GetNumofStates(); j++)
                    {
                        sLine = str_itos(j);
                        sLine += "  ";
                        sLine += m_pDESArr[i]->GetStateName(j);
                        fout << sLine << endl;
                    }
                    fout << endl;
                }
                fout.close();
            }

            //automata file
            if (savetype == HISC_SAVESUPER_AUTOMATA ||
                                            savetype == HISC_SAVESUPER_BOTH)
            {
                sCurFile = sSavePath + m_sSubName + "_sup.txt";
                fout.open(sCurFile.data());
                if (!fout)
                    throw -1;
                //print the DES order in the state vector
                fout << "# OUTPUT ORDER: ";
                for (int i = 0; i < this->GetNumofDES(); i++)
                {
                    fout << m_pDESArr[m_piDESPosArr[i]]->GetDESName() << " ";
                }
                fout << endl << endl;

                //put init state into statesMap
                //the index for initial state should be 0
                //(mainly for convieniently transforming it to TCT format later)
                if (PrintStateSet(fout, m_bddInit,  statesMap, 0) < 0)
                    throw -1;
                STATES::const_iterator csmi = statesMap.begin();
                if (csmi != statesMap.end())
                    sInitState = csmi->first;
                else
                    sInitState.clear();

                //print [States] Field
                fout << "[States]" << endl;
                if (PrintStateSet(fout, bddReach, statesMap, 1) < 0)
                    throw -1;

                //print [InitState] Field
                fout << endl << "[InitState]" << endl;
                if (!sInitState.empty())
                    fout << "0 #" << sInitState << endl;

                //print [MarkingStates] Field
                fout << endl << "[MarkingStates]" << endl;
                if (PrintStateSet(fout, m_bddMarking, statesMap, 2) < 0)
                    throw -1;

                //print [Events] Field
                fout << endl << "[Events]" << endl;
                if (PrintEvents(fout) < 0)
                    throw -1;

                //print [Transtions] Fields
                fout << endl << "[Transitions]" << endl;
            }

            for (int k = H_EVENT; k < LD_EVENT; k++)
            {
                //UnControllable events
                for (unsigned short usi = 2; usi <= m_usiMaxUnCon[k]; usi += 2)
                {
                    sEventName = this->SearchEventName((EVENTSUB)k, usi);
                    //\Gamma(N_\sigma \and C)
                    bddController = bdd_relprod(
                        m_pbdd_UnConTrans[k][(usi - 2) / 2],
                        bdd_replace(bddReach, m_pPair_UnCon[k][(usi - 2) / 2]),
                        m_pbdd_UnConVarPrim[k][(usi - 2) / 2]) & bddReach;

                    //print text transitions
                    if (savetype == HISC_SAVESUPER_AUTOMATA ||
                                            savetype == HISC_SAVESUPER_BOTH)
                    {
                        if (PrintTextTrans(fout, bddController, (EVENTSUB)k, usi,
                                            bddReach, sEventName, statesMap) < 0)
                            throw -1;
                    }
                }

                //Controllable events
                for (unsigned short usi = 1;
                            usi < (unsigned short) (m_usiMaxCon[k] + 1); usi += 2)
                {
                    sEventName = this->SearchEventName((EVENTSUB)k, usi);
                    bddController = bdd_relprod(
                        m_pbdd_ConTrans[k][(usi - 1) / 2],
                        bdd_replace(bddReach, m_pPair_Con[k][(usi - 1) / 2]),
                        m_pbdd_ConVarPrim[k][(usi - 1) / 2]) & bddReach;
                    bddSimController = SimplifyController(bddController,
                                                                (EVENTSUB)k, usi);

                    //high level: H, R events Low level: A, L events.
                    if ((m_iSubIndex == 0 && k <= R_EVENT) || (m_iSubIndex != 0 && k > R_EVENT))
                    {
                        //print bdd controller
                        if (savetype == HISC_SAVESUPER_BDD ||
                                                savetype == HISC_SAVESUPER_BOTH)
                        {
                            //not simplified
                            sCurFile = sSavePath + m_sSubName + "_" +
                                                            sEventName + ".bdd";
                            strcpy(scFileName, sCurFile.data());
                            if (bdd_fnsave(scFileName, bddController) != 0)
                                throw -1;

                            sCurFile = sSavePath + m_sSubName + "_" +
                                                            sEventName + ".dot";
                            strcpy(scFileName, sCurFile.data());
                            if (bdd_fnprintdot(scFileName, bddController) != 0)
                                throw -1;

                            //triple-prime simplified
                            sCurFile = sSavePath + m_sSubName + "_" +
                                                        sEventName + "_sim.bdd";
                            strcpy(scFileName, sCurFile.data());
                            if (bdd_fnsave(scFileName, bddSimController) != 0)
                                throw -1;

                            sCurFile = sSavePath + m_sSubName + "_" +
                                                        sEventName + "_sim.dot";
                            strcpy(scFileName, sCurFile.data());
                            if (bdd_fnprintdot(scFileName, bddSimController) != 0)
                                throw -1;

                            //prime simplified
                            bddSimController = bdd_simplify(bddController,
                                                                        m_bddSuper);
                            sCurFile = sSavePath + m_sSubName + "_" +
                                                        sEventName + "_re.bdd";
                            strcpy(scFileName, sCurFile.data());
                            if (bdd_fnsave(scFileName, bddSimController) != 0)
                                throw -1;

                            sCurFile = sSavePath + m_sSubName + "_" +
                                                            sEventName + "_re.dot";
                            strcpy(scFileName, sCurFile.data());
                            if (bdd_fnprintdot(scFileName, bddSimController) != 0)
                                throw -1;

                        }
                    }
                    //print text transitions
                    if (savetype == HISC_SAVESUPER_AUTOMATA ||
                                                savetype == HISC_SAVESUPER_BOTH)
                    {
                        if (PrintTextTrans(fout, bddController, (EVENTSUB)k, usi,
                                            bddReach, sEventName, statesMap) < 0)
                            throw -1;
                    }
                }
            }
            if (savetype == HISC_SAVESUPER_AUTOMATA ||
                                        savetype == HISC_SAVESUPER_BOTH)
                fout.close();
        }
        catch(...)
        {
            if (fout) fout.close();
            pPrj->SetErr("Unable to save the bdd controller or .",
                                HISC_BAD_SAVESUPER);
            return -1;
        }
        return 0;
    }

    /*
     * DESCR:   Print all the state vectors using state names
     * PARA:    fout: file stream (input)
     *          bddStateSet: BDD respresentation of the state set (input)
     *          statesMap: A STL Map to store (state name vector (key), integer
     *                      index)
     *          viSetFlat: 0: Initial state  1: All states 2: Marking States (input)
     * RETURN:  0: sucess -1: fail
     * ACCESS:  protected
     */
    int CSub::PrintStateSet(ofstream & fout, const bdd & bddStateSet,
                            STATES & statesMap, int viSetFlag)
    {
        int *statevec = NULL;
        int iStateIndex = 0;
        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)
                fout << 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)
                        fout << statesMap[sLine] << " #" << sLine << endl;
                    else  //all the states
                    {
                        if (bInitState)  //initial state alredy been printed
                        {
                            statesMap[sLine] = iStateIndex;
                            fout << iStateIndex << " #" << sLine << endl;
                        }
                        else
                        {
                            if (sLine != sInitState)
                            {
                                statesMap[sLine] = iStateIndex;
                                fout << iStateIndex << " #" << sLine << endl;
                            }
                            else
                            {
                                iStateIndex--;
                                bInitState = true;
                                fout << "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 = pPrj->GetInvAllEventsMap().begin();
            for (; ci != pPrj->GetInvAllEventsMap().end(); ++ci)
            {
                if (((ci->first & 0x0FFF0000) >> 16 == m_iSubIndex) ||
                   (((ci->first >> 28) == R_EVENT ||
                   (ci->first >> 28) == A_EVENT) && m_iSubIndex == 0))
                {
                    cSub = SubValueToLetter((EVENTSUB)(ci->first >> 28))[0];
                    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,
                             EVENTSUB EventSub, 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[EventSub][(usiLocalIndex - 2) / 2],
                               bddTemp,
                               m_pbdd_UnConVar[EventSub][(usiLocalIndex - 2) / 2]),
                            m_pPair_UnConPrim[EventSub][(usiLocalIndex - 2) / 2]) &
                        bddReach;
                else
                    bddNext =
                        bdd_replace(
                            bdd_relprod(
                                m_pbdd_ConTrans[EventSub][(usiLocalIndex - 1) / 2],
                                bddTemp,
                                m_pbdd_ConVar[EventSub][(usiLocalIndex - 1) / 2]),
                            m_pPair_ConPrim[EventSub][(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'/'LD'
     *          usiIndex: local index (in this sub)
     * RETURN:  triple-prime simplified BDD control predicate
     * ACCESS:  protected
     */
    bdd CSub::SimplifyController(const bdd & bddController, EVENTSUB EventSub,
                                 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[EventSub][(usiIndex - 1) / 2],
                                m_pbdd_ConVarPrim[EventSub][(usiIndex - 1) / 2]);
        //spec part
        bddSpecElig = bdd_exist(bddElig,
                                m_pbdd_ConPhysicVar[EventSub][(usiIndex - 1) / 2]);

        return bddSpecElig & bdd_simplify(bddController, m_bddSuper & bddElig);
    }
} //end of namespace BDDHISC
