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   mc_visited_pair_t reached_pair = NULL;
 469
 470   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 471
 472     if(current_pair->requests > 0){
 473
 474       if(current_pair->search_cycle){
 475
 476         if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 477           if((reached_pair = is_reached_acceptance_pair(current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) == NULL){
 478
 479             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 480             XBT_INFO("|             ACCEPTANCE CYCLE            |");
 481             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 482             XBT_INFO("Counter-example that violates formula :");
 483             MC_show_stack_liveness(mc_stack_liveness);
 484             MC_dump_stack_liveness(mc_stack_liveness);
 485             MC_print_statistics(mc_stats);
 486             xbt_abort();
 487
 488           }
 489         }
 490       }
 491
 492       if((visited_num = is_visited_pair(reached_pair, current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) != -1){
 493
 494         MC_SET_RAW_MEM;
 495         if(dot_output != NULL)
 496           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, visited_num, initial_state_liveness->prev_req);
 497         MC_UNSET_RAW_MEM;
 498
 499       }else{
 500
 501         while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 502
 503           MC_SET_RAW_MEM;
 504           if(dot_output != NULL){
 505             if(initial_state_liveness->prev_pair != 0 && initial_state_liveness->prev_pair != current_pair->num){
 506               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, current_pair->num, initial_state_liveness->prev_req);
 507               xbt_free(initial_state_liveness->prev_req);
 508             }
 509             initial_state_liveness->prev_pair = current_pair->num;
 510           }
 511           MC_UNSET_RAW_MEM;
 512
 513           /* Debug information */
 514           if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 515             req_str = MC_request_to_string(req, value);
 516             XBT_DEBUG("Execute: %s", req_str);
 517             xbt_free(req_str);
 518           }
 519
 520           MC_SET_RAW_MEM;
 521           if(dot_output != NULL){
 522             initial_state_liveness->prev_req = MC_request_get_dot_output(req, value);
 523             if(current_pair->search_cycle)
 524               fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
 525           }
 526           MC_UNSET_RAW_MEM;
 527
 528           MC_state_set_executed_request(current_pair->graph_state, req, value);
 529           mc_stats->executed_transitions++;
 530
 531           /* Answer the request */
 532           SIMIX_simcall_pre(req, value);
 533
 534           /* Wait for requests (schedules processes) */
 535           MC_wait_for_requests();
 536
 537           MC_SET_RAW_MEM;
 538           prop_values = get_atomic_propositions_values();
 539           MC_UNSET_RAW_MEM;
 540
 541           int new_pair = 0;
 542
 543           /* Evaluate enabled transition according to atomic propositions values */
 544           cursor= 0;
 545           xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 546
 547             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 548
 549             if(res == 1){ // enabled transition in automaton
 550
 551               if(new_pair)
 552                 MC_replay_liveness(mc_stack_liveness, 1);
 553
 554               MC_SET_RAW_MEM;
 555
 556               next_pair = MC_pair_new();
 557               next_pair->graph_state = MC_state_new();
 558               next_pair->automaton_state = transition_succ->dst;
 559               next_pair->atomic_propositions = get_atomic_propositions_values();
 560
 561               /* Get enabled process and insert it in the interleave set of the next graph_state */
 562               xbt_swag_foreach(process, simix_global->process_list){
 563                 if(MC_process_is_enabled(process)){
 564                   MC_state_interleave_process(next_pair->graph_state, process);
 565                 }
 566               }
 567
 568               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 569
 570               if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 571                 next_pair->search_cycle = 1;
 572
 573               xbt_fifo_unshift(mc_stack_liveness, next_pair);
 574
 575               if(mc_stats->expanded_pairs%1000000 == 0)
 576                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 577
 578               MC_UNSET_RAW_MEM;
 579
 580               new_pair = 1;
 581
 582               MC_ddfs();
 583
 584             }
 585
 586           }
 587
 588           /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
 589           cursor = 0;
 590           xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 591
 592             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 593
 594             if(res == 2){ // true transition in automaton
 595
 596               if(new_pair)
 597                 MC_replay_liveness(mc_stack_liveness, 1);
 598
 599               MC_SET_RAW_MEM;
 600
 601               next_pair = MC_pair_new();
 602               next_pair->graph_state = MC_state_new();
 603               next_pair->automaton_state = transition_succ->dst;
 604               next_pair->atomic_propositions = get_atomic_propositions_values();
 605
 606               /* Get enabled process and insert it in the interleave set of the next graph_state */
 607               xbt_swag_foreach(process, simix_global->process_list){
 608                 if(MC_process_is_enabled(process)){
 609                   MC_state_interleave_process(next_pair->graph_state, process);
 610                 }
 611               }
 612
 613               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 614
 615               if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 616                 next_pair->search_cycle = 1;
 617
 618               xbt_fifo_unshift(mc_stack_liveness, next_pair);
 619
 620               if(mc_stats->expanded_pairs%1000000 == 0)
 621                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 622
 623               MC_UNSET_RAW_MEM;
 624
 625               new_pair = 1;
 626
 627               MC_ddfs();
 628
 629             }
 630
 631           }
 632
 633           if(MC_state_interleave_size(current_pair->graph_state) > 0){
 634             XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 635             MC_replay_liveness(mc_stack_liveness, 0);
 636           }
 637
 638         }
 639
 640       }
 641
 642     }
 643
 644   }else{
 645
 646     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 647     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 648       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
 649       if(_sg_mc_max_depth == 1000)
 650         XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
 651     }
 652
 653   }
 654
 655   if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
 656     XBT_DEBUG("Pair %d (depth = %d) shifted in stack, maximum depth reached", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
 657   }else{
 658     XBT_DEBUG("Pair %d (depth = %d) shifted in stack", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
 659   }
 660
 661
 662   MC_SET_RAW_MEM;
 663   xbt_dynar_free(&prop_values);
 664   current_pair = xbt_fifo_shift(mc_stack_liveness);
 665   if(xbt_fifo_size(mc_stack_liveness) != _sg_mc_max_depth -1 && current_pair->requests > 0 && current_pair->search_cycle){
 666     remove_acceptance_pair(current_pair->num);
 667   }
 668   MC_pair_delete(current_pair);
 669
 670   MC_UNSET_RAW_MEM;
 671
 672 }