src/mc/mc_liveness.c

   1 #include "private.h"
   2 #include "unistd.h"
   3
   4 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
   5                                 "Logging specific to algorithms for liveness properties verification");
   6
   7 xbt_dynar_t initial_pairs = NULL;
   8 xbt_dynar_t reached_pairs;
   9 xbt_dynar_t successors = NULL;
  10 extern mc_snapshot_t initial_snapshot;
  11
  12 /* Global variables for stateless algorithm */
  13 mc_snapshot_t snapshot = NULL;
  14
  15 /* Global variables for stateful algorithm */
  16 mc_snapshot_t next_snapshot = NULL;
  17 mc_snapshot_t current_snapshot = NULL;
  18
  19
  20 mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
  21   mc_pair_t p = NULL;
  22   p = xbt_new0(s_mc_pair_t, 1);
  23   p->system_state = sn;
  24   p->automaton_state = st;
  25   p->graph_state = sg;
  26   mc_stats_pair->expanded_pairs++;
  27   return p;
  28
  29 }
  30
  31 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
  32
  33   if(s1->num_reg != s2->num_reg)
  34     return 1;
  35
  36   int i, errors=0;
  37
  38   for(i=0 ; i< s1->num_reg ; i++){
  39
  40     if(s1->regions[i]->size != s2->regions[i]->size)
  41       return 1;
  42
  43     if(s1->regions[i]->start_addr != s2->regions[i]->start_addr)
  44       return 1;
  45
  46     if(s1->regions[i]->type != s2->regions[i]->type)
  47       return 1;
  48
  49     if(s1->regions[i]->type == 0){
  50       if(mmalloc_compare_heap(s1->regions[i]->start_addr, s2->regions[i]->start_addr)){
  51         XBT_DEBUG("Different heap (mmalloc_compare)");
  52         sleep(1);
  53         errors++;
  54       }
  55     }else{
  56       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
  57         XBT_DEBUG("Different memcmp for data in libsimgrid");
  58         sleep(1);
  59         errors++;
  60       }
  61     }
  62
  63
  64   }
  65
  66   return (errors>0);
  67
  68 }
  69
  70 int reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s){
  71
  72
  73   if(xbt_dynar_is_empty(reached_pairs)){
  74     return 0;
  75   }else{
  76     MC_SET_RAW_MEM;
  77
  78     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
  79
  80     /* Get values of propositional symbols */
  81     unsigned int cursor = 0;
  82     xbt_propositional_symbol_t ps = NULL;
  83     xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
  84       int (*f)() = ps->function;
  85       int res = (*f)();
  86       xbt_dynar_push_as(prop_ato, int, res);
  87     }
  88
  89     cursor = 0;
  90     mc_pair_reached_t pair_test;
  91
  92     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
  93       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
  94         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
  95           if(snapshot_compare(pair_test->system_state, s) == 0){
  96             MC_UNSET_RAW_MEM;
  97             return 1;
  98           }
  99         }
 100       }
 101     }
 102
 103     MC_UNSET_RAW_MEM;
 104     return 0;
 105
 106   }
 107 }
 108
 109 void set_pair_reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t sn){
 110
 111
 112   MC_SET_RAW_MEM;
 113
 114   mc_pair_reached_t pair = NULL;
 115   pair = xbt_new0(s_mc_pair_reached_t, 1);
 116   pair->automaton_state = st;
 117   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 118   pair->system_state = sn;
 119
 120   /* Get values of propositional symbols */
 121   unsigned int cursor = 0;
 122   xbt_propositional_symbol_t ps = NULL;
 123   xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 124     int (*f)() = ps->function;
 125     int res = (*f)();
 126     xbt_dynar_push_as(pair->prop_ato, int, res);
 127   }
 128
 129   xbt_dynar_push(reached_pairs, &pair);
 130
 131   MC_UNSET_RAW_MEM;
 132
 133
 134 }
 135
 136 void MC_pair_delete(mc_pair_t pair){
 137   xbt_free(pair->graph_state->proc_status);
 138   xbt_free(pair->graph_state);
 139   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 140   xbt_free(pair);
 141 }
 142
 143
 144
 145 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 146
 147   switch(l->type){
 148   case 0 : {
 149     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 150     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 151     return (left_res || right_res);
 152     break;
 153   }
 154   case 1 : {
 155     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 156     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 157     return (left_res && right_res);
 158     break;
 159   }
 160   case 2 : {
 161     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
 162     return (!res);
 163     break;
 164   }
 165   case 3 : {
 166     unsigned int cursor = 0;
 167     xbt_propositional_symbol_t p = NULL;
 168     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
 169       if(strcmp(p->pred, l->u.predicat) == 0){
 170         int (*f)() = p->function;
 171         return (*f)();
 172       }
 173     }
 174     return -1;
 175     break;
 176   }
 177   case 4 : {
 178     return 2;
 179     break;
 180   }
 181   default :
 182     return -1;
 183   }
 184 }
 185
 186
 187
 188
 189
 190 /********************* Double-DFS stateless *******************/
 191
 192 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 193   xbt_free(pair->graph_state->proc_status);
 194   xbt_free(pair->graph_state);
 195   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 196   xbt_free(pair);
 197 }
 198
 199 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
 200   mc_pair_stateless_t p = NULL;
 201   p = xbt_new0(s_mc_pair_stateless_t, 1);
 202   p->automaton_state = st;
 203   p->graph_state = sg;
 204   mc_stats_pair->expanded_pairs++;
 205   return p;
 206 }
 207
 208
 209
 210 void MC_ddfs_stateless_init(xbt_automaton_t a){
 211
 212   XBT_DEBUG("**************************************************");
 213   XBT_DEBUG("Double-DFS stateless init");
 214   XBT_DEBUG("**************************************************");
 215
 216   mc_pair_stateless_t mc_initial_pair = NULL;
 217   mc_state_t initial_graph_state = NULL;
 218   smx_process_t process;
 219
 220   MC_wait_for_requests();
 221
 222   MC_SET_RAW_MEM;
 223
 224   initial_graph_state = MC_state_pair_new();
 225   xbt_swag_foreach(process, simix_global->process_list){
 226     if(MC_process_is_enabled(process)){
 227       MC_state_interleave_process(initial_graph_state, process);
 228     }
 229   }
 230
 231   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
 232   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 233   snapshot = xbt_new0(s_mc_snapshot_t, 1);
 234
 235   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 236   MC_take_snapshot(initial_snapshot);
 237
 238   MC_UNSET_RAW_MEM;
 239
 240   unsigned int cursor = 0;
 241   xbt_state_t state;
 242
 243   xbt_dynar_foreach(a->states, cursor, state){
 244     if(state->type == -1){
 245
 246       MC_SET_RAW_MEM;
 247       mc_initial_pair = new_pair_stateless(initial_graph_state, state);
 248       xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 249       MC_UNSET_RAW_MEM;
 250
 251       if(cursor == 0){
 252         MC_ddfs_stateless(a, 0, 0);
 253       }else{
 254         MC_restore_snapshot(initial_snapshot);
 255         MC_UNSET_RAW_MEM;
 256         MC_ddfs_stateless(a, 0, 0);
 257       }
 258     }else{
 259       if(state->type == 2){
 260
 261         MC_SET_RAW_MEM;
 262         mc_initial_pair = new_pair_stateless(initial_graph_state, state);
 263         xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 264         MC_UNSET_RAW_MEM;
 265
 266         if(cursor == 0){
 267           MC_ddfs_stateless(a, 1, 0);
 268         }else{
 269           MC_restore_snapshot(initial_snapshot);
 270           MC_UNSET_RAW_MEM;
 271           MC_ddfs_stateless(a, 1, 0);
 272         }
 273       }
 274     }
 275   }
 276
 277 }
 278
 279
 280 void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
 281
 282   smx_process_t process;
 283   mc_pair_stateless_t current_pair = NULL;
 284
 285   if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
 286     return;
 287
 288   if(replay == 1){
 289     MC_replay_liveness(mc_stack_liveness_stateless);
 290     current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 291     xbt_swag_foreach(process, simix_global->process_list){
 292       if(MC_process_is_enabled(process)){
 293         MC_state_interleave_process(current_pair->graph_state, process);
 294       }
 295     }
 296   }
 297
 298   /* Get current pair */
 299   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 300
 301   /* Update current state in buchi automaton */
 302   a->current_state = current_pair->automaton_state;
 303
 304
 305   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
 306   XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id, MC_state_interleave_size(current_pair->graph_state));
 307
 308
 309   mc_stats_pair->visited_pairs++;
 310
 311   int value;
 312   mc_state_t next_graph_state = NULL;
 313   smx_req_t req = NULL;
 314   char *req_str;
 315
 316   xbt_transition_t transition_succ;
 317   unsigned int cursor = 0;
 318   int res;
 319
 320   mc_pair_stateless_t next_pair = NULL;
 321   mc_pair_stateless_t pair_succ;
 322   //mc_snapshot_t next_snapshot = NULL;
 323
 324   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 325
 326     /* Debug information */
 327     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 328       req_str = MC_request_to_string(req, value);
 329       XBT_DEBUG("Execute: %s", req_str);
 330       xbt_free(req_str);
 331     }
 332
 333     //sleep(1);
 334
 335     MC_state_set_executed_request(current_pair->graph_state, req, value);
 336
 337     /* Answer the request */
 338     SIMIX_request_pre(req, value);
 339
 340     /* Wait for requests (schedules processes) */
 341     MC_wait_for_requests();
 342
 343
 344     MC_SET_RAW_MEM;
 345
 346     /* Create the new expanded graph_state */
 347     next_graph_state = MC_state_pair_new();
 348
 349     /* Get enabled process and insert it in the interleave set of the next graph_state */
 350     xbt_swag_foreach(process, simix_global->process_list){
 351       if(MC_process_is_enabled(process)){
 352         MC_state_interleave_process(next_graph_state, process);
 353       }
 354     }
 355
 356     xbt_dynar_reset(successors);
 357
 358     MC_UNSET_RAW_MEM;
 359
 360
 361     cursor= 0;
 362     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 363
 364       res = MC_automaton_evaluate_label(a, transition_succ->label);
 365
 366       if(res == 1){ // enabled transition in automaton
 367         MC_SET_RAW_MEM;
 368         next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
 369         xbt_dynar_push(successors, &next_pair);
 370         MC_UNSET_RAW_MEM;
 371       }
 372
 373     }
 374
 375     cursor = 0;
 376
 377     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 378
 379       res = MC_automaton_evaluate_label(a, transition_succ->label);
 380
 381       if(res == 2){ // true transition in automaton
 382         MC_SET_RAW_MEM;
 383         next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
 384         xbt_dynar_push(successors, &next_pair);
 385         MC_UNSET_RAW_MEM;
 386       }
 387
 388     }
 389
 390
 391     if(xbt_dynar_length(successors) == 0){
 392       MC_SET_RAW_MEM;
 393       next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);
 394       xbt_dynar_push(successors, &next_pair);
 395       MC_UNSET_RAW_MEM;
 396     }
 397
 398     cursor = 0;
 399
 400     xbt_dynar_foreach(successors, cursor, pair_succ){
 401
 402
 403
 404       if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) ){
 405
 406         XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1);
 407
 408         MC_SET_RAW_MEM;
 409         MC_take_snapshot(snapshot);
 410         MC_UNSET_RAW_MEM;
 411
 412         if(reached(a, pair_succ->automaton_state, snapshot) == 1){
 413           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 414           XBT_INFO("|             ACCEPTANCE CYCLE            |");
 415           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 416           XBT_INFO("Counter-example that violates formula :");
 417           MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 418           MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 419           MC_print_statistics_pairs(mc_stats_pair);
 420           exit(1);
 421         }
 422       }
 423
 424       int interleave = MC_state_interleave_size(pair_succ->graph_state);
 425
 426       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && ( interleave > 0)){
 427         XBT_DEBUG("Take snapshot of acceptance pair (depth = %d)", xbt_fifo_size(mc_stack_liveness_stateless) + 1 );
 428         MC_SET_RAW_MEM;
 429         MC_take_snapshot(snapshot);
 430         MC_UNSET_RAW_MEM;
 431       }
 432
 433       MC_SET_RAW_MEM;
 434       xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 435       MC_UNSET_RAW_MEM;
 436
 437       MC_ddfs_stateless(a, search_cycle, 0);
 438
 439       /* If pair_succ is the last state of the execution (0 interleave), no acceptance cycle possible */
 440       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && ( interleave > 0)){
 441
 442         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 443
 444
 445         set_pair_reached(a, pair_succ->automaton_state, snapshot);
 446
 447
 448         /* Pair shifted from stack when first MC_ddfs finished and returned at this point */
 449         MC_SET_RAW_MEM;
 450         xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 451         MC_UNSET_RAW_MEM;
 452
 453         MC_ddfs_stateless(a, 1, 1);
 454
 455         /* No acceptance cycle with this acceptance pair, we remove it from the list reached_pairs */
 456         MC_SET_RAW_MEM;
 457         xbt_dynar_pop(reached_pairs, NULL);
 458         MC_UNSET_RAW_MEM;
 459
 460       }
 461     }
 462
 463     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 464       XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
 465       MC_replay_liveness(mc_stack_liveness_stateless);
 466     }
 467
 468   }
 469
 470   MC_SET_RAW_MEM;
 471   xbt_fifo_shift(mc_stack_liveness_stateless);
 472   XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
 473   MC_UNSET_RAW_MEM;
 474
 475 }
 476
 477 /********************* Double-DFS stateful without visited state *******************/
 478
 479
 480 void MC_ddfs_stateful_init(xbt_automaton_t a){
 481
 482   XBT_DEBUG("**************************************************");
 483   XBT_DEBUG("Double-DFS stateful without visited state init");
 484   XBT_DEBUG("**************************************************");
 485
 486   mc_pair_t mc_initial_pair;
 487   mc_state_t initial_graph_state;
 488   smx_process_t process;
 489   mc_snapshot_t init_snapshot;
 490
 491   MC_wait_for_requests();
 492
 493   MC_SET_RAW_MEM;
 494
 495   initial_graph_state = MC_state_pair_new();
 496   xbt_swag_foreach(process, simix_global->process_list){
 497     if(MC_process_is_enabled(process)){
 498       MC_state_interleave_process(initial_graph_state, process);
 499     }
 500   }
 501
 502   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
 503   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 504   current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 505   next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 506
 507   init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 508   MC_take_snapshot(init_snapshot);
 509
 510   MC_UNSET_RAW_MEM;
 511
 512   unsigned int cursor = 0;
 513   xbt_state_t state = NULL;
 514
 515   xbt_dynar_foreach(a->states, cursor, state){
 516     if(state->type == -1){
 517
 518       MC_SET_RAW_MEM;
 519       mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
 520       xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
 521       MC_UNSET_RAW_MEM;
 522
 523       if(cursor == 0){
 524         MC_ddfs_stateful(a, 0, 0);
 525       }else{
 526         MC_restore_snapshot(init_snapshot);
 527         MC_UNSET_RAW_MEM;
 528         MC_ddfs_stateful(a, 0, 0);
 529       }
 530     }else{
 531        if(state->type == 2){
 532
 533          MC_SET_RAW_MEM;
 534          mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
 535          xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
 536          MC_UNSET_RAW_MEM;
 537
 538          if(cursor == 0){
 539            MC_ddfs_stateful(a, 1, 0);
 540          }else{
 541            MC_restore_snapshot(init_snapshot);
 542            MC_UNSET_RAW_MEM;
 543            MC_ddfs_stateful(a, 1, 0);
 544          }
 545        }
 546     }
 547   }
 548 }
 549
 550
 551 void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 552
 553   smx_process_t process = NULL;
 554   mc_pair_t current_pair = NULL;
 555
 556   if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
 557     return;
 558
 559   if(restore == 1){
 560     current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 561     MC_restore_snapshot(current_pair->system_state);
 562     xbt_swag_foreach(process, simix_global->process_list){
 563       if(MC_process_is_enabled(process)){
 564         MC_state_interleave_process(current_pair->graph_state, process);
 565       }
 566     }
 567     MC_UNSET_RAW_MEM;
 568   }
 569
 570   /* Get current state */
 571   current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 572
 573
 574   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle);
 575   XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state));
 576
 577   a->current_state = current_pair->automaton_state;
 578
 579   //sleep(1);
 580
 581   mc_stats_pair->visited_pairs++;
 582
 583   int value;
 584   mc_state_t next_graph_state = NULL;
 585   smx_req_t req = NULL;
 586   char *req_str;
 587
 588   mc_pair_t pair_succ;
 589   xbt_transition_t transition_succ;
 590   unsigned int cursor;
 591   int res;
 592
 593   mc_pair_t next_pair = NULL;
 594
 595   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 596
 597     MC_SET_RAW_MEM;
 598     MC_take_snapshot(current_snapshot);
 599     MC_UNSET_RAW_MEM;
 600
 601     /* Debug information */
 602     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 603       req_str = MC_request_to_string(req, value);
 604       XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state));
 605       XBT_DEBUG("Execute: %s", req_str);
 606       xbt_free(req_str);
 607     }
 608
 609     MC_state_set_executed_request(current_pair->graph_state, req, value);
 610
 611     /* Answer the request */
 612     SIMIX_request_pre(req, value);
 613
 614     /* Wait for requests (schedules processes) */
 615     MC_wait_for_requests();
 616
 617
 618     /* Create the new expanded graph_state */
 619     MC_SET_RAW_MEM;
 620
 621     next_graph_state = MC_state_pair_new();
 622
 623     /* Get enabled process and insert it in the interleave set of the next graph_state */
 624     xbt_swag_foreach(process, simix_global->process_list){
 625       if(MC_process_is_enabled(process)){
 626         MC_state_interleave_process(next_graph_state, process);
 627       }
 628     }
 629
 630     MC_take_snapshot(next_snapshot);
 631
 632     xbt_dynar_reset(successors);
 633
 634     MC_UNSET_RAW_MEM;
 635
 636
 637     cursor = 0;
 638     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 639
 640       res = MC_automaton_evaluate_label(a, transition_succ->label);
 641
 642       if(res == 1){ // enabled transition in automaton
 643         MC_SET_RAW_MEM;
 644         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 645         xbt_dynar_push(successors, &next_pair);
 646         MC_UNSET_RAW_MEM;
 647       }
 648
 649     }
 650
 651     cursor = 0;
 652     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 653
 654       res = MC_automaton_evaluate_label(a, transition_succ->label);
 655
 656       if(res == 2){ // transition always enabled in automaton
 657         MC_SET_RAW_MEM;
 658         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 659         xbt_dynar_push(successors, &next_pair);
 660         MC_UNSET_RAW_MEM;
 661       }
 662
 663
 664     }
 665
 666
 667     if(xbt_dynar_length(successors) == 0){
 668
 669       MC_SET_RAW_MEM;
 670       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
 671       xbt_dynar_push(successors, &next_pair);
 672       MC_UNSET_RAW_MEM;
 673
 674     }
 675
 676     cursor = 0;
 677     xbt_dynar_foreach(successors, cursor, pair_succ){
 678
 679       if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 680
 681         if(reached(a, pair_succ->automaton_state, next_snapshot) == 1){
 682           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 683           XBT_INFO("|             ACCEPTANCE CYCLE            |");
 684           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 685           XBT_INFO("Counter-example that violates formula :");
 686           MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
 687           MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
 688           MC_print_statistics_pairs(mc_stats_pair);
 689           exit(1);
 690         }
 691       }
 692
 693
 694       MC_SET_RAW_MEM;
 695       xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 696       MC_UNSET_RAW_MEM;
 697
 698       MC_ddfs_stateful(a, search_cycle, 0);
 699
 700
 701       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 702
 703         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 704         set_pair_reached(a, pair_succ->automaton_state, next_snapshot);
 705
 706         MC_SET_RAW_MEM;
 707         xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 708         MC_UNSET_RAW_MEM;
 709
 710         MC_ddfs_stateful(a, 1, 1);
 711
 712
 713         MC_SET_RAW_MEM;
 714         xbt_dynar_pop(reached_pairs, NULL);
 715         MC_UNSET_RAW_MEM;
 716       }
 717
 718     }
 719
 720     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 721       XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateful));
 722       MC_restore_snapshot(current_snapshot);
 723       MC_UNSET_RAW_MEM;
 724     }
 725
 726   }
 727
 728
 729   MC_SET_RAW_MEM;
 730   xbt_fifo_shift(mc_stack_liveness_stateful);
 731   XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
 732   MC_UNSET_RAW_MEM;
 733
 734 }