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