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

  FileName    [debug.c]

  PackageName [debug]

  Synopsis    [Debug package initialization, ending, and the command debug]

  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"
#include "imgInt.h"
#include "partInt.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 that build a bdd for the      */
/* simple example :                       */
/*     (state = 0) -> !(state = 1)        */
/******************************************/
mdd_t * buildDummyBdd(mdd_manager   *mddManager)
{
/** state0 = 0 **/
 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
 mdd_t * state0 =  mdd_one(mddManager);
 state0 = mdd_and(s0,s1,1,1);
/** state1 = 1 **/
 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
 mdd_t * state1 =  mdd_one(mddManager);
 state1 = mdd_and(ns0,ns1,1,1);
/** state = 0) -> !(state = 1) **/
 mdd_t * rel =  mdd_one(mddManager);
 rel =  mdd_or(state0,state1,0,0);
 
 return rel;
}


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

  Synopsis    [Implements the transtion command.]

  CommandName [_transition]

  CommandSynopsis [compute new transition relation]

  CommandArguments [\[-h\] \[-v\]]
  
  CommandDescription [This command create a new transition relation that is a
  and of the Bdd of the old one and an other bdd.
  <p>

  Command options:<p>  

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

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

  SideEffects [Change the fsm]

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

static int 
CommandTransition (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 _transition is under construction.\n");
}

Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
Ntk_Network_t  *network      = NIL(Ntk_Network_t);
mdd_manager    *mddManager; 
mdd_t          *rel          = NIL(mdd_t);
graph_t        *partition;
int            i;
/******************/
network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
if(network == NIL(Ntk_Network_t))
	return 1;
fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
if(fsm ==  NIL(Fsm_Fsm_t))
	return 1;
mddManager   = Fsm_FsmReadMddManager(fsm);



/**********   Build cex  ***********/
/* Here add the function           */
/* that build the Bdd to and       */
/* with the transtion relation     */
/***********************************/
rel = buildDummyBdd(mddManager);
if(rel == NIL(mdd_t))
{
	fprintf(vis_stdout,"Problem when building the new relation bdd");
	return 1;
}

/** Get image_info **/
Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
/**** The complete transtion relation ****/
// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
/*****************************************/
/*** For each latch rebuild the transition function ***/
/*** mvf table is composed of mdd for each possible ***/
/*** value of the latch                             ***/
ImgFunctionData_t * functionData = &(imageInfo->functionData);
array_t *roots = functionData->roots;
array_t *rangeVarMddIdArray = functionData->rangeVars;
char * nodeName;
arrayForEachItem(char *, roots, i, nodeName) {
	/* The new relation */ 
	vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
    int mddId = array_fetch(int, rangeVarMddIdArray, i);
	mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
	mdd_t * n_relation = mdd_and(relation,rel,1,1);
    /* Build for each possible value */
	int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
	int v ;
	Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
	for(v = 0; v<nbValue;v++)
	{
		 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
		 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
		 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
		 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);

	}
	/* Replace the function for the latch */
	Part_VertexSetFunction(vertex, newMvf);
//	printf("vertex %s changed % d\n",PartVertexReadName(vertex));
	Mvf_FunctionFree(mvf);
}

/** Change the fsm **/
fsm = Fsm_FsmCreateFromNetworkWithPartition(network, partition);
mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
Fsm_FsmComputeReachableStates(fsm,0,verbose,
				      0,0, 0,
				      0, 0, Fsm_Rch_Default_c,
				      0,1, NIL(array_t),
				      (verbose > 0),  NIL(array_t));
if(verbose)
	Fsm_FsmReachabilityPrintResults(fsm,3, 0);
/** Change Image Info **/
Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
					  (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
					  (void *) partition);


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 */

}