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 void MC_ddfs_with_restore_snapshot_init(xbt_automaton_t a){
 459
 460   XBT_DEBUG("**************************************************");
 461   XBT_DEBUG("Double-DFS without visited state and with restore snapshot init");
 462   XBT_DEBUG("**************************************************");
 463
 464   mc_pair_t mc_initial_pair;
 465   mc_state_t initial_graph_state;
 466   smx_process_t process;
 467   mc_snapshot_t init_snapshot;
 468
 469   MC_wait_for_requests();
 470
 471   MC_SET_RAW_MEM;
 472
 473   init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 474
 475   initial_graph_state = MC_state_pair_new();
 476   xbt_swag_foreach(process, simix_global->process_list){
 477     if(MC_process_is_enabled(process)){
 478       MC_state_interleave_process(initial_graph_state, process);
 479     }
 480   }
 481
 482   reached_pairs = xbt_dynar_new(sizeof(char *), NULL);
 483
 484   MC_take_snapshot(init_snapshot);
 485
 486   MC_UNSET_RAW_MEM;
 487
 488   /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
 489     -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
 490
 491   unsigned int cursor = 0;
 492   unsigned int cursor2 = 0;
 493   xbt_state_t state = NULL;
 494   int res;
 495   xbt_transition_t transition_succ;
 496   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 497   mc_pair_t pair_succ;
 498
 499   xbt_dynar_foreach(a->states, cursor, state){
 500     if(state->type == -1){
 501       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 502         res = MC_automaton_evaluate_label(a, transition_succ->label);
 503
 504         if((res == 1) || (res == 2)){
 505
 506           MC_SET_RAW_MEM;
 507
 508           mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 509           xbt_dynar_push(successors, &mc_initial_pair);
 510
 511           MC_UNSET_RAW_MEM;
 512
 513         }
 514       }
 515     }
 516   }
 517
 518   cursor = 0;
 519
 520   if(xbt_dynar_length(successors) == 0){
 521     xbt_dynar_foreach(a->states, cursor, state){
 522       if(state->type == -1){
 523         MC_SET_RAW_MEM;
 524
 525         mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 526         xbt_dynar_push(successors, &mc_initial_pair);
 527
 528         MC_UNSET_RAW_MEM;
 529       }
 530     }
 531   }
 532
 533   cursor = 0;
 534   xbt_dynar_foreach(successors, cursor, pair_succ){
 535     MC_SET_RAW_MEM;
 536
 537     xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 538
 539     MC_UNSET_RAW_MEM;
 540
 541     if(cursor == 0){
 542       MC_ddfs_with_restore_snapshot(a, 0, 0);
 543     }else{
 544       MC_ddfs_with_restore_snapshot(a, 0, 1);
 545     }
 546   }
 547 }
 548
 549
 550 void MC_ddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int restore){
 551
 552   smx_process_t process = NULL;
 553
 554
 555   if(xbt_fifo_size(mc_snapshot_stack) == 0)
 556     return;
 557
 558   if(restore == 1){
 559     MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
 560     MC_UNSET_RAW_MEM;
 561   }
 562
 563
 564   /* Get current state */
 565   mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 566
 567   if(restore==1){
 568     xbt_swag_foreach(process, simix_global->process_list){
 569       if(MC_process_is_enabled(process)){
 570         MC_state_interleave_process(current_pair->graph_state, process);
 571       }
 572     }
 573   }
 574
 575   XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
 576   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));
 577
 578
 579   mc_stats_pair->visited_pairs++;
 580
 581   int value;
 582   mc_state_t next_graph_state = NULL;
 583   smx_req_t req = NULL;
 584   char *req_str;
 585
 586   mc_pair_t pair_succ;
 587   xbt_transition_t transition_succ;
 588   unsigned int cursor;
 589   int res;
 590
 591   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 592
 593   mc_pair_t next_pair;
 594   mc_snapshot_t next_snapshot;
 595   mc_snapshot_t current_snapshot;
 596
 597
 598   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 599
 600     MC_SET_RAW_MEM;
 601     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 602     MC_take_snapshot(current_snapshot);
 603     MC_UNSET_RAW_MEM;
 604
 605
 606     /* Debug information */
 607     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 608       req_str = MC_request_to_string(req, value);
 609       XBT_DEBUG("Execute: %s", req_str);
 610       xbt_free(req_str);
 611     }
 612
 613     MC_state_set_executed_request(current_pair->graph_state, req, value);
 614
 615     /* Answer the request */
 616     SIMIX_request_pre(req, value);
 617
 618     /* Wait for requests (schedules processes) */
 619     MC_wait_for_requests();
 620
 621
 622     /* Create the new expanded graph_state */
 623     MC_SET_RAW_MEM;
 624
 625     next_graph_state = MC_state_pair_new();
 626
 627     /* Get enabled process and insert it in the interleave set of the next graph_state */
 628     xbt_swag_foreach(process, simix_global->process_list){
 629       if(MC_process_is_enabled(process)){
 630         MC_state_interleave_process(next_graph_state, process);
 631       }
 632     }
 633
 634     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 635     MC_take_snapshot(next_snapshot);
 636
 637     MC_UNSET_RAW_MEM;
 638
 639     xbt_dynar_reset(successors);
 640
 641     cursor = 0;
 642     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 643
 644       res = MC_automaton_evaluate_label(a, transition_succ->label);
 645
 646       MC_SET_RAW_MEM;
 647
 648       if((res == 1) || (res == 2)){ // enabled transition in automaton
 649         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 650         xbt_dynar_push(successors, &next_pair);
 651       }
 652
 653       MC_UNSET_RAW_MEM;
 654     }
 655
 656
 657     if(xbt_dynar_length(successors) == 0){
 658
 659       MC_SET_RAW_MEM;
 660       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
 661       xbt_dynar_push(successors, &next_pair);
 662       MC_UNSET_RAW_MEM;
 663
 664     }
 665
 666
 667     cursor = 0;
 668     xbt_dynar_foreach(successors, cursor, pair_succ){
 669
 670       //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 671
 672       if((search_cycle == 1) && (reached(pair_succ) == 1)){
 673         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 674         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 675         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 676         XBT_INFO("Counter-example that violates formula :");
 677         MC_show_snapshot_stack(mc_snapshot_stack);
 678         MC_dump_snapshot_stack(mc_snapshot_stack);
 679         MC_print_statistics_pairs(mc_stats_pair);
 680         exit(0);
 681       }
 682
 683       mc_stats_pair->executed_transitions++;
 684
 685       MC_SET_RAW_MEM;
 686       xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 687       MC_UNSET_RAW_MEM;
 688
 689       MC_ddfs_with_restore_snapshot(a, search_cycle, 0);
 690
 691       if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 692
 693         MC_restore_snapshot(current_pair->system_state);
 694         MC_UNSET_RAW_MEM;
 695
 696         xbt_swag_foreach(process, simix_global->process_list){
 697           if(MC_process_is_enabled(process)){
 698             MC_state_interleave_process(current_pair->graph_state, process);
 699           }
 700         }
 701
 702         set_pair_reached(current_pair);
 703         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
 704         MC_ddfs_with_restore_snapshot(a, 1, 1);
 705
 706       }
 707     }
 708
 709
 710     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 711       MC_restore_snapshot(current_snapshot);
 712       MC_UNSET_RAW_MEM;
 713     }
 714   }
 715
 716
 717   MC_SET_RAW_MEM;
 718   xbt_fifo_shift(mc_snapshot_stack);
 719   XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
 720   MC_UNSET_RAW_MEM;
 721
 722 }