From: Martin Quinson <martin.quinson@loria.fr>
Date: Fri, 13 Jan 2012 14:13:42 +0000 (+0100)
Subject: Merge branch 'MC_LTL'
X-Git-Tag: exp_20120216~133
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/15c81e44412415173de220954a453019c68714cd?hp=ab36e52cc954b2f03e681b0646a6518591aa43d8

Merge branch 'MC_LTL'
---

diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt
index bae8896280..82578b92e5 100644
--- a/examples/msg/mc/CMakeLists.txt
+++ b/examples/msg/mc/CMakeLists.txt
@@ -9,10 +9,9 @@ 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_liveness_with_cycle2 automaton.c
-automatonparse_promela.c example_liveness_with_cycle2.c)
-add_executable(example_liveness_with_cycle automaton.c
-automatonparse_promela.c example_liveness_with_cycle.c)
+add_executable(bugged1_liveness automaton.c automatonparse_promela.c bugged1_liveness.c)
+add_executable(bugged2_liveness automaton.c automatonparse_promela.c bugged2_liveness.c)
+add_executable(centralized_liveness automaton.c automatonparse_promela.c centralized_liveness.c)
 
 
 
@@ -23,5 +22,6 @@ 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_liveness_with_cycle2     simgrid m )
-target_link_libraries(example_liveness_with_cycle     simgrid m )
\ No newline at end of file
+target_link_libraries(bugged1_liveness     simgrid m )
+target_link_libraries(bugged2_liveness     simgrid m )
+target_link_libraries(centralized_liveness     simgrid m )
\ No newline at end of file
diff --git a/examples/msg/mc/automaton_PROMELA b/examples/msg/mc/automaton_PROMELA
deleted file mode 100644
index 2d0a31203d..0000000000
--- a/examples/msg/mc/automaton_PROMELA
+++ /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/examples/msg/mc/example_liveness_with_cycle.c b/examples/msg/mc/bugged1_liveness.c
similarity index 80%
rename from examples/msg/mc/example_liveness_with_cycle.c
rename to examples/msg/mc/bugged1_liveness.c
index 8f516874e3..3d051c9a4e 100644
--- a/examples/msg/mc/example_liveness_with_cycle.c
+++ b/examples/msg/mc/bugged1_liveness.c
@@ -1,30 +1,31 @@
 /***************** Centralized Mutual Exclusion Algorithm *********************/
 /* This example implements a centralized mutual exclusion algorithm.          */
 /* CS requests of client 2 not satisfied                                      */
+/* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok)            */
 /******************************************************************************/
 
 #include "msg/msg.h"
 #include "mc/mc.h"
 #include "xbt/automaton.h"
 #include "xbt/automatonparse_promela.h"
-#include "example_liveness_with_cycle.h"
+#include "bugged1_liveness.h"
 #include "y.tab.c"
 
 #define AMOUNT_OF_CLIENTS 2
-#define CS_PER_PROCESS 10
+#define CS_PER_PROCESS 1
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "my log messages");
 
 
-int p=0; 
-int q=0;
+int r=0; 
+int cs=0;
 
