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