/*************************************************************************
  FILE:  BddHiscLowSub1.cpp
  DESCR: Some misc functions for low-levels
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#include "BddHiscSub.h"
#include "BddHiscLowSub.h"
#include <string>
#include "BddHiscDES.h"
#include "BddHiscErrmsg.h"
#include "BddHiscType.h"
#include "BddHiscPubfunc.h"
#include "BddHiscProject.h"
#include <cassert>
#include <fstream>
#include <fdd.h>
#include <cstdlib>
//Added by zain for Counter example
#include "CounterExampleAlgo.h"

using namespace std;

namespace BDDHISC
{

extern CProject *pPrj;

/**
 * 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 << "[INTERFACE]" << endl;
        for (int i = 0; i < this->GetNumofDES(); i++)
        {
            if (m_pDESArr[i]->GetDESType() == INTERFACE_DES)
            {
                fout << m_pDESArr[0]->GetDESName() << endl;
                break;
            }
        }

        fout << "[PLANT]" << endl;
        for (int i = 1; i < m_iNumofPlants + m_iNumofIntfs; 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 + m_iNumofIntfs; 
                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:   Get the interface DES pointer for this low-level,used by high-level.
 * PARA:    None
 * RETURN:  This low-level interface DES pointer
 * ACCESS:  public
 */
CDES * CLowSub::GetIntfDES()
{
    assert(m_pDESArr != NULL);
    for (int i = 0; i < this->GetNumofDES(); i++)
    {
        if (m_pDESArr[i]->GetDESType() == INTERFACE_DES)
            return m_pDESArr[i];
    }
    assert(false); //should never come here
    return m_pDESArr[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,Hisc_ChkInfo&  checkInfo,const string &vsExtraInfo)
{
    int *piBad = fdd_scanallvar(bddBad);
    string sErr;
    if (piBad != NULL)
    {
        if (viErrCode == HISC_VERI_LOW_UNCON)
            sErr = GetSubName() + 
                        ": Level-wise controllable check failed state:\n[ ";
        else if (viErrCode == HISC_VERI_LOW_BLOCKING)
        {
            if (showtrace == HISC_SHOW_TRACE)
                sErr = GetSubName() + ": Blocking state ";
            else
                sErr = GetSubName() + ": Blocking state: \n [ ";
        }
        else if (viErrCode == HISC_VERI_LOW_P4FAILED)
            {
				sErr = GetSubName() + ": Interface consistent condition Point 4 check failed state:\n[ ";
				checkInfo.setIFailureType(Hisc_ChkInfo::ReqAcptAlgo);
			}

        else if (viErrCode == HISC_VERI_LOW_P5FAILED)
        {
			sErr = GetSubName() + 
			": Interface consistent condition Point 5 check failed state:\n[ ";
			checkInfo.setIFailureType(Hisc_ChkInfo::IntrfImplAlgo);
		}
        else if (viErrCode == HISC_VERI_LOW_P6FAILED)
		{
            sErr = GetSubName() + 
			": Interface consistent condition Point 6 check failed state:\n[ ";
			checkInfo.setIFailureType(Hisc_ChkInfo::IntrfImplAlgo);
		}   

        //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 (int k = 0; k < 5; 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 this low-level local event index.
 * PARA:    k: R_EVENT/A_EVENT/H_EVENT/L_EVENT/LD_EVENT
 *          usiLocalIndex: this low-level local event index.
 * RETURN:  event name
 * ACCESS:  public
 */
string CLowSub::SearchEventName(EVENTSUB k, unsigned short usiLocalIndex)
{
    int iEventIndex = 0;
    iEventIndex = pPrj->GenEventIndex((EVENTSUB)k, m_iSubIndex, usiLocalIndex);
    return (pPrj->GetInvAllEventsMap())[iEventIndex];
}


} //end of namespace BDDHISC
