Index: vis_dev/glu-2.3/src/cuPort/cuPort.c =================================================================== --- vis_dev/glu-2.3/src/cuPort/cuPort.c (revision 20) +++ vis_dev/glu-2.3/src/cuPort/cuPort.c (revision 21) @@ -706,5 +706,5 @@ ******************************************************************************/ bdd_t * -dd_and_smooth( +bdd_and_smooth( bdd_t *f, bdd_t *g, Index: vis_dev/vis-2.3/src/bmc/bmc.h =================================================================== --- vis_dev/vis-2.3/src/bmc/bmc.h (revision 20) +++ vis_dev/vis-2.3/src/bmc/bmc.h (revision 21) @@ -61,5 +61,5 @@ EXTERN MvfAig_Function_t * Bmc_NodeBuildMVF(Ntk_Network_t *network, Ntk_Node_t *node); EXTERN MvfAig_Function_t * Bmc_ReadMvfAig(Ntk_Node_t * node, st_table * nodeToMvfAigTable); - + BmcOption_t * ParseBmcOptions(int argc, char **argv); /**AutomaticEnd***************************************************************/ Index: vis_dev/vis-2.3/src/fsm/fsm.h =================================================================== --- vis_dev/vis-2.3/src/fsm/fsm.h (revision 20) +++ vis_dev/vis-2.3/src/fsm/fsm.h (revision 21) @@ -330,5 +330,5 @@ EXTERN void Fsm_ImageInfoConjoinWithWinningStrategy( Fsm_Fsm_t *modelFsm, Img_DirectionType directionType, mdd_t *winningStrategy); EXTERN void Fsm_ImageInfoRecoverFromWinningStrategy( Fsm_Fsm_t *modelFsm, Img_DirectionType directionType); - +int ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager, array_t *mddIdArray); /**AutomaticEnd***************************************************************/ Index: vis_dev/vis-2.3/src/rob/Robust.c =================================================================== --- vis_dev/vis-2.3/src/rob/Robust.c (revision 20) +++ vis_dev/vis-2.3/src/rob/Robust.c (revision 21) @@ -147,5 +147,5 @@ mvar_type mVar = array_fetch(mvar_type, mdd_ret_mvar_list(mddManager),mddId); - int protected = 0, j; + int protect = 0, j; for ( j = 0 ; j < array_n( wordArray ) ; j++ ) { char* w = array_fetch( char*, wordArray, j ); @@ -154,15 +154,15 @@ if (l > 0 && w[l-1] == '*') { if (strncmp(mVar.name, w, l-1) == 0) { - protected = 1; + protect = 1; break; } } else if (strcmp(mVar.name, w) == 0) { - protected = 1; + protect = 1; break; } } (void) fprintf(vis_stdout, "%-20s%10d", mVar.name, mVar.values); - if (protected) { + if (protect) { (void) fprintf(vis_stdout, " protected\n"); } @@ -187,5 +187,5 @@ int verbosityLevel, int printStep, - FILE* protected) { + FILE* protect) { mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); array_t *nonProtectedIdArray; @@ -195,5 +195,5 @@ // construction du vecteur des registres non protégés nonProtectedIdArray = - determine_non_protected_registers(fsm,protected); + determine_non_protected_registers(fsm,protect); if (array_n(nonProtectedIdArray) == @@ -483,5 +483,5 @@ mdd_t* error_states_us_ut(Fsm_Fsm_t *fsm, mdd_t* S, - FILE* protected) { + FILE* protect) { mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); array_t *nonProtectedIdArray, *bdd_vars; @@ -490,5 +490,5 @@ // construction du vecteur des registres non protégés nonProtectedIdArray = - determine_non_protected_registers(fsm,protected); + determine_non_protected_registers(fsm,protect); bdd_vars = getbddvars(mddManager, nonProtectedIdArray); @@ -503,5 +503,5 @@ mdd_t* error_states_ms_ut(Fsm_Fsm_t *fsm, mdd_t* S, - FILE* protected) { + FILE* protect) { mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); array_t *nonProtectedIdArray, *bdd_vars; @@ -510,5 +510,5 @@ // construction du vecteur des registres non protégés nonProtectedIdArray = - determine_non_protected_registers(fsm,protected); + determine_non_protected_registers(fsm,protect); bdd_vars = getbddvars(mddManager, nonProtectedIdArray); @@ -525,5 +525,5 @@ mdd_t* S0, mdd_t* S, - FILE* protected) { + FILE* protect) { mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); array_t *nonProtectedIdArray, *bdd_vars; @@ -536,5 +536,5 @@ nonProtectedIdArray = - determine_non_protected_registers(fsm,protected); + determine_non_protected_registers(fsm,protect); bdd_vars = getbddvars(mddManager, nonProtectedIdArray); @@ -632,10 +632,10 @@ mdd_t* error_states_us_mt(Fsm_Fsm_t *fsm, mdd_t *S, - FILE *protected) { + FILE *protect) { mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); // construction du vecteur des registres non protégés - array_t *nonProtectedIdArray = determine_non_protected_registers(fsm, protected); + array_t *nonProtectedIdArray = determine_non_protected_registers(fsm, protect); array_t *bdd_vars = getbddvars(mddManager, nonProtectedIdArray); // sauvegarde des états initiaux et accessibles courants Index: vis_dev/vis-2.3/src/rob/Robust.h =================================================================== --- vis_dev/vis-2.3/src/rob/Robust.h (revision 20) +++ vis_dev/vis-2.3/src/rob/Robust.h (revision 21) @@ -55,8 +55,10 @@ array_t* determine_non_protected_registers(Fsm_Fsm_t *fsm, FILE *f); mdd_t* compute_error_states (Fsm_Fsm_t *fsm, mdd_t* reachable, - int verbosityLevel, int printStep, - FILE* protected); -mdd_t* error_states_us_ut(Fsm_Fsm_t *fsm, mdd_t* reachable, - FILE* protected); + int verbosityLevel, int printStep, FILE* protect); +mdd_t* error_states_us_ut(Fsm_Fsm_t *fsm, mdd_t* reachable,FILE* protect); +mdd_t* error_states_us_mt(Fsm_Fsm_t *fsm, mdd_t *S, FILE *protect); +mdd_t* error_states_ms_ut(Fsm_Fsm_t *fsm, mdd_t *S, FILE *protect); +mdd_t* error_states_ms_mt(Fsm_Fsm_t *fsm, mdd_t* S0,mdd_t *S, FILE *protect) +; void compute_fair (Fsm_Fsm_t *fsm,int verbosityLevel); Hrc_Node_t * build_golden_faulty_compo(Hrc_Manager_t * hmgr,Hrc_Node_t * rootNode, Hrc_Model_t * newRootModel); Index: vis_dev/vis-2.3/src/rob/robCmd.c =================================================================== --- vis_dev/vis-2.3/src/rob/robCmd.c (revision 20) +++ vis_dev/vis-2.3/src/rob/robCmd.c (revision 21) @@ -170,5 +170,5 @@ int argc, char ** argv){ char* fichier="./test"; - int k=main_Count_test_(fichier); + int k= 0;//main_Count_test_(fichier); printf("res= %d \n",k); return 0;