model-checker : clean code

diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt
index 30241f9..bae8896 100644 (file)
--- a/examples/msg/mc/CMakeLists.txt
+++ b/examples/msg/mc/CMakeLists.txt
@@ -16,7 +16,6 @@ automatonparse_promela.c example_liveness_with_cycle.c)
 
 
 
-
 target_link_libraries(centralized simgrid m )
 target_link_libraries(bugged1     simgrid m )
 target_link_libraries(bugged1_stateful simgrid m)
@@ -25,4 +24,4 @@ target_link_libraries(bugged2     simgrid m )
 target_link_libraries(bugged3     simgrid m )
 target_link_libraries(random_test     simgrid m )
 target_link_libraries(example_liveness_with_cycle2     simgrid m )
-target_link_libraries(example_liveness_with_cycle     simgrid m )
+target_link_libraries(example_liveness_with_cycle     simgrid m )
\ No newline at end of file

diff --git a/examples/msg/mc/example_liveness_with_cycle.c b/examples/msg/mc/example_liveness_with_cycle.c
index 0927be0..8f51687 100644 (file)
--- a/examples/msg/mc/example_liveness_with_cycle.c
+++ b/examples/msg/mc/example_liveness_with_cycle.c
@@ -136,7 +136,7 @@ int main(int argc, char *argv[])
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_mutex2.xml");
-  MSG_main_liveness_stateless(automaton, argv[0]);
-  
+  MSG_main_liveness(automaton, argv[0]);
+
   return 0;
 }

diff --git a/examples/msg/mc/example_liveness_with_cycle2.c b/examples/msg/mc/example_liveness_with_cycle2.c
index f2a5dcb..148afb4 100644 (file)
--- a/examples/msg/mc/example_liveness_with_cycle2.c
+++ b/examples/msg/mc/example_liveness_with_cycle2.c
@@ -134,7 +134,7 @@ int main(int argc, char *argv[])
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_mutex2.xml");
-  MSG_main_liveness_stateless(automaton, argv[0]);
+  MSG_main_liveness(automaton, argv[0]);
   
   return 0;
 }

diff --git a/include/msg/msg.h b/include/msg/msg.h
index f30a1d1..bd0472d 100644 (file)
--- a/include/msg/msg.h
+++ b/include/msg/msg.h
@@ -23,8 +23,7 @@ XBT_PUBLIC(MSG_error_t) MSG_set_channel_number(int number);
 XBT_PUBLIC(int) MSG_get_channel_number(void);
 XBT_PUBLIC(MSG_error_t) MSG_main(void);
 XBT_PUBLIC(MSG_error_t) MSG_main_stateful(void);
-XBT_PUBLIC(MSG_error_t) MSG_main_liveness_stateful(xbt_automaton_t a);
-XBT_PUBLIC(MSG_error_t) MSG_main_liveness_stateless(xbt_automaton_t a, char *prgm);
+XBT_PUBLIC(MSG_error_t) MSG_main_liveness(xbt_automaton_t a, char *prgm);
 XBT_PUBLIC(MSG_error_t) MSG_clean(void);
 XBT_PUBLIC(void) MSG_function_register(const char *name,
                                        xbt_main_func_t code);

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 41f4425..66fdada 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -28,7 +28,7 @@ SG_BEGIN_DECL()
 /********************************* Global *************************************/
 XBT_PUBLIC(void) MC_init_safety_stateless(void);
 XBT_PUBLIC(void) MC_init_safety_stateful(void);
-XBT_PUBLIC(void) MC_init_liveness_stateful(xbt_automaton_t a);
+XBT_PUBLIC(void) MC_init_liveness_stateful(xbt_automaton_t a, char *prgm);
 XBT_PUBLIC(void) MC_init_liveness_stateless(xbt_automaton_t a, char *prgm);
 XBT_PUBLIC(void) MC_exit(void);
 XBT_PUBLIC(void) MC_exit_liveness(void);
@@ -38,7 +38,7 @@ XBT_PUBLIC(void) MC_assert_pair_stateful(int);
 XBT_PUBLIC(void) MC_assert_pair_stateless(int);
 XBT_PUBLIC(void) MC_modelcheck(void);
 XBT_PUBLIC(void) MC_modelcheck_stateful(void);
