model-checker : backtracking if there is no request to execute

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index f1e5e3d..f875704 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -510,120 +510,6 @@ void MC_ddfs(int search_cycle){
       }
 
  
       }
 
  

-    }else{  /*No request to execute, search evolution in Büchi automaton */
-
-      MC_SET_RAW_MEM;
-
-      /* Create the new expanded graph_state */
-      next_graph_state = MC_state_pair_new();
-
-      xbt_dynar_reset(successors);
-
-      MC_UNSET_RAW_MEM;
-
-
-      cursor= 0;
-      xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
-
-        res = MC_automaton_evaluate_label(transition_succ->label);
-
-        if(res == 1){ // enabled transition in automaton
-          MC_SET_RAW_MEM;
-          next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
-          xbt_dynar_push(successors, &next_pair);
-          MC_UNSET_RAW_MEM;
-        }
-
-      }
-
-      cursor = 0;
-   
-      xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
-      
-        res = MC_automaton_evaluate_label(transition_succ->label);
-  
-        if(res == 2){ // true transition in automaton
-          MC_SET_RAW_MEM;
-          next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
-          xbt_dynar_push(successors, &next_pair);
-          MC_UNSET_RAW_MEM;
-        }
-
-      }
-
-      cursor = 0; 
-     
-      xbt_dynar_foreach(successors, cursor, pair_succ){
-
-        if(search_cycle == 1){
-
-          if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
-
-            if(reached(pair_succ->automaton_state)){
-           
-              XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
-        
-              XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-              XBT_INFO("|             ACCEPTANCE CYCLE            |");
-              XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-              XBT_INFO("Counter-example that violates formula :");
-              MC_show_stack_liveness(mc_stack_liveness);
-              MC_dump_stack_liveness(mc_stack_liveness);
-              MC_print_statistics_pairs(mc_stats_pair);
-              exit(0);
-
-            }else{
-
-              XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
-        
-              XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-
-              MC_SET_RAW_MEM;
-              xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-              MC_UNSET_RAW_MEM;
-        
-              MC_ddfs(search_cycle);
-
-            }
-
-          }else{
-
-            MC_SET_RAW_MEM;
-            xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-            MC_UNSET_RAW_MEM;
-            
-            MC_ddfs(search_cycle);
-            
-          }
-      
-
-        }else{
-      
-          if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
-
-            set_pair_reached(pair_succ->automaton_state);
-         
-            search_cycle = 1;
-
-            XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-
-          }
-
-          MC_SET_RAW_MEM;
-          xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-          MC_UNSET_RAW_MEM;
-          
-          MC_ddfs(search_cycle);
-          
-        }
-
-        /* Restore system before checking others successors */
-        if(cursor != xbt_dynar_length(successors) - 1)
-          MC_replay_liveness(mc_stack_liveness, 1);
-
-   
-      }
-           

     }
     
   }else{
     }
     
   }else{