/*************************************************************************
  FILE:  BddSdLowSub1.cpp
  DESCR: Some misc functions for low-levels
  AUTH:  Raoguang Song, Yu Wang
  DATE:  (C) Jan, 2006, 2009
*************************************************************************/
#include "BddSdSub.h"
#include "BddSdLowSub.h"
#include <string>
#include "BddSdDES.h"
#include "BddSdErrmsg.h"
#include "BddSdType.h"
#include "BddSdPubfunc.h"
#include <cassert>
#include <fstream>
#include <fdd.h>
#include <cstdlib>
#include "CounterExampleAlgo.h"

using namespace std;

namespace BDDSD
{

extern CSub *pSub;

/**
 * DESCR:   Save DES list of low-levels in memory to a file (for checking)
 * PARA:    fout: output file stream
 * RETURN:  0: sucess -1: fail
 * ACCESS:  public
 */
int CLowSub::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 = 1; 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 < this->GetNumofDES(); 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 low-levels to a text file for checking
 * PARA:    fout: output file stream
 * RETURN:  0: sucess -1: fail
 * ACCESS:  public
 */
int CLowSub::PrintSubAll(ofstream & fout)
{
    try
    {
        if (PrintSub(fout) < 0)
            throw -1;

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

/*
 * DESCR: Generate Bad state info during verfication
 *        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 CLowSub::BadStateInfo(const bdd& bddBad, const int viErrCode,
                    const HISC_TRACETYPE showtrace, SD_ChkInfo& checkInfo,const string &vsExtraInfo)
{
    const char * DEBUG = "CLowSub::BadStateInfo():";
    if (bddfalse == bddBad)
    {
        VERBOSE(1) { PRINT_DEBUG << "bddBad = bddfalse" << endl; }
        return;
    }

    bdd bddBadTemp = bddBad;
    string sErr = GetSubName();

    if (viErrCode == HISC_VERI_LOW_UNCON)
        sErr += ": Untimed controllable check failed at following state(s):";
      //    else if (viErrCode == HISC_VERI_LOW_CON)
    else if (viErrCode == HISC_VERI_LOW_PCOMPLT)
        sErr += ": Plant Completeness check failed at following state(s):";
    else if (viErrCode == HISC_VERI_LOW_BLOCKING)
        sErr += ": Blocking state(s):";
    else if (viErrCode == HISC_VERI_LOW_P4FAILED)
        sErr += ": Interface consistent conditions Point 4 check failed state(s):";
    else if (viErrCode == HISC_VERI_LOW_P5FAILED)
        sErr += ": Interface consistent conditions Point 5 check failed state(s):";
    else if (viErrCode == HISC_VERI_LOW_P6FAILED)
        sErr += ": Interface consistent conditions Point 6 check failed state(s):";
    else if (viErrCode == HISC_VERI_LOW_ALF)
        sErr += ": ALF check failed state(s):";
    else if (viErrCode == HISC_VERI_LOW_PTB)
        sErr += ": Not proper timed behavior at state(s):";
    else if (viErrCode == HISC_VERI_LOW_SD_II)
        sErr += ": Failed SD Controllability condition II at state(s):";
    else if (viErrCode == HISC_VERI_LOW_SD_III_1)
        sErr += ": Failed SD Controllability condition III.1 at state(s):";
    else if (viErrCode == HISC_VERI_LOW_SD_III_2)
        sErr += ": Failed SD Controllability condition III.2 at state(s):";
    else if (viErrCode == HISC_VERI_LOW_SD_IV)
        sErr += ": Failed SD Controllability condition IV at state(s):";
    else if (viErrCode == HISC_VERI_LOW_ZERO_LB)
      // is this S-singular prohib behavior    
     //  sErr += ": S-singular Prohibitable Behavior fails:";
         sErr += ": There is some event has a lower bound less than 1 tick:";

    sErr += "\n\n";

    int count = 0;
    while (bddfalse != bddBadTemp && count < 10)
    {
        bdd bddstate = GetOneState(bddBadTemp);
        bddBadTemp -= bddstate;

        int *piBad = fdd_scanallvar(bddstate);

        if (NULL == piBad) break;

        //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_LOW_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 (unsigned short usi = 2;
                            usi <= m_usiMaxUnCon && bddNext == bddfalse;
                            usi += 2)
                    {
                        bddNext |=
                            bdd_replace(
                                bdd_relprod(
                                    m_pbdd_UnConTrans[(usi - 2) / 2],
                                    bddTemp,
                                    m_pbdd_UnConVar[(usi - 2) / 2]),
                                    m_pPair_UnConPrim[(usi - 2) / 2]) &
                            bddBad;
                    }
                    for (unsigned short usi = 1;
                        usi < (unsigned short) (m_usiMaxCon + 1) &&
                        bddNext == bddfalse; usi += 2)
                    {
                        bddNext |=
                            bdd_replace(
                                bdd_relprod(
                                    m_pbdd_ConTrans[(usi - 1) / 2],
                                    bddTemp,
                                    m_pbdd_ConVar[(usi - 1) / 2]),
                                    m_pPair_ConPrim[(usi - 1) / 2]) &
                            bddBad;
                    }

                    if (bddNext == bddfalse)  //this is a deadlock state
                    {
                        sErr += "[DeadLock]";
                        break;
                    }
                    else //not a deadlock state
                    {
                        bddBlock = bddBlock - bddTemp;
                        free(piBad);
                        piBad = NULL;
                        piBad = fdd_scanallvar(bddBlock);
                    }

                    count++;
                } while (piBad != NULL);

                if (piBad == NULL) //live lock
                {
                    sErr += "[LiveLock]";
                    piBad = fdd_scanallvar(bddBad);
                }
            }
        }

	  //        sErr += "\t<";
        sErr += "\t[";

		//Added by Zain for counter example
		//if(!checkInfo.getErrorAlgoFag())
		SD_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
				if(!checkInfo.getErrorAlgoFlag())
				{
					if(checkInfo.getErrorFlag())
					{
					int teststateid = (piBad[m_piDESPosArr[i] * 2])+1;
					temptuple[i]= (short)((piBad[m_piDESPosArr[i] * 2])+1);
					if(!checkInfo.getErrorAlgoFlag())
						{							
							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.getErrorAlgoFlag()))
				{
				//checkInfo.setErrorTuple(this->GetNumofDES(),temptuple);
				checkInfo.setErrorFlag();
				QString temp= QString::fromStdString(this->GetSubName());
				std::wstring temp1=temp.toStdWString();			
				checkInfo.setErrorSubSystemName(temp1);
				}


	//        sErr += ">\n";
        sErr += "]\n";

        free(piBad);
        piBad = NULL;

        count++;
    }

    if (bddfalse != bddBadTemp)
    {
        sErr += "\t...";
    }

    sErr += "\n" + vsExtraInfo;

    pSub->SetErr(sErr, viErrCode);

    return;
}

/**
 * DESCR:   Search event name from this low-level local event index.
 * PARA:    k: R_EVENT/A_EVENT/H_EVENT/L_EVENT
 *          usiLocalIndex: this low-level local event index.
 * RETURN:  event name
 * ACCESS:  public
 */
string CLowSub::SearchEventName(unsigned short usiLocalIndex)
{
    int iEventIndex = 0;
    iEventIndex = pSub->GenEventIndex(usiLocalIndex);
    return (pSub->GetInvAllEventsMap())[iEventIndex];
}

} //end of namespace BDDSD
