From 1f3dc5fab0ccdb98c1c77fdb2f96f662ea3e45a2 Mon Sep 17 00:00:00 2001
From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Tue, 23 Aug 2011 18:46:29 +0200
Subject: [PATCH] model-checker : ddfs stateless and stateful fixed

---
 examples/msg/mc/CMakeLists.txt                |  10 +-
 examples/msg/mc/automatonparse_promela.c      |  12 +-
 examples/msg/mc/bugged3.c                     |   2 +-
 examples/msg/mc/deploy_mutex.xml              |   2 +-
 .../msg/mc/example2_liveness_without_cycle.c  | 111 ++++++
 .../msg/mc/example2_liveness_without_cycle.h  |  14 +
 ...ton.c => example_liveness_without_cycle.c} |   4 +-
 ...ton.h => example_liveness_without_cycle.h} |   0
 examples/msg/mc/result_parse                  |  17 -
 examples/msg/mc/result_parse2                 |  28 --
 src/mc/mc_global.c                            |   4 +-
 src/mc/mc_liveness.c                          | 356 ++++++------------
 src/mc/private.h                              |   2 +-
 13 files changed, 273 insertions(+), 289 deletions(-)
 create mode 100644 examples/msg/mc/example2_liveness_without_cycle.c
 create mode 100644 examples/msg/mc/example2_liveness_without_cycle.h
 rename examples/msg/mc/{example_automaton.c => example_liveness_without_cycle.c} (92%)
 rename examples/msg/mc/{example_automaton.h => example_liveness_without_cycle.h} (100%)
 delete mode 100644 examples/msg/mc/result_parse
 delete mode 100644 examples/msg/mc/result_parse2

diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt
index d8ac83f5cd..3a9eb3e15b 100644
--- a/examples/msg/mc/CMakeLists.txt
+++ b/examples/msg/mc/CMakeLists.txt
@@ -9,7 +9,12 @@ add_executable(bugged2_stateful bugged2_stateful.c)
 add_executable(bugged2     bugged2.c)
 add_executable(bugged3	   bugged3.c)
 add_executable(random_test random_test.c)
-add_executable(example_automaton automaton.c automatonparse_promela.c example_automaton.c)
+add_executable(example_liveness_without_cycle automaton.c
+automatonparse_promela.c example_liveness_without_cycle.c)
+add_executable(example2_liveness_without_cycle automaton.c
+automatonparse_promela.c
+example2_liveness_without_cycle.c)
+
 
 target_link_libraries(centralized simgrid m )
 target_link_libraries(bugged1     simgrid m )
@@ -18,4 +23,5 @@ target_link_libraries(bugged2_stateful simgrid m)
 target_link_libraries(bugged2     simgrid m )
 target_link_libraries(bugged3     simgrid m )
 target_link_libraries(random_test     simgrid m )
