X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/1ee68a7d44ca89e57734578a1aa91c11ddb27de1..6659e698628302ff3b8663fe612044375e092fe3:/src/mc/mc_liveness.cpp

diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index b7cc85de65..a1f786d1f0 100644
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2011-2014. The SimGrid Team.
+/* Copyright (c) 2011-2015. The SimGrid Team.
  * All rights reserved.                                                     */
 
 /* This program is free software; you can redistribute it and/or modify it
@@ -18,6 +18,7 @@
 #include "mc_client.h"
 #include "mc_replay.h"
 #include "mc_safety.h"
+#include "mc_exit.h"
 
 extern "C" {
 
@@ -170,8 +171,6 @@ static void MC_modelcheck_liveness_main(void);
 
 static void MC_pre_modelcheck_liveness(void)
 {
-  initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
   mc_pair_t initial_pair = NULL;
   smx_process_t process;
 
@@ -248,11 +247,12 @@ static void MC_modelcheck_liveness_main(void)
           XBT_INFO("|             ACCEPTANCE CYCLE            |");
           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
           XBT_INFO("Counter-example that violates formula :");
+          MC_record_dump_path(mc_stack);
           MC_show_stack_liveness(mc_stack);
           MC_dump_stack_liveness(mc_stack);
           MC_print_statistics(mc_stats);
           XBT_INFO("Counter-example depth : %d", counter_example_depth);
-          xbt_abort();
+          exit(SIMGRID_EXIT_LIVENESS);
         }
       }
 
@@ -394,6 +394,7 @@ void MC_modelcheck_liveness(void)
   MC_pre_modelcheck_liveness();
 
   /* We're done */
+  XBT_INFO("No property violation found.");
   MC_print_statistics(mc_stats);
   xbt_free(mc_time);
 }