model-checker : warning message if max depth is reached

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 5587e6a..1238dfe 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -31,6 +31,13 @@ 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)){
@@ -109,6 +116,12 @@ void MC_dpor(void)
       MC_SET_RAW_MEM;
 
       next_state = MC_state_new();
+
+      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){
@@ -134,7 +147,20 @@ void MC_dpor(void)
 
       /* The interleave set is empty or the maximum depth is reached, let's back-track */
     } else {
-      XBT_DEBUG("There are no more processes to interleave.");
+
+      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{
+
+        XBT_DEBUG("There are no more processes to interleave.");
+
+      }
 
       /* Trash the current state, no longer needed */
       MC_SET_RAW_MEM;

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index fa20959..2401f8f 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -644,7 +644,6 @@ void MC_ddfs(int search_cycle){
         next_graph_state = MC_state_pair_new();
 
         /* Get enabled process and insert it in the interleave set of the next graph_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); 
@@ -916,8 +915,12 @@ void MC_ddfs(int search_cycle){
     
   }else{
     
-    XBT_DEBUG("Max depth reached");
-
+    XBT_WARN("/!\\ Max depth reached ! /!\\ ");
+    if(current_pair->requests > 0){
+      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.");
+    }
+    
   }
 
   if(xbt_fifo_size(mc_stack_liveness) == _surf_mc_max_depth ){