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