-target_link_libraries(example_automaton     simgrid m )
\ No newline at end of file
+target_link_libraries(example_liveness_without_cycle     simgrid m )
+target_link_libraries(example2_liveness_without_cycle     simgrid m )
\ No newline at end of file
diff --git a/examples/msg/mc/automatonparse_promela.c b/examples/msg/mc/automatonparse_promela.c
index 00678abc35..857ff0e53c 100644
--- a/examples/msg/mc/automatonparse_promela.c
+++ b/examples/msg/mc/automatonparse_promela.c
@@ -10,10 +10,16 @@ void new_state(char* id, int src){
 
   char* id_state = strdup(id);
   char* first_part = strtok(id,"_");
-  int type = 0 ; // -1=état initial, 0=état intermédiaire, 1=état final
+  int type = 0 ; // -1=état initial, 0=état intermédiaire, 1=état final, 2=état initial/final
 
   if(strcmp(first_part,"accept")==0){
-    type = 1;
+     char* second_part = strtok(NULL,"_");
+     if(strcmp(second_part,"init")==0){
+	type = 2;
+     }else{
+	type = 1;
+     }
+     
   }else{
     char* second_part = strtok(NULL,"_");
     if(strcmp(second_part,"init")==0){
@@ -27,7 +33,7 @@ void new_state(char* id, int src){
     state = xbt_automaton_new_state(automaton, type, id_state);
   }
 
-  if(type==-1)
+  if(type==-1 || type==2)
     automaton->current_state = state;
 
   if(src)
diff --git a/examples/msg/mc/bugged3.c b/examples/msg/mc/bugged3.c
index 8e33b31fa1..a398f0fa8a 100644
--- a/examples/msg/mc/bugged3.c
+++ b/examples/msg/mc/bugged3.c
@@ -29,7 +29,7 @@ int server(int argc, char *argv[])
   val1 = (long) MSG_task_get_data(task1);
   XBT_INFO("Received %lu", val1);
 
-  MC_assert(val1 == 2);
+  //MC_assert(val1 == 2);
 
   XBT_INFO("OK");
   return 0;
diff --git a/examples/msg/mc/deploy_mutex.xml b/examples/msg/mc/deploy_mutex.xml
index 1afcee4b17..68c3234813 100644
--- a/examples/msg/mc/deploy_mutex.xml
+++ b/examples/msg/mc/deploy_mutex.xml
@@ -14,7 +14,7 @@
 
   <process host="Geoff" function="client" />
   
-<!--  <process host="Disney" function="client" />
+  <!-- <process host="Disney" function="client" />
     
   <process host="iRMX" function="client" />
       
diff --git a/examples/msg/mc/example2_liveness_without_cycle.c b/examples/msg/mc/example2_liveness_without_cycle.c
new file mode 100644
index 0000000000..14c54b063a
--- /dev/null
+++ b/examples/msg/mc/example2_liveness_without_cycle.c
@@ -0,0 +1,111 @@
+/**************** Shared buffer between asynchronous receives *****************/
+/* Server process assumes that the data from the second communication comm2   */
+/* will overwrite the one from the first communication, because of the order  */
+/* of the wait calls. This is not true because data copy can be triggered by  */
+/* a call to wait on the other end of the communication (client).             */
+/* NOTE that the communications use different mailboxes, but they share the   */
+/* same buffer for reception (task1).                                         */
+/******************************************************************************/
+
+#include "xbt/automaton.h"
+#include "xbt/automatonparse_promela.h"
+#include "example2_liveness_without_cycle.h"
+#include "msg/msg.h"
+#include "mc/mc.h"
+
+#include "y.tab.c"
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "Example liveness with cycle");
+
+extern xbt_automaton_t automaton;
+
+
+int p=1;
+int q=0;
+
+
+int predP(){
+  return p;
+}
+
+
+int predQ(){
+  return q;
+}
+
+
+int server(int argc, char *argv[]);
+int client(int argc, char *argv[]);
+
+int server(int argc, char *argv[])
+{
+  m_task_t task1;
+  long val1;
+  msg_comm_t comm1, comm2;
+
+  comm1 = MSG_task_irecv(&task1, "mymailbox1");
+  comm2 = MSG_task_irecv(&task1, "mymailbox2");
+  MSG_comm_wait(comm1, -1);
+  MSG_comm_wait(comm2, -1);
+
+  val1 = (long) MSG_task_get_data(task1);
+  XBT_INFO("Received %lu", val1);
+
+  //MC_assert_pair_stateless(val1 == 2);
+
+  /*if(val1 == 2)
+    q = 1;
+  else
+  q = 0;*/
+
+  //XBT_INFO("q (server) = %d", q);
+
+  XBT_INFO("OK");
+ 
+  return 0;
+}
+
+int client(int argc, char *argv[])
+{
+  msg_comm_t comm;
+  char *mbox;
+  m_task_t task1 =
+      MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
+
+  mbox = bprintf("mymailbox%s", argv[1]);
+
+  XBT_INFO("Send %d!", atoi(argv[1]));
+  comm = MSG_task_isend(task1, mbox);
+
+  MSG_comm_wait(comm, -1);
+
+  xbt_free(mbox);
+
+  return 0;
+}
+
+int main(int argc, char *argv[])
+{
+
+  init();
+  yyparse();
+  automaton = get_automaton();
+  xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"p", &predP); 
+  ps = xbt_new_propositional_symbol(automaton,"q", &predQ); 
+      
+  //display_automaton();
+
+  MSG_global_init(&argc, argv);
+
+  MSG_create_environment("platform.xml");
+
+  MSG_function_register("server", server);
+
+  MSG_function_register("client", client);
+
+  MSG_launch_application("deploy_bugged3.xml");
+
+  MSG_main_liveness_stateless(automaton);
+
+  return 0;
+}
diff --git a/examples/msg/mc/example2_liveness_without_cycle.h b/examples/msg/mc/example2_liveness_without_cycle.h
new file mode 100644
index 0000000000..8363b17426
--- /dev/null
+++ b/examples/msg/mc/example2_liveness_without_cycle.h
@@ -0,0 +1,14 @@
+#ifndef _EXAMPLE2_LIVENESS_WITHOUT_CYCLE_H
+#define _EXAMPLE2_LIVENESS_WITHOUT_CYCLE_H
+
+int yyparse(void);
+int yywrap(void);
+int yylex(void);
+
+int predP(void);
+int predQ(void);
+
+int server(int argc, char **argv);
+int client(int argc, char **argv);
+
+#endif 
diff --git a/examples/msg/mc/example_automaton.c b/examples/msg/mc/example_liveness_without_cycle.c
similarity index 92%
rename from examples/msg/mc/example_automaton.c
rename to examples/msg/mc/example_liveness_without_cycle.c
index 69a5629573..a6e998cb24 100644
--- a/examples/msg/mc/example_automaton.c
+++ b/examples/msg/mc/example_liveness_without_cycle.c
@@ -1,6 +1,6 @@
 #include "xbt/automaton.h"
 #include "xbt/automatonparse_promela.h"
-#include "example_automaton.h"
+#include "example_liveness_without_cycle.h"
 #include "msg/msg.h"
 #include "mc/mc.h"
 
@@ -8,7 +8,7 @@
 
 #define N 3
 
-XBT_LOG_NEW_DEFAULT_CATEGORY(example, "Example with automaton");
+XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_without_cycle, "Example liveness without cycle");
 
 extern xbt_automaton_t automaton;
 