-int predP(){
-  return p;
+int predR(){
+  return r;
 }
 
-int predQ(){
-  return q;
+int predCS(){
+  return cs;
 }
 
 
@@ -60,7 +61,10 @@ int coordinator(int argc, char *argv[])
 	  MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
 	  todo--;
 	}else{
-	   CS_used = 0;
+	  xbt_dynar_pop(requests, &req);
+	  MSG_task_send(MSG_task_create("notgrant", 0, 1000, NULL), req);
+	  CS_used = 0;
+	  todo--;
 	}
       } else {                  // nobody wants it
         XBT_INFO("CS release. resource now idle");
@@ -88,19 +92,20 @@ int client(int argc, char *argv[])
     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
 
     if(strcmp(my_mailbox, "2") == 0){
-      p = 1;
-      q = 0;
-      XBT_DEBUG("Propositions changed : p=1, q=0");
+      r = 1;
+      cs = 0;
+      XBT_DEBUG("Propositions changed : r=1, cs=0");
     }
 
     // wait the answer
     m_task_t grant = NULL;
     MSG_task_receive(&grant, my_mailbox);
+    const char *kind = MSG_task_get_name(grant);
 
-    if(strcmp(my_mailbox, "2") == 0){
-      q = 1;
-      p = 0;
-      XBT_DEBUG("Propositions changed : p=0, q=1");
+    if((strcmp(my_mailbox, "2") == 0) && (strcmp("grant", kind) == 0)){
+      cs = 1;
+      r = 0;
+      XBT_DEBUG("Propositions changed : r=0, cs=1");
     }
 
 
@@ -112,9 +117,9 @@ int client(int argc, char *argv[])
     MSG_process_sleep(my_pid);
     
     if(strcmp(my_mailbox, "2") == 0){
-      q=0;
-      p=0;
-      XBT_DEBUG("Propositions changed : p=0, q=0");
+      cs=0;
+      r=0;
+      XBT_DEBUG("Propositions changed : r=0, cs=0");
     }
     
   }
@@ -128,14 +133,14 @@ int main(int argc, char *argv[])
   init();
   yyparse();
   automaton = get_automaton();
-  xbt_new_propositional_symbol(automaton,"p", &predP); 
-  xbt_new_propositional_symbol(automaton,"q", &predQ); 
+  xbt_new_propositional_symbol(automaton,"r", &predR); 
+  xbt_new_propositional_symbol(automaton,"cs", &predCS); 
   
   MSG_global_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
-  MSG_launch_application("deploy_mutex2.xml");
+  MSG_launch_application("deploy_bugged1_liveness.xml");
   MSG_main_liveness(automaton, argv[0]);
 
   return 0;
diff --git a/examples/msg/mc/example_liveness_with_cycle.h b/examples/msg/mc/bugged1_liveness.h
similarity index 56%
rename from examples/msg/mc/example_liveness_with_cycle.h
rename to examples/msg/mc/bugged1_liveness.h
index c614af2317..a33976881e 100644
--- a/examples/msg/mc/example_liveness_with_cycle.h
+++ b/examples/msg/mc/bugged1_liveness.h
@@ -1,12 +1,12 @@
-#ifndef _EXAMPLE_LIVENESS_WITH_CYCLE_H
-#define _EXAMPLE_LIVENESS_WITH_CYCLE_H
+#ifndef _BUGGED1_LIVENESS_H
+#define _BUGGED1_LIVENESS_H
 
 int yyparse(void);
 int yywrap(void);
 int yylex(void);
 
-int predP(void);
-int predQ(void);
+int predR(void);
+int predCS(void);
 
 int coordinator(int argc, char *argv[]);
 int client(int argc, char *argv[]);
diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c
new file mode 100644
index 0000000000..305771fbdc
--- /dev/null
+++ b/examples/msg/mc/bugged2_liveness.c
@@ -0,0 +1,189 @@
+/***************** Producer/Consumer Algorithm *************************/
+/* This example implements a producer/consumer algorithm.              */
+/* If consumer work before producer, message is empty                  */
+/***********************************************************************/
+
+
+#include "msg/msg.h"
+#include "mc/mc.h"
+#include "xbt/automaton.h"
+#include "xbt/automatonparse_promela.h"
+#include "bugged2_liveness.h"
+#include "y.tab.c"
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "my log messages");
+
+char* buffer;
+
+int consume = 0;
+int produce = 0;
+int cready = 0;
+int pready = 0;
+
+int predPready(){
+  return pready;
+}
+
+int predCready(){
+  return cready;
+}
+
+int predConsume(){
+  return consume;
+}
+
+int predProduce(){
+  return produce;
+}
+
+int coordinator(int argc, char *argv[])
+{
+  xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
+  int CS_used = 0;
+
+  while(1) {
+    m_task_t task = NULL;
+    MSG_task_receive(&task, "coordinator");
+    const char *kind = MSG_task_get_name(task);
+    if (!strcmp(kind, "request")) {
+      char *req = MSG_task_get_data(task);
+      if (CS_used) {
+	XBT_INFO("CS already used. Queue the request");
+	xbt_dynar_push(requests, &req);
+      } else {
+	m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
+	MSG_task_send(answer, req);
+	CS_used = 1;
+	XBT_INFO("CS idle. Grant immediatly");
+      }
+    } else {
+      if (xbt_dynar_length(requests) > 0) {
+	XBT_INFO("CS release. Grant to queued requests");
+	char *req;
+	xbt_dynar_pop(requests, &req);
+	MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
+      } else {
+	XBT_INFO("CS_realase, ressource now idle");
+	CS_used = 0;
+      }
+    }
+
+    MSG_task_destroy(task);
+
+  }
+
+  return 0;
+
+}
+
+int producer(int argc, char *argv[])
+{
+
+  char * my_mailbox = bprintf("%s", argv[1]);
+  
+  //while(1) {
+    
+    /* Create message */
+    const char *mess = "message";
+    
+    /* CS request */
+    XBT_INFO("Producer ask the request");
+    MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
+
+    /* Wait the answer */
+    m_task_t grant = NULL;
+    MSG_task_receive(&grant, my_mailbox);
+    MSG_task_destroy(grant);
+
+    pready = 1;
+
+    /* Push message (size of buffer = 1) */
+    buffer = strdup(mess);
+
+    /* CS release */
+    MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
+
+    produce = 1;
+    pready = 0;
+
+    //produce = 0;
+    //pready = 0;
+
+    //}
+
+  return 0;
+
+}
+
+int consumer(int argc, char *argv[])
+{
+
+  char * my_mailbox = bprintf("%s", argv[1]);
+  char *mess;
+
+
+  //while(1) {
+    
+    /* CS request */
+    XBT_INFO("Consumer ask the request");
+    MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
+
+    /* Wait the answer */
+    m_task_t grant = NULL;
+    MSG_task_receive(&grant, my_mailbox);
+    MSG_task_destroy(grant);
+
+    cready = 1;
+
+    /* Pop message  */
+    mess = malloc(8*sizeof(char));
+    mess = strdup(buffer);
+    buffer[0] = '\0'; 
+
+    /* CS release */
+    MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
+
+    /* Display message */
+    XBT_INFO("Message : %s", mess);
+    if(strcmp(mess, "") != 0)
+      consume = 1;
+
+    cready = 0;
+
+    free(mess);
+
+    //consume = 0;
+    //cready = 0;
+
+    //}
+
+  return 0;
+
+}
+
+
+int main(int argc, char *argv[])
+{
+
+  buffer = malloc(8*sizeof(char));
+  buffer[0]='\0';
+
+  init();
+  yyparse();
+  automaton = get_automaton();
+  xbt_new_propositional_symbol(automaton,"pready", &predPready); 
+  xbt_new_propositional_symbol(automaton,"cready", &predCready); 
+  xbt_new_propositional_symbol(automaton,"consume", &predConsume);
+  xbt_new_propositional_symbol(automaton,"produce", &predProduce); 
+  
+  MSG_global_init(&argc, argv);
+  MSG_create_environment("../msg_platform.xml");
+  MSG_function_register("coordinator", coordinator);
+  MSG_function_register("consumer", consumer);
+  MSG_function_register("producer", producer);
+  MSG_launch_application("deploy_bugged2_liveness.xml");
+  MSG_main_liveness(automaton, argv[0]);
+
+  return 0;
+
+}
diff --git a/examples/msg/mc/bugged2_liveness.h b/examples/msg/mc/bugged2_liveness.h
new file mode 100644
index 0000000000..43b271bb33
--- /dev/null
+++ b/examples/msg/mc/bugged2_liveness.h
@@ -0,0 +1,17 @@
+#ifndef _BUGGED2_LIVENESS_H
+#define _BUGGED2_LIVENESS_H
+
+int yyparse(void);
+int yywrap(void);
+int yylex(void);
+
+int predPready(void);
+int predCready(void);
+int predConsume(void);
+int predProduce(void);
+
+int coordinator(int argc, char *argv[]);
+int producer(int argc, char *argv[]);
+int consumer(int argc, char *argv[]);
+
+#endif 
diff --git a/examples/msg/mc/centralized_liveness.c b/examples/msg/mc/centralized_liveness.c
new file mode 100644
index 0000000000..350c59bb85
--- /dev/null
+++ b/examples/msg/mc/centralized_liveness.c
@@ -0,0 +1,108 @@
+#include "msg/msg.h"
+#include "mc/mc.h"
+#include "xbt/automaton.h"
+#include "xbt/automatonparse_promela.h"
+#include "centralized_liveness.h"
+#include "y.tab.c"
+
+#define AMOUNT_OF_CLIENTS 2
+#define CS_PER_PROCESS 1
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(centralized, "my log messages");
+ 
+int cs2 = 0;
+
+int predCS2(){
+  return cs2;
+}
+
+
+int coordinator(int argc, char **argv);
+int client(int argc, char **argv);
+
+int coordinator(int argc, char *argv[])
+{
+  xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);   // dynamic vector storing requests (which are char*)
+  int CS_used = 0;              // initially the CS is idle
+  
+  while (1) {
+    m_task_t task = NULL;
+    MSG_task_receive(&task, "coordinator");
+    const char *kind = MSG_task_get_name(task); //is it a request or a release?
+    if (!strcmp(kind, "request")) {     // that's a request
+      char *req = MSG_task_get_data(task);
+      if (CS_used) {            // need to push the request in the vector
+        XBT_INFO("CS already used. Queue the request");
+        xbt_dynar_push(requests, &req);
+      } else {                  // can serve it immediatly
+        XBT_INFO("CS idle. Grant immediatly");
+        m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
+        MSG_task_send(answer, req);
+        CS_used = 1;
+      }
+    } else {                    // that's a release. Check if someone was waiting for the lock
+      if (!xbt_dynar_is_empty(requests)) {
+        XBT_INFO("CS release. Grant to queued requests (queue size: %lu)",
+              xbt_dynar_length(requests));
+        char *req;
+        xbt_dynar_pop(requests, &req);
+        MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
+      } else {                  // nobody wants it
+        XBT_INFO("CS release. resource now idle");
+        CS_used = 0;
+      }
+    }
+    MSG_task_destroy(task);
+  }
+  
+  return 0;
+}
+
+int client(int argc, char *argv[])
+{
+  int my_pid = MSG_process_get_PID(MSG_process_self());
+  char *my_mailbox = bprintf("%s", argv[1]);
+ 
+  while(1){
+
+    if(!strcmp(my_mailbox, "2"))
+      cs2 = 0;
+
+    XBT_INFO("Client (%s) ask the request", my_mailbox);
+    MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox),
+                  "coordinator");
+    // wait the answer
+    m_task_t grant = NULL;
+    MSG_task_receive(&grant, my_mailbox);
+    MSG_task_destroy(grant);
+    XBT_INFO("got the answer. Sleep a bit and release it");
+
+    if(!strcmp(my_mailbox, "2"))
+      cs2 = 1;
+
+    MSG_process_sleep(1);
+    MSG_task_send(MSG_task_create("release", 0, 1000, NULL),
+                  "coordinator");
+    MSG_process_sleep(my_pid);
+  }
+
+  return 0;
+}
+
+int main(int argc, char *argv[])
+{
+  init();
+  yyparse();
+  automaton = get_automaton();
+  xbt_new_propositional_symbol(automaton,"cs2", &predCS2); 
+  
+  MSG_global_init(&argc, argv);
+  MSG_create_environment("../msg_platform.xml");
+  MSG_function_register("coordinator", coordinator);
+  MSG_function_register("client", client);
+  MSG_launch_application("deploy_centralized_liveness.xml");
+  MSG_main_liveness(automaton, argv[0]);
+
+  return 0;
+
+}
diff --git a/examples/msg/mc/centralized_liveness.h b/examples/msg/mc/centralized_liveness.h
new file mode 100644
index 0000000000..1c140317e3
--- /dev/null
+++ b/examples/msg/mc/centralized_liveness.h
@@ -0,0 +1,13 @@
+#ifndef _CENTRALIZED_LIVENESS_H
+#define _CENTRALIZED_LIVENESS_H
+
+int yyparse(void);
+int yywrap(void);
+int yylex(void);
+
+int predCS2(void);
+
+int coordinator(int argc, char *argv[]);
+int client(int argc, char *argv[]);
+
+#endif 
diff --git a/examples/msg/mc/deploy_mutex2.xml b/examples/msg/mc/deploy_bugged1_liveness.xml
similarity index 100%
rename from examples/msg/mc/deploy_mutex2.xml
rename to examples/msg/mc/deploy_bugged1_liveness.xml
diff --git a/examples/msg/mc/deploy_bugged2_liveness.xml b/examples/msg/mc/deploy_bugged2_liveness.xml
new file mode 100644
index 0000000000..f49fb1016a
--- /dev/null
+++ b/examples/msg/mc/deploy_bugged2_liveness.xml
@@ -0,0 +1,18 @@
+<?xml version='1.0'?>
+
+<!DOCTYPE platform SYSTEM "http://simgrid.gforge.inria.fr/simgrid.dtd">
+
+<platform version="3">
+
+  <process host="Tremblay" function="coordinator" />
+
+  <process host="Fafard" function="consumer" >
+    <argument value="1"/>
+  </process>
+
+  <process host="Boivin" function="producer" >
+    <argument value="2"/>
+  </process>
+
+
+</platform>
diff --git a/examples/msg/mc/deploy_centralized_liveness.xml b/examples/msg/mc/deploy_centralized_liveness.xml
new file mode 100644
index 0000000000..bd46ad782e
--- /dev/null
+++ b/examples/msg/mc/deploy_centralized_liveness.xml
@@ -0,0 +1,47 @@
+<?xml version='1.0'?>
+
+<!DOCTYPE platform SYSTEM "http://simgrid.gforge.inria.fr/simgrid.dtd">
+
+<platform version="3">
+
+  <process host="Tremblay" function="coordinator" />
+
+  <process host="Fafard" function="client" >
+    <argument value="1"/>
+  </process>
+
+  <process host="Boivin" function="client" >
+    <argument value="2"/>
+  </process>
+
+  <!-- <process host="TeX" function="client" >
+    <argument value="3"/>
+  </process>
+
+  <process host="Geoff" function="client" >
+    <argument value="4"/>
+  </process>
+  
+  <process host="Disney" function="client" />
+    
+  <process host="iRMX" function="client" />
+      
+  <process host="McGee" function="client" />
+
+  <process host="Gatien" function="client" />
+    
+  <process host="Laroche" function="client" />
+      
+  <process host="Tanguay" function="client" />
+
+  <process host="Morin" function="client" />
+
+  <process host="Ethernet" function="client" />
+
+  <process host="Bellemarre" function="client" />
+
+  <process host="Kuenning" function="client" />
+  
+  <process host="Gaston" function="client" /> -->
+
+</platform>
diff --git a/examples/msg/mc/example_liveness_with_cycle2.c b/examples/msg/mc/example_liveness_with_cycle2.c
deleted file mode 100644
index 148afb47e4..0000000000
--- a/examples/msg/mc/example_liveness_with_cycle2.c
+++ /dev/null
@@ -1,140 +0,0 @@
-/***************** Centralized Mutual Exclusion Algorithm *********************/
-/* This example implements a centralized mutual exclusion algorithm.          */
-/* CS requests of client 2 not satisfied                                      */
-/******************************************************************************/
-
-#include "msg/msg.h"
-#include "mc/mc.h"
-#include "xbt/automaton.h"
-#include "xbt/automatonparse_promela.h"
-#include "example_liveness_with_cycle.h"
-#include "y.tab.c"
-
-#define AMOUNT_OF_CLIENTS 2
-#define CS_PER_PROCESS 3
-
-XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle2, "my log messages");
-
-
-int p=0; 
-int q=0;
-
-int predP(){
-  return p;
-}
-
-int predQ(){
-  return q;
-}
-
-
-int coordinator(int argc, char *argv[])
-{
-  xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);   // dynamic vector storing requests (which are char*)
-  int CS_used = 0;              // initially the CS is idle
-
-  while(1){
-    m_task_t task = NULL;
-    MSG_task_receive(&task, "coordinator");
-    const char *kind = MSG_task_get_name(task); //is it a request or a release?
-    if (!strcmp(kind, "request")) {     // that's a request
-      char *req = MSG_task_get_data(task);
-      if (CS_used) {            // need to push the request in the vector
-        XBT_INFO("CS already used. Queue the request of client %d", atoi(req) +1);
-        xbt_dynar_push(requests, &req);
-      } else {                  // can serve it immediatly
-	if(strcmp(req, "1") == 0){
-	  m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
-	  MSG_task_send(answer, req);
-	  CS_used = 1;
-	  XBT_INFO("CS idle. Grant immediatly");
-	}
-      }
-    } else {                    // that's a release. Check if someone was waiting for the lock
-      if (xbt_dynar_length(requests) > 0) {
-        XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
-        char *req ;
-	xbt_dynar_get_cpy(requests, (xbt_dynar_length(requests) - 1), &req);
-	if(strcmp(req, "1") == 0){
-	  xbt_dynar_pop(requests, &req);
-	  MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
-	}else{
-	  CS_used = 0;
-	}
-      } else {                  // nobody wants it
-        XBT_INFO("CS release. resource now idle");
-        CS_used = 0;
-      }
-    }
-    MSG_task_destroy(task);
-  }
-  XBT_INFO("Received all releases, quit now"); 
-  return 0;
-}
-
-int client(int argc, char *argv[])
-{
-  int my_pid = MSG_process_get_PID(MSG_process_self());
-
-  char *my_mailbox = bprintf("%s", argv[1]);
- 
-  while(1){  
-
-    XBT_INFO("Ask the request");
-   
-    MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
-    
-    if(strcmp(my_mailbox, "2") == 0){
-      p = 1;
-      q = 0;
-      XBT_INFO("Propositions changed (p=1, q=0)");
-    }
-
-    // wait the answer
-
-    m_task_t grant = NULL;
-    MSG_task_receive(&grant, my_mailbox);
-
-    if((strcmp(my_mailbox, "2") == 0) && (strcmp(MSG_task_get_name(grant), "grant") == 0)){
-      q = 1;
-      p = 0;
-      XBT_INFO("Propositions changed (q=1, p=0)");
-    }
-
-    MSG_task_destroy(grant);
-    XBT_INFO("%s got the answer. Sleep a bit and release it", argv[1]);
-    MSG_process_sleep(1);
-    
-    MSG_task_send(MSG_task_create("release", 0, 1000, NULL), "coordinator");
-
-    MSG_process_sleep(my_pid);
-    
-    if(strcmp(my_mailbox, "2") == 0){
-      q=0;
-      p=0;
-      XBT_INFO("Propositions changed (q=0, p=0)");
-    }
-    
-  }
-
-  XBT_INFO("Got all the CS I wanted (%s), quit now", my_mailbox);
-  return 0;
-}
-
-int main(int argc, char *argv[])
-{
-  init();
-  yyparse();
-  automaton = get_automaton();
-  xbt_new_propositional_symbol(automaton,"p", &predP); 
-  xbt_new_propositional_symbol(automaton,"q", &predQ); 
-  
-  MSG_global_init(&argc, argv);
-  MSG_create_environment("../msg_platform.xml");
-  MSG_function_register("coordinator", coordinator);
-  MSG_function_register("client", client);
-  MSG_launch_application("deploy_mutex2.xml");
-  MSG_main_liveness(automaton, argv[0]);
-  
-  return 0;
-}
diff --git a/examples/msg/mc/promela1_bugged1_liveness b/examples/msg/mc/promela1_bugged1_liveness
new file mode 100644
index 0000000000..96b491d6af
--- /dev/null
+++ b/examples/msg/mc/promela1_bugged1_liveness
@@ -0,0 +1,11 @@
+never { /* !G(r->Fcs) */
+T0_init :    /* init */
+	if
+	:: (1) -> goto T0_init
+	:: (!cs && r) -> goto accept_S2
+	fi;
+accept_S2 :    /* 1 */
+	if
+	:: (!cs) -> goto accept_S2
+	fi;
+}
diff --git a/examples/msg/mc/promela2_bugged1_liveness b/examples/msg/mc/promela2_bugged1_liveness
new file mode 100644
index 0000000000..febfac5aab
--- /dev/null
+++ b/examples/msg/mc/promela2_bugged1_liveness
@@ -0,0 +1,11 @@
+never { /* !(G((!cs) -> F(cs))) */
+T0_init :    /* init */
+	if
+	:: (1) -> goto T0_init
+	:: (!cs) -> goto accept_S2
+	fi;
+accept_S2 :    /* 1 */
+	if
+	:: (!cs) -> goto accept_S2
+	fi;
+}
diff --git a/examples/msg/mc/promela2_bugged2_liveness b/examples/msg/mc/promela2_bugged2_liveness
new file mode 100644
index 0000000000..1b4359d9f6
--- /dev/null
+++ b/examples/msg/mc/promela2_bugged2_liveness
@@ -0,0 +1,17 @@
+never { /* !(G((pready U produce) -> F(cready U consume))) */
+T1_init :    /* init */
+	if
+	:: (1) -> goto T1_init
+	:: (pready && !consume) -> goto T0_S2
+	:: (produce && !consume) -> goto accept_S3
+	fi;
+T0_S2 :    /* 1 */
+	if
+	:: (pready && !consume) -> goto T0_S2
+	:: (produce && !consume) -> goto accept_S3
+	fi;
+accept_S3 :    /* 2 */
+	if
+	:: (!consume) -> goto accept_S3
+	fi;
+}
diff --git a/examples/msg/mc/promela_bugged2_liveness b/examples/msg/mc/promela_bugged2_liveness
new file mode 100644
index 0000000000..5d5edc9ddc
--- /dev/null
+++ b/examples/msg/mc/promela_bugged2_liveness
@@ -0,0 +1,23 @@
+never { /* !(GF((pready U produce) -> (cready U consume))) */
+T0_init :    /* init */
+	if
+	:: (1) -> goto T1_S1
+	:: (produce && !consume) -> goto accept_S5
+	:: (pready && !consume) -> goto T0_S5
+	fi;
+T1_S1 :    /* 1 */
+	if
+	:: (1) -> goto T1_S1
+	:: (produce && !consume) || (pready && !consume) -> goto accept_S5
+	fi;
+accept_S5 :    /* 2 */
+	if
+	:: (pready && !consume) -> goto T0_S5
+	:: (produce && !consume) -> goto accept_S5
+	fi;
+T0_S5 :    /* 3 */
+	if
+	:: (pready && !consume) -> goto T0_S5
+	:: (produce && !consume) -> goto accept_S5
+	fi;
+}
\ No newline at end of file
diff --git a/examples/msg/mc/automaton2_PROMELA b/examples/msg/mc/promela_centralized_liveness
similarity index 51%
rename from examples/msg/mc/automaton2_PROMELA
rename to examples/msg/mc/promela_centralized_liveness
index ba1afdadf2..c5169d114f 100644
--- a/examples/msg/mc/automaton2_PROMELA
+++ b/examples/msg/mc/promela_centralized_liveness
@@ -1,11 +1,11 @@
-never { /* !G(p->Fq) */
+never { /* !(GFcs2) */
 T0_init :    /* init */
 	if
 	:: (1) -> goto T0_init
-	:: (!q && p) -> goto accept_S2
+	:: (!cs2) -> goto accept_S2
 	fi;
 accept_S2 :    /* 1 */
 	if
-	:: (!q) -> goto accept_S2
+	:: (!cs2) -> goto accept_S2
 	fi;
 }
\ No newline at end of file
diff --git a/include/mc/modelchecker.h b/include/mc/modelchecker.h
index 50b887f08b..43870f023a 100644
--- a/include/mc/modelchecker.h
+++ b/include/mc/modelchecker.h
@@ -2,6 +2,4 @@
 
 XBT_PUBLIC(void) MC_assert(int);
 XBT_PUBLIC(void) MC_assert_stateful(int);
-XBT_PUBLIC(void) MC_assert_pair_stateful(int);
-XBT_PUBLIC(void) MC_assert_pair_stateless(int);
 XBT_PUBLIC(int) MC_random(int min, int max);
diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 8eda522cc8..2e9fc0f767 100644
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -28,19 +28,13 @@ 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, 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);
 XBT_PUBLIC(void) MC_assert(int);
 XBT_PUBLIC(void) MC_assert_stateful(int);
