model-checker : fix DPOR with visited states reduction

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 64a8837..14538c5 100644 (file)
--- 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;
   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) {
 
 
   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);
     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 &&
     /* 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)){
 
       /* 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);
       }
         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);
       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 {
 
       /* 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 ! /!\\ ");
 
           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)){
         /* 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){ 
             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;
                 }
                   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{
 
       }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()){
       
       /* 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){
       
       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))){
           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))){