/**CFile***********************************************************************

  FileName    [debug.c]

  PackageName [debug]

  Synopsis    [Test package initialization, ending, and the command test.]

  Author      [Originated from SIS.]

  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
  All rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.

  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

******************************************************************************/

#include "debugInt.h"

static char rcsid[] UNUSED = "$Id: debug.c,v 1.6 2011/04/12  braun Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int Commandtransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);


/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [Initializes the test package.]

  SideEffects []

  SeeAlso     [Debug_End]

******************************************************************************/
void
Debug_Init(void)
{
  /*
   * Add a command to the global command table.  By using the leading
   * underscore, the command will be listed under "help -a" but not "help".
   */
  Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0);
  Cmd_CommandAdd("transition",  Commandtransition,      0);

}


/**Function********************************************************************

  Synopsis    [Ends the test package.]

  SideEffects []

  SeeAlso     [Debug_Init]

******************************************************************************/
void
Debug_End(void)
{
  /*
   * For example, free any global memory (if any) which the test package is
   * responsible for.
   */
}


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [Implements the _Debug_test command.]

  CommandName [_Debug_test]

  CommandSynopsis [template for implementing commands]

  CommandArguments [\[-h\] \[-v\]]
  
  CommandDescription [This command does nothing useful.  It merely serves as a
  template for the implementation of new commands.<p>

  Command options:<p>  

  <dl>
  <dt> -h
  <dd> Print the command usage.
  </dl>

  <dt> -v
  <dd> Verbose mode.
  </dl>
  ]

  SideEffects []

******************************************************************************/
static int
CommandDebug(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int            c;
  int            verbose = 0;              /* default value */

  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "vh")) != EOF) {
    switch(c) {
      case 'v':
        verbose = 1;
        break;
      case 'h':
        goto usage;
      default:
        goto usage;
    }
  }

  if (verbose) {
    (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
  }

  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
  printf("** DEBUG MODE **\n");
  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
  printf("model : %s\n", Hrc_NodeReadModelName(n));

  mdd_t * safe   = getSafe(fsm);
  mdd_t * forbid = getForbidden(fsm);
  mdd_t * reach  = getReach(fsm);
  
  if(safe == NIL(mdd_t))
  {
	printf("call command set_safe before\n");
	return 1;
  }
  if(forbid == NIL(mdd_t))
  {
	printf("call command set_forbidden before\n");
	return 1;
  }

  FILE*  oFile;
  oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
//  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);

  mdd_t * EFState = mdd_and(reach,safe,1,1);
//  mdd_t * errorState = mdd_and(reach,forbid,1,1);

  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
  array_t *careStatesArray = array_alloc(mdd_t *, 0);
  array_insert(mdd_t *, careStatesArray, 0,mddOne);

  mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
		   EFState,
           fsm->fairnessInfo.states,
           careStatesArray,
		   0,
           McDcLevelNone_c);

  mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
  mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);

  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
		   EXEFState,
           fsm->fairnessInfo.states,
           careStatesArray,
		   0,
           McDcLevelNone_c);
  mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
  mdd_t * andState =  mdd_xor(EXEFState2,EXEFState);
  mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
		   andState,
           fsm->fairnessInfo.states,
           careStatesArray,
		   0,
           McDcLevelNone_c);
  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
  andState =  mdd_xor(EXEFState2,andState);
  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
		   andState,
           fsm->fairnessInfo.states,
           careStatesArray,
		   0,
           McDcLevelNone_c);
  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
  andState =  mdd_xor(EXEFState2,andState);
  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);



  //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
  //mdd_GetState_Values(mddManager , EFState, stdout);
  fclose(oFile);





  return 0;		/* normal exit */

  usage:
  (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
  return 1;		/* error exit */
}



