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

  FileName    [robCmd.c]

  PackageName [rob]

  Synopsis    [Commands for the Robustness package.]

  Author      [Souheib Baarir, Denis Poitrenaud,J.M Ilié ]

  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. Paris VI].
  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 PARIS VI 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 "Robust.h"

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
static jmp_buf timeOutEnv;

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

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


/*************** Robustness functions  ******************************************/

static int CommandprintmddID     (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandRobustness     (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandSetSafe        (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandSetRequired    (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandSetForbidden   (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandSetInitial     (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandResetRequired  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandResetForbidden (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandResetSafe      (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandResetInitial   (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandPrintRequired  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandPrintSafe      (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandPrintForbidden (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandConvForbToProp (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandConvReachToProp (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandConvSafeToProp (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandConvReqToProp  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandConvInitToProp (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandSetLtlFormula  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandBmcRob         (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandResLtlFile     (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandTestCount      (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandComposeGolden  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandProtectGolden  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandProtectOutput  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandProtectRegister(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static int CommandTestRob        (Hrc_Manager_t ** hmgr,int  argc, char ** argv);


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

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


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


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

  Synopsis    [Initializes the rob package.]

  SideEffects []

  SeeAlso     [rob_End]

******************************************************************************/
void
Rob_Init(void)
{

/*************** Robustness commands  ****************************************/
  Cmd_CommandAdd("printmddID",     CommandprintmddID,       0);
  Cmd_CommandAdd("robustness",     CommandRobustness,       0);
  Cmd_CommandAdd("set_safe",       CommandSetSafe,          0);
  Cmd_CommandAdd("set_forbidden",  CommandSetForbidden,     0);
  Cmd_CommandAdd("set_required",   CommandSetRequired,      0);
  Cmd_CommandAdd("set_init",       CommandSetInitial,       0);
  Cmd_CommandAdd("reset_required", CommandResetRequired,    0);
  Cmd_CommandAdd("reset_forbidden",CommandResetForbidden,   0);
  Cmd_CommandAdd("reset_safe",     CommandResetSafe,        0);
  Cmd_CommandAdd("reset_init",     CommandResetInitial,     0);
  Cmd_CommandAdd("print_forbidden",CommandPrintForbidden,   0);
  Cmd_CommandAdd("print_required", CommandPrintRequired,    0);
  Cmd_CommandAdd("print_safe",      CommandPrintSafe,       0);
  Cmd_CommandAdd("conv_reach_prop", CommandConvReachToProp, 0);
  Cmd_CommandAdd("conv_safe_prop",  CommandConvSafeToProp,  0);
  Cmd_CommandAdd("conv_forb_prop",  CommandConvForbToProp,  0);
  Cmd_CommandAdd("conv_req_prop",   CommandConvReqToProp,   0);
  Cmd_CommandAdd("conv_init_prop",  CommandConvInitToProp,  0);
  Cmd_CommandAdd("add_ltl_formula", CommandSetLtlFormula,   0);
  Cmd_CommandAdd("bmc_rob",         CommandBmcRob,          0);
  Cmd_CommandAdd("reset_ltl_file",  CommandResLtlFile,      0);
  Cmd_CommandAdd("Test_count"    ,  CommandTestCount,       0);
  Cmd_CommandAdd("compose_golden",  CommandComposeGolden,   0);
  Cmd_CommandAdd("protect_golden",  CommandProtectGolden,   0);
  Cmd_CommandAdd("protect_outputs",  CommandProtectOutput,  0);
  Cmd_CommandAdd("protect_registers",CommandProtectRegister,0);
  Cmd_CommandAdd("test_rob",         CommandTestRob,        0);
 
/*****************************************************************************/

}

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/
void
Rob_End(void)
{
}

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

static int 
CommandprintmddID (Hrc_Manager_t ** hmgr,
		   int  argc, char ** argv){
  Fsm_Fsm_t  *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  mdd_manager      *mddManager = Fsm_FsmReadMddManager(fsm);
  array_t         *psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
  int                  arrSize = array_n( psVarsArray );
  int i;

  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 : %d\n", mVar.name, mddId);
  }
  return 0;
}

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

static int 
CommandTestCount (Hrc_Manager_t ** hmgr,
		   int  argc, char ** argv){
  char* fichier="./test";
  int k= 0;//main_Count_test_(fichier);
  printf("res= %d \n",k);
  return 0;
}


// Reset to empty, the file 
// of ltl properties.
static int 
CommandResLtlFile (Hrc_Manager_t ** hmgr,
		   int  argc, char ** argv){

  FILE* oFile = NIL(FILE);
  if (argc == 2) {
    oFile = Cmd_FileOpen(argv[1],
			 "w", NIL(char *), 0);
  }
  else{
    oFile = Cmd_FileOpen("properties.ltl",
			 "w", NIL(char *), 0);
  }
  
  fclose(oFile);

  return 0; 
}

// Add an ltl formula to the 
// the file of ltl properties.
static int 
CommandSetLtlFormula (Hrc_Manager_t ** hmgr,
		      int  argc, char ** argv){

  
  char c;
  int i=1;
  FILE* oFile=NIL(FILE); 

  if (argc < 2) {
    conv_error_msg(vis_stderr, "add_ltl_formula",earg); 
    return 1;
  }

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "f:")) != EOF) {
    switch(c) {
    case 'f':
      oFile = Cmd_FileOpen(util_optarg, 
			   "a+", NIL(char *), 0);
      i=3;
      break;
    default :
     break;
    }
  }
  
  if (i!=3) {
    oFile = Cmd_FileOpen("properties.ltl", 
			 "a+", NIL(char *), 0);
  }

  if (oFile == NIL(FILE)) {
    conv_error_msg(vis_stderr, 
		   "add_ltl_formula",eofile);
    return 1;
  }	
  
  fprintf(oFile," %s ;\n",argv[i]);
  fclose(oFile);
  
  return 0; 
}

// Convert the set of initial states
// to a propositional formula
// and put it in the proprerties file. 
static int 
CommandConvInitToProp (Hrc_Manager_t ** hmgr,
		       int  argc, char ** argv){

  FILE* oFile=NIL(FILE);
  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);

  if(fsm == NIL(Fsm_Fsm_t))
    return 1;
  
  if (argc == 2) {
    oFile = Cmd_FileOpen(argv[1],
			 "a+", NIL(char *), 0);
  }
  else{
    oFile = Cmd_FileOpen("properties.ltl",
		       "a+", NIL(char *), 0);
  }

  if (oFile == NIL(FILE)) {
     conv_error_msg(vis_stderr, "conv_init_prop",eofile);
    return 1;
  }
  
  mdd_t* set = getInitial(fsm);
  if (set == NIL(mdd_t)){
    conv_error_msg(vis_stderr, "conv_init_prop",ecmd);
    return 1;
  }
  
   mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
			 set, "INIT", oFile);
  
   fclose(oFile);		       
  return 0; 
}

// Convert the set of safe states
// to a propotitional formula
// and put it in the proprerties file. 
static int 
CommandConvReachToProp (Hrc_Manager_t ** hmgr,
		       int  argc, char ** argv){
  
  FILE* oFile=NIL(FILE);
  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);
 
  if(fsm == NIL(Fsm_Fsm_t))
    return 1;

  if (argc == 2) {
    oFile = Cmd_FileOpen(argv[1],
			 "a+", NIL(char *), 0);
  } else{
    oFile = Cmd_FileOpen("properties.ltl",
			 "a+", NIL(char *), 0);
  }

  if (oFile == NIL(FILE)) {
     conv_error_msg(vis_stderr, 
		    "conv_reach_prop",eofile);
    return 1;
  }
  
  mdd_t* set = getReach(fsm);
  if (set == NIL(mdd_t)){
    conv_error_msg(vis_stderr, 
		   "conv_reach_prop",ecmd);
   
    return 1;
  }
  
   mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
			 set, "REACH", oFile);
  
   fclose(oFile);		       
   return 0;
}

// Convert the set of safe states
// to a propotitional formula
// and put it in the proprerties file. 
static int 
CommandConvSafeToProp (Hrc_Manager_t ** hmgr,
		       int  argc, char ** argv){
  
  FILE* oFile=NIL(FILE);
  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);
 
  if(fsm == NIL(Fsm_Fsm_t))
    return 1;

  if (argc == 2) {
    oFile = Cmd_FileOpen(argv[1],
			 "a+", NIL(char *), 0);
  } else{
    oFile = Cmd_FileOpen("properties.ltl",
			 "a+", NIL(char *), 0);
  }

  if (oFile == NIL(FILE)) {
     conv_error_msg(vis_stderr, 
		    "conv_safe_prop",eofile);
    return 1;
  }
  
  mdd_t* set = getSafe(fsm);
  if (set == NIL(mdd_t)){
    conv_error_msg(vis_stderr, 
		   "conv_safe_prop",ecmd);
   
    return 1;
  }
  
   mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
			 set, "SAFE", oFile);
  
   fclose(oFile);		       
   return 0;
}

// Convert the set of required states
// to a propotitional formula
// and put it in the proprerties file. 
static int 
CommandConvReqToProp (Hrc_Manager_t ** hmgr,
		       int  argc, char ** argv){
  FILE* oFile=NIL(FILE);
  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);
 
  if(fsm == NIL(Fsm_Fsm_t))
    return 1;

  if (argc == 2) {
    oFile = Cmd_FileOpen(argv[1],
			 "a+", NIL(char *), 0);
  } else{
    oFile = Cmd_FileOpen("properties.ltl",
			 "a+", NIL(char *), 0);
  }
  
  if (oFile == NIL(FILE)) {
     conv_error_msg(vis_stderr, 
		    "conv_req_prop",eofile);
    return 1;
  }
  
  mdd_t* set = getRequired(fsm);
  if (set == NIL(mdd_t)){
    conv_error_msg(vis_stderr, 
		   "conv_req_prop",ecmd);
    return 1;
  }
  
   mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
			 set, "REQ", oFile);
   fclose(oFile);
		       
   return 0;
}

// Convert the set of forbidden states
// to a propotitional formula
// and put it in the proprerties file. 
static int 
CommandConvForbToProp (Hrc_Manager_t ** hmgr,
		       int  argc, char ** argv){
 FILE* oFile=NIL(FILE);
  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);
 
  if(fsm == NIL(Fsm_Fsm_t))
    return 1;

  if (argc == 2) {
    oFile = Cmd_FileOpen(argv[1],
			 "a+", NIL(char *), 0);
  } else{
    oFile = Cmd_FileOpen("properties.ltl",
			 "a+", NIL(char *), 0);
  }

  if (oFile == NIL(FILE)) {
    conv_error_msg(vis_stderr, 
		   "conv_forb_prop",eofile);
    return 1;
  }
  
  mdd_t* set = getForbidden(fsm);
  if (set == NIL(mdd_t)){
    conv_error_msg(vis_stderr, 
		   "conv_forb_prop",ecmd);
    return 1;
  }
  
  mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
			set, "FORB", oFile);
  fclose(oFile);       
  return 0;

}


// This command computes the set of forbiden states 
// w.r.t a given ctl formula. This formula is read from 
// a file given as a parameter.
static int
CommandSetForbidden( Hrc_Manager_t ** hmgr,
		    int  argc,
		    char ** argv){
  int c;
  FILE* forFile=NIL(FILE);
  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);
 
  if(fsm == NIL(Fsm_Fsm_t))
    return 1;

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "h")) != EOF) {
    switch(c) {
      case 'h':
      default:
	(void)error_msg(vis_stderr,"forbiden", ecmd) ;
        return 1;
    }
  }

  if ((argc - util_optind == 0) || 
      (argc - util_optind > 1) ) {
    (void)error_msg(vis_stderr, "forbiden",enfile ) ;
    return 1;
  }
 
  forFile = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
  if (forFile == NIL(FILE)) {
    error_msg(vis_stderr, "forbiden",eofile);
    return 1;
  }
  
  fsm->RobSets.fForb=forFile;

  if (fsm->RobSets.Forb != NIL(mdd_t))
    mdd_free(fsm->RobSets.Forb);

  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
  array_t *careStatesArray = array_alloc(mdd_t *, 0);
  array_insert(mdd_t *, careStatesArray, 0,mddOne);
 
  if (Fsm_FsmReadFairnessConstraint(fsm)!=
	   NIL(Fsm_Fairness_t)) {
    Fsm_FsmComputeFairStates(fsm,
			     careStatesArray,
			     0, 
			     McDcLevelNone_c,
			     McGSH_Unassigned_c ,
			     McBwd_c, FALSE );
    }
  else {
    
    fsm->fairnessInfo.states = 
      mdd_one(Fsm_FsmReadMddManager(fsm));

  }

  fsm->RobSets.Forb=
    evaluate(fsm,forFile,  
	     fsm->fairnessInfo.states, 
	     Fsm_FsmReadFairnessConstraint(fsm),0);
  
  array_free(careStatesArray);
  mdd_free(mddOne);

  
  return 0; 
}

// This command sets the forbiden set of states to 
// mdd_zero.This means that all states are allowed.
static int
CommandResetForbidden( Hrc_Manager_t ** hmgr,
		      int  argc,
		      char ** argv){
  
  Fsm_Fsm_t *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);

  if(fsm == NIL(Fsm_Fsm_t))
    return 1;
  
  if (fsm->RobSets.Forb != NIL(mdd_t))
    mdd_free(fsm->RobSets.Forb);

  fsm->RobSets.Forb=
    mdd_zero(Fsm_FsmReadMddManager(fsm));
  fsm->RobSets.fForb = NIL(FILE);
  return 0;
}

