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