diff --git a/examples/msg/mc/example_automaton.h b/examples/msg/mc/example_liveness_without_cycle.h
similarity index 100%
rename from examples/msg/mc/example_automaton.h
rename to examples/msg/mc/example_liveness_without_cycle.h
diff --git a/examples/msg/mc/result_parse b/examples/msg/mc/result_parse
deleted file mode 100644
index 92702b12e2..0000000000
--- a/examples/msg/mc/result_parse
+++ /dev/null
@@ -1,17 +0,0 @@
-never { /* !([]<>p->[](q-><>r)) */
-T0_init:
-	if
-	:: (1) -> goto T0_init
-	:: (!r && q) -> goto T1_S4
-	fi;
-T1_S4:
-	if
-	:: (!r) -> goto T1_S4
-	:: (!r && p) -> goto accept_S4
-	fi;
-accept_S4:
-	if
-	:: (!r) -> goto T1_S4
-	:: (!r && p) -> goto accept_S4
-	fi;
-}
diff --git a/examples/msg/mc/result_parse2 b/examples/msg/mc/result_parse2
deleted file mode 100644
index 2d0a31203d..0000000000
--- a/examples/msg/mc/result_parse2
+++ /dev/null
@@ -1,28 +0,0 @@
-never {
-T0_init:
-	if
-	:: (!d) || (r) -> goto accept_S1
-	:: (1) -> goto T1_S4
-	:: (1) -> goto T0_S2
-	:: (!e) -> goto accept_S3
-	fi;
-T1_S4:
-	if
-	:: (1) -> goto T1_S4
-	:: (r) -> goto accept_S1
-	fi;
-accept_S1:
-	if
-	:: (!d) || (r) -> goto accept_S1
-	:: (1) -> goto T1_S4
-	fi;
-T0_S2:
-	if
-	:: (1) -> goto T0_S2
-	:: (!e) -> goto accept_S3
-	fi;
-accept_S3:
-	if
-	:: (!e) -> goto accept_S3
-	fi;
-}
diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 556fa707fb..addfdbbcc4 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -116,8 +116,8 @@ void MC_init_liveness_stateful(xbt_automaton_t a){
 
   MC_UNSET_RAW_MEM;
 
-  MC_vddfs_stateful_init(a);
-  //MC_ddfs_stateful_init(a);
+  //MC_vddfs_stateful_init(a);
+  MC_ddfs_stateful_init(a);
   //MC_dpor2_init(a);
   //MC_dpor3_init(a);
 }
diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 65e780da44..d6ff58b114 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -178,89 +178,9 @@ void MC_vddfs_stateful_init(xbt_automaton_t a){
 
   MC_UNSET_RAW_MEM; 
 
-  /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système 
-    -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
-
   unsigned int cursor = 0;
-  //unsigned int cursor2 = 0;
   xbt_state_t state = NULL;
-  //int res;
-  //xbt_transition_t transition_succ;
-  //xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
-  //mc_pair_t pair_succ;
-
-  /* xbt_dynar_foreach(a->states, cursor, state){
-    if(state->type == -1){
-      xbt_dynar_foreach(state->out, cursor2, transition_succ){
-  	res = MC_automaton_evaluate_label(a, transition_succ->label);
-	
-  	if(res == 1){
-	 
-  	  MC_SET_RAW_MEM;
-
-  	  mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-  	  xbt_dynar_push(successors, &mc_initial_pair);
-
-  	  MC_UNSET_RAW_MEM;
-
-	}
-      }
-    }
-  }
-
-  cursor = 0;
-  cursor2 = 0;
-
-  xbt_dynar_foreach(a->states, cursor, state){
-    if(state->type == -1){
-      xbt_dynar_foreach(state->out, cursor2, transition_succ){
-  	res = MC_automaton_evaluate_label(a, transition_succ->label);
-	
-  	if(res == 2){
-	 
-  	  MC_SET_RAW_MEM;
-
-  	  mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-  	  xbt_dynar_push(successors, &mc_initial_pair);
-
-  	  MC_UNSET_RAW_MEM;
-
-	}
-      }
-    }
-  }
-
-  cursor = 0;
-
-  if(xbt_dynar_length(successors) == 0){
-    xbt_dynar_foreach(a->states, cursor, state){
-      if(state->type == -1){
-	MC_SET_RAW_MEM;
-
-	mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-	xbt_dynar_push(successors, &mc_initial_pair);
-	
-	MC_UNSET_RAW_MEM;
-      }
-    }
-  }
-
-  cursor = 0;
-  xbt_dynar_foreach(successors, cursor, pair_succ){
-    MC_SET_RAW_MEM;
-
-    xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 
-    MC_UNSET_RAW_MEM;
-
-    if(cursor == 0){
-      MC_vddfs_stateful(a, 0, 0);
-    }else{
-      MC_vddfs_stateful(a, 0, 1);
-    }
-  } */
-
-  cursor = 0;
   xbt_dynar_foreach(a->states, cursor, state){
     if(state->type == -1){
     
@@ -272,8 +192,26 @@ void MC_vddfs_stateful_init(xbt_automaton_t a){
       if(cursor == 0){
 	MC_vddfs_stateful(a, 0, 0);
       }else{
-	MC_vddfs_stateful(a, 0, 1);
+	MC_restore_snapshot(init_snapshot);
+	MC_UNSET_RAW_MEM;
+	MC_vddfs_stateful(a, 0, 0);
       }
+    }else{
+       if(state->type == 2){
+    
+	 MC_SET_RAW_MEM;
+	 mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
+	 xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
+	 MC_UNSET_RAW_MEM;
+	 
+	 if(cursor == 0){
+	   MC_vddfs_stateful(a, 1, 0);
+	 }else{
+	   MC_restore_snapshot(init_snapshot);
+	   MC_UNSET_RAW_MEM;
+	   MC_vddfs_stateful(a, 1, 0);
+	 }
+       }
     }
   } 
 }
@@ -443,46 +381,44 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 	MC_vddfs_stateful(a, search_cycle, 0);
 
 	//XBT_DEBUG("Pair (graph=%p, automaton=%p) expanded", pair_succ->graph_state, pair_succ->automaton_state);
+
+	if((search_cycle == 0) && ((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2))){
+
+	  MC_restore_snapshot(current_pair->system_state);
+	  MC_UNSET_RAW_MEM;
+      
+	  xbt_swag_foreach(process, simix_global->process_list){
+	    if(MC_process_is_enabled(process)){
+	      MC_state_interleave_process(current_pair->graph_state, process);
+	    }
+	  }
+      
+      
+	  set_pair_reached(current_pair);
+	  XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
+	  MC_vddfs_stateful(a, 1, 1);
+	  xbt_dynar_pop(reached_pairs, NULL);
+
+	}
 	
       }else{
 
 	XBT_DEBUG("Pair already visited !");
-
       }