static int
CommandPrintForbidden( Hrc_Manager_t ** hmgr,
		      int  argc,
		      char ** argv){

  char formula[1024] ;

  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);
  
  if(fsm == NIL(Fsm_Fsm_t))
    return 1;
  
  if (fsm->RobSets.fForb != NIL(FILE)){
    fseek(fsm->RobSets.fForb,0,SEEK_SET);
    fread (formula,sizeof(char),1024,fsm->RobSets.fForb);
    printf("Forbiden is the set of states that satisfy: %s\n",formula);
  }
  else{
     printf("Forbiden is the set of states that satisfy: FALSE \n");
  }

  return 0;

}

// This command computes the set of required states 
// w.r.t a given ctl formula. This formula is read from 
// a file given as a parameter.
static int
CommandSetRequired( Hrc_Manager_t ** hmgr,
		    int  argc,
		    char ** argv){ 

  int c;
  FILE* reqFile=NIL(FILE);
  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);

  if(fsm == NIL(Fsm_Fsm_t))
    return 1;

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "h")) != EOF) {
    switch(c) {
      case 'h':
      default:
      	(void)error_msg(vis_stderr,"required", ecmd); 
        return 1;
    }
  }

  if ((argc - util_optind == 0) || 
      (argc - util_optind > 1) ) {
    (void)error_msg(vis_stderr, "required", enfile); 
    return 1;
  }
 
  reqFile = 
    Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);

  if (reqFile == NIL(FILE)) {
    error_msg(vis_stderr, "required", eofile);  
    return 1;
  }

  fsm->RobSets.fReq=reqFile;

  if (fsm->RobSets.Req != NIL(mdd_t))
    mdd_free(fsm->RobSets.Req);


  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
  array_t *careStatesArray = array_alloc(mdd_t *, 0);
  array_insert(mdd_t *, careStatesArray, 0,mddOne);
 
  if (Fsm_FsmReadFairnessConstraint(fsm)!=
	   NIL(Fsm_Fairness_t)) {
    Fsm_FsmComputeFairStates(fsm,
			     careStatesArray,
			     0, 
			     McDcLevelNone_c,
			     McGSH_Unassigned_c ,
			     McBwd_c, FALSE );
    }
  else {
    
    fsm->fairnessInfo.states = 
      mdd_one(Fsm_FsmReadMddManager(fsm));

  }

  fsm->RobSets.Req=  
    evaluate(fsm,reqFile,  
	     fsm->fairnessInfo.states, 
	     Fsm_FsmReadFairnessConstraint(fsm),0);
  
  array_free(careStatesArray);
  mdd_free(mddOne);

 
  return 0;
 
}

