model-checker : minor fix in ddfs algorithm

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 27889ac..a360a24 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -637,7 +637,6 @@ void MC_ddfs(){
   unsigned int cursor = 0;
   int res;
   int reached_num, visited_num;
-  int new_pair = 0;
 
   mc_pair_t next_pair = NULL;
   xbt_dynar_t prop_values = NULL;
@@ -731,9 +730,6 @@ void MC_ddfs(){
 
             if(res == 1){ // enabled transition in automaton
 
-              if(new_pair)
-               MC_replay_liveness(mc_stack_liveness, 1); 
-
               MC_SET_RAW_MEM;
 
               next_pair = MC_pair_new();
@@ -760,8 +756,6 @@ void MC_ddfs(){
 
               MC_UNSET_RAW_MEM;
 
-              new_pair = 1;
-
               MC_ddfs();
 
             }
@@ -775,9 +769,6 @@ void MC_ddfs(){
             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
   
             if(res == 2){ // true transition in automaton
-
-              if(new_pair)
-                MC_replay_liveness(mc_stack_liveness, 1); 
             
               MC_SET_RAW_MEM;
             
@@ -805,8 +796,6 @@ void MC_ddfs(){
             
               MC_UNSET_RAW_MEM;
 
-              new_pair = 1;
-
               MC_ddfs();
 
             }
@@ -871,9 +860,6 @@ void MC_ddfs(){
 
           if(res == 1){ // enabled transition in automaton
 
-            if(new_pair)
-              MC_replay_liveness(mc_stack_liveness, 1);
-
             MC_SET_RAW_MEM;
 
             next_pair = MC_pair_new();
@@ -895,8 +881,6 @@ void MC_ddfs(){
 
             MC_UNSET_RAW_MEM;
 
-            new_pair = 1;
-
             MC_ddfs();
 
           }
@@ -911,9 +895,6 @@ void MC_ddfs(){
   
           if(res == 2){ // true transition in automaton
 
-            if(new_pair)
-              MC_replay_liveness(mc_stack_liveness, 1);
-
             MC_SET_RAW_MEM;
             
             next_pair = MC_pair_new();
@@ -935,8 +916,6 @@ void MC_ddfs(){
 
             MC_UNSET_RAW_MEM;
 
-            new_pair = 1;
-
             MC_ddfs();
 
           }
@@ -975,6 +954,7 @@ void MC_ddfs(){
     else if(current_pair->visited_removed)
       MC_pair_delete(current_pair);
   }
+
   MC_UNSET_RAW_MEM;
 
 }