-    }
-
-    if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
-
-      /*MC_restore_snapshot(current_pair->system_state);
-	MC_UNSET_RAW_MEM;
- 
-	xbt_swag_foreach(process, simix_global->process_list){
-	if(MC_process_is_enabled(process)){
-	MC_state_interleave_process(current_pair->graph_state, process);
-	}
-	}*/
-	    
-      set_pair_reached(current_pair);
-      XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
-      MC_vddfs_stateful(a, 1, 1);
 
     }
     
-    
-    
     if(MC_state_interleave_size(current_pair->graph_state) > 0){
       MC_restore_snapshot(current_snapshot);
       MC_UNSET_RAW_MEM;
+      
     }
   }
 
   
   MC_SET_RAW_MEM;
-  mc_pair_t top_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
-  if((top_pair->graph_state == current_pair->graph_state) && (top_pair->automaton_state == current_pair->automaton_state)){  
-    xbt_fifo_shift(mc_stack_liveness_stateful);
-    XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
-  }
+  xbt_fifo_shift(mc_stack_liveness_stateful);
+  XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
   MC_UNSET_RAW_MEM;
 
   
@@ -524,74 +460,9 @@ void MC_ddfs_stateful_init(xbt_automaton_t a){
 
   MC_UNSET_RAW_MEM; 
 
-  /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système 
-    -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
-
   unsigned int cursor = 0;
-  //unsigned int cursor2 = 0;
   xbt_state_t state = NULL;
-  //int res;
-  //xbt_transition_t transition_succ;
-  //xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
-  //mc_pair_t pair_succ;
-
-  /*xbt_dynar_foreach(a->states, cursor, state){
-    if(state->type == -1){
-      xbt_dynar_foreach(state->out, cursor2, transition_succ){
-  	res = MC_automaton_evaluate_label(a, transition_succ->label);
-	
-  	if(res == 1){
-	 
-  	  MC_SET_RAW_MEM;
-
-  	  mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-  	  xbt_dynar_push(successors, &mc_initial_pair);
-
-  	  MC_UNSET_RAW_MEM;
-
-	}
-      }
-    }
-  }
-
-  cursor = 0;
-  cursor2 = 0;
 
-  xbt_dynar_foreach(a->states, cursor, state){
-    if(state->type == -1){
-      xbt_dynar_foreach(state->out, cursor2, transition_succ){
-  	res = MC_automaton_evaluate_label(a, transition_succ->label);
-	
-  	if(res == 2){
-	 
-  	  MC_SET_RAW_MEM;
-
-  	  mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-  	  xbt_dynar_push(successors, &mc_initial_pair);
-
-  	  MC_UNSET_RAW_MEM;
-
-	}
-      }
-    }
-  }
-
-  cursor = 0;
-
-  if(xbt_dynar_length(successors) == 0){
-    xbt_dynar_foreach(a->states, cursor, state){
-      if(state->type == -1){
-	MC_SET_RAW_MEM;
-
-	mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-	xbt_dynar_push(successors, &mc_initial_pair);
-	
-	MC_UNSET_RAW_MEM;
-      }
-    }
-    }*/
-
-  cursor = 0;
   xbt_dynar_foreach(a->states, cursor, state){
     if(state->type == -1){
     
@@ -603,8 +474,26 @@ void MC_ddfs_stateful_init(xbt_automaton_t a){
       if(cursor == 0){
 	MC_ddfs_stateful(a, 0, 0);
       }else{
-	MC_ddfs_stateful(a, 0, 1);
+	MC_restore_snapshot(init_snapshot);
+	MC_UNSET_RAW_MEM;
+	MC_ddfs_stateful(a, 0, 0);
       }
+    }else{
+       if(state->type == 2){
+    
+	 MC_SET_RAW_MEM;
+	 mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
+	 xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
+	 MC_UNSET_RAW_MEM;
+	 
+	 if(cursor == 0){
+	   MC_ddfs_stateful(a, 1, 0);
+	 }else{
+	   MC_restore_snapshot(init_snapshot);
+	   MC_UNSET_RAW_MEM;
+	   MC_ddfs_stateful(a, 1, 0);
+	 }
+       }
     }
   } 
 }
@@ -655,6 +544,8 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
   mc_pair_t next_pair;
   mc_snapshot_t next_snapshot;
   mc_snapshot_t current_snapshot;
+
+  //sleep(1);
   
   
   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
@@ -722,7 +613,7 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 
       MC_SET_RAW_MEM;
 	
-      if(res == 2){ // enabled transition in automaton
+      if(res == 2){ // transition always enabled in automaton
 	next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 	xbt_dynar_push(successors, &next_pair);
       }
@@ -758,41 +649,34 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 	exit(0);
       }
 	
-      mc_stats_pair->executed_transitions++;
+      //mc_stats_pair->executed_transitions++;
  
       MC_SET_RAW_MEM;
       xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
       MC_UNSET_RAW_MEM;
 
       MC_ddfs_stateful(a, search_cycle, 0);
-    }
     