// This command sets the required set of states to 
// mdd_one.This means that no restriction is given.
static int
CommandResetRequired( Hrc_Manager_t ** hmgr,
		      int  argc,
		      char ** argv){
  
  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);

  if(fsm == NIL(Fsm_Fsm_t))
    return 1;
  
  if (fsm->RobSets.Req != NIL(mdd_t))
    mdd_free(fsm->RobSets.Req);

  fsm->RobSets.Req=
    mdd_one(Fsm_FsmReadMddManager(fsm));
   fsm->RobSets.fReq = NIL(FILE);
  return 0;
}

static int
CommandPrintRequired( Hrc_Manager_t ** hmgr,
		    int  argc,
		    char ** argv){

  char formula[1024] ;

  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);
  
  if(fsm == NIL(Fsm_Fsm_t))
    return 1;
  
  if (fsm->RobSets.fReq != NIL(FILE)){
    fseek(fsm->RobSets.fReq,0,SEEK_SET);
    fread (formula,sizeof(char),1024,fsm->RobSets.fReq);
    printf("Required is the set of states that satisfy: %s\n",formula);
  }
  else{
     printf("Required is the set of states that satisfy: TRUE \n");
  }

  return 0;

}
// This command computes the set of safe states 
// w.r.t a given ctl formula. This formula is read from 
// a file given as a parameter.
static int
CommandSetSafe( Hrc_Manager_t ** hmgr,
		int  argc,
		char ** argv){
  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);
  FILE *safeFile=NIL(FILE);
  int        c;
 
  if(fsm == NIL(Fsm_Fsm_t))
    return 1;

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "h")) != EOF) {
    switch(c) {
      case 'h':
      default:
	(void) error_msg(vis_stderr, "safe", ecmd); 
        return 1;
    }
  }

  if ((argc - util_optind == 0) || 
      (argc - util_optind > 1) ) {
    (void)error_msg(vis_stderr, "safe", enfile);
    return 1;
  }

  safeFile = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);

  if (safeFile == NIL(FILE)) {
    error_msg(vis_stderr, "safe", eofile);
    return 1;
  }



  fsm->RobSets.fSafe=safeFile;

  if (fsm->RobSets.Safe != NIL(mdd_t))
    mdd_free(fsm->RobSets.Safe);

  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
  array_t *careStatesArray = array_alloc(mdd_t *, 0);
  array_insert(mdd_t *, careStatesArray, 0,mddOne);
 
  if (Fsm_FsmReadFairnessConstraint(fsm)!=
	   NIL(Fsm_Fairness_t)) {
    Fsm_FsmComputeFairStates(fsm,
			     careStatesArray,
			     0, 
			     McDcLevelNone_c,
			     McGSH_Unassigned_c ,
			     McBwd_c, FALSE );
    }
  else {
    
    fsm->fairnessInfo.states = 
      mdd_one(Fsm_FsmReadMddManager(fsm));

  }

  fsm->RobSets.Safe=
    evaluate(fsm,safeFile,  
	     fsm->fairnessInfo.states, 
	     Fsm_FsmReadFairnessConstraint(fsm),0);
  
  array_free(careStatesArray);
  mdd_free(mddOne);

  return 0;
}

