X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/eaecea92dde01d850f6da36ec4cdfe86992a0f68..7ef55d47978f2f2ef20bd27c85881faa99147034:/src/mc/mc_liveness.c

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index d0303b5cdf..54f5143d8b 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -36,6 +36,10 @@ static xbt_dynar_t get_atomic_propositions_values(){
   return values;
 }
 
+/** \brief Find a suitable subrange of candidate duplicates for a given state
+ *
+ *  See mc_dpor.c with a similar (same?) function.
+ */
 static int get_search_interval(xbt_dynar_t all_pairs, mc_visited_pair_t pair, int *min, int *max){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@ -114,12 +118,15 @@ static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_
     index = get_search_interval(acceptance_pairs, pair, &min, &max);
 
     if(min != -1 && max != -1){ // Acceptance pair with same number of processes and same heap bytes used exists
+
+      // Parallell implementation
       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair);
       if(res != -1){
         if(!raw_mem_set)
           MC_UNSET_RAW_MEM;
         return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
         }*/
+
       cursor = min;
       while(cursor <= max){
         pair_test = (mc_visited_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_visited_pair_t);
@@ -167,8 +174,6 @@ static void remove_acceptance_pair(int pair_num){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
-  fprintf(stderr, "Search acceptance pair %d\n", pair_num);
-
   MC_SET_RAW_MEM;
 
   unsigned int cursor = 0;
@@ -194,6 +199,9 @@ static void remove_acceptance_pair(int pair_num){
     MC_UNSET_RAW_MEM;
 }
 
+/** \brief Checks whether a given state has already been visited by the algorithm.
+ *
+ */
 static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
 
   if(_sg_mc_visited == 0)
@@ -266,7 +274,7 @@ static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_s
                 if(dot_output == NULL)
                   XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
                 else
-                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_pair->num, pair_test->num, pair->other_num);
+                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_pair->num, pair_test->num, new_pair->other_num);
                 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
                 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
                 pair_test->visited_removed = 1;
@@ -465,8 +473,8 @@ void MC_ddfs(){
 
   mc_pair_t next_pair = NULL;
   xbt_dynar_t prop_values = NULL;
-  int new_pair = 0;
   mc_visited_pair_t reached_pair = NULL;
+  int counter_example_depth = 0;
   
   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 
@@ -477,6 +485,7 @@ void MC_ddfs(){
         if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){ 
           if((reached_pair = is_reached_acceptance_pair(current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) == NULL){
 
+            counter_example_depth = xbt_fifo_size(mc_stack_liveness);
             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
             XBT_INFO("|             ACCEPTANCE CYCLE            |");
             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
@@ -484,6 +493,7 @@ void MC_ddfs(){
             MC_show_stack_liveness(mc_stack_liveness);
             MC_dump_stack_liveness(mc_stack_liveness);
             MC_print_statistics(mc_stats);
+            XBT_INFO("Counter-example depth : %d", counter_example_depth);
             xbt_abort();
 
           }
@@ -538,6 +548,8 @@ void MC_ddfs(){
           MC_SET_RAW_MEM;
           prop_values = get_atomic_propositions_values();
           MC_UNSET_RAW_MEM;
+
+          int new_pair = 0;
          
           /* Evaluate enabled transition according to atomic propositions values */
           cursor= 0;