model-checker : fix dpor algorithm if max depth reached

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

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 1d698bd..a54411d 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -14,7 +14,7 @@ static int is_visited_state(void);
 
 static int is_visited_state(){
 
-  if(_surf_mc_stateful == 0)
+  if(_surf_mc_visited == 0)
     return 0;
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@ -57,7 +57,7 @@ static int is_visited_state(){
       }   
     }
 
-    if(xbt_dynar_length(visited_states) == _surf_mc_stateful){
+    if(xbt_dynar_length(visited_states) == _surf_mc_visited){
       mc_snapshot_t state_to_remove = NULL;
       xbt_dynar_shift(visited_states, &state_to_remove);
       MC_free_snapshot(state_to_remove);
@@ -101,13 +101,7 @@ void MC_dpor_init()
   MC_wait_for_requests();
 
   MC_SET_RAW_MEM;
-
-  xbt_swag_foreach(process, simix_global->process_list){
-    if(MC_process_is_enabled(process)){
-      XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); 
-    }
-  }
-  
+ 
   /* Get an enabled process and insert it in the interleave set of the initial state */
   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){
@@ -125,10 +119,6 @@ void MC_dpor_init()
   else
     MC_UNSET_RAW_MEM;
   
-    
-  /* FIXME: Update Statistics 
-     mc_stats->state_size +=
-     xbt_setset_set_size(initial_state->enabled_transitions); */
 }
 
 
@@ -188,18 +178,13 @@ void MC_dpor(void)
       next_state = MC_state_new();
 
       if(!is_visited_state()){
-
-        xbt_swag_foreach(process, simix_global->process_list){
-          if(MC_process_is_enabled(process)){
-            XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); 
-          }
-        }
-        
+     
         /* Get an enabled process and insert it in the interleave set of the next state */
         xbt_swag_foreach(process, simix_global->process_list){
           if(MC_process_is_enabled(process)){
             MC_state_interleave_process(next_state, process);
-            break;
+            if((xbt_fifo_size(mc_stack_safety) + 1) != (_surf_mc_max_depth - 1))
+              break;
           }
         }
 
@@ -207,6 +192,10 @@ void MC_dpor(void)
           next_state->system_state = MC_take_snapshot();
         }
 
+      }else{
+
+        XBT_DEBUG("State already visited !");
+        
       }
 
       xbt_fifo_unshift(mc_stack_safety, next_state);
@@ -221,20 +210,11 @@ void MC_dpor(void)
       /* The interleave set is empty or the maximum depth is reached, let's back-track */
     } else {
 
-      if(xbt_fifo_size(mc_stack_safety) == _surf_mc_max_depth){
-        
+      if(xbt_fifo_size(mc_stack_safety) == _surf_mc_max_depth)  
         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
-        if(req != NULL){
-          XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ "); 
-          XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
-        }
-
-      }else{
-
+      else
         XBT_DEBUG("There are no more processes to interleave.");
 
-      }
-
       /* Trash the current state, no longer needed */
       MC_SET_RAW_MEM;
       xbt_fifo_shift(mc_stack_safety);
@@ -254,6 +234,7 @@ void MC_dpor(void)
          (from it's predecesor state), depends on any other previous request 
          executed before it. If it does then add it to the interleave set of the
          state that executed that previous request. */
+      
       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
         req = MC_state_get_internal_request(state);
         xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
@@ -276,8 +257,14 @@ void MC_dpor(void)
               XBT_DEBUG("Process %p is in done set", req->issuer);
 
             break;
+
+          }else if(req->issuer == MC_state_get_executed_request(prev_state, &value)->issuer){
+
+            break;
+
           }
         }
+
         if (MC_state_interleave_size(state)) {
           /* We found a back-tracking point, let's loop */
           if(_surf_mc_checkpoint){