-    if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
-
-	set_pair_reached(current_pair);
-	XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
+    
+      if((search_cycle == 0) && ((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2))){
 
-	/*MC_restore_snapshot(current_pair->system_state);
+	MC_restore_snapshot(current_pair->system_state);
 	MC_UNSET_RAW_MEM;
- 
+
 	xbt_swag_foreach(process, simix_global->process_list){
 	  if(MC_process_is_enabled(process)){
 	    MC_state_interleave_process(current_pair->graph_state, process);
 	  }
 	}
-	    
-	mc_pair_t top_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
-	if((top_pair->graph_state != current_pair->graph_state) || (top_pair->automaton_state != current_pair->automaton_state)){ 
-	  MC_SET_RAW_MEM;
-	  xbt_fifo_unshift(mc_stack_liveness_stateful, current_pair);
-	  MC_UNSET_RAW_MEM;
-	  }*/
 
+	set_pair_reached(current_pair);
+	XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
 	MC_ddfs_stateful(a, 1, 1);
 
-    }
+	xbt_dynar_pop(reached_pairs, NULL);
+      }
 
-     
+    }
     if(MC_state_interleave_size(current_pair->graph_state) > 0){
       MC_restore_snapshot(current_snapshot);
       MC_UNSET_RAW_MEM;
@@ -802,11 +686,8 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 
   
   MC_SET_RAW_MEM;
-  mc_pair_t top_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
-  if((top_pair->graph_state == current_pair->graph_state) && (top_pair->automaton_state == current_pair->automaton_state)){  
-    xbt_fifo_shift(mc_stack_liveness_stateful);
-    XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
-  }
+  xbt_fifo_shift(mc_stack_liveness_stateful);
+  XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
   MC_UNSET_RAW_MEM;
 
 }
@@ -991,24 +872,49 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){
       MC_UNSET_RAW_MEM;
       
       if(cursor == 0){
-	MC_ddfs_stateless(a, 0);
+	MC_ddfs_stateless(a, 0, 0);
       }else{
 	MC_restore_snapshot(initial_snapshot);
 	MC_UNSET_RAW_MEM;
-	MC_ddfs_stateless(a, 0);
+	MC_ddfs_stateless(a, 0, 0);
+      }
+    }else{
+      if(state->type == 2){
+      
+	MC_SET_RAW_MEM;
+	mc_initial_pair = new_pair_stateless(initial_graph_state, state);
+	xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
+	
+	initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
+	MC_take_snapshot(initial_snapshot);
+	
+	MC_UNSET_RAW_MEM;
+	
+	if(cursor == 0){
+	  MC_ddfs_stateless(a, 1, 0);
+	}else{
+	  MC_restore_snapshot(initial_snapshot);
+	  MC_UNSET_RAW_MEM;
+	  MC_ddfs_stateless(a, 1, 0);
+	}
       }
     }
   } 
