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         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 480           req_str = MC_request_to_string(req, value);
 481           XBT_DEBUG("Execute: %s", req_str);
 482           xbt_free(req_str);
 483         }
 484
 485         MC_state_set_executed_request(current_pair->graph_state, req, value);
 486
 487         /* Answer the request */
 488         SIMIX_simcall_pre(req, value);
 489
 490         /* Wait for requests (schedules processes) */
 491         MC_wait_for_requests();
 492
 493         MC_SET_RAW_MEM;
 494
 495         /* Create the new expanded graph_state */
 496         next_graph_state = MC_state_pair_new();
 497
 498         /* Get enabled process and insert it in the interleave set of the next graph_state */
 499         xbt_swag_foreach(process, simix_global->process_list){
 500           if(MC_process_is_enabled(process)){
 501             XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
 502           }
 503         }
 504
 505         xbt_swag_foreach(process, simix_global->process_list){
 506           if(MC_process_is_enabled(process)){
 507             MC_state_interleave_process(next_graph_state, process);
 508           }
 509         }
 510
 511         xbt_dynar_reset(successors);
 512
 513         MC_UNSET_RAW_MEM;
 514
 515
 516         cursor= 0;
 517         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 518
 519           res = MC_automaton_evaluate_label(transition_succ->label);
 520
 521           if(res == 1){ // enabled transition in automaton
 522             MC_SET_RAW_MEM;
 523             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 524             xbt_dynar_push(successors, &next_pair);
 525             MC_UNSET_RAW_MEM;
 526           }
 527
 528         }
 529
 530         cursor = 0;
 531
 532         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 533
 534           res = MC_automaton_evaluate_label(transition_succ->label);
 535
 536           if(res == 2){ // true transition in automaton
 537             MC_SET_RAW_MEM;
 538             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 539             xbt_dynar_push(successors, &next_pair);
 540             MC_UNSET_RAW_MEM;
 541           }
 542
 543         }
 544
 545         cursor = 0;
 546
 547         xbt_dynar_foreach(successors, cursor, pair_succ){
 548
 549           if(search_cycle == 1){
 550
 551             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 552
 553               if(reached(pair_succ->automaton_state)){
 554
 555                 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));
 556
 557                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 558                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 559                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 560                 XBT_INFO("Counter-example that violates formula :");
 561                 MC_show_stack_liveness(mc_stack_liveness);
 562                 MC_dump_stack_liveness(mc_stack_liveness);
 563                 MC_print_statistics_pairs(mc_stats_pair);
 564                 xbt_abort();
 565
 566               }else{
 567
 568                 if(visited(pair_succ->automaton_state)){
 569
 570                   XBT_DEBUG("Next pair already visited !");
 571                   break;
 572
 573                 }else{
 574
 575                   XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 576
 577                   XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 578
 579                   MC_SET_RAW_MEM;
 580                   xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 581                   MC_UNSET_RAW_MEM;
 582
 583                   MC_ddfs(search_cycle);
 584
 585                 }
 586
 587               }
 588
 589             }else{
 590
 591               if(visited(pair_succ->automaton_state)){
 592
 593                 XBT_DEBUG("Next pair already visited !");
 594                 break;
 595
 596               }else{
 597
 598                 MC_SET_RAW_MEM;
 599                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 600                 MC_UNSET_RAW_MEM;
 601
 602                 MC_ddfs(search_cycle);
 603               }
 604
 605             }
 606
 607           }else{
 608
 609             if(visited(pair_succ->automaton_state)){
 610
 611               XBT_DEBUG("Next pair already visited !");
 612               break;
 613
 614             }else{
 615
 616               if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 617
 618                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 619
 620                 set_pair_reached(pair_succ->automaton_state);
 621
 622                 search_cycle = 1;
 623
 624                 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 625
 626               }
 627
 628               MC_SET_RAW_MEM;
 629               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 630               MC_UNSET_RAW_MEM;
 631
 632               MC_ddfs(search_cycle);
 633
 634             }
 635
 636           }
 637
 638           /* Restore system before checking others successors */
 639           if(cursor != (xbt_dynar_length(successors) - 1))
 640             MC_replay_liveness(mc_stack_liveness, 1);
 641
 642         }
 643
 644         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 645           XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 646           MC_replay_liveness(mc_stack_liveness, 0);
 647         }
 648       }
 649
 650
 651     }else{
 652
 653       XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
 654
 655       MC_SET_RAW_MEM;
 656
 657       /* Create the new expanded graph_state */
 658       next_graph_state = MC_state_pair_new();
 659
 660       xbt_dynar_reset(successors);
 661
 662       MC_UNSET_RAW_MEM;
 663
 664
 665       cursor= 0;
 666       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 667
 668         res = MC_automaton_evaluate_label(transition_succ->label);
 669
 670         if(res == 1){ // enabled transition in automaton
 671           MC_SET_RAW_MEM;
 672           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 673           xbt_dynar_push(successors, &next_pair);
 674           MC_UNSET_RAW_MEM;
 675         }
 676
 677       }
 678
 679       cursor = 0;
 680
 681       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 682
 683         res = MC_automaton_evaluate_label(transition_succ->label);
 684
 685         if(res == 2){ // true transition in automaton
 686           MC_SET_RAW_MEM;
 687           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 688           xbt_dynar_push(successors, &next_pair);
 689           MC_UNSET_RAW_MEM;
 690         }
 691
 692       }
 693
 694       cursor = 0;
 695
 696       xbt_dynar_foreach(successors, cursor, pair_succ){
 697
 698         if(search_cycle == 1){
 699
 700           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 701
 702             if(reached(pair_succ->automaton_state)){
 703
 704               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
 705
 706               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 707               XBT_INFO("|             ACCEPTANCE CYCLE            |");
 708               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 709               XBT_INFO("Counter-example that violates formula :");
 710               MC_show_stack_liveness(mc_stack_liveness);
 711               MC_dump_stack_liveness(mc_stack_liveness);
 712               MC_print_statistics_pairs(mc_stats_pair);
 713               xbt_abort();
 714
 715             }else{
 716
 717               XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 718
 719               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 720
 721               MC_SET_RAW_MEM;
 722               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 723               MC_UNSET_RAW_MEM;
 724
 725               MC_ddfs(search_cycle);
 726
 727             }
 728
 729           }else{
 730
 731             MC_SET_RAW_MEM;
 732             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 733             MC_UNSET_RAW_MEM;
 734
 735             MC_ddfs(search_cycle);
 736
 737           }
 738
 739
 740         }else{
 741
 742           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 743
 744             set_pair_reached(pair_succ->automaton_state);
 745
 746             search_cycle = 1;
 747
 748             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 749
 750           }
 751
 752           MC_SET_RAW_MEM;
 753           xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 754           MC_UNSET_RAW_MEM;
 755
 756           MC_ddfs(search_cycle);
 757
 758         }
 759
 760         /* Restore system before checking others successors */
 761         if(cursor != xbt_dynar_length(successors) - 1)
 762           MC_replay_liveness(mc_stack_liveness, 1);
 763
 764       }
 765
 766     }
 767
 768   }else{
 769
 770     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 771     if(current_pair->requests > 0){
 772       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
 773       XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
 774     }
 775
 776   }
 777
 778   if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
 779     XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
 780   }else{
 781     XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
 782   }
 783
 784
 785   MC_SET_RAW_MEM;
 786   remove_pair = xbt_fifo_shift(mc_stack_liveness);
 787   xbt_fifo_remove(mc_stack_liveness, remove_pair);
 788   remove_pair = NULL;
 789   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 790     remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t);
 791     pair_reached_free(remove_pair_reached);
 792     remove_pair_reached = NULL;
 793   }
 794   MC_UNSET_RAW_MEM;
 795
 796   /*if(initial_state_liveness->raw_mem_set)
 797     MC_SET_RAW_MEM;*/
 798
 799 }