From b8ef9510aee1b2c8a7da1cdd3a2f062b4ad3269a Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 12 Jan 2012 10:55:28 +0100 Subject: [PATCH] model-checker : add informations when log debug enabled --- src/mc/mc_liveness.c | 33 ++++++++++++++++++++++++++++++--- 1 file changed, 30 insertions(+), 3 deletions(-) diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 01d0124b81..c0aa52a2ce 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -207,8 +207,14 @@ int reached(xbt_state_t st){ xbt_free(prop_ato); MC_UNSET_RAW_MEM; return 1; + }else{ + XBT_DEBUG("Different snapshot"); } + }else{ + XBT_DEBUG("Different values of propositional symbols"); } + }else{ + XBT_DEBUG("Different automaton state"); } } @@ -306,11 +312,16 @@ int reached_hash(xbt_state_t st){ xbt_free(prop_ato); MC_UNSET_RAW_MEM; return 1; + }else{ + XBT_DEBUG("Different snapshot"); } + }else{ + XBT_DEBUG("Different values of propositional symbols"); } + }else{ + XBT_DEBUG("Different automaton state"); } - - + region_diff = 0; } @@ -407,9 +418,17 @@ int visited(xbt_state_t st, int sc){ return 1; + }else{ + XBT_DEBUG("Different snapshot"); } + }else{ + XBT_DEBUG("Different values of propositional symbols"); } + }else{ + XBT_DEBUG("Different automaton state"); } + }else{ + XBT_DEBUG("Different value of search_cycle"); } } @@ -479,11 +498,19 @@ int visited_hash(xbt_state_t st, int sc){ xbt_free(prop_ato); MC_UNSET_RAW_MEM; return 1; + }else{ + XBT_DEBUG("Different snapshot"); } + }else{ + XBT_DEBUG("Different values of propositional symbols"); } + }else{ + XBT_DEBUG("Different automaton state"); } + }else{ + XBT_DEBUG("Different value of search_cycle"); } - + region_diff = 0; } -- 2.30.2