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

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index 18535fd..9f260a3 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -23,6 +23,7 @@ XBT_PUBLIC(int) MC_random(void);
 XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, void* fct);
 XBT_PUBLIC(void *) MC_snapshot(void);
 XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2);
+XBT_PUBLIC(void) MC_max_depth(int);
 
 #else
 

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 08990a5..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){
@@ -417,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) {

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index ab6b9bc..a2aa358 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -32,6 +32,8 @@ int _sg_mc_max_depth=1000;
 int _sg_mc_visited=0;
 char *_sg_mc_dot_output_file = NULL;
 
+int user_max_depth_reached = 0;
+
 extern int _sg_init_status;
 void _mc_cfg_cb_reduce(const char *name, int pos) {
   if (_sg_init_status && !_sg_do_model_check) {

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index f5bd47d..a0bb49a 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -69,6 +69,8 @@ extern double *mc_time;
 extern FILE *dot_output;
 extern const char* colors[13];
 
+extern int user_max_depth_reached;
+
 int MC_deadlock_check(void);
 void MC_replay(xbt_fifo_t stack, int start);
 void MC_replay_liveness(xbt_fifo_t stack, int all_stack);