src/mc/mc_liveness.c

   1 /* Copyright (c) 2011-2013. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include "mc_private.h"
   8 #include <unistd.h>
   9 #include <sys/wait.h>
  10
  11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
  12                                 "Logging specific to algorithms for liveness properties verification");
  13
  14 /********* Global variables *********/
  15
  16 xbt_dynar_t acceptance_pairs;
  17 xbt_dynar_t visited_pairs;
  18 xbt_dynar_t successors;
  19 xbt_parmap_t parmap;
  20
  21 /********* Static functions *********/
  22
  23 static xbt_dynar_t get_atomic_propositions_values(){
  24   int res;
  25   int_f_void_t f;
  26   unsigned int cursor = 0;
  27   xbt_automaton_propositional_symbol_t ps = NULL;
  28   xbt_dynar_t values = xbt_dynar_new(sizeof(int), NULL);
  29
  30   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
  31     f = (int_f_void_t)ps->function;
  32     res = f();
  33     xbt_dynar_push_as(values, int, res);
  34   }
  35
  36   return values;
  37 }
  38
  39 static int get_search_interval(xbt_dynar_t all_pairs, mc_visited_pair_t pair, int *min, int *max){
  40
  41   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  42
  43   MC_SET_RAW_MEM;
  44
  45   int cursor = 0, previous_cursor, next_cursor;
  46   mc_visited_pair_t pair_test;
  47   int start = 0;
  48   int end = xbt_dynar_length(all_pairs) - 1;
  49
  50   while(start <= end){
  51     cursor = (start + end) / 2;
  52     pair_test = (mc_visited_pair_t)xbt_dynar_get_as(all_pairs, cursor, mc_visited_pair_t);
  53     if(pair_test->nb_processes < pair->nb_processes){
  54       start = cursor + 1;
  55     }else if(pair_test->nb_processes > pair->nb_processes){
  56       end = cursor - 1;
  57     }else{
  58       if(pair_test->heap_bytes_used < pair->heap_bytes_used){
  59         start = cursor +1;
  60       }else if(pair_test->heap_bytes_used > pair->heap_bytes_used){
  61         end = cursor - 1;
  62       }else{
  63         *min = *max = cursor;
  64         previous_cursor = cursor - 1;
  65         while(previous_cursor >= 0){
  66           pair_test = (mc_visited_pair_t)xbt_dynar_get_as(all_pairs, previous_cursor, mc_visited_pair_t);
  67           if(pair_test->nb_processes != pair->nb_processes || pair_test->heap_bytes_used != pair->heap_bytes_used)
  68             break;
  69           *min = previous_cursor;
  70           previous_cursor--;
  71         }
  72         next_cursor = cursor + 1;
  73         while(next_cursor < xbt_dynar_length(all_pairs)){
  74           pair_test = (mc_visited_pair_t)xbt_dynar_get_as(all_pairs, next_cursor, mc_visited_pair_t);
  75           if(pair_test->nb_processes != pair->nb_processes || pair_test->heap_bytes_used != pair->heap_bytes_used)
  76             break;
  77           *max = next_cursor;
  78           next_cursor++;
  79         }
  80         if(!raw_mem_set)
  81           MC_UNSET_RAW_MEM;
  82         return -1;
  83       }
  84      }
  85   }
  86
  87   if(!raw_mem_set)
  88     MC_UNSET_RAW_MEM;
  89
  90   return cursor;
  91 }
  92
  93 static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
  94
  95   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  96
  97   MC_SET_RAW_MEM;
  98
  99   mc_visited_pair_t pair = NULL;
 100   pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
 101   pair->acceptance_pair = 1;
 102
 103   if(xbt_dynar_is_empty(acceptance_pairs)){
 104
 105     xbt_dynar_push(acceptance_pairs, &pair);
 106
 107   }else{
 108
 109     int min = -1, max = -1, index;
 110     //int res;
 111     mc_visited_pair_t pair_test;
 112     int cursor;
 113
 114     index = get_search_interval(acceptance_pairs, pair, &min, &max);
 115
 116     if(min != -1 && max != -1){ // Acceptance pair with same number of processes and same heap bytes used exists
 117       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair);
 118       if(res != -1){
 119         if(!raw_mem_set)
 120           MC_UNSET_RAW_MEM;
 121         return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
 122         }*/
 123       cursor = min;
 124       while(cursor <= max){
 125         pair_test = (mc_visited_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_visited_pair_t);
 126         if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
 127           if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
 128             if(snapshot_compare(pair_test, pair) == 0){
 129               XBT_INFO("Pair %d already reached (equal to pair %d) !", pair->num, pair_test->num);
 130
 131               xbt_fifo_shift(mc_stack_liveness);
 132               if(dot_output != NULL)
 133                 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, pair_test->num, initial_state_liveness->prev_req);
 134
 135               if(!raw_mem_set)
 136                 MC_UNSET_RAW_MEM;
 137
 138               return NULL;
 139             }
 140           }
 141         }
 142         cursor++;
 143       }
 144       xbt_dynar_insert_at(acceptance_pairs, min, &pair);
 145     }else{
 146       pair_test = (mc_visited_pair_t)xbt_dynar_get_as(acceptance_pairs, index, mc_visited_pair_t);
 147       if(pair_test->nb_processes < pair->nb_processes){
 148         xbt_dynar_insert_at(acceptance_pairs, index+1, &pair);
 149       }else{
 150         if(pair_test->heap_bytes_used < pair->heap_bytes_used)
 151           xbt_dynar_insert_at(acceptance_pairs, index + 1, &pair);
 152         else
 153           xbt_dynar_insert_at(acceptance_pairs, index, &pair);
 154       }
 155     }
 156
 157   }
 158
 159   if(!raw_mem_set)
 160     MC_UNSET_RAW_MEM;
 161
 162   return pair;
 163
 164 }
 165
 166 static void remove_acceptance_pair(int pair_num){
 167
 168   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 169
 170   fprintf(stderr, "Search acceptance pair %d\n", pair_num);
 171
 172   MC_SET_RAW_MEM;
 173
 174   unsigned int cursor = 0;
 175   mc_visited_pair_t pair_test = NULL;
 176
 177   xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){
 178     if(pair_test->num == pair_num){
 179       break;
 180     }
 181   }
 182
 183   xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
 184
 185   pair_test->acceptance_removed = 1;
 186
 187   if(_sg_mc_visited == 0){
 188     MC_visited_pair_delete(pair_test);
 189   }else if(pair_test->visited_removed == 1){
 190     MC_visited_pair_delete(pair_test);
 191   }
 192
 193   if(!raw_mem_set)
 194     MC_UNSET_RAW_MEM;
 195 }
 196
 197 static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
 198
 199   if(_sg_mc_visited == 0)
 200     return -1;
 201
 202   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 203
 204   MC_SET_RAW_MEM;
 205
 206   mc_visited_pair_t new_pair = NULL;
 207
 208   if(pair == NULL){
 209     new_pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
 210   }else{
 211     new_pair = pair;
 212   }
 213
 214   if(xbt_dynar_is_empty(visited_pairs)){
 215
 216     xbt_dynar_push(visited_pairs, &new_pair);
 217
 218   }else{
 219
 220     int min = -1, max = -1, index;
 221     //int res;
 222     mc_visited_pair_t pair_test;
 223     int cursor;
 224
 225     index = get_search_interval(visited_pairs, new_pair, &min, &max);
 226
 227     if(min != -1 && max != -1){ // Visited pair with same number of processes and same heap bytes used exists
 228       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
 229       if(res != -1){
 230         pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
 231         if(pair_test->other_num == -1)
 232           pair->other_num = pair_test->num;
 233         else
 234           pair->other_num = pair_test->other_num;
 235         if(dot_output == NULL)
 236           XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 237         else
 238           XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 239         xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
 240         xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
 241         pair_test->visited_removed = 1;
 242         if(pair_test->stack_removed && pair_test->visited_removed){
 243           if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 244             if(pair_test->acceptance_removed){
 245               MC_pair_delete(pair_test);
 246             }
 247           }else{
 248             MC_pair_delete(pair_test);
 249           }
 250         }
 251         if(!raw_mem_set)
 252           MC_UNSET_RAW_MEM;
 253         return pair->other_num;
 254         }*/
 255       cursor = min;
 256       while(cursor <= max){
 257         pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
 258         //if(pair_test->acceptance_pair == 0){ /* Acceptance pair have been already checked before */
 259           if(xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0){
 260             if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_pair->atomic_propositions) == 0){
 261               if(snapshot_compare(pair_test, new_pair) == 0){
 262                 if(pair_test->other_num == -1)
 263                   new_pair->other_num = pair_test->num;
 264                 else
 265                   new_pair->other_num = pair_test->other_num;
 266                 if(dot_output == NULL)
 267                   XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
 268                 else
 269                   XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_pair->num, pair_test->num, pair->other_num);
 270                 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
 271                 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
 272                 pair_test->visited_removed = 1;
 273                 if(pair_test->acceptance_pair){
 274                   if(pair_test->acceptance_removed == 1)
 275                     MC_visited_pair_delete(pair_test);
 276                 }else{
 277                   MC_visited_pair_delete(pair_test);
 278                 }
 279                 if(!raw_mem_set)
 280                   MC_UNSET_RAW_MEM;
 281                 return new_pair->other_num;
 282               }
 283             }
 284             //}
 285         }
 286         cursor++;
 287       }
 288       xbt_dynar_insert_at(visited_pairs, min, &new_pair);
 289     }else{
 290       pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
 291       if(pair_test->nb_processes < new_pair->nb_processes){
 292         xbt_dynar_insert_at(visited_pairs, index+1, &new_pair);
 293       }else{
 294         if(pair_test->heap_bytes_used < new_pair->heap_bytes_used)
 295           xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
 296         else
 297           xbt_dynar_insert_at(visited_pairs, index, &new_pair);
 298       }
 299     }
 300
 301     if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
 302       int min2 = mc_stats->expanded_pairs;
 303       unsigned int cursor2 = 0;
 304       unsigned int index2 = 0;
 305       xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
 306         if(pair_test->num < min2){
 307           index2 = cursor2;
 308           min2 = pair_test->num;
 309         }
 310       }
 311       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
 312       pair_test->visited_removed = 1;
 313       if(pair_test->acceptance_pair){
 314         if(pair_test->acceptance_removed)
 315           MC_visited_pair_delete(pair_test);
 316       }else{
 317         MC_visited_pair_delete(pair_test);
 318       }
 319     }
 320
 321   }
 322
 323   if(!raw_mem_set)
 324     MC_UNSET_RAW_MEM;
 325
 326   return -1;
 327 }
 328
 329 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, xbt_dynar_t atomic_propositions_values){
 330
 331   switch(l->type){
 332   case 0 : {
 333     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
 334     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
 335     return (left_res || right_res);
 336   }
 337   case 1 : {
 338     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
 339     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
 340     return (left_res && right_res);
 341   }
 342   case 2 : {
 343     int res = MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values);
 344     return (!res);
 345   }
 346   case 3 : {
 347     unsigned int cursor = 0;
 348     xbt_automaton_propositional_symbol_t p = NULL;
 349     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
 350       if(strcmp(p->pred, l->u.predicat) == 0)
 351         return (int)xbt_dynar_get_as(atomic_propositions_values, cursor, int);
 352     }
 353     return -1;
 354   }
 355   case 4 : {
 356     return 2;
 357   }
 358   default :
 359     return -1;
 360   }
 361 }
 362
 363
 364 /********* DDFS Algorithm *********/
 365
 366
 367 void MC_ddfs_init(void){
 368
 369   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 370
 371   XBT_DEBUG("**************************************************");
 372   XBT_DEBUG("Double-DFS init");
 373   XBT_DEBUG("**************************************************");
 374
 375   mc_pair_t initial_pair = NULL;
 376   smx_process_t process;
 377
 378   MC_wait_for_requests();
 379
 380   MC_ignore_heap(simix_global->process_to_run->data, 0);
 381   MC_ignore_heap(simix_global->process_that_ran->data, 0);
 382
 383   MC_SET_RAW_MEM;
 384
 385   acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
 386   visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
 387   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 388
 389   initial_state_liveness->snapshot = MC_take_snapshot(0);
 390   initial_state_liveness->prev_pair = 0;
 391
 392   MC_UNSET_RAW_MEM;
 393
 394   unsigned int cursor = 0;
 395   xbt_automaton_state_t automaton_state;
 396
 397   xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
 398     if(automaton_state->type == -1){ /* Initial automaton state */
 399
 400       MC_SET_RAW_MEM;
 401
 402       initial_pair = MC_pair_new();
 403       initial_pair->automaton_state = automaton_state;
 404       initial_pair->graph_state = MC_state_new();
 405       initial_pair->atomic_propositions = get_atomic_propositions_values();
 406
 407       /* Get enabled process and insert it in the interleave set of the graph_state */
 408       xbt_swag_foreach(process, simix_global->process_list){
 409         if(MC_process_is_enabled(process)){
 410           MC_state_interleave_process(initial_pair->graph_state, process);
 411         }
 412       }
 413
 414       initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
 415       initial_pair->search_cycle = 0;
 416
 417       xbt_fifo_unshift(mc_stack_liveness, initial_pair);
 418
 419       MC_UNSET_RAW_MEM;
 420
 421       MC_ddfs();
 422
 423       if(cursor != 0){
 424         MC_restore_snapshot(initial_state_liveness->snapshot);
 425         MC_UNSET_RAW_MEM;
 426       }
 427     }
 428   }
 429
 430   if(initial_state_liveness->raw_mem_set)
 431     MC_SET_RAW_MEM;
 432   else
 433     MC_UNSET_RAW_MEM;
 434
 435
 436 }
 437
 438
 439 void MC_ddfs(){
 440
 441   smx_process_t process;
 442   mc_pair_t current_pair = NULL;
 443
 444   if(xbt_fifo_size(mc_stack_liveness) == 0)
 445     return;
 446
 447   /* Get current pair */
 448   current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 449
 450   /* Update current state in buchi automaton */
 451   _mc_property_automaton->current_state = current_pair->automaton_state;
 452
 453   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size %d, pair_num %d)", xbt_fifo_size(mc_stack_liveness), current_pair->search_cycle, MC_state_interleave_size(current_pair->graph_state), current_pair->num);
 454
 455   mc_stats->visited_pairs++;
 456
 457   int value;
 458   smx_simcall_t req = NULL;
 459   char *req_str;
 460
 461   xbt_automaton_transition_t transition_succ;
 462   unsigned int cursor = 0;
 463   int res;
 464   int visited_num;
 465
 466   mc_pair_t next_pair = NULL;
 467   xbt_dynar_t prop_values = NULL;
 468   int new_pair = 0;
 469   mc_visited_pair_t reached_pair = NULL;
 470
 471   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 472
 473     if(current_pair->requests > 0){
 474
 475       if(current_pair->search_cycle){
 476
 477         if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 478           if((reached_pair = is_reached_acceptance_pair(current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) == NULL){
 479
 480             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 481             XBT_INFO("|             ACCEPTANCE CYCLE            |");
 482             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 483             XBT_INFO("Counter-example that violates formula :");
 484             MC_show_stack_liveness(mc_stack_liveness);
 485             MC_dump_stack_liveness(mc_stack_liveness);
 486             MC_print_statistics(mc_stats);
 487             xbt_abort();
 488
 489           }
 490         }
 491       }
 492
 493       if((visited_num = is_visited_pair(reached_pair, current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) != -1){
 494
 495         MC_SET_RAW_MEM;
 496         if(dot_output != NULL)
 497           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, visited_num, initial_state_liveness->prev_req);
 498         MC_UNSET_RAW_MEM;
 499
 500       }else{
 501
 502         while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 503
 504           MC_SET_RAW_MEM;
 505           if(dot_output != NULL){
 506             if(initial_state_liveness->prev_pair != 0 && initial_state_liveness->prev_pair != current_pair->num){
 507               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, current_pair->num, initial_state_liveness->prev_req);
 508               xbt_free(initial_state_liveness->prev_req);
 509             }
 510             initial_state_liveness->prev_pair = current_pair->num;
 511           }
 512           MC_UNSET_RAW_MEM;
 513
 514           /* Debug information */
 515           if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 516             req_str = MC_request_to_string(req, value);
 517             XBT_DEBUG("Execute: %s", req_str);
 518             xbt_free(req_str);
 519           }
 520
 521           MC_SET_RAW_MEM;
 522           if(dot_output != NULL){
 523             initial_state_liveness->prev_req = MC_request_get_dot_output(req, value);
 524             if(current_pair->search_cycle)
 525               fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
 526           }
 527           MC_UNSET_RAW_MEM;
 528
 529           MC_state_set_executed_request(current_pair->graph_state, req, value);
 530           mc_stats->executed_transitions++;
 531
 532           /* Answer the request */
 533           SIMIX_simcall_pre(req, value);
 534
 535           /* Wait for requests (schedules processes) */
 536           MC_wait_for_requests();
 537
 538           MC_SET_RAW_MEM;
 539           prop_values = get_atomic_propositions_values();
 540           MC_UNSET_RAW_MEM;
 541
 542           /* Evaluate enabled transition according to atomic propositions values */
 543           cursor= 0;
 544           xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 545
 546             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 547
 548             if(res == 1){ // enabled transition in automaton
 549
 550               if(new_pair)
 551                 MC_replay_liveness(mc_stack_liveness, 1);
 552
 553               MC_SET_RAW_MEM;
 554
 555               next_pair = MC_pair_new();
 556               next_pair->graph_state = MC_state_new();
 557               next_pair->automaton_state = transition_succ->dst;
 558               next_pair->atomic_propositions = get_atomic_propositions_values();
 559
 560               /* Get enabled process and insert it in the interleave set of the next graph_state */
 561               xbt_swag_foreach(process, simix_global->process_list){
 562                 if(MC_process_is_enabled(process)){
 563                   MC_state_interleave_process(next_pair->graph_state, process);
 564                 }
 565               }
 566
 567               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 568
 569               if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 570                 next_pair->search_cycle = 1;
 571
 572               xbt_fifo_unshift(mc_stack_liveness, next_pair);
 573
 574               if(mc_stats->expanded_pairs%1000000 == 0)
 575                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 576
 577               MC_UNSET_RAW_MEM;
 578
 579               new_pair = 1;
 580
 581               MC_ddfs();
 582
 583             }
 584
 585           }
 586
 587           /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
 588           cursor = 0;
 589           xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 590
 591             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 592
 593             if(res == 2){ // true transition in automaton
 594
 595               if(new_pair)
 596                 MC_replay_liveness(mc_stack_liveness, 1);
 597
 598               MC_SET_RAW_MEM;
 599
 600               next_pair = MC_pair_new();
 601               next_pair->graph_state = MC_state_new();
 602               next_pair->automaton_state = transition_succ->dst;
 603               next_pair->atomic_propositions = get_atomic_propositions_values();
 604
 605               /* Get enabled process and insert it in the interleave set of the next graph_state */
 606               xbt_swag_foreach(process, simix_global->process_list){
 607                 if(MC_process_is_enabled(process)){
 608                   MC_state_interleave_process(next_pair->graph_state, process);
 609                 }
 610               }
 611
 612               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 613
 614               if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 615                 next_pair->search_cycle = 1;
 616
 617               xbt_fifo_unshift(mc_stack_liveness, next_pair);
 618
 619               if(mc_stats->expanded_pairs%1000000 == 0)
 620                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 621
 622               MC_UNSET_RAW_MEM;
 623
 624               new_pair = 1;
 625
 626               MC_ddfs();
 627
 628             }
 629
 630           }
 631
 632           if(MC_state_interleave_size(current_pair->graph_state) > 0){
 633             XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 634             MC_replay_liveness(mc_stack_liveness, 0);
 635           }
 636
 637         }
 638
 639       }
 640
 641     }
 642
 643   }else{
 644
 645     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 646     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 647       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
 648       if(_sg_mc_max_depth == 1000)
 649         XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
 650     }
 651
 652   }
 653
 654   if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
 655     XBT_DEBUG("Pair %d (depth = %d) shifted in stack, maximum depth reached", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
 656   }else{
 657     XBT_DEBUG("Pair %d (depth = %d) shifted in stack", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
 658   }
 659
 660
 661   MC_SET_RAW_MEM;
 662   xbt_dynar_free(&prop_values);
 663   current_pair = xbt_fifo_shift(mc_stack_liveness);
 664   if(xbt_fifo_size(mc_stack_liveness) != _sg_mc_max_depth -1 && current_pair->requests > 0 && current_pair->search_cycle){
 665     remove_acceptance_pair(current_pair->num);
 666   }
 667   MC_pair_delete(current_pair);
 668
 669   MC_UNSET_RAW_MEM;
 670
 671 }