From 139c5f52fbe9304c2c437876a332a4bce68358d3 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 14 Jun 2012 09:29:05 +0200 Subject: [PATCH] model-checker : move print statistics if property is valid --- src/mc/mc_dpor.c | 1 + src/mc/mc_global.c | 21 ++++++++------------- 2 files changed, 9 insertions(+), 13 deletions(-) diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index ebb68bdd94..ed50ac0f50 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -173,6 +173,7 @@ void MC_dpor(void) MC_UNSET_RAW_MEM; } } + MC_print_statistics(mc_stats); MC_UNSET_RAW_MEM; return; } diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index e9e5940b46..884933a22a 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -525,19 +525,14 @@ void MC_print_statistics_pairs(mc_stats_pair_t stats) void MC_assert(int prop) { - if (MC_IS_ENABLED ){ - if(!prop) { - XBT_INFO("**************************"); - XBT_INFO("*** PROPERTY NOT VALID ***"); - XBT_INFO("**************************"); - XBT_INFO("Counter-example execution trace:"); - MC_dump_stack_safety_stateless(mc_stack_safety_stateless); - MC_print_statistics(mc_stats); - xbt_abort(); - }else{ - MC_print_statistics(mc_stats); - xbt_abort(); - } + if (MC_IS_ENABLED && !prop){ + XBT_INFO("**************************"); + XBT_INFO("*** PROPERTY NOT VALID ***"); + XBT_INFO("**************************"); + XBT_INFO("Counter-example execution trace:"); + MC_dump_stack_safety_stateless(mc_stack_safety_stateless); + MC_print_statistics(mc_stats); + xbt_abort(); } } -- 2.20.1