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)*160);
  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)*160);
  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)*160);
  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)*160) ;
 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)*160);
 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)*160);
 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     if(cursor == 0){
 277       MC_dfs(a, 0, 0);
 278     }else{
 279       MC_dfs(a, 0, 1);
 280     }
 281   }
 282
 283
 284
 285
 286
 287 }
 288
 289
 290 void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
 291
 292   smx_process_t process = NULL;
 293
 294
 295   if(xbt_fifo_size(mc_snapshot_stack) == 0)
 296     return;
 297
 298   if(restore == 1){
 299     MC_restore_snapshot(((mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
 300     MC_UNSET_RAW_MEM;
 301   }
 302
 303
 304   /* Get current state */
 305   mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 306
 307   if(restore==1){
 308     xbt_swag_foreach(process, simix_global->process_list){
 309       if(MC_process_is_enabled(process)){
 310         //XBT_DEBUG("Pid : %lu", process->pid);
 311         MC_state_interleave_process(current_pair->graph_state, process);
 312       }
 313     }
 314   }
 315
 316   XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
 317   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));
 318
 319
 320   mc_stats_pair->visited_pairs++;
 321
 322   int value;
 323   mc_state_t next_graph_state = NULL;
 324   smx_req_t req = NULL;
 325   char *req_str;
 326
 327   mc_pairs_t pair_succ;
 328   xbt_transition_t transition_succ;
 329   unsigned int cursor;
 330   int res;
 331   //int enabled_transition = 0;
 332
 333   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
 334
 335   mc_pairs_t next_pair;
 336   mc_snapshot_t next_snapshot;
 337   mc_snapshot_t current_snapshot;
 338
 339
 340   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 341
 342     MC_SET_RAW_MEM;
 343     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 344     MC_take_snapshot(current_snapshot);
 345     MC_UNSET_RAW_MEM;
 346
 347
 348     /* Debug information */
 349     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 350       req_str = MC_request_to_string(req, value);
 351       XBT_DEBUG("Execute: %s", req_str);
 352       xbt_free(req_str);
 353     }
 354
 355     MC_state_set_executed_request(current_pair->graph_state, req, value);
 356
 357     /* Answer the request */
 358     SIMIX_request_pre(req, value);
 359
 360     /* Wait for requests (schedules processes) */
 361     MC_wait_for_requests();
 362
 363
 364     /* Create the new expanded graph_state */
 365     MC_SET_RAW_MEM;
 366
 367     next_graph_state = MC_state_pair_new();
 368
 369     /* Get enabled process and insert it in the interleave set of the next graph_state */
 370     xbt_swag_foreach(process, simix_global->process_list){
 371       if(MC_process_is_enabled(process)){
 372         MC_state_interleave_process(next_graph_state, process);
 373       }
 374     }
 375
 376     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 377     MC_take_snapshot(next_snapshot);
 378
 379     MC_UNSET_RAW_MEM;
 380
 381     xbt_dynar_reset(successors);
 382
 383     cursor = 0;
 384     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 385
 386       res = MC_automaton_evaluate_label(a, transition_succ->label);
 387
 388       MC_SET_RAW_MEM;
 389
 390       if((res == 1) || (res == 2)){ // enabled transition in automaton
 391         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 392         xbt_dynar_push(successors, &next_pair);
 393       }
 394
 395       MC_UNSET_RAW_MEM;
 396     }
 397
 398
 399     if(xbt_dynar_length(successors) == 0){
 400
 401       MC_SET_RAW_MEM;
 402       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
 403       xbt_dynar_push(successors, &next_pair);
 404       MC_UNSET_RAW_MEM;
 405
 406     }
 407
 408
 409     cursor = 0;
 410     xbt_dynar_foreach(successors, cursor, pair_succ){
 411
 412       //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 413
 414       if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){
 415         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 416         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 417         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 418         XBT_INFO("Counter-example that violates formula :");
 419         MC_show_snapshot_stack(mc_snapshot_stack);
 420         MC_dump_snapshot_stack(mc_snapshot_stack);
 421         MC_print_statistics_pairs(mc_stats_pair);
 422         exit(0);
 423       }
 424
 425       if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
 426
 427         //XBT_DEBUG("Unvisited pair !");
 428
 429         mc_stats_pair->executed_transitions++;
 430
 431         MC_SET_RAW_MEM;
 432         xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 433         set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
 434         MC_UNSET_RAW_MEM;
 435
 436         MC_dfs(a, search_cycle, 0);
 437
 438         if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 439
 440           MC_restore_snapshot(current_pair->system_state);
 441           MC_UNSET_RAW_MEM;
 442
 443           xbt_swag_foreach(process, simix_global->process_list){
 444             if(MC_process_is_enabled(process)){
 445               //XBT_DEBUG("Pid : %lu", process->pid);
 446               MC_state_interleave_process(current_pair->graph_state, process);
 447             }
 448           }
 449
 450           set_pair_reached(current_pair->graph_state, current_pair->automaton_state);
 451           XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
 452           MC_dfs(a, 1, 1);
 453
 454         }
 455       }else{
 456
 457         XBT_DEBUG("Pair already visited !");
 458
 459       }
 460     }
 461
 462
 463     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 464       MC_restore_snapshot(current_snapshot);
 465       MC_UNSET_RAW_MEM;
 466       //XBT_DEBUG("Snapshot restored");
 467     }
 468   }
 469
 470
 471   MC_SET_RAW_MEM;
 472   //remove_pair_reached(current_pair->graph_state);
 473   xbt_fifo_shift(mc_snapshot_stack);
 474   XBT_DEBUG("State (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
 475   MC_UNSET_RAW_MEM;
 476
 477 }
 478
 479 void MC_show_snapshot_stack(xbt_fifo_t stack){
 480   int value;
 481   mc_pairs_t pair;
 482   xbt_fifo_item_t item;
 483   smx_req_t req;
 484   char *req_str = NULL;
 485
 486   for (item = xbt_fifo_get_last_item(stack);
 487        (item ? (pair = (mc_pairs_t) (xbt_fifo_get_item_content(item)))
 488         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 489     req = MC_state_get_executed_request(pair->graph_state, &value);
 490     if(req){
 491       req_str = MC_request_to_string(req, value);
 492       XBT_INFO("%s", req_str);
 493       xbt_free(req_str);
 494     }
 495   }
 496 }
 497
 498 void MC_dump_snapshot_stack(xbt_fifo_t stack){
 499   mc_pairs_t pair;
 500
 501   MC_SET_RAW_MEM;
 502   while ((pair = (mc_pairs_t) xbt_fifo_pop(stack)) != NULL)
 503     MC_pair_delete(pair);
 504   MC_UNSET_RAW_MEM;
 505 }
 506
 507 void MC_pair_delete(mc_pairs_t pair){
 508   xbt_free(pair->graph_state->proc_status);
 509   xbt_free(pair->graph_state);
 510   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 511   xbt_free(pair);
 512 }
 513
 514
 515 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 516
 517   switch(l->type){
 518   case 0 : {
 519     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 520     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 521     return (left_res || right_res);
 522     break;
 523   }
 524   case 1 : {
 525     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 526     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 527     return (left_res && right_res);
 528     break;
 529   }
 530   case 2 : {
 531     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
 532     return (!res);
 533     break;
 534   }
 535   case 3 : {
 536     unsigned int cursor = 0;
 537     xbt_propositional_symbol_t p = NULL;
 538     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
 539       if(strcmp(p->pred, l->u.predicat) == 0){
 540         int (*f)() = p->function;
 541         return (*f)();
 542       }
 543     }
 544     return -1;
 545     break;
 546   }
 547   case 4 : {
 548     return 2;
 549     break;
 550   }
 551   default :
 552     return -1;
 553   }
 554 }
 555
 556
 557 /********************* Double DFS using color pair *********************/
 558
 559
 560
 561
 562
 563
 564 /********************* DPOR without replay *********************/
 565
 566
 567
 568 void MC_dpor_with_restore_snapshot_init(xbt_automaton_t a){
 569
 570   XBT_DEBUG("**************************************************");
 571   XBT_DEBUG("DPOR (with restore snapshot) init");
 572   XBT_DEBUG("**************************************************");
 573
 574   mc_pairs_t initial_pair;
 575   mc_state_t initial_graph_state;
 576   smx_process_t process;
 577   mc_snapshot_t initial_snapshot;
 578
 579   MC_wait_for_requests();
 580
 581   MC_SET_RAW_MEM;
 582
 583   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 584
 585   initial_graph_state = MC_state_pair_new();
 586   xbt_swag_foreach(process, simix_global->process_list){
 587     if(MC_process_is_enabled(process)){
 588       MC_state_interleave_process(initial_graph_state, process);
 589       break;
 590     }
 591   }
 592
 593   visited_pairs = xbt_dynar_new(sizeof(mc_visited_pairs_t), NULL);
 594   reached_pairs = xbt_dynar_new(sizeof(mc_reached_pairs_t), NULL);
 595
 596   MC_take_snapshot(initial_snapshot);
 597
 598   MC_UNSET_RAW_MEM;
 599
 600   unsigned int cursor = 0;
 601   unsigned int cursor2 = 0;
 602   xbt_state_t state = NULL;
 603   int res;
 604   xbt_transition_t transition_succ;
 605
 606   xbt_dynar_foreach(a->states, cursor, state){
 607     if(state->type == -1){
 608       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 609         res = MC_automaton_evaluate_label(a, transition_succ->label);
 610
 611         if((res == 1) || (res == 2)){
 612
 613           MC_SET_RAW_MEM;
 614
 615           initial_pair = new_pair(initial_snapshot, initial_graph_state, transition_succ->dst);
 616           xbt_fifo_unshift(mc_snapshot_stack, initial_pair);
 617
 618           MC_UNSET_RAW_MEM;
 619
 620           /* Add pair to list of visited pairs*/
 621           set_pair_visited(initial_pair->graph_state, initial_pair->automaton_state, 0);
 622
 623           MC_dpor_with_restore_snapshot(a, 0, 0);
 624
 625           break;
 626
 627         }
 628       }
 629     }
 630
 631     if(xbt_fifo_size(mc_snapshot_stack)>0)
 632       break;
 633   }
 634
 635   /* Initial state of automaton is initial state for initial pair*/
 636   if(xbt_fifo_size(mc_snapshot_stack) == 0){
 637
 638     cursor = 0;
 639
 640     xbt_dynar_foreach(a->states, cursor, state){
 641       if(state->type == -1){
 642
 643         MC_SET_RAW_MEM;
 644
 645         initial_pair = new_pair(initial_snapshot, initial_graph_state, state);
 646         xbt_fifo_unshift(mc_snapshot_stack, initial_pair);
 647
 648         MC_UNSET_RAW_MEM;
 649
 650         /* Add pair to list of visited pairs*/
 651         set_pair_visited(initial_pair->graph_state, initial_pair->automaton_state, 0);
 652
 653         MC_dpor_with_restore_snapshot(a, 0, 0);
 654
 655         break;
 656       }
 657     }
 658
 659   }
 660
 661 }
 662
 663
 664 /* 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 */
 665 void MC_dpor_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int restore){
 666
 667   smx_process_t process = NULL;
 668
 669   if(xbt_fifo_size(mc_snapshot_stack) == 0)
 670     return;
 671
 672   int value;
 673   mc_state_t next_graph_state = NULL;
 674   smx_req_t req = NULL, prev_req = NULL;
 675   char *req_str;
 676   xbt_fifo_item_t item = NULL;
 677
 678   xbt_transition_t transition_succ;
 679   unsigned int cursor;
 680   int res;
 681
 682   mc_pairs_t next_pair;
 683   mc_snapshot_t next_snapshot;
 684   mc_snapshot_t current_snapshot;
 685   mc_pairs_t current_pair;
 686   mc_pairs_t prev_pair;
 687   int new_pair_created;
 688
 689   while(xbt_fifo_size(mc_snapshot_stack) > 0){
 690
 691     current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 692
 693
 694     XBT_DEBUG("**************************************************");
 695     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));
 696
 697     mc_stats_pair->visited_pairs++;
 698
 699     /* Add pair to list of visited pairs*/
 700     set_pair_visited(current_pair->graph_state, current_pair->automaton_state, search_cycle);
 701
 702     if((xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH) && (req = MC_state_get_request(current_pair->graph_state, &value))){
 703
 704       MC_SET_RAW_MEM;
 705       current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 706       MC_take_snapshot(current_snapshot);
 707       MC_UNSET_RAW_MEM;
 708
 709       /* Debug information */
 710       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 711         req_str = MC_request_to_string(req, value);
 712         XBT_DEBUG("Execute: %s", req_str);
 713         xbt_free(req_str);
 714       }
 715
 716       MC_state_set_executed_request(current_pair->graph_state, req, value);
 717
 718       /* Answer the request */
 719       SIMIX_request_pre(req, value);
 720
 721       /* Wait for requests (schedules processes) */
 722       MC_wait_for_requests();
 723
 724       /* Create the new expanded graph_state */
 725       MC_SET_RAW_MEM;
 726
 727       next_graph_state = MC_state_pair_new();
 728
 729       /* Get an enabled process and insert it in the interleave set of the next graph_state */
 730       xbt_swag_foreach(process, simix_global->process_list){
 731         if(MC_process_is_enabled(process)){
 732           MC_state_interleave_process(next_graph_state, process);
 733           break;
 734         }
 735       }
 736
 737       next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 738       MC_take_snapshot(next_snapshot);
 739
 740       MC_UNSET_RAW_MEM;
 741
 742       new_pair_created = 0;
 743
 744       cursor = 0;
 745       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 746         res = MC_automaton_evaluate_label(a, transition_succ->label);
 747
 748         if((res == 1) || (res == 2)){
 749
 750           MC_SET_RAW_MEM;
 751           next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 752           xbt_fifo_unshift(mc_snapshot_stack, next_pair);
 753           MC_UNSET_RAW_MEM;
 754
 755           new_pair_created = 1;
 756
 757           break;
 758
 759         }
 760       }
 761
 762       /* Pas d'avancement possible dans l'automate */
 763       if(new_pair_created == 0){
 764
 765         MC_SET_RAW_MEM;
 766         next_pair = new_pair(next_snapshot,next_graph_state,current_pair->automaton_state);
 767         xbt_fifo_unshift(mc_snapshot_stack, next_pair);
 768         MC_UNSET_RAW_MEM;
 769
 770       }
 771
 772     }else{
 773       XBT_DEBUG("There are no more processes to interleave.");
 774
 775       /* Trash the current state, no longer needed */
 776       MC_SET_RAW_MEM;
 777       xbt_fifo_shift(mc_snapshot_stack);
 778       MC_UNSET_RAW_MEM;
 779
 780       while((current_pair = xbt_fifo_shift(mc_snapshot_stack)) != NULL){
 781         req = MC_state_get_internal_request(current_pair->graph_state);
 782         xbt_fifo_foreach(mc_snapshot_stack, item, prev_pair, mc_pairs_t) {
 783           if(MC_request_depend(req, MC_state_get_internal_request(prev_pair->graph_state))){
 784             if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 785               XBT_DEBUG("Dependent Transitions:");
 786               prev_req = MC_state_get_executed_request(prev_pair->graph_state, &value);
 787               req_str = MC_request_to_string(prev_req, value);
 788               XBT_DEBUG("%s (state=%p)", req_str, prev_pair->graph_state);
 789               xbt_free(req_str);
 790               prev_req = MC_state_get_executed_request(current_pair->graph_state, &value);
 791               req_str = MC_request_to_string(prev_req, value);
 792               XBT_DEBUG("%s (state=%p)", req_str, current_pair->graph_state);
 793               xbt_free(req_str);
 794             }
 795
 796             if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer)){
 797               MC_state_interleave_process(prev_pair->graph_state, req->issuer);
 798
 799             } else {
 800               XBT_DEBUG("Process %p is in done set", req->issuer);
 801             }
 802
 803             break;
 804           }
 805         }
 806
 807         if(MC_state_interleave_size(current_pair->graph_state)){
 808           MC_restore_snapshot(current_pair->system_state);
 809           xbt_fifo_unshift(mc_snapshot_stack, current_pair);
 810           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));
 811           MC_UNSET_RAW_MEM;
 812           break;
 813         }
 814       }
 815
 816       MC_UNSET_RAW_MEM;
 817
 818     }
 819   }
 820   MC_UNSET_RAW_MEM;
 821   return;
 822 }