// This command sets the safe set of states to 
// the reachable set of states (without bit-flips).
static int
CommandResetSafe( Hrc_Manager_t ** hmgr,
		  int  argc,
		  char ** argv){
  
  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);

  if(fsm == NIL(Fsm_Fsm_t))
    return 1;
  
  if (fsm->RobSets.Safe != NIL(mdd_t))
    mdd_free(fsm->RobSets.Safe);

  mdd_t* inits=fsm->reachabilityInfo.initialStates;
  mdd_t* reachs=fsm->reachabilityInfo.reachableStates;
  fsm->reachabilityInfo.initialStates=NIL(mdd_t);
  fsm->reachabilityInfo.reachableStates=NIL(mdd_t);

  (void)Fsm_FsmComputeInitialStates(fsm);
  (void)Fsm_FsmComputeReachableStates(fsm,0,0,
				      0,0, 0,
				      0, 0, Fsm_Rch_Default_c,
				      0,0, NIL(array_t),
				      0,  NIL(array_t));

  fsm->RobSets.Safe=
    mdd_dup(fsm->reachabilityInfo.reachableStates);

  mdd_free(fsm->reachabilityInfo.initialStates);
  mdd_free(fsm->reachabilityInfo.reachableStates);
  fsm->reachabilityInfo.initialStates=inits;
  fsm->reachabilityInfo.reachableStates=reachs;
  fsm->RobSets.fSafe = NIL(FILE);
 
  return 0;
}

static int
CommandPrintSafe( Hrc_Manager_t ** hmgr,
		    int  argc,
		    char ** argv){

  char formula[1024] ;

  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);
  
  if(fsm == NIL(Fsm_Fsm_t))
    return 1;
  
  if (fsm->RobSets.fSafe != NIL(FILE)){
    fseek(fsm->RobSets.fSafe,0,SEEK_SET);
    fread (formula,sizeof(char),1024,fsm->RobSets.fSafe);
    printf("Safe is the set of states that satisfy: %s\n",formula);
  }
  else{
    printf("Safe is the set of states that is orginaly rechable from the design  \n");
  }

  return 0;

}