-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(xbt_automaton_t a, char *prgm);
-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);
 XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 89ac9b98e0..a1953a4c6d 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -34,6 +34,10 @@ mc_snapshot_t initial_snapshot_liveness = NULL;
 xbt_automaton_t automaton;
 char *prog_name;
 
+static void MC_init_liveness(xbt_automaton_t a, char *prgm);
+static void MC_assert_pair(int prop);
+
+
 /**
  *  \brief Initialize the model-checker data structures
  */
diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 3c093ad07f..01d0124b81 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -30,80 +30,139 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
   
   if(s1->num_reg != s2->num_reg){
-    //XBT_DEBUG("Different num_reg (s1 = %d, s2 = %d)", s1->num_reg, s2->num_reg);
+    XBT_DEBUG("Different num_reg (s1 = %d, s2 = %d)", s1->num_reg, s2->num_reg);
     return 1;
   }
 
   int i;
+  int errors = 0;
 
   for(i=0 ; i< s1->num_reg ; i++){
 
     if(s1->regions[i]->type != s2->regions[i]->type){
-      //XBT_DEBUG("Different type of region");
-      return 1;
+      if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+	XBT_DEBUG("Different type of region");
+	errors++;
+      }else{
+	return 1;
+      }
     }
 
     switch(s1->regions[i]->type){
     case 0:
       if(s1->regions[i]->size != s2->regions[i]->size){
-	//XBT_DEBUG("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
-	return 1;
+	if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+	  XBT_DEBUG("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
+	  errors++;
+	}else{
+	  return 1;
+	}
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
-	//XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
-	return 1;
+	if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+	  XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+	  errors++;
+	}else{
+	  return 1;
+	}
       }
       if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){
-	//XBT_DEBUG("Different heap (mmalloc_compare)");
-	return 1; 
+	if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+	  XBT_DEBUG("Different heap (mmalloc_compare)");
+	  errors++; 
+	}else{
+	  return 1;
+	}
       }
       break;
     case 1 :
       if(s1->regions[i]->size != s2->regions[i]->size){
-	//XBT_DEBUG("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
-	return 1;
+	if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+	  XBT_DEBUG("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
+	  errors++;
+	}else{
+	  return 1;
+	}
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
-	//XBT_DEBUG("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
-	return 1;
+	if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+	  XBT_DEBUG("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+ 	  errors++;
+	}else{
+	  return 1;
+	}
       }
       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
