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

  FileName    [debug.c]

  PackageName [debug]

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

  Author      [Cecile B.]

  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 CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandGenerateNetworkCNF(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, 1);
  Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
  Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);
  Cmd_CommandAdd("print_network_cnf",  CommandGenerateNetworkCNF, 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                                            */
/*---------------------------------------------------------------------------*/


static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
{
  Ntk_Network_t * ntk;
  int c,verbose;
  Dbg_Abnormal_t * abnormal;
  ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (ntk == NIL(Ntk_Network_t)) {
	(void) fprintf(vis_stdout, "** abn error: No network\n");
	return 1;
  }
  while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
	switch(c) {
		case 'v':
			verbose = 1;
			break;
		}
 }
  abnormal = Dbg_DebugAbnormalAlloc(ntk);
  abnormal->verbose = verbose;
  Dbg_AddAbnormalPredicatetoNetwork(abnormal);
}
/**Function********************************************************************

  Synopsis    [Implements the _sat_debug command.]

  CommandName [_sat_debug]

  CommandSynopsis [locate faulty candidates]

  CommandArguments [\[-h\] \[-v\]]
  
  CommandDescription [This command compute the fault candidates of a given
  properties.<p>

  Command options:<p>  

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

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

  SideEffects []

******************************************************************************/
static int 
CommandSatDebug(
Hrc_Manager_t ** hmgr, 
int argc, 
char ** argv){
int            c,i;
int            verbose = 0;              /* default value */
BmcOption_t      * options = BmcOptionAlloc();
Ntk_Network_t    * network;
bAig_Manager_t   * manager;
array_t          * formulaArray;
array_t          * LTLformulaArray;
char             * ltlFileName     = NIL(char);
array_t          * faultNodes = array_alloc(Ntk_Node_t*,0);

/*
 * Parse command line options.
 */
if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
     return 1;
}


printf("MAX K %d", options->maxK);

if (verbose) {
  (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
}
/*
 *  Read the network
 */
network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
if (network == NIL(Ntk_Network_t)) {
  (void) fprintf(vis_stdout, "** _sat_debug error: No network\n");
  BmcOptionFree(options);
  return 1;
}
manager = Ntk_NetworkReadMAigManager(network);
if (manager == NIL(mAig_Manager_t)) {
  (void) fprintf(vis_stdout, "** _sat_debug error: run build_partition_maigs command first\n");
  BmcOptionFree(options);
  return 1;
}

Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
if(abn == NIL(Dbg_Abnormal_t)){
  (void) fprintf(vis_stdout, "_sat_debug error: Build Abnormal predicate.\n");
  return 1;
}
if(verbose)
  printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));


formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
if (formulaArray == NIL(array_t)) {
  (void) fprintf(vis_stderr,
  	   "** bmc error: error in parsing CTL* Fromula from file\n");
  BmcOptionFree(options);
  return 1;
}
if (array_n(formulaArray) == 0) {
  (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
  BmcOptionFree(options);
  Ctlsp_FormulaArrayFree(formulaArray);
  return 1;
}
LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
Ctlsp_FormulaArrayFree(formulaArray);
if (LTLformulaArray ==  NIL(array_t)){
  (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
  BmcOptionFree(options);
  return 1;
}
Ctlsp_Formula_t *ltlFormula  = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);



 /*
    Compute the cone of influence 
	here : a list of state variables (latches)
    TODO refine to COI of the property
  */
	st_table        *CoiTable =  generateAllLatches(network);
  /*
      Generate clauses for each time frame.  This is the old way of generating
      clauses in BMC.
    */
  	if(verbose)
	{	
		(void) fprintf(vis_stdout, "------      COI       ----\n");
		printLatch(CoiTable);
		(void) fprintf(vis_stdout, "--------------------------\n");
    }
    BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);


    //Generate ltl CNF
    // BmcGenerateCnfForLtl Génére la formule borné et retourne un index 
    // après il faut ajouter l'objectif de l'index avec boucle ou pas ...
    // cf. BmcLtlVerifyGeneralLtl
    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
    fprintf(vis_stdout, "\n");
    int k = options->maxK;
    int l;
    // return the clause number
    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);
   

	array_t *objClause = NIL(array_t);
	objClause = array_alloc(int, 0);   
	array_insert_last(int, objClause, noLoopIndex);
	BmcCnfInsertClause(cnfClauses, objClause);
    array_free(objClause);

	//Add Abnormal
    st_table * nodeToMvfAigTable =  NIL(st_table);
    nodeToMvfAigTable =
    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
    assert(nodeToMvfAigTable != NIL(st_table));

    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses);

    //loop abnormal
    int aIndex;
    Ntk_Node_t * abnNode;
    Dbg_ForEachAbnormal(abn,aIndex,abnNode){
      char * nodeName =  Ntk_NodeReadName(abnNode);
    //set abnormal
      int cnfIndex = array_fetch(int,abn->abnCnfIndexArray, aIndex);
      bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex);
      int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],0,cnfClauses);
      array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex);
      FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
      fclose(cnfFile);
      
      //SAT procedure 
      //assig assig input from cex
      //TODO build cex correctly
      int res = Dbg_SatCheck("assig",options->cnfFileName,options->verbosityLevel);
      // Build set of FaultCandidates
      if (res == SAT_SAT)
      {
        char * realNodeName = util_strsav(nodeName);
        realNodeName[strlen(nodeName)-4] = '\0';
        Ntk_Node_t * realNode =  Ntk_NetworkFindNodeByName(network,realNodeName);
        array_insert_last(Ntk_Node_t*,faultNodes,realNode);
      }


      array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
   }

	 if(verbose)
		(void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
		latches %d \n",cnfClauses->noOfClauses,st_count(CoiTable));
  
 	(void) fprintf(vis_stdout,"Number of Fault candidates %d\n",
    array_n(faultNodes));
 	(void) fprintf(vis_stdout,"gates : \n");
    printNodeArray(faultNodes);

    
Ctlsp_FormulaArrayFree(LTLformulaArray);    
BmcCnfClausesFree(cnfClauses);
BmcOptionFree(options);
array_free(faultNodes);
return 0;
 
}
/**Function********************************************************************

  Synopsis    [Implements the generate_network_cnf.]

  CommandName [generate_network_cnf]

  CommandSynopsis [generate a CNF view of the network]

  CommandArguments [\[-h\] \[-v\] \[-k\]  [fileName] ]
  
  CommandDescription [This command geerate a CNF of the network in DMACS form.
  The network may be unroll within k steps.
  <p>

  Command options:<p>  

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

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

  <dt> -k
  <dd> number of steps (default 1).
  </dl>
  ]

  SideEffects []

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

static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv)
{
  BmcOption_t  *options = BmcOptionAlloc();
  int c;
  unsigned int i;
  Ntk_Network_t * network;
  bAig_Manager_t   * manager;
  char *  outName = NIL(char);
   FILE *cnfFile;
  if (!options){
    return 1;
  }
  options->dbgOut = 0;
  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) {
    switch(c) {
    case 'h':
      goto usage;
    case 'k':
      options->maxK = atoi(util_optarg);
      break;
    case 'v':
      for (i = 0; i < strlen(util_optarg); i++) {
	if (!isdigit((int)util_optarg[i])) {
	  goto usage;
	}
      }
      options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
      break;
    default:
      goto usage;
    }
  }
   if (argc - util_optind != 0)
   {
      outName  = util_strsav(argv[util_optind]);
      /* create SAT Solver input file */
     options->cnfFileName= outName;
    options->satInFile = options->cnfFileName;
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
  }
  
 
/*
 *  Read the network
 */
network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
if (network == NIL(Ntk_Network_t)) {
  (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n");
  BmcOptionFree(options);
  return 1;
}
manager = Ntk_NetworkReadMAigManager(network);
if (manager == NIL(mAig_Manager_t)) {
  (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n");
  BmcOptionFree(options);
  return 1;
}

 /*
    Compute the cone of influence 
	here : a list of state variables (latches)
  */
st_table        *CoiTable =  generateAllLatches(network);

if(options->verbosityLevel)
{	
	(void) fprintf(vis_stdout, "------      COI       ----\n");
	printLatch(CoiTable);
	(void) fprintf(vis_stdout, "--------------------------\n");
}
BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
  if(outName != NIL(char))
  {
    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
    fclose(cnfFile);
  }
  else
     BmcWriteClauses(manager, vis_stdout, cnfClauses, options);

if(options->verbosityLevel)
{	
	(void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK);
    (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses,
    st_count(CoiTable));
} 
    
BmcOptionFree(options);
 return 0;
 usage:
  (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] <cnf_file>\n");
  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
  (void) fprintf(vis_stderr, "   -v <verbosity_level>\n");
  (void) fprintf(vis_stderr, "       verbosity_level = 0 => no feedback (Default)\n");
  (void) fprintf(vis_stderr, "       verbosity_level = 1 => code status\n");
  (void) fprintf(vis_stderr, "       verbosity_level = 2 => code status and CPU usage profile\n");
  (void) fprintf(vis_stderr, "   <cnf_file> The output file containing CNF of the network.\n");

  BmcOptionFree(options);
  return 1;
}

/**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;
}
if (verbose)
  mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);


/** 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));
}

/** Change the fsm and the network with a new partition and the new fsm **/
Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
					  (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
					  (void *) partition);
fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t));
mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
				      0,0, 0,
				      0, 0, Fsm_Rch_Default_c,
				      0,1, NIL(array_t),
				      (verbose > 0),  NIL(array_t));
fsm->reachabilityInfo.initialStates = init;
fsm->reachabilityInfo.reachableStates = reach;
if(verbose)
	Fsm_FsmReachabilityPrintResults(fsm,3, 0);

Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
			 (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
			 (void *) fsm);

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

}