+
 }
 
 
-void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle){
+void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
 
   smx_process_t process = NULL;
 
   if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
     return;
 
+  if(replay == 1){
+    MC_replay_liveness(mc_stack_liveness_stateless);
+  }
+
   //XBT_DEBUG("Stack size before restore %u", xbt_fifo_size(mc_stack_liveness_stateless));
 
   /* Get current state */
@@ -1032,22 +938,16 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle){
   xbt_dynar_t successors;
 
   mc_pair_stateless_t next_pair;  
-  mc_snapshot_t current_snap;
-
+  //mc_snapshot_t current_snap;
+    
   
   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
-    
-    MC_SET_RAW_MEM;
-    current_snap = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot(current_snap);
-    MC_UNSET_RAW_MEM;
-    
+   
     //XBT_DEBUG("Interleave size %u", MC_state_interleave_size(current_pair->graph_state));
 
     /* Debug information */
     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
       req_str = MC_request_to_string(req, value);
-      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));
       XBT_DEBUG("Execute: %s", req_str);
       xbt_free(req_str);
     }
@@ -1145,47 +1045,39 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle){
       xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
       MC_UNSET_RAW_MEM;
 
-      MC_ddfs_stateless(a, search_cycle);
+      MC_ddfs_stateless(a, search_cycle, 0);
 
       //XBT_DEBUG("Stack size %u", xbt_fifo_size(mc_stack_liveness_stateless));
-    }
 
-    //xbt_dynar_reset(successors);
-    
-    if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
+      if((search_cycle == 0) && ((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2))){
 
-	set_pair_stateless_reached(current_pair);
-	XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
-	MC_restore_snapshot(current_snap);
-	MC_UNSET_RAW_MEM;
-
-	xbt_swag_foreach(process, simix_global->process_list){
+	/*xbt_swag_foreach(process, simix_global->process_list){
 	  if(MC_process_is_enabled(process)){
-	    MC_state_interleave_process(current_pair->graph_state, process);
+	  MC_state_interleave_process(current_pair->graph_state, process);
 	  }
-	}
+	  }*/
 
-	MC_ddfs_stateless(a, 1);
+	set_pair_stateless_reached(current_pair);
+	XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
+      
+	MC_ddfs_stateless(a, 1, 1);
+      
+	xbt_dynar_pop(reached_pairs, NULL);
+      }
     }
 
     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);
-      MC_restore_snapshot(current_snap);
-      MC_UNSET_RAW_MEM;
-    }
-
+      XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
+      MC_replay_liveness(mc_stack_liveness_stateless);
+    }    
+   
   }
 
   
   MC_SET_RAW_MEM;
-  mc_pair_stateless_t top_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
-  if((top_pair->graph_state == current_pair->graph_state) && (top_pair->automaton_state == current_pair->automaton_state)){  
-    xbt_fifo_shift(mc_stack_liveness_stateless);
-    XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
-  }
+  xbt_fifo_shift(mc_stack_liveness_stateless);
+  XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
   MC_UNSET_RAW_MEM;
-  //XBT_DEBUG("Stack size after shift %u", xbt_fifo_size(mc_stack_liveness_stateless));
 
 }
 
diff --git a/src/mc/private.h b/src/mc/private.h
index ba7cc37114..339d97baa8 100644
--- a/src/mc/private.h
+++ b/src/mc/private.h
@@ -239,7 +239,7 @@ extern xbt_fifo_t mc_stack_liveness_stateless;
 
 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st);
 void MC_ddfs_stateless_init(xbt_automaton_t a);
-void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle);
+void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay);
 int reached_stateless(mc_pair_stateless_t p);
 void set_pair_stateless_reached(mc_pair_stateless_t p);
 void MC_show_stack_liveness_stateless(xbt_fifo_t stack);
-- 
2.20.1