model-checker : application alert for state equality detection

diff --git a/examples/msg/mc/bugged1_liveness.c b/examples/msg/mc/bugged1_liveness.c
index 378ede3..f8ac5c9 100644 (file)
--- 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");
       } 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;
           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 18442d1..1fae467 100644 (file)
--- 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);
 
 /********************************* Snapshot comparison test *************************************/
 void MC_test_snapshot_comparison(void);
 

+void MC_compare(void);
+

 SG_END_DECL()
 
 #endif                          /* _MC_MC_H */
 SG_END_DECL()
 
 #endif                          /* _MC_MC_H */

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index ad54b84..461f6c0 100644 (file)
--- 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;
 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;
 
 
 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)
 {
 
 void MC_modelcheck(void)
 {


@@ -156,6 +161,8 @@ void MC_modelcheck_liveness(){
   
   mc_time = xbt_new0(double, simix_process_maxpid);
 
   
   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) */
 
   /* 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 d3da48c..ef53fb7 100644 (file)
--- 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);
 
 
   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;
 
 
     return 0;
 


@@ -137,6 +137,8 @@ int reached(xbt_state_t st){
       MC_SET_RAW_MEM;
     else
       MC_UNSET_RAW_MEM;
       MC_SET_RAW_MEM;
     else
       MC_UNSET_RAW_MEM;

+
+    compare = 0;

     
     return 0;
     
     
     return 0;
     

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 1ef5c96..0de5a9e 100644 (file)
--- 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 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;
 
 typedef struct s_mc_pair{
   mc_snapshot_t system_state;