From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Mon, 25 Mar 2013 21:36:36 +0000 (+0100)
Subject: model-checker : if acceptance cycle is detected, get num of equal pairs
X-Git-Tag: v3_9_90~412^2~93
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/c12f31e0bf110c61b506ef20c1d4de6b2cd2db87?hp=d2bf506bf4ebad03e01464d88a0635165ca8a4ed

model-checker : if acceptance cycle is detected, get num of equal pairs
---

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            |");