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