model-checker : args prgm and automaton changed in global variables

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 0181c4d..acdafa7 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -112,7 +112,7 @@ void MC_take_snapshot(mc_snapshot_t snapshot)
 }
 
 
-void MC_take_snapshot_liveness(mc_snapshot_t snapshot, char *prgm)
+void MC_take_snapshot_liveness(mc_snapshot_t snapshot)
 {
   unsigned int i = 0;
   s_map_region reg;
@@ -138,7 +138,7 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot, char *prgm)
         if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){
           MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
         } else {
-         if (!memcmp(basename(maps->regions[i].pathname), basename(prgm), strlen(basename(prgm)))){
+         if (!memcmp(basename(maps->regions[i].pathname), basename(prog_name), strlen(basename(prog_name)))){
            MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
          } /*else {
            if (!memcmp(maps->regions[i].pathname, "[stack]", 7)){
@@ -154,7 +154,7 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot, char *prgm)
   /* FIXME: free the memory map */
 }
 
-void MC_take_snapshot_to_restore_liveness(mc_snapshot_t snapshot, char *prgm)
+void MC_take_snapshot_to_restore_liveness(mc_snapshot_t snapshot)
 {
   unsigned int i = 0;
   s_map_region reg;
@@ -180,7 +180,7 @@ void MC_take_snapshot_to_restore_liveness(mc_snapshot_t snapshot, char *prgm)
         if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){
           MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
         } else {
-         if (!memcmp(basename(maps->regions[i].pathname), basename(prgm), strlen(basename(prgm)))){
+         if (!memcmp(basename(maps->regions[i].pathname), basename(prog_name), strlen(basename(prog_name)))){
            MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
          } 
        }

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 128e06d..e093b3d 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -32,6 +32,8 @@ mc_stats_pair_t mc_stats_pair = NULL;
 xbt_fifo_t mc_stack_liveness_stateless = NULL;
 mc_snapshot_t initial_snapshot_liveness = NULL;
 
+xbt_automaton_t automaton;
+char *prog_name;
 
 /**
  *  \brief Initialize the model-checker data structures
@@ -143,7 +145,10 @@ void MC_init_liveness_stateless(xbt_automaton_t a, char *prgm){
 
   MC_UNSET_RAW_MEM;
 
-  MC_ddfs_stateless_init(a, prgm);
+  automaton = a;
+  prog_name = strdup(prgm);
+
+  MC_ddfs_stateless_init();
 
   
 }

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 7d5eb8a..518ef2c 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -97,7 +97,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
   
 }
 
-int reached(xbt_automaton_t a, xbt_state_t st, char *prgm){
+int reached(xbt_state_t st){
 
 
   if(xbt_fifo_size(reached_pairs) == 0){
@@ -115,14 +115,14 @@ int reached(xbt_automaton_t a, xbt_state_t st, char *prgm){
     /* Get values of propositional symbols */
     unsigned int cursor = 0;
     xbt_propositional_symbol_t ps = NULL;
-    xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
+    xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
       f = ps->function;
       res = (*f)();
       xbt_dynar_push_as(prop_ato, int, res);
     }
 
     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot_liveness(sn, prgm);    
+    MC_take_snapshot_liveness(sn);    
     
     int i=0;
     xbt_fifo_item_t item = xbt_fifo_get_first_item(reached_pairs);
@@ -163,7 +163,7 @@ int reached(xbt_automaton_t a, xbt_state_t st, char *prgm){
   }
 }
 