/**Function********************************************************************

  Synopsis [Returns a BDD array from an Mvf array]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static array_t *
markGetBddArray(array_t *mvfArray,  mdd_manager* mddManager)
{
    int 	  i,phase;
    array_t *bddArray;
    Mvf_Function_t *mvf;

    FILE*  oFile;
  oFile = Cmd_FileOpen("trans.bdd", "w", NIL(char *), 0);

    bddArray = array_alloc(bdd_node *,0);
 printf("mvf array : %d \n" , array_n(mvfArray));

    arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) {
	mdd_t     *mddTemp;
	bdd_node    *ddNode;

	mddTemp = array_fetch(mdd_t *, mvf, 1);
	ddNode = (bdd_node *) bdd_get_node(mddTemp,&phase);
	bdd_ref(ddNode);
    mdd_FunctionPrintMain(mddManager, mddTemp, "TRANS", oFile);
    printf("\n");
  	ddNode = phase ? bdd_not_bdd_node(ddNode) : ddNode;
    printf("%d --->",i);
    bdd_print(mddTemp);
    printf("\n");
	array_insert_last(bdd_node *, bddArray, ddNode);
    }
    fclose(oFile);
    return bddArray;
}

/**Function********************************************************************

  Synopsis [Returns a BDD array given an integer array of variable indices.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static bdd_node **
BddNodeArrayFromIdArray(
  bdd_manager	*ddManager,
  array_t	*idArray)
{
    bdd_node **xvars;
    int i,id;
    int nvars = array_n(idArray);

    xvars = ALLOC(bdd_node *, nvars);
    if (xvars == NULL)
	return NULL;

    for(i = 0; i < nvars; i++) {
	id = array_fetch(int,idArray,i);
	xvars[i] = bdd_bdd_ith_var(ddManager,id);
	bdd_ref(xvars[i]);
    }
    return xvars;
}
/**Function********************************************************************

  Synopsis [Compute the relation between an array of function and a 
  corresponding array of variables. A BDD is returned which represents
  AND(i=0 -> i<nVars)(yVars[i]==nextBdds). ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static bdd_node *
computeTransitionRelationWithIds(
  bdd_manager	*ddManager,
  array_t	*nextBdds,
  bdd_node	**yVars,
  int		nVars)
{
    bdd_node	*ddtemp1, *ddtemp2;
    bdd_node	*oldTR, *fn;
    int 		 i;


    oldTR = bdd_read_one(ddManager);

    for(i = 0; i < nVars; i++) {
	ddtemp2  = array_fetch(bdd_node *, nextBdds, i);

    bdd_print(ddtemp2);
	fn = bdd_bdd_xnor(ddManager,ddtemp2,yVars[i]);
	bdd_ref(fn);
	ddtemp1 = bdd_bdd_and(ddManager,oldTR,fn);
	bdd_ref(ddtemp1);
	bdd_recursive_deref(ddManager,fn);
	bdd_recursive_deref(ddManager,oldTR);
	oldTR = ddtemp1;
    }
    return oldTR;
}
/*
static mdd_t *
computeTransitionRelationWithIds_mdd(
  mdd_manager	*ddManager,
  array_t	*nextBdds,
  mdd_t	**yVars,
  int		nVars)
{
    mdd_t	*ddtemp1, *ddtemp2;
    mdd_t	*oldTR, *fn;
    int 		 i;


    oldTR = mdd_one(ddManager);

    for(i = 0; i < nVars; i++) {
	ddtemp2  = array_fetch(mdd_t *, nextBdds, i);

	fn = mdd_xnor(ddtemp2,yVars[i],1,1);
	ddtemp1 = mdd_and(oldTR,fn,1,1);
	mdd_free(oldTR);
	oldTR = ddtemp1;
    }

	mdd_ref(ddtemp1);
	mdd_free(fn);
    return oldTR;
}
*/

static int 
Commandtransition (Hrc_Manager_t ** hmgr,
		   int  argc, char ** argv){
  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  Ntk_Network_t *network = Fsm_FsmReadNetwork(fsm);
  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
  printf("** TRANSITION RELATION **\n");
  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
  printf("model : %s\n", Hrc_NodeReadModelName(n));

   graph_t *partition;
   bdd_node *tranRelation;
   bdd_node **xVars,**yVars, **piVars;

   
   array_t *tranFunArray, *leaveIds;
   array_t *nextBdds, *nextMvfs;
   int nVars, nPi;

   
    /*
     * tranFunArray is a list of next state funs.
     */

    tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm);
    char *name;
    int i;
    arrayForEachItem(char*, tranFunArray, i, name){
      Ntk_Node_t * latch = Ntk_NetworkFindNodeByName(network, name);
      printf("%s : mddid : %d\n",name , Ntk_NodeReadMddId(latch) );
      //int c =   Ntk_NodeReadMddId(latch);
    }

 array_t         *psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
  int                  arrSize = array_n( psVarsArray );

  for ( i = 0 ; i < arrSize ; ++i ) {
    int      mddId = array_fetch( int, psVarsArray, i );
    mvar_type mVar = array_fetch(mvar_type, 
				 mdd_ret_mvar_list(mddManager),mddId);
    printf("%s : mddid %d\n", mVar.name, mddId);
  }

 array_t *nsVarsArray  =  Fsm_FsmReadNextStateVars(fsm);