// This command computes the disign's initial set of states, 
// starting from the reachable states and  
// taking into acount all bit-flips arriving on non 
// protected sequecial elements. The set of protected sequencial 
// elements are given as parameter in a given file. 
static int 
CommandSetInitial(Hrc_Manager_t ** hmgr,
		  int  argc,
		  char ** argv){
  FILE       *proFile=NIL(FILE);
  FILE       *forFile=NIL(FILE);
  Fsm_Fsm_t  *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  static int  verbosityLevel=0;
  static int  printStep=0;
  int         formula=0;
  long        initialTime;
  long        finalTime;
  int         c;
  int         fmodel = 1;
 
  if(fsm == NIL(Fsm_Fsm_t))
    return 1;

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "hg:s:v:f:m:")) != EOF) {
    switch(c) {
     case 'g' :
       proFile = Cmd_FileOpen(util_optarg,"r", NIL(char *), 0);
       if (proFile == NIL(FILE)) {
	 error_msg(vis_stderr, "init", eiofile);
	return 1;
       }	
      break;
    case 'f' :
       forFile = Cmd_FileOpen(util_optarg,"r", NIL(char *), 0);
       if (forFile == NIL(FILE)) {
	 error_msg(vis_stderr, "init", eiofile);
	return 1;
       }	
       formula=1;
      break;
     case 's' :
       printStep = atoi(util_optarg); break;
     case 'v' :
       verbosityLevel = atoi(util_optarg); break; 
     case 'm' :
       
       if (strcmp(util_optarg, "usut") == 0) {fmodel = 2;break;}
       if (strcmp(util_optarg, "usmt") == 0) {fmodel = 3;break;}
       if (strcmp(util_optarg, "msut") == 0) {fmodel = 4;break;}
       if (strcmp(util_optarg, "msmt") == 0) {fmodel = 5;break;}
       

     case 'h':	
     default : error_msg(vis_stderr, "init", eicmd); return 1;
    }
  }

  if (fsm->reachabilityInfo.initialStates!=NIL(mdd_t)){
    mdd_free(fsm->reachabilityInfo.initialStates);
    fsm->reachabilityInfo.initialStates=NIL(mdd_t);
  }

  if (fsm->reachabilityInfo.reachableStates!=NIL(mdd_t)){
    mdd_free(fsm->reachabilityInfo.reachableStates);
    fsm->reachabilityInfo.reachableStates=NIL(mdd_t);
  }

  initialTime = util_cpu_time();
  (void)Fsm_FsmComputeInitialStates(fsm);
  (void)Fsm_FsmComputeReachableStates(fsm,0,0,
				      0,0, 0,
				      0,0, Fsm_Rch_Default_c,
				      0,0, NIL(array_t),
				      0,   NIL(array_t));
  
  fsm->RobSets.originalreachableStates = 
    mdd_dup(fsm->reachabilityInfo.reachableStates);
  
  if (fsm->reachabilityInfo.initialStates!=NIL(mdd_t)){
    mdd_free(fsm->reachabilityInfo.initialStates);
    fsm->reachabilityInfo.initialStates=NIL(mdd_t);
  }

 //mdd_free(fsm->reachabilityInfo.initialStates);
 
  if (fmodel == 1)
    fsm->reachabilityInfo.initialStates= 
      compute_error_states(fsm,fsm->reachabilityInfo.reachableStates,   
			   verbosityLevel,printStep, proFile);
  
  if (fmodel == 2)
    fsm->reachabilityInfo.initialStates= 
      error_states_us_ut(fsm,fsm->reachabilityInfo.reachableStates,proFile);

  if (fmodel == 3)
    fsm->reachabilityInfo.initialStates= 
      error_states_us_mt(fsm,fsm->reachabilityInfo.reachableStates, proFile);

  if (fmodel == 4)
    fsm->reachabilityInfo.initialStates= 
      error_states_ms_ut(fsm,fsm->reachabilityInfo.reachableStates, proFile);

  if (fmodel == 5){
     (void)Fsm_FsmComputeInitialStates(fsm);
     mdd_t* S0 = mdd_dup(fsm->reachabilityInfo.initialStates);
      mdd_free(fsm->reachabilityInfo.initialStates);
    fsm->reachabilityInfo.initialStates= 
      error_states_ms_mt(fsm,S0,fsm->reachabilityInfo.reachableStates, proFile);
    mdd_free(S0);
  }
    
  
  mdd_free(fsm->reachabilityInfo.reachableStates);
  fsm->reachabilityInfo.reachableStates=NIL(mdd_t);
  
  if(!formula) {
    fsm->reachabilityInfo.reachableStates=
      Fsm_FsmComputeReachableStates(fsm,0,0,
				  0,0, 0,
				  0, 0, Fsm_Rch_Default_c,
				  0,0, NIL(array_t),
				  0,  NIL(array_t));
  }
  else {
    mdd_t* newinit_tmp=evaluate(fsm,forFile,NIL(mdd_t), 
				Fsm_FsmReadFairnessConstraint(fsm),0);
    mdd_t* newinit=mdd_and(fsm->reachabilityInfo.initialStates,
  			   newinit_tmp,1,1);

    mdd_free(newinit_tmp);
    mdd_free(fsm->reachabilityInfo.initialStates);
    fsm->reachabilityInfo.initialStates=newinit;
    mdd_free(fsm->reachabilityInfo.reachableStates);
    fsm->reachabilityInfo.reachableStates=
      Fsm_FsmComputeReachableStates(fsm,0,0,
				  0,0, 0,
				  0, 0, Fsm_Rch_Default_c,
				  0,0, NIL(array_t),
				  0,  NIL(array_t));
  }

  finalTime = util_cpu_time();
    
  if(verbosityLevel){ 
   (void) fprintf(vis_stdout,"********************************\n");
     print_number_of_states("Error states                        = ", fsm,  
			   fsm->reachabilityInfo.initialStates);
     print_number_of_states("States reachable from error states  = ", fsm,  
			   fsm->reachabilityInfo.reachableStates);
     print_number_of_states("Reachable states whithout faults   = ", fsm,  
			    fsm->RobSets.originalreachableStates);
    (void) fprintf(vis_stdout, "%-50s%15g\n",
	                    "Analysis time                       = ",
		            (double)(finalTime-initialTime)/1000.0);

//    printf("-----------------------------------------------\n");
//    print_bdd(Fsm_FsmReadMddManager(fsm), fsm->reachabilityInfo.reachableStates);
//    bdd_print(fsm->reachabilityInfo.reachableStates);
//    printf("-----------------------------------------------\n");
  }
  
  return 0;
}

// This command sets the design's initial set of states 
// to the original one (without bit-flips). It also computes 
// the reachable states according to this initial set.  
static int
CommandResetInitial( Hrc_Manager_t ** hmgr,
		     int  argc,
		     char ** argv){
  
  Fsm_Fsm_t  *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);

  if(fsm == NIL(Fsm_Fsm_t))
    return 1;

  if (fsm->reachabilityInfo.initialStates!=NIL(mdd_t)){
    mdd_free(fsm->reachabilityInfo.initialStates);
    fsm->reachabilityInfo.initialStates=NIL(mdd_t);
  }
  
  if (fsm->reachabilityInfo.reachableStates!=NIL(mdd_t)){
    mdd_free(fsm->reachabilityInfo.reachableStates);
    fsm->reachabilityInfo.reachableStates=NIL(mdd_t);
  }
  (void)Fsm_FsmComputeInitialStates(fsm);
  (void)Fsm_FsmComputeReachableStates(fsm,0,0,
				      0,0, 0,
				      0, 0, Fsm_Rch_Default_c,
				      0,0, NIL(array_t),
				      0,  NIL(array_t));
  return 0;
}

// This command computes the design's robustness. 
// This needs the evaluation of the diffirent ctl formulae :
// 1- A[!forbiden U Required & A[!forbiden U Safe]]
// 2- A[!forbiden U Required & E[!forbiden U Safe]]
// 3- E[!forbiden U Required & A[!forbiden U Safe]]
// 4- E[!forbiden U Required & E[!forbiden U Safe]].

