From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Sat, 10 Aug 2013 10:28:48 +0000 (+0200)
Subject: model-checker : fix DPOR with visited states reduction
X-Git-Tag: v3_9_90~128^2~21
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/e3314a95b4f2e372c4876abb6ba3ff38ff76b4be?ds=sidebyside

model-checker : fix DPOR with visited states reduction
---

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 64a8837ab8..14538c5a50 100644
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -275,8 +275,8 @@ void MC_dpor(void)
   smx_process_t process = NULL;
   xbt_fifo_item_t item = NULL;
   int pos;
-  int visited_state;
-  int enabled = 0, max_depth_reached;
+  int visited_state = -1;
+  int enabled = 0;
 
   while (xbt_fifo_size(mc_stack_safety) > 0) {
 
@@ -288,14 +288,14 @@ void MC_dpor(void)
     XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
               xbt_fifo_size(mc_stack_safety), state, state->num,
               MC_state_interleave_size(state), user_max_depth_reached);
-
+      
     /* Update statistics */
     mc_stats->visited_states++;
 
     /* If there are processes to interleave and the maximum depth has not been reached
        then perform one step of the exploration algorithm */
     if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
-        (req = MC_state_get_request(state, &value))) {
+        (req = MC_state_get_request(state, &value)) && visited_state == -1) {
 
       /* Debug information */
       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
@@ -303,7 +303,7 @@ void MC_dpor(void)
         XBT_DEBUG("Execute: %s", req_str);
         xbt_free(req_str);
       }
-        
+      
       MC_SET_RAW_MEM;
       if(dot_output != NULL)
         req_str = MC_request_get_dot_output(req, value);
@@ -377,14 +377,16 @@ 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) > _sg_mc_max_depth) || user_max_depth_reached){  
 
-        if(user_max_depth_reached)
-          XBT_WARN("User max depth reached !");
-        else
+      if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){  
+
+        if(user_max_depth_reached && visited_state == -1)
+          XBT_DEBUG("User max depth reached !");
+        else if(visited_state == -1)
           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 
+        visited_state = -1;
+
         /* Interleave enabled processes in the state in which they have been enabled for the first time */
         xbt_swag_foreach(process, simix_global->process_list){
           if(MC_process_is_enabled(process)){
@@ -396,7 +398,8 @@ void MC_dpor(void)
             int cursor = xbt_fifo_size(mc_stack_safety);
             xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
               if(cursor-- == enabled){ 
-                if(!MC_state_process_is_done(state_test, process)){ 
+                if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){ 
+                  XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
                   MC_state_interleave_process(state_test, process);
                   break;
                 }
@@ -405,32 +408,18 @@ void MC_dpor(void)
           }
         }
 
-        if(MC_state_interleave_size(state) > 0){
-          max_depth_reached = 1;
-        }else{
-          /* Trash the current state, no longer needed */
-          MC_SET_RAW_MEM;
-          xbt_fifo_shift(mc_stack_safety);
-          MC_state_delete(state);
-          MC_UNSET_RAW_MEM;
-
-          max_depth_reached = 0;
-        }
-        
-
       }else{
 
-        XBT_DEBUG("There are no more processes to interleave.");
+        XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
 
-        /* Trash the current state, no longer needed */
-        MC_SET_RAW_MEM;
-        xbt_fifo_shift(mc_stack_safety);
-        MC_state_delete(state);
-        XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
-        MC_UNSET_RAW_MEM;
-        
-        max_depth_reached = 0;
       }
+
+      /* Trash the current state, no longer needed */
+      MC_SET_RAW_MEM;
+      xbt_fifo_shift(mc_stack_safety);
+      MC_state_delete(state);
+      XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
+      MC_UNSET_RAW_MEM;        
       
       /* Check for deadlocks */
       if(MC_deadlock_check()){
@@ -448,11 +437,6 @@ void MC_dpor(void)
       
       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
         if(mc_reduce_kind != e_mc_reduce_none){
-          if(((xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth) && max_depth_reached) || user_max_depth_reached){
-            req = MC_state_get_request(state, &value);
-            MC_state_set_executed_request(state, req, value);
-            user_max_depth_reached = 0;
-          }
           req = MC_state_get_internal_request(state);
           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){