Changeset 21

Timestamp:

Jul 19, 2011, 4:51:20 PM (13 years ago)

Author:

cecile

Message:

un delete de trop

Location:

vis_dev

Files:

• glu-2.3/src/cuPort/cuPort.c (modified) (1 diff)
• vis-2.3/src/bmc/bmc.h (modified) (1 diff)
• vis-2.3/src/fsm/fsm.h (modified) (1 diff)
• vis-2.3/src/rob/Robust.c (modified) (11 diffs)
• vis-2.3/src/rob/Robust.h (modified) (1 diff)
• vis-2.3/src/rob/robCmd.c (modified) (1 diff)

vis_dev/glu-2.3/src/cuPort/cuPort.c

@@ -706 +706 @@
 ******************************************************************************/
 bdd_t *
-dd_and_smooth(
+bdd_and_smooth(
   bdd_t *f,
   bdd_t *g,

vis_dev/vis-2.3/src/bmc/bmc.h

@@ -61 +61 @@
 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***************************************************************/
 

vis_dev/vis-2.3/src/fsm/fsm.h

@@ -330 +330 @@
 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***************************************************************/

vis_dev/vis-2.3/src/rob/Robust.c

@@ -147 +147 @@
     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 +154 @@
       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 +187 @@
                             int verbosityLevel, 
                             int printStep, 
-                            FILE* protected) {
+                            FILE* protect) {
   mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
   array_t       *nonProtectedIdArray;
@@ -195 +195 @@
   // 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 +483 @@
 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 +490 @@
   // 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 +503 @@
 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 +510 @@
   // 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 +525 @@
                           mdd_t* S0,
                           mdd_t* S,
-                          FILE* protected) {
+                          FILE* protect) {
   mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
    array_t     *nonProtectedIdArray, *bdd_vars;
@@ -536 +536 @@
 
   nonProtectedIdArray = 
-    determine_non_protected_registers(fsm,protected);
+    determine_non_protected_registers(fsm,protect);
    bdd_vars = getbddvars(mddManager, nonProtectedIdArray); 
 
@@ -632 +632 @@
 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

vis_dev/vis-2.3/src/rob/Robust.h

@@ -55 +55 @@
 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);

vis_dev/vis-2.3/src/rob/robCmd.c

@@ -170 +170 @@
                    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;