arrSize = array_n( nsVarsArray );

  for ( i = 0 ; i < arrSize ; ++i ) {
    int      mddId = array_fetch( int, nsVarsArray, i );
    mvar_type mVar = array_fetch(mvar_type, 
				 mdd_ret_mvar_list(mddManager),mddId);
    printf("%s : mddid %d\n", mVar.name, mddId);
  }


    leaveIds = array_join(Fsm_FsmReadInputVars(fsm),
			  Fsm_FsmReadPresentStateVars(fsm));
    /*
     * Get the BDDs for transition functions.Duplicate functions are returned.
     */
    partition = Fsm_FsmReadPartition(fsm);
    nextMvfs = Part_PartitionBuildFunctions(partition,tranFunArray,leaveIds,
					    NIL(mdd_t));

    array_free(leaveIds);
    array_free(tranFunArray);

 Mvf_Function_t *mvf = array_fetch(Mvf_Function_t *,nextMvfs,1);
 mdd_t * recupdd = array_fetch(mdd_t *, mvf, 0);
 printf("plop\n");
 bdd_print(recupdd);
/** Build cex **/

/** state0 **/
 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
 printf("****************\n");
 bdd_print (s0);
 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
 printf("****************\n");
 bdd_print (s1);
 mdd_t * and =  mdd_one(mddManager);
 and = mdd_and(s0,s1,1,1);
 mdd_t* reach = mdd_one(mddManager);
 reach = Fsm_FsmReadReachableStates(fsm);
 mdd_t * state0 =  mdd_and(and,reach,1,1);
/** next state1 **/
 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
 mdd_t * state1 = mdd_and(ns0,ns1,1,1);
/** new rel **/
 mdd_t * rel =  mdd_or(state0,state1,0,0);




// Get image_info 

  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);

   Img_PrintPartitionedTransitionRelation(mddManager,imageInfo, 0);

array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
 arrayForEachItem(mdd_t *, transRelation, i, recupdd){
 printf("****************\n");

    bdd_print(recupdd);
}
  mdd_t* new_rel = mdd_and(recupdd,rel,1,1);
FILE * oFile = fopen("relation.bdd","w");
 mdd_FunctionPrintMain(mddManager, recupdd, "TRANS", oFile);
 mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
 mdd_FunctionPrintMain(mddManager, rel, "REL", oFile);
 mdd_FunctionPrintMain(mddManager, new_rel, "new_rel", oFile);

fclose(oFile);
array_insert(mdd_t*,transRelation,0,new_rel);
Img_ReplacePartitionedTransitionRelation(imageInfo, transRelation,0);
 printf("****************\n");

Img_PrintPartitionedTransitionRelation(mddManager,imageInfo, 0);

 arrayForEachItem(mdd_t *, transRelation, i, recupdd){
 printf("****************\n");
 FsmResetReachabilityFields(fsm, 0);

    bdd_print(recupdd);
}

/*
FILE * dotFile = fopen("relation.dot","w");

mdd_dump_dot(reach,NIL(char),dotFile);
fclose(dotFile);
*/
//    nextBdds = markGetBddArray(nextMvfs,mddManager);

    Mvf_FunctionArrayFree(nextMvfs);
/*
 // Get the DdNodes for all the variables.

    piVars = BddNodeArrayFromIdArray(mddManager, 
					 Fsm_FsmReadInputVars(fsm));
    xVars = BddNodeArrayFromIdArray(mddManager, 
					Fsm_FsmReadPresentStateVars(fsm));
    yVars = BddNodeArrayFromIdArray(mddManager,
					Fsm_FsmReadNextStateVars(fsm));

    nVars = array_n(Fsm_FsmReadNextStateVars(fsm));
    nPi = array_n(Fsm_FsmReadInputVars(fsm));

    // Compute the transition relation 
    tranRelation = computeTransitionRelationWithIds(mddManager, nextBdds,
						    yVars, nVars);
 */
/*
 FILE*  oFile;
  oFile = Cmd_FileOpen("trans.bdd", "w", NIL(char *), 0);
mdd_FunctionPrintMain(mddManager, tranRelation, "TRANS", oFile);
 fclose(oFile);
 */
  return 0;
}