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