static int
CommandRobustness( Hrc_Manager_t ** hmgr,
		   int  argc,
		   char ** argv) {  
  int        c;
  mdd_t      *reachableStates = NIL(mdd_t);
  mdd_t      *initialStates;
  long        initialTime;
  long        finalTime;
  static int  verbosityLevel;
  static int  printStep;
  static int  timeOutPeriod;
  Fsm_Fsm_t  *fsm = 
    Fsm_HrcManagerReadCurrentFsm(*hmgr);
  static int reorderFlag;
  static int reorderThreshold;
  static int shellFlag;
  static int depthValue;
  static int incrementalFlag;
  static int approxFlag;
  static int ardc;
  static int recompute;
  Fsm_RchType_t rchType;

  static int req;
  FILE *reqFile=NIL(FILE);
  static int forb;
  FILE *forFile=NIL(FILE);
  static int pro;
  FILE *proFile=NIL(FILE);
  static int fair;
  FILE *fairFile=NIL(FILE);
  static int init=0;
  boolean rob1 = 0;

  FILE *guideFile = NIL(FILE); /* file of hints for guided search */
  array_t *guideArray = NIL(array_t);

  Img_MethodType imgMethod;
  mdd_t      * error_states;
  mdd_t      *reach,   *notReach; /* Etats accessibles du syst�me original */
  mdd_t      *tmp1,    *tmp2;
  EpDouble   *error    = EpdAlloc();
  EpDouble   *err      = EpdAlloc();
  EpDouble   *nbstates = EpdAlloc();
  EpDouble   *rch      = EpdAlloc();
  EpDouble   *error0   = EpdAlloc();
  char        percent[1024];
  char        nbst[1024];
  mdd_t      *forbiden, *required, *notforbiden,*fairS;
  mdd_t      *XU_notForb_And_Safe;
  mdd_t      *Req_And_XU_notForb_And_Safe;
  mdd_t      *Setformula;
  mdd_t      *res,*res_r,*res_0;
  Fsm_Fairness_t * fairCons=NIL(Fsm_Fairness_t);

 
  verbosityLevel = 0;
  printStep      = 0;
  timeOutPeriod  = 0;
  shellFlag = 0;
  depthValue = 0;
  incrementalFlag = 0;
  rchType = Fsm_Rch_Default_c;
  approxFlag = 0;
  ardc = 0;
  recompute = 0;
 
  if(fsm == NIL(Fsm_Fsm_t))
    return 1;

  util_getopt_reset();

  while ((c = util_getopt(argc, argv, "hs:r:v:")) != EOF) {
    switch(c) {
    case 's':
      printStep = atoi(util_optarg);
      break;
    case 'v':
      verbosityLevel = atoi(util_optarg);
      break; 
	case 'r':
		rob1= atoi(util_optarg);
		break;
    case 'h':
    default : 
      error_msg(vis_stderr, "rob", ercmd); return 1;
    }
  }

  mdd_t* Forb = getForbidden(fsm);
  mdd_t* Req  = getRequired(fsm); 
  mdd_t* Safe = getSafe(fsm); 
  mdd_t* Init = getInitial(fsm) ;
  mdd_t* Orig = getReachOrg(fsm);

  if ((Fsm_FsmReadFairnessConstraint(fsm))!=
      NIL(Fsm_Fairness_t)) {
    compute_fair(fsm,verbosityLevel);
  } 
  else {
    fsm->fairnessInfo.states = 
      mdd_one(Fsm_FsmReadMddManager(fsm)); 
  }
  
  get_number_of_states(fsm,fsm->reachabilityInfo.reachableStates, error); 
  get_number_of_states(fsm,Init, error0);
  get_number_of_states(fsm,Orig, rch);
  
  //Compute robustness 1
  if(rob1)
  {
	    (void) fprintf(vis_stdout,"********************************\n");
	    (void) fprintf(vis_stdout, 
		 "Dealing with  F = AG[Safe]]\n");
	    initialTime = util_cpu_time(); 
		Setformula= mdd_not(evaluate_EF(fsm, Safe, fsm->fairnessInfo.states,
		verbosityLevel));
		finalTime = util_cpu_time();
		res_0=mdd_and(Init, Setformula, 1, 1);
		res_r=mdd_and(Orig,Setformula, 1, 1); 
		mdd_free(Setformula);
  
		get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0);
		EpdGetString(nbstates, nbst);EpdCopy(error0, err);  EpdSubtract2(err, nbstates);
		EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
		(void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
			 "  --Error states satisfying F                                        = ", 
			 nbst,percent);
  
		get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r);
		EpdGetString(nbstates, nbst); EpdCopy(rch, err);  EpdSubtract2(err, nbstates);
		EpdDivide2(nbstates, rch);  EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
		(void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
		  "  --Error states originaly reachable by the design and satisfying F  = ", 
		  nbst,percent);
   
		(void) fprintf(vis_stdout, "%-50s%15g\n",
		  "  Analysis time                                                      = ", 
		  (double)(finalTime-initialTime)/1000.0);
	// EG	     
     (void) fprintf(vis_stdout,"********************************\n");	
     (void) fprintf(vis_stdout,
      	  "Dealing with F =  EG[Safe]] \n");
 
     initialTime = util_cpu_time();

     Setformula=evaluate_EG(fsm, mdd_not(Safe), fsm->fairnessInfo.states,NIL(Fsm_Fairness_t),verbosityLevel);
     finalTime = util_cpu_time();
     
     res_0=mdd_and(Init, Setformula, 1, 1);
     res_r=mdd_and(Orig,Setformula, 1, 1); mdd_free(Setformula);
 
     get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0);
     EpdGetString(nbstates, nbst);EpdCopy(error0, err);  EpdSubtract2(err, nbstates);
     EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
     (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
      	  "  --Error states satisfying F                                        = ", 
      	  nbst,percent);
    
     get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r);
     EpdGetString(nbstates, nbst); EpdCopy(rch, err);  EpdSubtract2(err, nbstates);
     EpdDivide2(nbstates, rch);EpdMultiply(nbstates,100);  EpdGetString(nbstates, percent);
     (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
      	  "  --Error states originaly reachable by the design and satisfying F  = ", 
      	  nbst,percent);
  
     (void) fprintf(vis_stdout, "%-50s%15g\n",               
      	  "  Analysis time                                                      = ", 
      	  (double)(finalTime-initialTime)/1000.0);

  } 
 else{
 	   (void) fprintf(vis_stdout,"********************************\n");
 	   (void) fprintf(vis_stdout, 
 	     	 "Dealing with  F = A[!forbiden U Required & A[!forbiden U Safe]]\n");
 	   initialTime = util_cpu_time(); 
 	   Setformula= evaluate_Formula_AF_AF (fsm, Req,Forb,Safe, verbosityLevel );
 	   finalTime = util_cpu_time();
 	   res_0=mdd_and(Init, Setformula, 1, 1);
 	   res_r=mdd_and(Orig,Setformula, 1, 1); 
        mdd_free(Setformula);
 	   
 	   get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0);
 	   EpdGetString(nbstates, nbst);EpdCopy(error0, err);  EpdSubtract2(err, nbstates);
 	   EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
 	   (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
 	     	 "  --Error states satisfying F                                        = ", 
          	 nbst,percent);
 	   
 	   get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r);
 	   EpdGetString(nbstates, nbst); EpdCopy(rch, err);  EpdSubtract2(err, nbstates);
 	    EpdDivide2(nbstates, rch);  EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
 	    (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
 	     	  "  --Error states originaly reachable by the design and satisfying F  = ", 
          	  nbst,percent);
 	    
 	    (void) fprintf(vis_stdout, "%-50s%15g\n",
      	  "  Analysis time                                                      = ", 
      	  (double)(finalTime-initialTime)/1000.0);
     
     
     (void) fprintf(vis_stdout,"********************************\n");	
     (void) fprintf(vis_stdout,
      	  "Dealing with F =  E[!forbiden U Required & A[!forbiden U Safe]] \n");
 
     initialTime = util_cpu_time();
     Setformula=evaluate_Formula_EF_AF (fsm, Req,Forb,Safe, verbosityLevel );
     finalTime = util_cpu_time();
     
     res_0=mdd_and(Init, Setformula, 1, 1);
     res_r=mdd_and(Orig,Setformula, 1, 1); mdd_free(Setformula);
 
     get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0);
     EpdGetString(nbstates, nbst);EpdCopy(error0, err);  EpdSubtract2(err, nbstates);
     EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
     (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
      	  "  --Error states satisfying F                                        = ", 
      	  nbst,percent);
    
     get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r);
     EpdGetString(nbstates, nbst); EpdCopy(rch, err);  EpdSubtract2(err, nbstates);
     EpdDivide2(nbstates, rch);EpdMultiply(nbstates,100);  EpdGetString(nbstates, percent);
     (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
      	  "  --Error states originaly reachable by the design and satisfying F  = ", 
      	  nbst,percent);
  
     (void) fprintf(vis_stdout, "%-50s%15g\n",               
      	  "  Analysis time                                                      = ", 
      	  (double)(finalTime-initialTime)/1000.0);
    }
  /* 
   (void) fprintf(vis_stdout,"********************************\n");	
   (void) fprintf(vis_stdout,
		  "Dealing with F = A[!forbiden U Required & E[!forbiden U Safe]] \n");
   initialTime = util_cpu_time();
   Setformula=evaluate_Formula_AF_EF (fsm, Req,Forb,Safe, verbosityLevel );
   finalTime = util_cpu_time();

   res_0=mdd_and(Init, Setformula, 1, 1);
   res_r=mdd_and(Orig,Setformula, 1, 1); mdd_free(Setformula);
   
   get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0);
   EpdGetString(nbstates, nbst);EpdCopy(error0, err);  EpdSubtract2(err, nbstates);
   EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
   (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
		  "  --Error states satisfying F                                        = ", 
		  nbst,percent);

   get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r);
   EpdGetString(nbstates, nbst); EpdCopy(rch, err);  EpdSubtract2(err, nbstates);
   EpdDivide2(nbstates, rch); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
   (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
		  "  --Error states originaly reachable by the design and satisfying F  = ", 
		  nbst,percent);
 
  
   (void) fprintf(vis_stdout, "%-50s%15g\n",
		  "  Analysis time                                                      = ", 
		  (double)(finalTime-initialTime)/1000.0);
   
   (void) fprintf(vis_stdout,"*******************************\n");	
   (void) fprintf(vis_stdout,
		  "Dealing with F = E[!forbiden U Required & E[!forbiden U Safe]] \n");
   initialTime = util_cpu_time();
   Setformula=evaluate_Formula_EF_EF (fsm, Req,Forb,Safe, verbosityLevel );
   finalTime = util_cpu_time();

   res_0=mdd_and(Init, Setformula, 1, 1);
   res_r=mdd_and(Orig,Setformula, 1, 1); mdd_free(Setformula);

   get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0);
   EpdGetString(nbstates, nbst);EpdCopy(error0, err);  EpdSubtract2(err, nbstates);
   EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
   (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
		  "  --Error states satisfying F                                        = ", 
		  nbst,percent);

   get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r);
   EpdGetString(nbstates, nbst); EpdCopy(rch, err);  EpdSubtract2(err, nbstates);
   EpdDivide2(nbstates, rch); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
   (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
		  "  --Error states originaly reachable by the design and satisfying F  = ", 
		  nbst,percent);
 
  
   (void) fprintf(vis_stdout, "%-50s%15g\n",               
		  "  Analysis time                                                      = ", 
		  (double)(finalTime-initialTime)/1000.0);
   */
   mdd_free(Forb);
   mdd_free(Req);
   mdd_free(Safe); 
   mdd_free(Init);
   mdd_free(Orig);
   
   alarm(0);
   return (0);
   
 
   return 1;
}


