src/mc/mc_liveness.c

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