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