model checker : dfs algorithm corrected

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

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 8c3f171..508ef28 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -54,24 +54,27 @@ void MC_init(void)
 }
 
 void MC_init_with_automaton(xbt_automaton_t a){
+
+  XBT_DEBUG("Start init mc");
   
   mc_time = xbt_new0(double, simix_process_maxpid);
 
   /* Initialize the data structures that must be persistent across every
      iteration of the model-checker (in RAW memory) */
+
   MC_SET_RAW_MEM;
 
   /* Initialize statistics */
   mc_stats = xbt_new0(s_mc_stats_t, 1);
   mc_stats->state_size = 1;
 
+  XBT_DEBUG("Creating snapshot_stack");
+
  /* Create exploration stack */
   mc_snapshot_stack = xbt_fifo_new();
 
   MC_UNSET_RAW_MEM;
 
-  XBT_DEBUG("---------- Avant dfs init -----------");
-
   MC_dfs_init(a);
 }
 
@@ -265,6 +268,19 @@ void MC_assert(int prop)
   }
 }
 
+void MC_assert_pair(int prop){
+  if (MC_IS_ENABLED && !prop) {
+    XBT_INFO("**************************");
+    XBT_INFO("*** PROPERTY NOT VALID ***");
+    XBT_INFO("**************************");
+    //XBT_INFO("Counter-example execution trace:");
+    //MC_show_snapshot_stack(mc_snapshot_stack);
+    //MC_dump_snapshot_stack(mc_snapshot_stack);
+    //MC_print_statistics(mc_stats);
+    xbt_abort();
+  }
+}
+
 void MC_process_clock_add(smx_process_t process, double amount)
 {
   mc_time[process->pid] += amount;