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