model-checker : new primitive MC_max_depth, to define a maximum exploration depth...

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

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index ebb65ea..839ac05 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -248,7 +248,7 @@ void MC_dpor(void)
   xbt_fifo_item_t item = NULL;
   int pos;
   int visited_state;
-  int enabled = 0, max_depth_reached = 0;
+  int enabled = 0, max_depth_reached;
 
   while (xbt_fifo_size(mc_stack_safety) > 0) {
 
@@ -257,16 +257,16 @@ void MC_dpor(void)
       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 
     XBT_DEBUG("**************************************************");
-    XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave)",
+    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));
+              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 &&
+    if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
         (req = MC_state_get_request(state, &value))) {
 
       /* Debug information */
@@ -349,10 +349,13 @@ 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(xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth){  
-
-        XBT_WARN("/!\\ Max depth reached ! /!\\ ");
+        if(user_max_depth_reached)
+          XBT_WARN("User max depth reached !");
+        else
+          XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 
         /* Interleave enabled processes in the state in which they have been enabled for the first time */
         xbt_swag_foreach(process, simix_global->process_list){
@@ -395,8 +398,9 @@ void MC_dpor(void)
         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;
       }
       
@@ -416,9 +420,10 @@ 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){
+          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) {
@@ -427,11 +432,11 @@ void MC_dpor(void)
                 XBT_DEBUG("Dependent Transitions:");
                 prev_req = MC_state_get_executed_request(prev_state, &value);
                 req_str = MC_request_to_string(prev_req, value);
-                XBT_DEBUG("%s (state=%p)", req_str, prev_state);
+                XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
                 xbt_free(req_str);
                 prev_req = MC_state_get_executed_request(state, &value);
                 req_str = MC_request_to_string(prev_req, value);
-                XBT_DEBUG("%s (state=%p)", req_str, state);
+                XBT_DEBUG("%s (state=%d)", req_str, state->num);
                 xbt_free(req_str);              
               }
 
@@ -447,13 +452,17 @@ void MC_dpor(void)
               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
               break;
 
+            }else{
+
+              XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant", req->call, req->issuer->pid, state->num, MC_state_get_internal_request(prev_state)->call, MC_state_get_internal_request(prev_state)->issuer->pid, prev_state->num);
+
             }
           }
         }
              
         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
-          XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety) + 1);
+          XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
           if(_sg_mc_checkpoint){
             if(state->system_state != NULL){
               MC_restore_snapshot(state->system_state);
@@ -481,10 +490,10 @@ void MC_dpor(void)
             MC_UNSET_RAW_MEM;
             MC_replay(mc_stack_safety, -1);
           }
-          XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
+          XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety));
           break;
         } else {
-          XBT_DEBUG("Delete state at depth %d",xbt_fifo_size(mc_stack_safety) + 1); 
+          XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); 
           MC_state_delete(state);
         }
       }