X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/adcfb1a36dc3a193da6b595829fef2d7f4c9a4dd..d8710e879515b185393e2fa3a53d7377853cd25c:/src/mc/mc_safety.c

diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c
index 83460ff5da..38e0999740 100644
--- a/src/mc/mc_safety.c
+++ b/src/mc/mc_safety.c
@@ -15,6 +15,20 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
                                 "Logging specific to MC safety verification ");
 
+static int is_exploration_stack_state(mc_state_t current_state){
+
+  xbt_fifo_item_t item;
+  mc_state_t stack_state;
+  for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) {
+    stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
+    if(snapshot_compare(stack_state, current_state) == 0){
+      XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
+      return 1;
+    }
+  }
+  return 0;
+}
+
 /**
  *  \brief Initialize the DPOR exploration algorithm
  */
@@ -118,6 +132,11 @@ void MC_modelcheck_safety(void)
 
       next_state = MC_state_new();
 
+      if(_sg_mc_termination && is_exploration_stack_state(next_state)){
+          MC_show_non_termination();
+          return;
+      }
+
       if ((visited_state = is_visited_state(next_state)) == NULL) {
 
         /* Get an enabled process and insert it in the interleave set of the next state */