-    	//XBT_DEBUG("Different memcmp for data in libsimgrid");
-    	return 1;
+	if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+	  XBT_DEBUG("Different memcmp for data in libsimgrid");
+ 	  errors++;
+	}else{
+	  return 1;
+	}
       }
       break;
-    case 2:
+      /*case 2:
       if(s1->regions[i]->size != s2->regions[i]->size){
-	//XBT_DEBUG("Different size of program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
-	return 1;
-      }
+	if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+	  XBT_DEBUG("Different size of program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
+	  errors++;
+	}else{
+	  return 1;
+	}
+      } 
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
-	//XBT_DEBUG("Different start addr of program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
-	return 1;
+	if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+	  XBT_DEBUG("Different start addr of program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+	  errors++;
+	}else{
+	  return 1;
+	}
       }
       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
-    	//XBT_DEBUG("Different memcmp for data in program");
-    	return 1;
+	if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+	  XBT_DEBUG("Different memcmp for data in program");
+	  errors++;
+	}else{
+	  return 1;
+	}
       }
-      break;
+      break;*/
     case 3:
       if(s1->regions[i]->size != s2->regions[i]->size){
-	//XBT_DEBUG("Different size of stack (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
-	return 1;
+	if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+	  XBT_DEBUG("Different size of stack (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
+	  errors++;
+	}else{
+	  return 1;
+	}
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
-	//XBT_DEBUG("Different start addr of stack (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
-	return 1;
+	if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+	  XBT_DEBUG("Different start addr of stack (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+	  errors++;
+	}else{
+	  return 1;
+	}
       }
       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