-void set_pair_reached(xbt_automaton_t a, xbt_state_t st, char *prgm){
+void set_pair_reached(xbt_state_t st){
 
  
   MC_SET_RAW_MEM;
@@ -173,7 +173,7 @@ void set_pair_reached(xbt_automaton_t a, xbt_state_t st, char *prgm){
   pair->automaton_state = st;
   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_liveness(pair->system_state, prgm);
+  MC_take_snapshot_liveness(pair->system_state);
 
   /* Get values of propositional symbols */
   unsigned int cursor = 0;
@@ -181,7 +181,7 @@ void set_pair_reached(xbt_automaton_t a, xbt_state_t st, char *prgm){
   int res;
   int (*f)(); 
 
-  xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
+  xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
     f = ps->function;
     res = (*f)();
     xbt_dynar_push_as(pair->prop_ato, int, res);
@@ -194,7 +194,7 @@ void set_pair_reached(xbt_automaton_t a, xbt_state_t st, char *prgm){
   
 }
 
-int visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){
+int visited(xbt_state_t st, int sc){
 
 
   if(xbt_fifo_size(visited_pairs) == 0){
@@ -213,14 +213,14 @@ int visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){
     int res;
     int (*f)();
 
-    xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
+    xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
       f = ps->function;
       res = (*f)();
       xbt_dynar_push_as(prop_ato, int, res);
     }
 
     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot_liveness(sn, prgm);
+    MC_take_snapshot_liveness(sn);
 
     int i=0;
     xbt_fifo_item_t item = xbt_fifo_get_first_item(visited_pairs);
@@ -263,7 +263,7 @@ int visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){
   }
 }
 
-void set_pair_visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){
+void set_pair_visited(xbt_state_t st, int sc){
 
  
   MC_SET_RAW_MEM;
@@ -273,7 +273,7 @@ void set_pair_visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){
   pair->automaton_state = st;
   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_liveness(pair->system_state, prgm);
+  MC_take_snapshot_liveness(pair->system_state);
   pair->search_cycle = sc;
 
   /* Get values of propositional symbols */
@@ -282,7 +282,7 @@ void set_pair_visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){
   int res;
   int (*f)();
 
-  xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
+  xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
     f = ps->function;
     res = (*f)();
     xbt_dynar_push_as(pair->prop_ato, int, res);
@@ -303,30 +303,30 @@ void MC_pair_delete(mc_pair_t pair){
 
 
 
-int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
+int MC_automaton_evaluate_label(xbt_exp_label_t l){
   
   switch(l->type){
   case 0 : {
-    int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
-    int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
+    int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
+    int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
     return (left_res || right_res);
     break;
   }
   case 1 : {
-    int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
-    int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
+    int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
+    int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
     return (left_res && right_res);
     break;
   }
   case 2 : {
-    int res = MC_automaton_evaluate_label(a, l->u.exp_not);
+    int res = MC_automaton_evaluate_label(l->u.exp_not);
     return (!res);
     break;
   }
   case 3 : { 
     unsigned int cursor = 0;
     xbt_propositional_symbol_t p = NULL;
-    xbt_dynar_foreach(a->propositional_symbols, cursor, p){
+    xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){
       if(strcmp(p->pred, l->u.predicat) == 0){
        int (*f)() = p->function;
        return (*f)();
@@ -366,7 +366,7 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
   return p;
 }
 
-void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){
+void MC_ddfs_stateless_init(){
 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Double-DFS stateless init");
@@ -393,14 +393,14 @@ void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){
 
   /* Save the initial state */
   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_to_restore_liveness(initial_snapshot_liveness, prgm);
+  MC_take_snapshot_to_restore_liveness(initial_snapshot_liveness);
 
   MC_UNSET_RAW_MEM; 
 
   unsigned int cursor = 0;
   xbt_state_t state;
 
-  xbt_dynar_foreach(a->states, cursor, state){
+  xbt_dynar_foreach(automaton->states, cursor, state){
     if(state->type == -1){
       
       MC_SET_RAW_MEM;
@@ -413,7 +413,7 @@ void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){
        MC_UNSET_RAW_MEM;
       }
 
-      MC_ddfs_stateless(a, 0, 0, prgm);
+      MC_ddfs_stateless(0);
 
     }else{
       if(state->type == 2){
@@ -423,14 +423,14 @@ void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){
        xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
        MC_UNSET_RAW_MEM;
 
-       set_pair_reached(a, state, prgm);
+       set_pair_reached(state);
        
        if(cursor != 0){
          MC_restore_snapshot(initial_snapshot_liveness);
          MC_UNSET_RAW_MEM;
        }
        
-       MC_ddfs_stateless(a, 1, 0, prgm);
+       MC_ddfs_stateless(1);
        
       }
     }
@@ -439,7 +439,7 @@ void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){
 }
 
 
-void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *prgm){
+void MC_ddfs_stateless(int search_cycle){
 
   smx_process_t process;
   mc_pair_stateless_t current_pair = NULL;
@@ -447,21 +447,12 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
   if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
     return;
 
-  if(replay == 1){
-    MC_replay_liveness(mc_stack_liveness_stateless, 0);
-    current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
-    xbt_swag_foreach(process, simix_global->process_list){
-      if(MC_process_is_enabled(process)){
-       MC_state_interleave_process(current_pair->graph_state, process);
-      }
-    }
-  }
 
   /* Get current pair */
   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 
   /* Update current state in buchi automaton */
-  a->current_state = current_pair->automaton_state;
+  automaton->current_state = current_pair->automaton_state;
 
  
   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
@@ -485,9 +476,9 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
 
   if(xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS){
 
-    set_pair_visited(a, current_pair->automaton_state, search_cycle, prgm);
+    set_pair_visited(current_pair->automaton_state, search_cycle);
 
-    //XBT_DEBUG("Visited pairs : %d", xbt_fifo_size(visited_pairs));
+    XBT_DEBUG("Visited pairs : %d", xbt_fifo_size(visited_pairs));
 
     if(current_pair->requests > 0){
 
@@ -529,7 +520,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
        cursor= 0;
        xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 
-         res = MC_automaton_evaluate_label(a, transition_succ->label);
+         res = MC_automaton_evaluate_label(transition_succ->label);
 
          if(res == 1){ // enabled transition in automaton
            MC_SET_RAW_MEM;
@@ -544,7 +535,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
    
        xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
       
-         res = MC_automaton_evaluate_label(a, transition_succ->label);
+         res = MC_automaton_evaluate_label(transition_succ->label);
        
          if(res == 2){ // true transition in automaton
            MC_SET_RAW_MEM;
@@ -559,13 +550,13 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
        
        xbt_dynar_foreach(successors, cursor, pair_succ){
 
-         if(!visited(a, pair_succ->automaton_state, search_cycle, prgm)){
+         if(!visited(pair_succ->automaton_state, search_cycle)){
 
            if(search_cycle == 1){
 
              if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
                      
-               if(reached(a, pair_succ->automaton_state, prgm) == 1){
+               if(reached(pair_succ->automaton_state) == 1){
 
                  XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1, MC_state_interleave_size(pair_succ->graph_state));
 
@@ -582,9 +573,9 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
 
                  XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
              
-                 set_pair_reached(a, pair_succ->automaton_state, prgm); 
+                 set_pair_reached(pair_succ->automaton_state); 
 
-                 //XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs));
+                 XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs));
 
                }
 
@@ -596,11 +587,11 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
 
                XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
            
-               set_pair_reached(a, pair_succ->automaton_state, prgm); 
+               set_pair_reached(pair_succ->automaton_state); 
              
                search_cycle = 1;
 
-               //XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs));
+               XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs));
 
              }
 
@@ -610,7 +601,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
            xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
            MC_UNSET_RAW_MEM;
 
-           MC_ddfs_stateless(a, search_cycle, 0, prgm);
+           MC_ddfs_stateless(search_cycle);
 
            /* Restore system before checking others successors */
            if(cursor != (xbt_dynar_length(successors) - 1))
@@ -619,6 +610,28 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
          }else{
            
            XBT_DEBUG("Next pair already visited");
+
+           if(search_cycle == 1){
+
+             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
+                     
+               if(reached(pair_succ->automaton_state) == 1){
+
+                 XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1, MC_state_interleave_size(pair_succ->graph_state));
+
+                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
+                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+                 XBT_INFO("Counter-example that violates formula :");
+                 MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
+                 MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
+                 MC_print_statistics_pairs(mc_stats_pair);
+                 exit(0);
+
+               }
+
+             }
+           }
            
          }
        }
@@ -645,7 +658,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
       cursor= 0;
       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 
-       res = MC_automaton_evaluate_label(a, transition_succ->label);
+       res = MC_automaton_evaluate_label(transition_succ->label);
 
        if(res == 1){ // enabled transition in automaton
          MC_SET_RAW_MEM;
@@ -660,7 +673,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
    
       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
       
-       res = MC_automaton_evaluate_label(a, transition_succ->label);
+       res = MC_automaton_evaluate_label(transition_succ->label);
        
        if(res == 2){ // true transition in automaton
          MC_SET_RAW_MEM;
@@ -675,13 +688,13 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
      
       xbt_dynar_foreach(successors, cursor, pair_succ){
 
-       if(!visited(a, pair_succ->automaton_state, search_cycle, prgm)){
+       if(!visited(pair_succ->automaton_state, search_cycle)){
 
          if(search_cycle == 1){
 
            if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
 
-             if(reached(a, pair_succ->automaton_state, prgm) == 1){
+             if(reached(pair_succ->automaton_state) == 1){
 
                XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1);
 
@@ -698,9 +711,9 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
 
                XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
              
-               set_pair_reached(a, pair_succ->automaton_state, prgm); 
+               set_pair_reached(pair_succ->automaton_state); 
                
-               //XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs));
+               XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs));
 
              }
 
@@ -710,11 +723,11 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
          
            if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (xbt_fifo_size(mc_stack_liveness_stateless) < (MAX_DEPTH_LIVENESS - 1))){
 
-             set_pair_reached(a, pair_succ->automaton_state, prgm); 
+             set_pair_reached(pair_succ->automaton_state); 
                    
              search_cycle = 1;
 
-             //XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs));
+             XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs));
 
            }
 
@@ -724,7 +737,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
          xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
          MC_UNSET_RAW_MEM;
 
-         MC_ddfs_stateless(a, search_cycle, 0, prgm);
+         MC_ddfs_stateless(search_cycle);
 
          /* Restore system before checking others successors */
          if(cursor != xbt_dynar_length(successors) - 1)
@@ -733,7 +746,29 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr
        }else{
            
          XBT_DEBUG("Next pair already visited");
-         
+
+         if(search_cycle == 1){
+
+           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
+             
+             if(reached(pair_succ->automaton_state) == 1){
+               
+               XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1, MC_state_interleave_size(pair_succ->graph_state));
+               
+               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+               XBT_INFO("|             ACCEPTANCE CYCLE            |");
+               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+               XBT_INFO("Counter-example that violates formula :");
+               MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
+               MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
+               MC_print_statistics_pairs(mc_stats_pair);
+               exit(0);
+                 
+             }
+               
+           }
+             
+         }
        }
       
       }

diff --git a/src/mc/private.h b/src/mc/private.h
index 0ee7413..415a8bc 100644 (file)
--- a/src/mc/private.h
+++ b/src/mc/private.h
@@ -35,9 +35,11 @@ typedef struct s_mc_snapshot{
   mc_mem_region_t *regions;
 } s_mc_snapshot_t, *mc_snapshot_t;
 
+extern char *prog_name;
+
 void MC_take_snapshot(mc_snapshot_t);
-void MC_take_snapshot_liveness(mc_snapshot_t s, char *prgm);
-void MC_take_snapshot_to_restore_liveness(mc_snapshot_t s, char *prgm);
+void MC_take_snapshot_liveness(mc_snapshot_t s);
+void MC_take_snapshot_to_restore_liveness(mc_snapshot_t s);
 void MC_restore_snapshot(mc_snapshot_t);
 void MC_free_snapshot(mc_snapshot_t);
 
@@ -227,19 +229,19 @@ typedef struct s_mc_pair_visited{
   int search_cycle;
 }s_mc_pair_visited_t, *mc_pair_visited_t;
 
-int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l);
+int MC_automaton_evaluate_label(xbt_exp_label_t l);
 mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st);
 
-int reached(xbt_automaton_t a, xbt_state_t st, char *prgm);
-void set_pair_reached(xbt_automaton_t a, xbt_state_t st, char *prgm);
+int reached(xbt_state_t st);
+void set_pair_reached(xbt_state_t st);
 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2);
 void MC_show_stack_liveness_stateful(xbt_fifo_t stack);
 void MC_dump_stack_liveness_stateful(xbt_fifo_t stack);
 void MC_pair_delete(mc_pair_t pair);
 void MC_exit_liveness(void);
 mc_state_t MC_state_pair_new(void);
-int visited(xbt_automaton_t a, xbt_state_t st, int search_cycle, char *prgm);
-void set_pair_visited(xbt_automaton_t a, xbt_state_t st, int search_cycle, char *prgm);
+int visited(xbt_state_t st, int search_cycle);
+void set_pair_visited(xbt_state_t st, int search_cycle);
 
 /* **** Double-DFS stateful without visited state **** */
 
@@ -258,10 +260,11 @@ typedef struct s_mc_pair_stateless{
 
 extern xbt_fifo_t mc_stack_liveness_stateless;
 extern mc_snapshot_t initial_snapshot_liveness;
+extern xbt_automaton_t automaton;
 
 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r);
-void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm);
-void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *prgm);
+void MC_ddfs_stateless_init();
+void MC_ddfs_stateless(int search_cycle);
 void MC_show_stack_liveness_stateless(xbt_fifo_t stack);
 void MC_dump_stack_liveness_stateless(xbt_fifo_t stack);
 void MC_pair_stateless_delete(mc_pair_stateless_t pair);