src/mc/mc_liveness.c

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