From a0c5f40f68a69e5fd2c22643c98aed7570191e21 Mon Sep 17 00:00:00 2001
From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Wed, 11 Jul 2012 14:18:21 +0200
Subject: [PATCH] model-checker : application alert for state equality
 detection

---
 examples/msg/mc/bugged1_liveness.c | 1 +
 src/include/mc/mc.h                | 2 ++
 src/mc/mc_global.c                 | 7 +++++++
 src/mc/mc_liveness.c               | 4 +++-
 src/mc/mc_private.h                | 1 +
 5 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/examples/msg/mc/bugged1_liveness.c b/examples/msg/mc/bugged1_liveness.c
index 378ede355e..f8ac5c91fa 100644
--- a/examples/msg/mc/bugged1_liveness.c
+++ b/examples/msg/mc/bugged1_liveness.c
@@ -39,6 +39,7 @@ int coordinator(int argc, char *argv[])
       } else {               
         if(strcmp(req, "2") == 0){
           XBT_INFO("CS idle. Grant immediatly");
+          MC_compare();
           answer = MSG_task_create("grant", 0, 1000, NULL);
           MSG_task_send(answer, req);
           CS_used = 1;
diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 18442d1eb0..1fae467c8d 100644
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -44,6 +44,8 @@ XBT_PUBLIC(void) MC_memory_exit(void);
 /********************************* Snapshot comparison test *************************************/
 void MC_test_snapshot_comparison(void);
 
+void MC_compare(void);
+
 SG_END_DECL()
 
 #endif                          /* _MC_MC_H */
diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index ad54b842ad..461f6c0f20 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -71,6 +71,7 @@ mc_stats_t mc_stats = NULL;
 mc_stats_pair_t mc_stats_pair = NULL;
 xbt_fifo_t mc_stack_liveness = NULL;
 mc_snapshot_t initial_snapshot_liveness = NULL;
+int compare;
 
 xbt_automaton_t _mc_property_automaton = NULL;
 
@@ -139,6 +140,10 @@ void MC_init_safety(void)
   
 }
 
+void MC_compare(void){
+  compare = 1;
+}
+
 
 void MC_modelcheck(void)
 {
@@ -156,6 +161,8 @@ void MC_modelcheck_liveness(){
   
   mc_time = xbt_new0(double, simix_process_maxpid);
 
+  compare = 0;
+
   /* Initialize the data structures that must be persistent across every
      iteration of the model-checker (in RAW memory) */
 
diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index d3da48c1be..ef53fb71af 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -75,7 +75,7 @@ int reached(xbt_state_t st){
 
   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
-  if(xbt_dynar_is_empty(reached_pairs)){
+  if(xbt_dynar_is_empty(reached_pairs) || !compare){
 
     return 0;
 
@@ -137,6 +137,8 @@ int reached(xbt_state_t st){
       MC_SET_RAW_MEM;
     else
       MC_UNSET_RAW_MEM;
+
+    compare = 0;
     
     return 0;
     
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 1ef5c9666c..0de5a9e9f0 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -203,6 +203,7 @@ void MC_init_safety(void);
 
 extern mc_snapshot_t initial_snapshot_liveness;
 extern xbt_automaton_t _mc_property_automaton;
+extern int compare;
 
 typedef struct s_mc_pair{
   mc_snapshot_t system_state;
-- 
2.20.1