-    	//XBT_DEBUG("Different memcmp for data in stack");
-    	return 1;
+	if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+	  XBT_DEBUG("Different memcmp for data in stack");
+	  errors++;
+	}else{
+	  return 1;
+	}
       }
       break;
+    default:
+      break;
     }
   }
 
-  return 0;
+  if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+    return (errors>0);
+  }else{
+    return 0;
+  }
   
 }
 
@@ -141,6 +200,7 @@ int reached(xbt_state_t st){
     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 	if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+	  XBT_DEBUG("Pair reached %d", cursor+1);
 	  if(snapshot_compare(pair_test->system_state, sn) == 0){
 	    MC_free_snapshot(sn);
 	    xbt_dynar_reset(prop_ato);
@@ -602,8 +662,8 @@ void MC_ddfs_init(void){
     }
   }
 
-  //reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
-  reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
+  reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
+  //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
   //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
   visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
@@ -640,8 +700,8 @@ void MC_ddfs_init(void){
 	xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 	MC_UNSET_RAW_MEM;
 
-	//set_pair_reached(state);
-	set_pair_reached_hash(state);
+	set_pair_reached(state);
+	//set_pair_reached_hash(state);
 
 	if(cursor != 0){
 	  MC_restore_snapshot(initial_snapshot_liveness);
@@ -678,7 +738,7 @@ void MC_ddfs(int search_cycle){
  
   mc_stats_pair->visited_pairs++;
 
-  //sleep(1);
+  sleep(1);
 
   int value;
   mc_state_t next_graph_state = NULL;
@@ -774,8 +834,8 @@ void MC_ddfs(int search_cycle){
 
 	    if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
 		      
-	      //if(reached(pair_succ->automaton_state)){
-	      if(reached_hash(pair_succ->automaton_state)){
+	      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) + 1, MC_state_interleave_size(pair_succ->graph_state));
 
@@ -792,11 +852,11 @@ void MC_ddfs(int search_cycle){
 
 		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);
+		set_pair_reached(pair_succ->automaton_state);
+		//set_pair_reached_hash(pair_succ->automaton_state);
 
-		//XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-		XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+		XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+		//XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 
 		MC_SET_RAW_MEM;
 		xbt_fifo_unshift(mc_stack_liveness, pair_succ);
@@ -831,13 +891,13 @@ void MC_ddfs(int search_cycle){
 
 	      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);
+	      set_pair_reached(pair_succ->automaton_state); 
+	      //set_pair_reached_hash(pair_succ->automaton_state);
 
 	      search_cycle = 1;
 
-	      //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-	      XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+	      XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+	      //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 
 	    }
 
@@ -922,8 +982,8 @@ void MC_ddfs(int search_cycle){
 
 	  if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
 
-	    //if(reached(pair_succ->automaton_state)){
-	    if(reached_hash(pair_succ->automaton_state)){
+	    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) + 1);
 
@@ -940,11 +1000,11 @@ void MC_ddfs(int search_cycle){
 
 	      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);
+	      set_pair_reached(pair_succ->automaton_state);
+	      //set_pair_reached_hash(pair_succ->automaton_state);
 		
-	      //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-	      XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+	      XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+	      //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 
 	      MC_SET_RAW_MEM;
 	      xbt_fifo_unshift(mc_stack_liveness, pair_succ);
@@ -977,18 +1037,18 @@ void MC_ddfs(int search_cycle){
 	    
 	  if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
-	    //set_pair_reached(pair_succ->automaton_state);
-	    set_pair_reached_hash(pair_succ->automaton_state);
+	    set_pair_reached(pair_succ->automaton_state);
+	    //set_pair_reached_hash(pair_succ->automaton_state);
 	    	    
 	    search_cycle = 1;
 
-	    //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-	    XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+	    XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+	    //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 
 	  }
 
-	  //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
-	  if(!visited(pair_succ->automaton_state, search_cycle)){
+	  if(!visited_hash(pair_succ->automaton_state, search_cycle)){
+	    //if(!visited(pair_succ->automaton_state, search_cycle)){
 
 	    MC_SET_RAW_MEM;
 	    xbt_fifo_unshift(mc_stack_liveness, pair_succ);
@@ -1029,8 +1089,8 @@ void MC_ddfs(int search_cycle){
   MC_SET_RAW_MEM;
   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);
+    xbt_dynar_pop(reached_pairs, NULL);
+    //xbt_dynar_pop(reached_pairs_hash, NULL);
   }
   MC_UNSET_RAW_MEM;