From c12f31e0bf110c61b506ef20c1d4de6b2cd2db87 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Mon, 25 Mar 2013 22:36:36 +0100 Subject: [PATCH] model-checker : if acceptance cycle is detected, get num of equal pairs --- src/mc/mc_liveness.c | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 362e331a89..424929e3e7 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -605,6 +605,7 @@ void MC_ddfs(int search_cycle){ xbt_automaton_transition_t transition_succ; unsigned int cursor = 0; int res; + int reached_num; mc_pair_t next_pair = NULL; mc_pair_t pair_succ; @@ -694,9 +695,9 @@ void MC_ddfs(int search_cycle){ if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ - if(is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state) != -1){ + if((reached_num = is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state)) != -1){ - XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state)); + XBT_INFO("Next pair (depth = %d, %u interleave) already reached (equal to state %d) !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state), reached_num); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); @@ -845,9 +846,9 @@ void MC_ddfs(int search_cycle){ if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ - if(is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state) != -1){ + if((reached_num = is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state)) != -1){ - XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1); + XBT_INFO("Next pair (depth = %d) already reached (equal to state %d)!", xbt_fifo_size(mc_stack_liveness) + 1, reached_num); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); -- 2.20.1