model-checker : add state equality reduction in ddfs algorithm

[simgrid.git] / src / mc / mc_liveness.c

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 8067a73..06265cb 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -71,7 +71,7 @@ int reached(xbt_state_t st){
   xbt_propositional_symbol_t ps = NULL;
   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
-    res = (*f)();
+    res = f();
     xbt_dynar_push_as(new_pair->prop_ato, int, res);
   }
   
@@ -155,7 +155,7 @@ void set_pair_reached(xbt_state_t st){
 
   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
-    res = (*f)();
+    res = f();
     xbt_dynar_push_as(pair->prop_ato, int, res);
   }
 
@@ -190,7 +190,7 @@ int visited(xbt_state_t st){
   xbt_propositional_symbol_t ps = NULL;
   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
-    res = (*f)();
+    res = f();
     xbt_dynar_push_as(new_pair->prop_ato, int, res);
   }
   
@@ -285,7 +285,7 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
       if(strcmp(p->pred, l->u.predicat) == 0){
         f = (int_f_void_t)p->function;
-        return (*f)();
+        return f();
       }
     }
     return -1;
@@ -303,7 +303,6 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
 
 void pair_visited_free(mc_pair_visited_t pair){
   if(pair){
-    pair->automaton_state = NULL;
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);
     xbt_free(pair);
@@ -337,7 +336,6 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 
 void pair_reached_free(mc_pair_reached_t pair){
   if(pair){
-    pair->automaton_state = NULL;
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);
     xbt_free(pair);
@@ -476,9 +474,11 @@ void MC_ddfs(int search_cycle){
    
         /* Debug information */
        
-        req_str = MC_request_to_string(req, value);
-        XBT_DEBUG("Execute: %s", req_str);
-        xbt_free(req_str);
+        if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
+          req_str = MC_request_to_string(req, value);
+          XBT_DEBUG("Execute: %s", req_str);
+          xbt_free(req_str);
+        }
 
         MC_state_set_executed_request(current_pair->graph_state, req, value);   
 
@@ -712,46 +712,73 @@ void MC_ddfs(int search_cycle){
 
             }else{
 
-              XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
+              if(visited(pair_succ->automaton_state)){
+                
+                XBT_DEBUG("Next pair already visited !");
+                break;
+                
+              }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));
+                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_SET_RAW_MEM;
+                xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+                MC_UNSET_RAW_MEM;
         
-              MC_ddfs(search_cycle);
+                MC_ddfs(search_cycle);
+              
+              }
 
             }
 
           }else{
+            
+            if(visited(pair_succ->automaton_state)){
+              
+              XBT_DEBUG("Next pair already visited !");
+              break;
+              
+            }else{
 
-            MC_SET_RAW_MEM;
-            xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-            MC_UNSET_RAW_MEM;
+              MC_SET_RAW_MEM;
+              xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+              MC_UNSET_RAW_MEM;
             
-            MC_ddfs(search_cycle);
+              MC_ddfs(search_cycle);
+
+            }
             
           }
       
 
         }else{
       
-          if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
+          if(visited(pair_succ->automaton_state)){
+
+            XBT_DEBUG("Next pair already visited !");
+            break;
+            
+          }else{
 
-            set_pair_reached(pair_succ->automaton_state);
+            if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
+
+              set_pair_reached(pair_succ->automaton_state);
          
-            search_cycle = 1;
+              search_cycle = 1;
 
-            XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+              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_SET_RAW_MEM;
+            xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+            MC_UNSET_RAW_MEM;
           
-          MC_ddfs(search_cycle);
+            MC_ddfs(search_cycle);
+          
+          }
           
         }