-XBT_PUBLIC(void) MC_modelcheck_liveness_stateful(xbt_automaton_t a);
+XBT_PUBLIC(void) MC_modelcheck_liveness_stateful(xbt_automaton_t a, char *prgm);
 XBT_PUBLIC(void) MC_modelcheck_liveness_stateless(xbt_automaton_t a, char *prgm);
 XBT_PUBLIC(int) MC_random(int, int);
 XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index e093b3d..3dcbfc8 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -27,9 +27,8 @@ mc_stats_t mc_stats = NULL;
 
 /* Liveness */
 
-xbt_fifo_t mc_stack_liveness_stateful = NULL;
 mc_stats_pair_t mc_stats_pair = NULL;
-xbt_fifo_t mc_stack_liveness_stateless = NULL;
+xbt_fifo_t mc_stack_liveness = NULL;
 mc_snapshot_t initial_snapshot_liveness = NULL;
 
 xbt_automaton_t automaton;
@@ -96,35 +95,7 @@ void MC_init_safety_stateful(void){
 
 }
 
-void MC_init_liveness_stateful(xbt_automaton_t a){
-
-  XBT_DEBUG("Start init mc");
-  
-  mc_time = xbt_new0(double, simix_process_maxpid);
-
-  /* Initialize the data structures that must be persistent across every
-     iteration of the model-checker (in RAW memory) */
-
-  MC_SET_RAW_MEM;
-
-  /* Initialize statistics */
-  mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
-  //mc_stats = xbt_new0(s_mc_stats_t, 1);
-
-  XBT_DEBUG("Creating snapshot_stack");
-
- /* Create exploration stack */
-  mc_stack_liveness_stateful = xbt_fifo_new();
-
-
-  MC_UNSET_RAW_MEM;
-
-  //MC_ddfs_stateful_init(a);
-  //MC_dpor2_init(a);
-  //MC_dpor3_init(a);
-}
-
-void MC_init_liveness_stateless(xbt_automaton_t a, char *prgm){
+void MC_init_liveness(xbt_automaton_t a, char *prgm){
 
   XBT_DEBUG("Start init mc");
   
@@ -141,14 +112,14 @@ void MC_init_liveness_stateless(xbt_automaton_t a, char *prgm){
   XBT_DEBUG("Creating stack");
 
  /* Create exploration stack */
-  mc_stack_liveness_stateless = xbt_fifo_new();
+  mc_stack_liveness = xbt_fifo_new();
 
   MC_UNSET_RAW_MEM;
 
   automaton = a;
   prog_name = strdup(prgm);
 
-  MC_ddfs_stateless_init();
+  MC_ddfs_init();
 
   
 }
@@ -168,13 +139,9 @@ void MC_modelcheck_stateful(void)
   MC_exit();
 }
 
-void MC_modelcheck_liveness_stateful(xbt_automaton_t a){
-  MC_init_liveness_stateful(a);
-  MC_exit_liveness();
-}
 
-void MC_modelcheck_liveness_stateless(xbt_automaton_t a, char *prgm){
-  MC_init_liveness_stateless(a, prgm);
+void MC_modelcheck_liveness(xbt_automaton_t a, char *prgm){
+  MC_init_liveness(a, prgm);
   MC_exit_liveness();
 }
 
@@ -492,35 +459,8 @@ void MC_show_stack_safety_stateful(xbt_fifo_t stack)
   }
 }
 
-void MC_show_stack_liveness_stateful(xbt_fifo_t stack){
-  int value;
-  mc_pair_t pair;
-  xbt_fifo_item_t item;
-  smx_req_t req;
-  char *req_str = NULL;
-  
-  for (item = xbt_fifo_get_last_item(stack);
-       (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
-        : (NULL)); item = xbt_fifo_get_prev_item(item)) {
-    req = MC_state_get_executed_request(pair->graph_state, &value);
-    if(req){
-      req_str = MC_request_to_string(req, value);
-      XBT_INFO("%s", req_str);
-      xbt_free(req_str);
-    }
-  }
-}
-
-void MC_dump_stack_liveness_stateful(xbt_fifo_t stack){
-  mc_pair_t pair;
-
-  MC_SET_RAW_MEM;
-  while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
-    MC_pair_delete(pair);
-  MC_UNSET_RAW_MEM;
-}
 
