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