// (Adpateted) Bounded model checking 
// command for robustness properties.
static int
CommandBmcRob( Hrc_Manager_t ** hmgr,
	       int             argc,
	       char          ** argv){
  Ntk_Network_t     *network;
  BmcOption_t       *options;
  int               i;
  array_t           *formulaArray;
  array_t           *LTLformulaArray;
  bAig_Manager_t    *manager;
  array_t           *constraintArray = NIL(array_t);
 
/* Virer dans un premier temps par Denis, seule les techniques non-sat sont intégrées
   dans cette version.
*/


  // Parse command line options.
  if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
      return 1;
  }
  
  // Read the network
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    (void) fprintf(vis_stdout, "** bmc_rob error: No network\n");
    BmcOptionFree(options);
    return 1;
  }

  manager = Ntk_NetworkReadMAigManager(network);
  if (manager == NIL(mAig_Manager_t)) {
    (void) fprintf(vis_stdout, 
		   "** bmc_rob error: run build_partition_maigs command first\n");
    BmcOptionFree(options);
    return 1;
  }
  
 
  // We need the bdd when building the transition 
  // relation of the automaton
  if(options->inductiveStep !=0){
    Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
 
    designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
    if (designFsm == NIL(Fsm_Fsm_t)) {
      return 1;
    }
  }
 
  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;
  }

  if (options->fairFile != NIL(FILE)) {
    constraintArray = BmcReadFairnessConstraints(options->fairFile);
    if(constraintArray == NIL(array_t)){
      Ctlsp_FormulaArrayFree(LTLformulaArray);
      BmcOptionFree(options);
      return 1;
    }
    if(!Ctlsp_LtlFormulaArrayIsPropositional(constraintArray)){
      Ctlsp_FormulaArrayAddLtlFairnessConstraints(LTLformulaArray,
						  constraintArray);
      Ctlsp_FormulaArrayFree(constraintArray);
      constraintArray = NIL(array_t);
    }
  }
  
  //  Call the BMC function.
  for (i = 0; i < array_n(LTLformulaArray); i++) { 
    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *,
						  LTLformulaArray, i);
   callBmcRob(network, ltlFormula, constraintArray, options);
  }
  
  //  Free used memeory
  if (constraintArray != NIL(array_t)){
    Ctlsp_FormulaArrayFree(constraintArray);
  }
  Ctlsp_FormulaArrayFree(LTLformulaArray);
  BmcOptionFree(options);
  fflush(vis_stdout);
  fflush(vis_stderr);
  alarm(0);

  return 0;
}
static int 
CommandComposeGolden(Hrc_Manager_t ** hmgr,
		   int  argc, char ** argv){
	printf("*** Rob3 ***\n");
	//Former root
	Hrc_Node_t  * rootNode   =  Hrc_ManagerReadRootNode(*hmgr);
	if(Hrc_ManagerFindModelByName(*hmgr, "rob3_model") != NIL(Hrc_Model_t))
	{
		fprintf(vis_stderr, "Composition already made, read a new design\n");
		return 1;
		
	}
	//New Root
	Hrc_Model_t * newRootModel = Hrc_ModelAlloc(*hmgr, "rob3_model");
	
	build_golden_faulty_compo(*hmgr,rootNode,newRootModel);

  return 0;
}
static int 
CommandProtectGolden(Hrc_Manager_t ** hmgr,
		   int  argc, char ** argv)
{

Hrc_Node_t * rootNode = Hrc_ManagerReadRootNode(*hmgr);
if(rootNode == NIL(Hrc_Node_t)){
	printf("Please build the network first");
	return 1;
}
char * name = (char*) malloc(10);
sprintf(name,"golden");
Hrc_Node_t * goldenNode = Hrc_NodeFindChildByName(rootNode, name);
if(goldenNode == NIL(Hrc_Node_t)){
	printf("Please build the network first");
	return 1;
}

FILE * oFile =  Cmd_FileOpen("protect_golden.reg","w", NIL(char *), 0);
Fsm_Fsm_t  *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
if(fsm == NIL(Fsm_Fsm_t))
  return 1;
array_t         *psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
mdd_manager     *mddManager = Fsm_FsmReadMddManager(fsm);
int nbLatches = 0;
int k;
int arrSize = array_n( psVarsArray );
  for ( k = 0 ; k < arrSize ; k++ ) {
    int      mddId = array_fetch( int, psVarsArray,k);
    mvar_type mVar = array_fetch(mvar_type, 
				 mdd_ret_mvar_list(mddManager),mddId);
		if(strstr(mVar.name,"faulty") == NULL){
			fprintf(oFile,"%s\n",mVar.name);
			nbLatches++;
		}
	}
	st_generator * gen;
    Hrc_Latch_t * latch;	
	Hrc_NodeForEachLatch(rootNode, gen,name,latch){
		fprintf(oFile,"%s\n",name);
	 }
	 
/*
nbLatches += Hrc_NodeReadNumLatches(rootNode);

	int i;
	Var_Variable_t * var;
	Hrc_NodeForEachFormalOutput(rootNode,i,var){
		fprintf(oFile,"%s\n", Var_VariableReadName(var));
	 }
	nbLatches += Hrc_NodeReadNumFormalOutputs(rootNode);
*/
	 printf("file protect_golden.reg  created (contains %d registers)\n",nbLatches);
	fclose(oFile);
	return 0;
	
}