-void MC_show_stack_liveness_stateless(xbt_fifo_t stack){
+void MC_show_stack_liveness(xbt_fifo_t stack){
   int value;
   mc_pair_stateless_t pair;
   xbt_fifo_item_t item;
@@ -543,7 +483,7 @@ void MC_show_stack_liveness_stateless(xbt_fifo_t stack){
   }
 }
 
-void MC_dump_stack_liveness_stateless(xbt_fifo_t stack){
+void MC_dump_stack_liveness(xbt_fifo_t stack){
   mc_pair_stateless_t pair;
 
   MC_SET_RAW_MEM;
@@ -602,26 +542,14 @@ void MC_assert_stateful(int prop)
   }
 }
 
-void MC_assert_pair_stateful(int prop){
-  if (MC_IS_ENABLED && !prop) {
-    XBT_INFO("**************************");
-    XBT_INFO("*** PROPERTY NOT VALID ***");
-    XBT_INFO("**************************");
-    //XBT_INFO("Counter-example execution trace:");
-    MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
-    //MC_dump_snapshot_stack(mc_snapshot_stack);
-    MC_print_statistics_pairs(mc_stats_pair);
-    xbt_abort();
-  }
-}
 
-void MC_assert_pair_stateless(int prop){
+void MC_assert_pair(int prop){
   if (MC_IS_ENABLED && !prop) {
     XBT_INFO("**************************");
     XBT_INFO("*** PROPERTY NOT VALID ***");
     XBT_INFO("**************************");
     //XBT_INFO("Counter-example execution trace:");
-    MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
+    MC_show_stack_liveness(mc_stack_liveness);
     //MC_dump_snapshot_stack(mc_snapshot_stack);
     MC_print_statistics_pairs(mc_stats_pair);
     xbt_abort();

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 440ea9c..bf2be95 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -10,6 +10,7 @@ xbt_dynar_t visited_pairs;
 xbt_dynar_t visited_pairs_hash;
 xbt_dynar_t successors;
 
+
 /* fast implementation of djb2 algorithm */
 unsigned int hash_region(char *str, int str_len){
 
@@ -580,10 +581,10 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
   return p;
 }
 
-void MC_ddfs_stateless_init(){
+void MC_ddfs_init(){
 
   XBT_DEBUG("**************************************************");
-  XBT_DEBUG("Double-DFS stateless init");
+  XBT_DEBUG("Double-DFS init");
   XBT_DEBUG("**************************************************");
 
   mc_pair_stateless_t mc_initial_pair = NULL;
@@ -621,7 +622,7 @@ void MC_ddfs_stateless_init(){
       
       MC_SET_RAW_MEM;
       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
-      xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
+      xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
       MC_UNSET_RAW_MEM;
       
       if(cursor != 0){
@@ -629,14 +630,14 @@ void MC_ddfs_stateless_init(){
        MC_UNSET_RAW_MEM;
       }
 
-      MC_ddfs_stateless(0);
+      MC_ddfs(0);
 
     }else{
       if(state->type == 2){
       
        MC_SET_RAW_MEM;
        mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
-       xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
+       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
        MC_UNSET_RAW_MEM;
 
        //set_pair_reached(state);
@@ -647,7 +648,7 @@ void MC_ddfs_stateless_init(){
          MC_UNSET_RAW_MEM;
        }
        
-       MC_ddfs_stateless(1);
+       MC_ddfs(1);
        
       }
     }
@@ -656,23 +657,23 @@ void MC_ddfs_stateless_init(){
 }
 
 
-void MC_ddfs_stateless(int search_cycle){
+void MC_ddfs(int search_cycle){
 
   smx_process_t process;
   mc_pair_stateless_t current_pair = NULL;
 
-  if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
+  if(xbt_fifo_size(mc_stack_liveness) == 0)
     return;
 
 
   /* Get current pair */
-  current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
+  current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 
   /* Update current state in buchi automaton */
   automaton->current_state = current_pair->automaton_state;
 
  
-  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
+  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
   XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id, MC_state_interleave_size(current_pair->graph_state));
  
   mc_stats_pair->visited_pairs++;
@@ -691,7 +692,7 @@ void MC_ddfs_stateless(int search_cycle){
   mc_pair_stateless_t next_pair = NULL;
   mc_pair_stateless_t pair_succ;
 
-  if(xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS){
+  if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
 
     //set_pair_visited(current_pair->automaton_state, search_cycle);
     set_pair_visited_hash(current_pair->automaton_state, search_cycle);
@@ -776,20 +777,20 @@ void MC_ddfs_stateless(int search_cycle){
              //if(reached(pair_succ->automaton_state)){
              if(reached_hash(pair_succ->automaton_state)){
              
-               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_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 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_show_stack_liveness(mc_stack_liveness);
+               MC_dump_stack_liveness(mc_stack_liveness);
                MC_print_statistics_pairs(mc_stats_pair);
                exit(0);
 
              }else{
 
-               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);
+               XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
              
                //set_pair_reached(pair_succ->automaton_state);
                set_pair_reached_hash(pair_succ->automaton_state);
@@ -798,10 +799,10 @@ void MC_ddfs_stateless(int search_cycle){
                XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 
                MC_SET_RAW_MEM;
-               xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
                MC_UNSET_RAW_MEM;
                
-               MC_ddfs_stateless(search_cycle);
+               MC_ddfs(search_cycle);
 
              }
 
@@ -811,10 +812,10 @@ void MC_ddfs_stateless(int search_cycle){
                //if(!visited(pair_succ->automaton_state, search_cycle)){
                
                MC_SET_RAW_MEM;
-               xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
                MC_UNSET_RAW_MEM;
                
-               MC_ddfs_stateless(search_cycle);
+               MC_ddfs(search_cycle);
                
              }else{
 
@@ -828,7 +829,7 @@ void MC_ddfs_stateless(int search_cycle){
          
            if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
-             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);
+             XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
            
              //set_pair_reached(pair_succ->automaton_state); 
              set_pair_reached_hash(pair_succ->automaton_state);
@@ -844,10 +845,10 @@ void MC_ddfs_stateless(int search_cycle){
              //if(!visited(pair_succ->automaton_state, search_cycle)){
              
              MC_SET_RAW_MEM;
-             xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
              MC_UNSET_RAW_MEM;
              
-             MC_ddfs_stateless(search_cycle);
+             MC_ddfs(search_cycle);
              
            }else{
 
@@ -860,14 +861,14 @@ void MC_ddfs_stateless(int search_cycle){
         
          /* Restore system before checking others successors */
          if(cursor != (xbt_dynar_length(successors) - 1))
-           MC_replay_liveness(mc_stack_liveness_stateless, 1);
+           MC_replay_liveness(mc_stack_liveness, 1);
        
          
        }
 
        if(MC_state_interleave_size(current_pair->graph_state) > 0){
-         XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
-         MC_replay_liveness(mc_stack_liveness_stateless, 0);
+         XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness));
+         MC_replay_liveness(mc_stack_liveness, 0);
        }
       }
 
@@ -924,20 +925,20 @@ void MC_ddfs_stateless(int search_cycle){
            //if(reached(pair_succ->automaton_state)){
            if(reached_hash(pair_succ->automaton_state)){
 
-             XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1);
+             XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
 
              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_show_stack_liveness(mc_stack_liveness);
+             MC_dump_stack_liveness(mc_stack_liveness);
              MC_print_statistics_pairs(mc_stats_pair);
              exit(0);
 
            }else{
 
-             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);
+             XBT_DEBUG("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
              
              //set_pair_reached(pair_succ->automaton_state);
              set_pair_reached_hash(pair_succ->automaton_state);
@@ -946,10 +947,10 @@ void MC_ddfs_stateless(int search_cycle){
              XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 
              MC_SET_RAW_MEM;
-             xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
              MC_UNSET_RAW_MEM;
              
-             MC_ddfs_stateless(search_cycle);
+             MC_ddfs(search_cycle);
 
            }
 
@@ -959,10 +960,10 @@ void MC_ddfs_stateless(int search_cycle){
              //if(!visited(pair_succ->automaton_state, search_cycle)){
 
              MC_SET_RAW_MEM;
-             xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
              MC_UNSET_RAW_MEM;
              
-             MC_ddfs_stateless(search_cycle);
+             MC_ddfs(search_cycle);
              
            }else{
 
@@ -990,10 +991,10 @@ void MC_ddfs_stateless(int search_cycle){
          if(!visited(pair_succ->automaton_state, search_cycle)){
 
            MC_SET_RAW_MEM;
-           xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+           xbt_fifo_unshift(mc_stack_liveness, pair_succ);
            MC_UNSET_RAW_MEM;
            
-           MC_ddfs_stateless(search_cycle);
+           MC_ddfs(search_cycle);
            
          }else{
 
@@ -1005,7 +1006,7 @@ void MC_ddfs_stateless(int search_cycle){
 
        /* Restore system before checking others successors */
        if(cursor != xbt_dynar_length(successors) - 1)
-         MC_replay_liveness(mc_stack_liveness_stateless, 1);
+         MC_replay_liveness(mc_stack_liveness, 1);
 
         
       }
@@ -1018,15 +1019,15 @@ void MC_ddfs_stateless(int search_cycle){
 
   }
 
-  if(xbt_fifo_size(mc_stack_liveness_stateless) == MAX_DEPTH_LIVENESS ){
-    XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness_stateless) );
+  if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
+    XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
   }else{
-    XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness_stateless) );
+    XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
   }
 
   
   MC_SET_RAW_MEM;
-  xbt_fifo_shift(mc_stack_liveness_stateless);
+  xbt_fifo_shift(mc_stack_liveness);
   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
     //xbt_dynar_pop(reached_pairs, NULL);
     xbt_dynar_pop(reached_pairs_hash, NULL);
@@ -1036,4 +1037,3 @@ void MC_ddfs_stateless(int search_cycle){
   
 
 }
-

diff --git a/src/mc/private.h b/src/mc/private.h
index 06fb32c..21f6bfb 100644 (file)
--- a/src/mc/private.h
+++ b/src/mc/private.h
@@ -46,7 +46,7 @@ extern double *mc_time;
 
 /* Bound of the MC depth-first search algorithm */
 #define MAX_DEPTH 1000
-#define MAX_DEPTH_LIVENESS 20
+#define MAX_DEPTH_LIVENESS 500
 
 int MC_deadlock_check(void);
 void MC_replay(xbt_fifo_t stack);
@@ -208,6 +208,9 @@ void MC_exit_stateful(void);
 
 /********************************** Double-DFS for liveness property**************************************/
 
+extern mc_snapshot_t initial_snapshot_liveness;
+extern xbt_automaton_t automaton;
+
 typedef struct s_mc_pair{
   mc_snapshot_t system_state;
   mc_state_t graph_state;
@@ -248,8 +251,6 @@ void set_pair_reached(xbt_state_t st);
 int reached_hash(xbt_state_t st);
 void set_pair_reached_hash(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);
@@ -257,13 +258,8 @@ int visited(xbt_state_t st, int search_cycle);
 void set_pair_visited(xbt_state_t st, int search_cycle);
 int visited_hash(xbt_state_t st, int search_cycle);
 void set_pair_visited_hash(xbt_state_t st, int search_cycle);
+unsigned int hash_region(char *str, int str_len);
 
-/* **** Double-DFS stateful without visited state **** */
-
-extern xbt_fifo_t mc_stack_liveness_stateful;
-
-void MC_ddfs_stateful_init(xbt_automaton_t a);
-void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore);
 
 /* **** Double-DFS stateless **** */
 
@@ -273,19 +269,14 @@ typedef struct s_mc_pair_stateless{
   int requests;
 }s_mc_pair_stateless_t, *mc_pair_stateless_t;
 
-extern xbt_fifo_t mc_stack_liveness_stateless;
-extern mc_snapshot_t initial_snapshot_liveness;
-extern xbt_automaton_t automaton;
+extern xbt_fifo_t mc_stack_liveness;
 
 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r);
-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_ddfs_init();
+void MC_ddfs(int search_cycle);
+void MC_show_stack_liveness(xbt_fifo_t stack);
+void MC_dump_stack_liveness(xbt_fifo_t stack);
 void MC_pair_stateless_delete(mc_pair_stateless_t pair);
 
-unsigned int hash_region(char *str, int str_len);
-
-
 
 #endif

diff --git a/src/msg/msg_global.c b/src/msg/msg_global.c
index 99240fd..59a644c 100644 (file)
--- a/src/msg/msg_global.c
+++ b/src/msg/msg_global.c
@@ -168,29 +168,15 @@ MSG_error_t MSG_main_stateful(void)
   return MSG_OK;
 }
 
-MSG_error_t MSG_main_liveness_stateful(xbt_automaton_t a)
-{
-  /* Clean IO before the run */
-  fflush(stdout);
-  fflush(stderr);
-
-  if (MC_IS_ENABLED) {
-    MC_modelcheck_liveness_stateful(a);
-  }
-  else {
-    SIMIX_run();
-  }
-  return MSG_OK;
-}
 
-MSG_error_t MSG_main_liveness_stateless(xbt_automaton_t a, char *prgm)
+MSG_error_t MSG_main_liveness(xbt_automaton_t a, char *prgm)
 {
   /* Clean IO before the run */
   fflush(stdout);
   fflush(stderr);
 
   if (MC_IS_ENABLED) {
-    MC_modelcheck_liveness_stateless(a, prgm);
+    MC_modelcheck_liveness(a, prgm);
   }
   else {
     SIMIX_run();