src/mc/mc_liveness.c

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