static int 
CommandProtectOutput(Hrc_Manager_t ** hmgr,
		   int  argc, char ** argv){
	Hrc_Node_t * rootNode = Hrc_ManagerReadRootNode(*hmgr);
	if(rootNode == NIL(Hrc_Node_t)){
		printf("Please build the network first\n");
		return 1;
	}
	FILE * oFile =  Cmd_FileOpen("protect_output.reg","w", NIL(char *), 0);
	int nbLatches = 0;
	int i;
	Var_Variable_t * var;
	Hrc_NodeForEachFormalOutput(rootNode,i,var){
		fprintf(oFile,"%s\n", Var_VariableReadName(var));
	 }
	nbLatches += Hrc_NodeReadNumFormalOutputs(rootNode);
	 printf("file protect_output  created (contains %d signals)\n",nbLatches);
	fclose(oFile);
	return 0;
	
}
static int 
CommandProtectRegister(Hrc_Manager_t ** hmgr,
		   int  argc, char ** argv){
	Hrc_Node_t * rootNode = Hrc_ManagerReadRootNode(*hmgr);
	if(rootNode == NIL(Hrc_Node_t)){
		printf("Please build the network first");
		return 1;
	}

	FILE * oFile =  Cmd_FileOpen("register.reg","w", NIL(char *), 0);

	int nbLatches = generateProtectFile(rootNode, oFile,""); 
	char * name;
	st_generator * gen;
    Hrc_Latch_t * latch;	
	 
	nbLatches += Hrc_NodeReadNumLatches(rootNode);

	printf("file register.reg  created (contains %d registers)\n",nbLatches);
	fclose(oFile);
	return 0;
	
}
static int 
CommandTestRob(Hrc_Manager_t ** hmgr,
		   int  argc, char ** argv)
{


  Fsm_Fsm_t  *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  mdd_t      *initialStates = getInitial(fsm);
  mdd_manager      *mddManager = Fsm_FsmReadMddManager(fsm);

FILE * oFile =  Cmd_FileOpen("init.prop","w", NIL(char *), 0);

mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
			 initialStates, "INIT",oFile);

  array_t * golden = array_alloc(int, 0);
  array_t         *psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
  int                  arrSize = array_n( psVarsArray );
  int i;
  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);
  if(strstr(mVar.name,"golden") !=NULL)
  {
    printf("-> %s\n",mVar.name);
    array_insert_last(int,golden,mddId);
  }
}

mdd_print_array (golden);
mdd_t * tmp1 = mdd_cproject(mddManager,initialStates,golden);
mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
			 tmp1, "GOLDEN",oFile);
   fclose(oFile);		       
  return 0;

}