/*************************************************************************
  FILE:  BddHiscHighSub1.cpp
  DESCR: Some misc functions for high-level
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#include "BddHiscSub.h"
#include "BddHiscHighSub.h"
#include "BddHiscLowSub.h"
#include <string>
#include "BddHiscErrmsg.h"
#include "BddHiscType.h"
#include <fdd.h>
#include "BddHiscDES.h"
#include "BddHiscProject.h"
#include <fstream>
#include "BddHiscPubfunc.h"
#include <cstdlib>
#include "CounterExampleAlgo.h"

using namespace std;

namespace BDDHISC
{
    extern CProject *pPrj;

    /**
     * DESCR:   Save DES list of high-level in memory to a file (for checking)
     * PARA:    fout: output file stream
     * RETURN:  0: sucess -1: fail
     * ACCESS:  public
     */
    int CHighSub::PrintSub(ofstream& fout)
    {
        try
        {
            fout << "#Sub system: " <<  m_sSubName << endl;
            fout << endl;

            fout << "[SYSTEM]" << endl;
            fout << m_iNumofPlants << endl;
            fout << m_iNumofSpecs << endl;
            fout << endl;

            fout << "[PLANT]" << endl;
            for (int i = 0; i < m_iNumofPlants; i++)
            {
                for (int j = 0; j < this->GetNumofDES(); j++)
                {
                    if (m_piDESOrderArr[j] == i)
                    {
                        fout << m_pDESArr[j]->GetDESName() << endl;
                        break;
                    }
                }
            }

            fout << "[SPEC]" << endl;
            for (int i = m_iNumofPlants; i < m_iNumofPlants + m_iNumofSpecs; i++)
            {
                for (int j = 0; j < this->GetNumofDES(); j++)
                {
                    if (m_piDESOrderArr[j] == i)
                    {
                        fout << m_pDESArr[j]->GetDESName() << endl;
                        break;
                    }
                }
            }

            fout << "################################################" << endl;
        }
        catch(...)
        {
            return -1;
        }
        return 0;
    }

    /**
     * DESCR:   Save all the DES in high-level to a text file for checking
     * PARA:    fout: output file stream
     * RETURN:  0: sucess -1: fail
     * ACCESS:  public
     */
    int CHighSub::PrintSubAll(ofstream & fout)
    {
        try
        {
            if (PrintSub(fout) < 0)
                throw -1;

            for (int i = 0; i < m_iNumofPlants + m_iNumofSpecs; i++)
            {
                if (m_pDESArr[i]->PrintDES(fout) < 0)
                    throw -1;
            }
        }
        catch(...)
        {
            return -1;
        }
        return 0;
    }

    /*
     * DESCR: Generate Bad state info during verfication
     *        Updated to support LD Events --H.I.
     *        Note: showtrace is not implemented, currently it is used for showing
     *              a blocking is a deadlock or livelock (very slow).
     * PARA:    bddBad: BDD for the set of bad states
     *          viErrCode: error code (see errmsg.h)
     *          showtrace: show a trace from the initial state to a bad state or not
     *                     (not implemented)
     *          vsExtraInfo: Extra errmsg.
     * RETURN:  None
     * ACCESS:  private
     */
    void CHighSub::BadStateInfo(const bdd& bddBad, const int viErrCode,
                        const HISC_TRACETYPE showtrace, Hisc_ChkInfo& checkInfo, const string &vsExtraInfo)
    {
        int *piBad = fdd_scanallvar(bddBad);
        string sErr;
        if (piBad != NULL)
        {
            if (viErrCode == HISC_VERI_HIGH_UNCON)
                sErr = GetSubName() +
                            ": Level-wise controllable check failed state:\n[ ";
            else if (viErrCode == HISC_VERI_HIGH_P3FAILED)
            {
				sErr = GetSubName() +
                ": Interface consistent conditions Point 3 check failed state:\n[ ";
				checkInfo.setIFailureType(Hisc_ChkInfo::AnsAcptAlgo);
			}
            else if (viErrCode == HISC_VERI_HIGH_BLOCKING)
            {
                if (showtrace == HISC_SHOW_TRACE)
                    sErr = GetSubName() + ": Blocking state ";
                else
                    sErr = GetSubName() + ": Blocking state: \n [ ";
            }

            //for blocking state, try to find the deadlock state
            //if there is no deadlock state, only show one of the live lock states
            if (showtrace == HISC_SHOW_TRACE)
            {
                if (viErrCode == HISC_VERI_HIGH_BLOCKING)
                {
                    bdd bddBlock = bddBad;
                    bdd bddNext = bddtrue;
                    bdd bddTemp = bddtrue;
                    do
                    {
                        bddTemp = bddtrue;
                        for (int i = 0; i < this->GetNumofDES(); i++)
                            bddTemp &= fdd_ithvar(i * 2, piBad[i * 2]);

                        bddNext = bddfalse;

                        for (int k = H_EVENT; k < NUMBER_OF_EVENTS; k++)
                        {
                            for (unsigned short usi = 2;
                                    usi <= m_usiMaxUnCon[k] &&
                                        bddNext == bddfalse; usi += 2)
                                bddNext |=
                                    bdd_replace(
                                        bdd_relprod(
                                            m_pbdd_UnConTrans[k][(usi - 2) / 2],
                                            bddTemp,
                                            m_pbdd_UnConVar[k][(usi - 2) / 2]),
                                        m_pPair_UnConPrim[k][(usi - 2) / 2]) &
                                    bddBad;
                            for (unsigned short usi = 1;
                                usi < (unsigned short) (m_usiMaxCon[k] + 1) &&
                                    bddNext == bddfalse; usi += 2)
                            {
                                bddNext |=
                                    bdd_replace(
                                        bdd_relprod(
                                            m_pbdd_ConTrans[k][(usi - 1) / 2],
                                            bddTemp,
                                            m_pbdd_ConVar[k][(usi - 1) / 2]),
                                        m_pPair_ConPrim[k][(usi - 1) / 2]) &
                                    bddBad;
                            }
                        }
                        if (bddNext == bddfalse)  //this is a deadlock state
                        {
                            sErr += "(dead lock):\n[ ";
                            break;
                        }
                        else //not a deadlock state
                        {
                            bddBlock = bddBlock - bddTemp;
                            free(piBad);
                            piBad = NULL;
                            piBad = fdd_scanallvar(bddBlock);
                        }
                    } while (piBad != NULL);

                    if (piBad == NULL) //live lock
                    {
                        sErr += "(live lock):\n[ ";
                        piBad = fdd_scanallvar(bddBad);
                    }
                }
            }


            if (piBad != NULL)
            {	
				//Added by Zain for counter example
				Hisc_ChkInfo::CounterExampleStateTuple temptuple(this->GetNumofDES());

                for (int i = 0; i < this->GetNumofDES(); i++)
                {
                    sErr += m_pDESArr[m_piDESPosArr[i]]->GetDESName() + ":" +
					m_pDESArr[m_piDESPosArr[i]]->GetStateName(piBad[m_piDESPosArr[i] * 2]);
					 if (i < this->GetNumofDES() -1)
                        sErr += ", ";

					// Added by zain for Counter example
					// Converting Error state tuple from bdd format to Counter example algo format
					if(checkInfo.getErrorFlag())
					{
					int teststateid = (piBad[m_piDESPosArr[i] * 2])+1;
					temptuple[i]= (short)((piBad[m_piDESPosArr[i] * 2])+1);
					QString tempName = QString::fromStdString( m_pDESArr[m_piDESPosArr[i]]->GetStateName(piBad[m_piDESPosArr[i] * 2]));
					checkInfo.CE_tuplemap[m_pDESArr[m_piDESPosArr[i]]->GetDESName()] = tempName.toStdWString();	
					}                   
                }
				// Added by Zain for Counter example
				if(checkInfo.getErrorFlag())
				{
				//checkInfo.setErrorTuple(this->GetNumofDES(),temptuple);
				checkInfo.setErrorFlag();
				QString temp= QString::fromStdString(this->GetSubName());
				std::wstring temp1=temp.toStdWString();				
				checkInfo.setErrorSubSystemName(temp1);
				}


            }
            sErr += " ]\n";

            sErr += vsExtraInfo;

            pPrj->SetErr(sErr, viErrCode);

            free(piBad);
            piBad = NULL;
        }
        return;
    }


    /**
     * DESCR: Search event name from high-level local event index.
     *        Mainly handle request events and answer events.
     * PARA:    k: R_EVENT/A_EVENT/H_EVENT/L_EVENT/LD_EVENT
     *          usiLocalIndex: high-level local event index.
     * RETURN:  event name
     * ACCESS:  public
     */
    string CHighSub::SearchEventName(EVENTSUB k, unsigned short usiLocalIndex)
    {
        int iEventIndex = 0;

        if (k == R_EVENT || k == A_EVENT || k == LD_EVENT)
        {
            int iSub = 0;
            unsigned short usiIndex = 0;

            if (usiLocalIndex % 2 == 0)
            {
                for (iSub = 0; iSub < m_iNumofIntfs - 1; iSub++)
                {
                    if (m_piUArr[k - 1][iSub] <= (usiLocalIndex - 2) / 2 &&
                                m_piUArr[k - 1][iSub + 1] > (usiLocalIndex - 2) /2)
                        break;
                }
                usiIndex = usiLocalIndex - m_piUArr[k - 1][iSub] * 2;
            }
            else
            {
                for (iSub = 0; iSub < m_iNumofIntfs - 1; iSub++)
                {
                    if (m_piCArr[k - 1][iSub] <= (usiLocalIndex - 1) / 2 &&
                                m_piCArr[k - 1][iSub + 1] > (usiLocalIndex - 1) /2)
                        break;
                }
                usiIndex = usiLocalIndex - m_piCArr[k - 1][iSub] * 2;
            }
            iEventIndex = pPrj->GenEventIndex((EVENTSUB)k, iSub + 1, usiIndex);
        }
        else
            iEventIndex = pPrj->GenEventIndex((EVENTSUB)k, m_iSubIndex,
                                                                usiLocalIndex);

        return (pPrj->GetInvAllEventsMap())[iEventIndex];
    }

} //end of namespace BDDHISC
