model-checker : non-progressive cycle detection (enabled with --cfg=model-check/termi...

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

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 5b867af..59425b3 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -173,7 +173,7 @@ void MC_init()
 
   MC_SET_STD_HEAP;
 
-  if (_sg_mc_visited > 0 || _sg_mc_liveness) {
+  if (_sg_mc_visited > 0 || _sg_mc_liveness  || _sg_mc_termination) {
     /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
     MC_ignore_local_variable("e", "*");
     MC_ignore_local_variable("__ex_cleanup", "*");
@@ -333,7 +333,10 @@ void MC_do_the_modelcheck_for_real()
   } else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
     if (mc_reduce_kind == e_mc_reduce_unset)
       mc_reduce_kind = e_mc_reduce_dpor;
-    XBT_INFO("Check a safety property");
+    if(_sg_mc_termination)
+      XBT_INFO("Check non progressive cycles");
+    else
+      XBT_INFO("Check a safety property");
     MC_modelcheck_safety_init();
   } else {
     if (mc_reduce_kind == e_mc_reduce_unset)
@@ -454,14 +457,16 @@ void MC_replay(xbt_fifo_t stack)
   XBT_DEBUG("**** Begin Replay ****");
 
   /* Intermediate backtracking */
-  start_item = xbt_fifo_get_first_item(stack);
-  state = (mc_state_t)xbt_fifo_get_item_content(start_item);
-  if(state->system_state){
-    MC_restore_snapshot(state->system_state);
-    if(_sg_mc_comms_determinism || _sg_mc_send_determinism) 
-      MC_restore_communications_pattern(state);
-    MC_SET_STD_HEAP;
-    return;
+  if(_sg_mc_checkpoint > 0) {
+    start_item = xbt_fifo_get_first_item(stack);
+    state = (mc_state_t)xbt_fifo_get_item_content(start_item);
+    if(state->system_state){
+      MC_restore_snapshot(state->system_state);
+      if(_sg_mc_comms_determinism || _sg_mc_send_determinism) 
+        MC_restore_communications_pattern(state);
+      MC_SET_STD_HEAP;
+      return;
+    }
   }
 
 
@@ -552,12 +557,14 @@ void MC_replay_liveness(xbt_fifo_t stack)
   XBT_DEBUG("**** Begin Replay ****");
 
   /* Intermediate backtracking */
-  item = xbt_fifo_get_first_item(stack);
-  pair = (mc_pair_t) xbt_fifo_get_item_content(item);
-  if(pair->graph_state->system_state){
-    MC_restore_snapshot(pair->graph_state->system_state);
-    MC_SET_STD_HEAP;
-    return;
+  if(_sg_mc_checkpoint > 0) {
+    item = xbt_fifo_get_first_item(stack);
+    pair = (mc_pair_t) xbt_fifo_get_item_content(item);
+    if(pair->graph_state->system_state){
+      MC_restore_snapshot(pair->graph_state->system_state);
+      MC_SET_STD_HEAP;
+      return;
+    }
   }
 
   /* Restore the initial state */
@@ -686,6 +693,15 @@ void MC_show_deadlock(smx_simcall_t req)
   MC_print_statistics(mc_stats);
 }
 
+void MC_show_non_termination(void){
+  XBT_INFO("******************************************");
+  XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
+  XBT_INFO("******************************************");
+  XBT_INFO("Counter-example execution trace:");
+  MC_dump_stack_safety(mc_stack);
+  MC_print_statistics(mc_stats);
+}
+
 
 void MC_show_stack_liveness(xbt_fifo_t stack)
 {