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 xbt_dynar_t reached_pairs;
   9 xbt_dynar_t successors = NULL;
  10 extern mc_snapshot_t initial_snapshot;
  11
  12 /* Global variables for stateless algorithm */
  13 mc_snapshot_t snapshot = NULL;
  14
  15 /* Global variables for stateful algorithm */
  16 mc_snapshot_t next_snapshot = NULL;
  17 mc_snapshot_t current_snapshot = NULL;
  18
  19
  20 mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
  21   mc_pair_t p = NULL;
  22   p = xbt_new0(s_mc_pair_t, 1);
  23   p->system_state = sn;
  24   p->automaton_state = st;
  25   p->graph_state = sg;
  26   mc_stats_pair->expanded_pairs++;
  27   return p;
  28
  29 }
  30
  31 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
  32
  33   if(s1->num_reg != s2->num_reg)
  34     return 1;
  35
  36   int i, errors=0;
  37
  38   for(i=0 ; i< s1->num_reg ; i++){
  39
  40     if(s1->regions[i]->size != s2->regions[i]->size)
  41       return 1;
  42
  43     if(s1->regions[i]->start_addr != s2->regions[i]->start_addr)
  44       return 1;
  45
  46     if(s1->regions[i]->type != s2->regions[i]->type)
  47       return 1;
  48
  49     if(s1->regions[i]->type == 0){
  50       if(mmalloc_compare_heap(s1->regions[i]->start_addr, s2->regions[i]->start_addr)){
  51         XBT_DEBUG("Different heap (mmalloc_compare)");
  52         sleep(1);
  53         errors++;
  54       }
  55     }else{
  56       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
  57         XBT_DEBUG("Different memcmp for data in libsimgrid");
  58         sleep(1);
  59         errors++;
  60       }
  61     }
  62
  63
  64   }
  65
  66   return (errors>0);
  67
  68 }
  69
  70 int reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s){
  71
  72
  73   if(xbt_dynar_is_empty(reached_pairs)){
  74     return 0;
  75   }else{
  76     MC_SET_RAW_MEM;
  77
  78     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
  79
  80     /* Get values of propositional symbols */
  81     unsigned int cursor = 0;
  82     xbt_propositional_symbol_t ps = NULL;
  83     xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
  84       int (*f)() = ps->function;
  85       int res = (*f)();
  86       xbt_dynar_push_as(prop_ato, int, res);
  87     }
  88
  89     cursor = 0;
  90     mc_pair_reached_t pair_test;
  91
  92     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
  93       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
  94         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
  95           if(snapshot_compare(pair_test->system_state, s) == 0){
  96             MC_UNSET_RAW_MEM;
  97             return 1;
  98           }
  99         }
 100       }
 101     }
 102
 103     MC_UNSET_RAW_MEM;
 104     return 0;
 105
 106   }
 107 }
 108
 109 void set_pair_reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t sn){
 110
 111
 112   MC_SET_RAW_MEM;
 113
 114   mc_pair_reached_t pair = NULL;
 115   pair = xbt_new0(s_mc_pair_reached_t, 1);
 116   pair->automaton_state = st;
 117   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 118   pair->system_state = sn;
 119
 120   /* Get values of propositional symbols */
 121   unsigned int cursor = 0;
 122   xbt_propositional_symbol_t ps = NULL;
 123   xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 124     int (*f)() = ps->function;
 125     int res = (*f)();
 126     xbt_dynar_push_as(pair->prop_ato, int, res);
 127   }
 128
 129   xbt_dynar_push(reached_pairs, &pair);
 130
 131   MC_UNSET_RAW_MEM;
 132
 133
 134 }
 135
 136 void MC_pair_delete(mc_pair_t pair){
 137   xbt_free(pair->graph_state->proc_status);
 138   xbt_free(pair->graph_state);
 139   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 140   xbt_free(pair);
 141 }
 142
 143
 144
 145 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 146
 147   switch(l->type){
 148   case 0 : {
 149     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 150     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 151     return (left_res || right_res);
 152     break;
 153   }
 154   case 1 : {
 155     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 156     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 157     return (left_res && right_res);
 158     break;
 159   }
 160   case 2 : {
 161     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
 162     return (!res);
 163     break;
 164   }
 165   case 3 : {
 166     unsigned int cursor = 0;
 167     xbt_propositional_symbol_t p = NULL;
 168     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
 169       if(strcmp(p->pred, l->u.predicat) == 0){
 170         int (*f)() = p->function;
 171         return (*f)();
 172       }
 173     }
 174     return -1;
 175     break;
 176   }
 177   case 4 : {
 178     return 2;
 179     break;
 180   }
 181   default :
 182     return -1;
 183   }
 184 }
 185
 186
 187
 188
 189
 190 /********************* Double-DFS stateless *******************/
 191
 192 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 193   xbt_free(pair->graph_state->proc_status);
 194   xbt_free(pair->graph_state);
 195   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 196   xbt_free(pair);
 197 }
 198
 199 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 200   mc_pair_stateless_t p = NULL;
 201   p = xbt_new0(s_mc_pair_stateless_t, 1);
 202   p->automaton_state = st;
 203   p->graph_state = sg;
 204   p->requests = r;
 205   mc_stats_pair->expanded_pairs++;
 206   return p;
 207 }
 208
 209
 210
 211 void MC_ddfs_stateless_init(xbt_automaton_t a){
 212
 213   XBT_DEBUG("**************************************************");
 214   XBT_DEBUG("Double-DFS stateless init");
 215   XBT_DEBUG("**************************************************");
 216
 217   mc_pair_stateless_t mc_initial_pair = NULL;
 218   mc_state_t initial_graph_state = NULL;
 219   smx_process_t process;
 220
 221   MC_wait_for_requests();
 222
 223   MC_SET_RAW_MEM;
 224
 225   initial_graph_state = MC_state_pair_new();
 226   xbt_swag_foreach(process, simix_global->process_list){
 227     if(MC_process_is_enabled(process)){
 228       MC_state_interleave_process(initial_graph_state, process);
 229     }
 230   }
 231
 232   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
 233   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 234   snapshot = xbt_new0(s_mc_snapshot_t, 1);
 235
 236   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 237   MC_take_snapshot(initial_snapshot);
 238
 239   MC_UNSET_RAW_MEM;
 240
 241   unsigned int cursor = 0;
 242   xbt_state_t state;
 243
 244   xbt_dynar_foreach(a->states, cursor, state){
 245     if(state->type == -1){
 246
 247       MC_SET_RAW_MEM;
 248       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 249       xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 250       MC_UNSET_RAW_MEM;
 251
 252       if(cursor == 0){
 253         MC_ddfs_stateless(a, 0, 0);
 254       }else{
 255         MC_restore_snapshot(initial_snapshot);
 256         MC_UNSET_RAW_MEM;
 257         MC_ddfs_stateless(a, 0, 0);
 258       }
 259     }else{
 260       if(state->type == 2){
 261
 262         MC_SET_RAW_MEM;
 263         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 264         xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 265         MC_UNSET_RAW_MEM;
 266
 267         if(cursor == 0){
 268           MC_ddfs_stateless(a, 1, 0);
 269         }else{
 270           MC_restore_snapshot(initial_snapshot);
 271           MC_UNSET_RAW_MEM;
 272           MC_ddfs_stateless(a, 1, 0);
 273         }
 274       }
 275     }
 276   }
 277
 278 }
 279
 280
 281 void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
 282
 283   smx_process_t process;
 284   mc_pair_stateless_t current_pair = NULL;
 285
 286   if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
 287     return;
 288
 289   if(replay == 1){
 290     MC_replay_liveness(mc_stack_liveness_stateless);
 291     current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 292     xbt_swag_foreach(process, simix_global->process_list){
 293       if(MC_process_is_enabled(process)){
 294         MC_state_interleave_process(current_pair->graph_state, process);
 295       }
 296     }
 297   }
 298
 299   /* Get current pair */
 300   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 301
 302   /* Update current state in buchi automaton */
 303   a->current_state = current_pair->automaton_state;
 304
 305
 306   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
 307   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));
 308
 309
 310   mc_stats_pair->visited_pairs++;
 311
 312   int value;
 313   mc_state_t next_graph_state = NULL;
 314   smx_req_t req = NULL;
 315   char *req_str;
 316
 317   xbt_transition_t transition_succ;
 318   unsigned int cursor = 0;
 319   int res;
 320
 321   mc_pair_stateless_t next_pair = NULL;
 322   mc_pair_stateless_t pair_succ;
 323
 324
 325   if(MC_state_interleave_size(current_pair->graph_state) > 0){
 326
 327     while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL && (xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS)){
 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       //sleep(1);
 337
 338       MC_state_set_executed_request(current_pair->graph_state, req, value);
 339
 340       /* Answer the request */
 341       SIMIX_request_pre(req, value);
 342
 343       /* Wait for requests (schedules processes) */
 344       MC_wait_for_requests();
 345
 346
 347       MC_SET_RAW_MEM;
 348
 349       /* Create the new expanded graph_state */
 350       next_graph_state = MC_state_pair_new();
 351
 352       /* Get enabled process and insert it in the interleave set of the next graph_state */
 353       xbt_swag_foreach(process, simix_global->process_list){
 354         if(MC_process_is_enabled(process)){
 355           MC_state_interleave_process(next_graph_state, process);
 356         }
 357       }
 358
 359       xbt_dynar_reset(successors);
 360
 361       MC_UNSET_RAW_MEM;
 362
 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         if(res == 1){ // enabled transition in automaton
 370           MC_SET_RAW_MEM;
 371           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 372           xbt_dynar_push(successors, &next_pair);
 373           MC_UNSET_RAW_MEM;
 374         }
 375
 376       }
 377
 378       cursor = 0;
 379
 380       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 381
 382         res = MC_automaton_evaluate_label(a, transition_succ->label);
 383
 384         if(res == 2){ // true transition in automaton
 385           MC_SET_RAW_MEM;
 386           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 387           xbt_dynar_push(successors, &next_pair);
 388           MC_UNSET_RAW_MEM;
 389         }
 390
 391       }
 392
 393
 394       if(xbt_dynar_length(successors) == 0){
 395         MC_SET_RAW_MEM;
 396         next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state, MC_state_interleave_size(next_graph_state));
 397         xbt_dynar_push(successors, &next_pair);
 398         MC_UNSET_RAW_MEM;
 399       }
 400
 401       cursor = 0;
 402
 403       xbt_dynar_foreach(successors, cursor, pair_succ){
 404
 405
 406
 407         if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) ){
 408
 409           MC_SET_RAW_MEM;
 410           MC_take_snapshot(snapshot);
 411           MC_UNSET_RAW_MEM;
 412
 413           if(reached(a, pair_succ->automaton_state, snapshot) == 1){
 414
 415             XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1);
 416
 417             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 418             XBT_INFO("|             ACCEPTANCE CYCLE            |");
 419             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 420             XBT_INFO("Counter-example that violates formula :");
 421             MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 422             MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 423             MC_print_statistics_pairs(mc_stats_pair);
 424             exit(0);
 425           }
 426         }
 427
 428
 429         if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 430           XBT_DEBUG("Take snapshot of acceptance pair (depth = %d)", xbt_fifo_size(mc_stack_liveness_stateless) + 1 );
 431           MC_SET_RAW_MEM;
 432           MC_take_snapshot(snapshot);
 433           MC_UNSET_RAW_MEM;
 434         }
 435
 436         MC_SET_RAW_MEM;
 437         xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 438         MC_UNSET_RAW_MEM;
 439
 440         MC_ddfs_stateless(a, search_cycle, 0);
 441
 442
 443         if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 444
 445           XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 446
 447
 448           set_pair_reached(a, pair_succ->automaton_state, snapshot);
 449
 450
 451           /* Pair shifted from stack when first MC_ddfs finished and returned at this point */
 452           MC_SET_RAW_MEM;
 453           xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 454           MC_UNSET_RAW_MEM;
 455
 456           MC_ddfs_stateless(a, 1, 1);
 457
 458           /* No acceptance cycle with this acceptance pair, we remove it from the list reached_pairs */
 459           MC_SET_RAW_MEM;
 460           xbt_dynar_pop(reached_pairs, NULL);
 461           MC_UNSET_RAW_MEM;
 462
 463         }
 464       }
 465
 466
 467       XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
 468       MC_replay_liveness(mc_stack_liveness_stateless);
 469
 470     }
 471
 472
 473   }else{  /*No request to execute, search evolution in Büchi automaton */
 474
 475     if((xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS)){
 476
 477       // MC_state_set_executed_request(current_pair->graph_state, NULL, value);
 478
 479       /* Answer the request */
 480       //SIMIX_request_pre(req, value);
 481
 482       /* Wait for requests (schedules processes) */
 483       //MC_wait_for_requests();
 484
 485       MC_SET_RAW_MEM;
 486
 487       /* Create the new expanded graph_state */
 488       next_graph_state = MC_state_pair_new();
 489
 490       xbt_dynar_reset(successors);
 491
 492       MC_UNSET_RAW_MEM;
 493
 494
 495       cursor= 0;
 496       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 497
 498         res = MC_automaton_evaluate_label(a, transition_succ->label);
 499
 500         if(res == 1){ // enabled transition in automaton
 501           MC_SET_RAW_MEM;
 502           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 503           xbt_dynar_push(successors, &next_pair);
 504           MC_UNSET_RAW_MEM;
 505         }
 506
 507       }
 508
 509       cursor = 0;
 510
 511       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 512
 513         res = MC_automaton_evaluate_label(a, transition_succ->label);
 514
 515         if(res == 2){ // true transition in automaton
 516           MC_SET_RAW_MEM;
 517           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 518           xbt_dynar_push(successors, &next_pair);
 519           MC_UNSET_RAW_MEM;
 520         }
 521
 522       }
 523
 524
 525       if(xbt_dynar_length(successors) == 0){
 526         MC_SET_RAW_MEM;
 527         next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state, MC_state_interleave_size(next_graph_state));
 528         xbt_dynar_push(successors, &next_pair);
 529         MC_UNSET_RAW_MEM;
 530       }
 531
 532       cursor = 0;
 533
 534       xbt_dynar_foreach(successors, cursor, pair_succ){
 535
 536         if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) ){
 537
 538           MC_SET_RAW_MEM;
 539           MC_take_snapshot(snapshot);
 540           MC_UNSET_RAW_MEM;
 541
 542           if(reached(a, pair_succ->automaton_state, snapshot) == 1){
 543
 544             XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1);
 545
 546             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 547             XBT_INFO("|             ACCEPTANCE CYCLE            |");
 548             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 549             XBT_INFO("Counter-example that violates formula :");
 550             MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 551             MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 552             MC_print_statistics_pairs(mc_stats_pair);
 553             exit(0);
 554           }
 555         }
 556
 557
 558         if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 559           XBT_DEBUG("Take snapshot of acceptance pair (depth = %d)", xbt_fifo_size(mc_stack_liveness_stateless) + 1 );
 560           MC_SET_RAW_MEM;
 561           MC_take_snapshot(snapshot);
 562           MC_UNSET_RAW_MEM;
 563         }
 564
 565         MC_SET_RAW_MEM;
 566         xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 567         MC_UNSET_RAW_MEM;
 568
 569         MC_ddfs_stateless(a, search_cycle, 0);
 570
 571
 572         if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 573
 574           XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 575
 576
 577           set_pair_reached(a, pair_succ->automaton_state, snapshot);
 578
 579
 580           /* Pair shifted from stack when first MC_ddfs finished and returned at this point */
 581           MC_SET_RAW_MEM;
 582           xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 583           MC_UNSET_RAW_MEM;
 584
 585           MC_ddfs_stateless(a, 1, 1);
 586
 587           /* No acceptance cycle with this acceptance pair, we remove it from the list reached_pairs */
 588           MC_SET_RAW_MEM;
 589           xbt_dynar_pop(reached_pairs, NULL);
 590           MC_UNSET_RAW_MEM;
 591
 592         }
 593       }
 594     }
 595
 596   }
 597
 598   MC_SET_RAW_MEM;
 599   xbt_fifo_shift(mc_stack_liveness_stateless);
 600   XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
 601   MC_UNSET_RAW_MEM;
 602
 603 }
 604
 605 /********************* Double-DFS stateful without visited state *******************/
 606
 607
 608 void MC_ddfs_stateful_init(xbt_automaton_t a){
 609
 610   XBT_DEBUG("**************************************************");
 611   XBT_DEBUG("Double-DFS stateful without visited state init");
 612   XBT_DEBUG("**************************************************");
 613
 614   mc_pair_t mc_initial_pair;
 615   mc_state_t initial_graph_state;
 616   smx_process_t process;
 617   mc_snapshot_t init_snapshot;
 618
 619   MC_wait_for_requests();
 620
 621   MC_SET_RAW_MEM;
 622
 623   initial_graph_state = MC_state_pair_new();
 624   xbt_swag_foreach(process, simix_global->process_list){
 625     if(MC_process_is_enabled(process)){
 626       MC_state_interleave_process(initial_graph_state, process);
 627     }
 628   }
 629
 630   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
 631   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 632   current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 633   next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 634
 635   init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 636   MC_take_snapshot(init_snapshot);
 637
 638   MC_UNSET_RAW_MEM;
 639
 640   unsigned int cursor = 0;
 641   xbt_state_t state = NULL;
 642
 643   xbt_dynar_foreach(a->states, cursor, state){
 644     if(state->type == -1){
 645
 646       MC_SET_RAW_MEM;
 647       mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
 648       xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
 649       MC_UNSET_RAW_MEM;
 650
 651       if(cursor == 0){
 652         MC_ddfs_stateful(a, 0, 0);
 653       }else{
 654         MC_restore_snapshot(init_snapshot);
 655         MC_UNSET_RAW_MEM;
 656         MC_ddfs_stateful(a, 0, 0);
 657       }
 658     }else{
 659        if(state->type == 2){
 660
 661          MC_SET_RAW_MEM;
 662          mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
 663          xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
 664          MC_UNSET_RAW_MEM;
 665
 666          if(cursor == 0){
 667            MC_ddfs_stateful(a, 1, 0);
 668          }else{
 669            MC_restore_snapshot(init_snapshot);
 670            MC_UNSET_RAW_MEM;
 671            MC_ddfs_stateful(a, 1, 0);
 672          }
 673        }
 674     }
 675   }
 676 }
 677
 678
 679 void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 680
 681   smx_process_t process = NULL;
 682   mc_pair_t current_pair = NULL;
 683
 684   if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
 685     return;
 686
 687   if(restore == 1){
 688     current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 689     MC_restore_snapshot(current_pair->system_state);
 690     xbt_swag_foreach(process, simix_global->process_list){
 691       if(MC_process_is_enabled(process)){
 692         MC_state_interleave_process(current_pair->graph_state, process);
 693       }
 694     }
 695     MC_UNSET_RAW_MEM;
 696   }
 697
 698   /* Get current state */
 699   current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 700
 701
 702   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle);
 703   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));
 704
 705   a->current_state = current_pair->automaton_state;
 706
 707   //sleep(1);
 708
 709   mc_stats_pair->visited_pairs++;
 710
 711   int value;
 712   mc_state_t next_graph_state = NULL;
 713   smx_req_t req = NULL;
 714   char *req_str;
 715
 716   mc_pair_t pair_succ;
 717   xbt_transition_t transition_succ;
 718   unsigned int cursor;
 719   int res;
 720
 721   mc_pair_t next_pair = NULL;
 722
 723   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 724
 725     MC_SET_RAW_MEM;
 726     MC_take_snapshot(current_snapshot);
 727     MC_UNSET_RAW_MEM;
 728
 729     /* Debug information */
 730     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 731       req_str = MC_request_to_string(req, value);
 732       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));
 733       XBT_DEBUG("Execute: %s", req_str);
 734       xbt_free(req_str);
 735     }
 736
 737     MC_state_set_executed_request(current_pair->graph_state, req, value);
 738
 739     /* Answer the request */
 740     SIMIX_request_pre(req, value);
 741
 742     /* Wait for requests (schedules processes) */
 743     MC_wait_for_requests();
 744
 745
 746     /* Create the new expanded graph_state */
 747     MC_SET_RAW_MEM;
 748
 749     next_graph_state = MC_state_pair_new();
 750
 751     /* Get enabled process and insert it in the interleave set of the next graph_state */
 752     xbt_swag_foreach(process, simix_global->process_list){
 753       if(MC_process_is_enabled(process)){
 754         MC_state_interleave_process(next_graph_state, process);
 755       }
 756     }
 757
 758     MC_take_snapshot(next_snapshot);
 759
 760     xbt_dynar_reset(successors);
 761
 762     MC_UNSET_RAW_MEM;
 763
 764
 765     cursor = 0;
 766     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 767
 768       res = MC_automaton_evaluate_label(a, transition_succ->label);
 769
 770       if(res == 1){ // enabled transition in automaton
 771         MC_SET_RAW_MEM;
 772         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 773         xbt_dynar_push(successors, &next_pair);
 774         MC_UNSET_RAW_MEM;
 775       }
 776
 777     }
 778
 779     cursor = 0;
 780     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 781
 782       res = MC_automaton_evaluate_label(a, transition_succ->label);
 783
 784       if(res == 2){ // transition always enabled in automaton
 785         MC_SET_RAW_MEM;
 786         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 787         xbt_dynar_push(successors, &next_pair);
 788         MC_UNSET_RAW_MEM;
 789       }
 790
 791
 792     }
 793
 794
 795     if(xbt_dynar_length(successors) == 0){
 796
 797       MC_SET_RAW_MEM;
 798       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
 799       xbt_dynar_push(successors, &next_pair);
 800       MC_UNSET_RAW_MEM;
 801
 802     }
 803
 804     cursor = 0;
 805     xbt_dynar_foreach(successors, cursor, pair_succ){
 806
 807       if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 808
 809         if(reached(a, pair_succ->automaton_state, next_snapshot) == 1){
 810           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 811           XBT_INFO("|             ACCEPTANCE CYCLE            |");
 812           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 813           XBT_INFO("Counter-example that violates formula :");
 814           MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
 815           MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
 816           MC_print_statistics_pairs(mc_stats_pair);
 817           exit(1);
 818         }
 819       }
 820
 821
 822       MC_SET_RAW_MEM;
 823       xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 824       MC_UNSET_RAW_MEM;
 825
 826       MC_ddfs_stateful(a, search_cycle, 0);
 827
 828
 829       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 830
 831         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 832         set_pair_reached(a, pair_succ->automaton_state, next_snapshot);
 833
 834         MC_SET_RAW_MEM;
 835         xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 836         MC_UNSET_RAW_MEM;
 837
 838         MC_ddfs_stateful(a, 1, 0);
 839
 840
 841         MC_SET_RAW_MEM;
 842         xbt_dynar_pop(reached_pairs, NULL);
 843         MC_UNSET_RAW_MEM;
 844       }
 845
 846     }
 847
 848     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 849       XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateful));
 850       MC_restore_snapshot(current_snapshot);
 851       MC_UNSET_RAW_MEM;
 852     }
 853
 854   }
 855
 856
 857   MC_SET_RAW_MEM;
 858   xbt_fifo_shift(mc_stack_liveness_stateful);
 859   XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
 860   MC_UNSET_RAW_MEM;
 861
 862 }