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