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   char* hash_reached = malloc(sizeof(char)*160);
  28   unsigned int c= 0;
  29
  30   MC_SET_RAW_MEM;
  31   char *hash = malloc(sizeof(char)*160);
  32   xbt_sha((char *)&pair, hash);
  33   xbt_dynar_foreach(reached_pairs, c, hash_reached){
  34     if(strcmp(hash, hash_reached) == 0){
  35       MC_UNSET_RAW_MEM;
  36       return 1;
  37     }
  38   }
  39
  40   MC_UNSET_RAW_MEM;
  41   return 0;
  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 = malloc(sizeof(char)*160) ;
  49     xbt_sha((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 = malloc(sizeof(char)*160);
 119   xbt_sha((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   char* hash_visited = malloc(sizeof(char)*160);
 128   unsigned int c= 0;
 129
 130   MC_SET_RAW_MEM;
 131   mc_visited_pair_t p = NULL;
 132   p = xbt_new0(s_mc_visited_pair_t, 1);
 133   p->pair = pair;
 134   p->search_cycle = sc;
 135   char *hash = malloc(sizeof(char)*160);
 136   xbt_sha((char *)&p, hash);
 137   xbt_dynar_foreach(visited_pairs, c, hash_visited){
 138     if(strcmp(hash, hash_visited) == 0){
 139       MC_UNSET_RAW_MEM;
 140       return 1;
 141     }
 142   }
 143
 144   MC_UNSET_RAW_MEM;
 145   return 0;
 146
 147 }
 148
 149
 150 void MC_vddfs_stateful_init(xbt_automaton_t a){
 151
 152   XBT_DEBUG("**************************************************");
 153   XBT_DEBUG("Double-DFS stateful with visited state init");
 154   XBT_DEBUG("**************************************************");
 155
 156   mc_pair_t mc_initial_pair;
 157   mc_state_t initial_graph_state;
 158   smx_process_t process;
 159   mc_snapshot_t init_snapshot;
 160
 161   MC_wait_for_requests();
 162
 163   MC_SET_RAW_MEM;
 164
 165   init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 166
 167   initial_graph_state = MC_state_pair_new();
 168   xbt_swag_foreach(process, simix_global->process_list){
 169     if(MC_process_is_enabled(process)){
 170       MC_state_interleave_process(initial_graph_state, process);
 171     }
 172   }
 173
 174   visited_pairs = xbt_dynar_new(sizeof(char *), NULL);
 175   reached_pairs = xbt_dynar_new(sizeof(char *), NULL);
 176
 177   MC_take_snapshot(init_snapshot);
 178
 179   MC_UNSET_RAW_MEM;
 180
 181   unsigned int cursor = 0;
 182   xbt_state_t state = NULL;
 183
 184   xbt_dynar_foreach(a->states, cursor, state){
 185     if(state->type == -1){
 186
 187       MC_SET_RAW_MEM;
 188       mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
 189       xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
 190       MC_UNSET_RAW_MEM;
 191
 192       if(cursor == 0){
 193         MC_vddfs_stateful(a, 0, 0);
 194       }else{
 195         MC_restore_snapshot(init_snapshot);
 196         MC_UNSET_RAW_MEM;
 197         MC_vddfs_stateful(a, 0, 0);
 198       }
 199     }else{
 200        if(state->type == 2){
 201
 202          MC_SET_RAW_MEM;
 203          mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
 204          xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
 205          MC_UNSET_RAW_MEM;
 206
 207          if(cursor == 0){
 208            MC_vddfs_stateful(a, 1, 0);
 209          }else{
 210            MC_restore_snapshot(init_snapshot);
 211            MC_UNSET_RAW_MEM;
 212            MC_vddfs_stateful(a, 1, 0);
 213          }
 214        }
 215     }
 216   }
 217 }
 218
 219
 220 void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 221
 222   smx_process_t process = NULL;
 223
 224
 225   if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
 226     return;
 227
 228   if(restore == 1){
 229     MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state);
 230     MC_UNSET_RAW_MEM;
 231   }
 232
 233
 234   /* Get current state */
 235   mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 236
 237   if(restore==1){
 238     xbt_swag_foreach(process, simix_global->process_list){
 239       if(MC_process_is_enabled(process)){
 240         MC_state_interleave_process(current_pair->graph_state, process);
 241       }
 242     }
 243   }
 244
 245   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle);
 246   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));
 247
 248
 249   mc_stats_pair->visited_pairs++;
 250
 251   int value;
 252   mc_state_t next_graph_state = NULL;
 253   smx_req_t req = NULL;
 254   char *req_str;
 255
 256   mc_pair_t pair_succ;
 257   xbt_transition_t transition_succ;
 258   unsigned int cursor;
 259   int res;
 260
 261   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 262
 263   mc_pair_t next_pair;
 264   mc_snapshot_t next_snapshot;
 265   mc_snapshot_t current_snapshot;
 266
 267
 268   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 269
 270     MC_SET_RAW_MEM;
 271     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 272     MC_take_snapshot(current_snapshot);
 273     MC_UNSET_RAW_MEM;
 274
 275
 276     /* Debug information */
 277     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 278       req_str = MC_request_to_string(req, value);
 279       XBT_DEBUG("Execute: %s", req_str);
 280       xbt_free(req_str);
 281     }
 282
 283     MC_state_set_executed_request(current_pair->graph_state, req, value);
 284
 285     /* Answer the request */
 286     SIMIX_request_pre(req, value);
 287
 288     /* Wait for requests (schedules processes) */
 289     MC_wait_for_requests();
 290
 291
 292     /* Create the new expanded graph_state */
 293     MC_SET_RAW_MEM;
 294
 295     next_graph_state = MC_state_pair_new();
 296
 297     /* Get enabled process and insert it in the interleave set of the next graph_state */
 298     xbt_swag_foreach(process, simix_global->process_list){
 299       if(MC_process_is_enabled(process)){
 300         MC_state_interleave_process(next_graph_state, process);
 301       }
 302     }
 303
 304     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 305     MC_take_snapshot(next_snapshot);
 306
 307     MC_UNSET_RAW_MEM;
 308
 309     xbt_dynar_reset(successors);
 310
 311     cursor = 0;
 312     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 313
 314       res = MC_automaton_evaluate_label(a, transition_succ->label);
 315
 316       MC_SET_RAW_MEM;
 317
 318       if(res == 1){
 319         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 320         xbt_dynar_push(successors, &next_pair);
 321       }
 322
 323       MC_UNSET_RAW_MEM;
 324     }
 325
 326     cursor = 0;
 327     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 328
 329       res = MC_automaton_evaluate_label(a, transition_succ->label);
 330
 331       MC_SET_RAW_MEM;
 332
 333       if(res == 2){
 334         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 335         xbt_dynar_push(successors, &next_pair);
 336       }
 337
 338       MC_UNSET_RAW_MEM;
 339     }
 340
 341
 342
 343     if(xbt_dynar_length(successors) == 0){
 344
 345       MC_SET_RAW_MEM;
 346       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
 347       xbt_dynar_push(successors, &next_pair);
 348       MC_UNSET_RAW_MEM;
 349
 350     }
 351
 352
 353     //XBT_DEBUG("Successors length %lu", xbt_dynar_length(successors));
 354
 355     cursor = 0;
 356     xbt_dynar_foreach(successors, cursor, pair_succ){
 357
 358       //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 359
 360       if((search_cycle == 1) && (reached(pair_succ) == 1)){
 361         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 362         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 363         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 364         XBT_INFO("Counter-example that violates formula :");
 365         MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
 366         MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
 367         MC_print_statistics_pairs(mc_stats_pair);
 368         exit(0);
 369       }
 370
 371       if(visited(pair_succ, search_cycle) == 0){
 372
 373         mc_stats_pair->executed_transitions++;
 374
 375         MC_SET_RAW_MEM;
 376         xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 377         set_pair_visited(pair_succ, search_cycle);
 378         //XBT_DEBUG("New pair (graph=%p, automaton=%p) in stack", pair_succ->graph_state, pair_succ->automaton_state);
 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) && ((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2))){
 386
 387           MC_restore_snapshot(current_pair->system_state);
 388           MC_UNSET_RAW_MEM;
 389
 390           xbt_swag_foreach(process, simix_global->process_list){
 391             if(MC_process_is_enabled(process)){
 392               MC_state_interleave_process(current_pair->graph_state, process);
 393             }
 394           }
 395
 396
 397           set_pair_reached(current_pair);
 398           XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
 399           MC_vddfs_stateful(a, 1, 1);
 400           xbt_dynar_pop(reached_pairs, NULL);
 401
 402         }
 403
 404       }else{
 405
 406         XBT_DEBUG("Pair already visited !");
 407       }
 408
 409     }
 410
 411     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 412       MC_restore_snapshot(current_snapshot);
 413       MC_UNSET_RAW_MEM;
 414
 415     }
 416   }
 417
 418
 419   MC_SET_RAW_MEM;
 420   xbt_fifo_shift(mc_stack_liveness_stateful);
 421   XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
 422   MC_UNSET_RAW_MEM;
 423
 424
 425
 426 }
 427
 428
 429
 430 /********************* Double-DFS stateful without visited state *******************/
 431
 432
 433 void MC_ddfs_stateful_init(xbt_automaton_t a){
 434
 435   XBT_DEBUG("**************************************************");
 436   XBT_DEBUG("Double-DFS stateful without visited state init");
 437   XBT_DEBUG("**************************************************");
 438
 439   mc_pair_t mc_initial_pair;
 440   mc_state_t initial_graph_state;
 441   smx_process_t process;
 442   mc_snapshot_t init_snapshot;
 443
 444   MC_wait_for_requests();
 445
 446   MC_SET_RAW_MEM;
 447
 448   init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 449
 450   initial_graph_state = MC_state_pair_new();
 451   xbt_swag_foreach(process, simix_global->process_list){
 452     if(MC_process_is_enabled(process)){
 453       MC_state_interleave_process(initial_graph_state, process);
 454     }
 455   }
 456
 457   reached_pairs = xbt_dynar_new(sizeof(char *), NULL);
 458
 459   MC_take_snapshot(init_snapshot);
 460
 461   MC_UNSET_RAW_MEM;
 462
 463   unsigned int cursor = 0;
 464   xbt_state_t state = NULL;
 465
 466   xbt_dynar_foreach(a->states, cursor, state){
 467     if(state->type == -1){
 468
 469       MC_SET_RAW_MEM;
 470       mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
 471       xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
 472       MC_UNSET_RAW_MEM;
 473
 474       if(cursor == 0){
 475         MC_ddfs_stateful(a, 0, 0);
 476       }else{
 477         MC_restore_snapshot(init_snapshot);
 478         MC_UNSET_RAW_MEM;
 479         MC_ddfs_stateful(a, 0, 0);
 480       }
 481     }else{
 482        if(state->type == 2){
 483
 484          MC_SET_RAW_MEM;
 485          mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
 486          xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
 487          MC_UNSET_RAW_MEM;
 488
 489          if(cursor == 0){
 490            MC_ddfs_stateful(a, 1, 0);
 491          }else{
 492            MC_restore_snapshot(init_snapshot);
 493            MC_UNSET_RAW_MEM;
 494            MC_ddfs_stateful(a, 1, 0);
 495          }
 496        }
 497     }
 498   }
 499 }
 500
 501
 502 void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 503
 504   smx_process_t process = NULL;
 505
 506
 507   if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
 508     return;
 509
 510   if(restore == 1){
 511     MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state);
 512     MC_UNSET_RAW_MEM;
 513   }
 514
 515
 516   /* Get current state */
 517   mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 518
 519   if(restore==1){
 520     xbt_swag_foreach(process, simix_global->process_list){
 521       if(MC_process_is_enabled(process)){
 522         MC_state_interleave_process(current_pair->graph_state, process);
 523       }
 524     }
 525   }
 526
 527   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle);
 528   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));
 529
 530   mc_stats_pair->visited_pairs++;
 531
 532   int value;
 533   mc_state_t next_graph_state = NULL;
 534   smx_req_t req = NULL;
 535   char *req_str;
 536
 537   mc_pair_t pair_succ;
 538   xbt_transition_t transition_succ;
 539   unsigned int cursor;
 540   int res;
 541
 542   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 543
 544   mc_pair_t next_pair;
 545   mc_snapshot_t next_snapshot;
 546   mc_snapshot_t current_snapshot;
 547
 548   //sleep(1);
 549
 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     MC_UNSET_RAW_MEM;
 591
 592     xbt_dynar_reset(successors);
 593
 594     cursor = 0;
 595     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 596
 597       res = MC_automaton_evaluate_label(a, transition_succ->label);
 598
 599       MC_SET_RAW_MEM;
 600
 601       if(res == 1){ // enabled transition in automaton
 602         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 603         xbt_dynar_push(successors, &next_pair);
 604       }
 605
 606       MC_UNSET_RAW_MEM;
 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       MC_SET_RAW_MEM;
 615
 616       if(res == 2){ // transition always enabled in automaton
 617         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 618         xbt_dynar_push(successors, &next_pair);
 619       }
 620
 621       MC_UNSET_RAW_MEM;
 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) && ((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2))){
 662
 663         MC_restore_snapshot(current_pair->system_state);
 664         MC_UNSET_RAW_MEM;
 665
 666         xbt_swag_foreach(process, simix_global->process_list){
 667           if(MC_process_is_enabled(process)){
 668             MC_state_interleave_process(current_pair->graph_state, process);
 669           }
 670         }
 671
 672         set_pair_reached(current_pair);
 673         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
 674         MC_ddfs_stateful(a, 1, 1);
 675
 676         xbt_dynar_pop(reached_pairs, NULL);
 677       }
 678
 679     }
 680     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 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   char* hash_reached = malloc(sizeof(char)*160);
 719   unsigned int c= 0;
 720
 721   MC_SET_RAW_MEM;
 722   char *hash = malloc(sizeof(char)*160);
 723   xbt_sha((char *)&pair, hash);
 724   xbt_dynar_foreach(reached_pairs, c, hash_reached){
 725     if(strcmp(hash, hash_reached) == 0){
 726       MC_UNSET_RAW_MEM;
 727       return 1;
 728     }
 729   }
 730
 731   MC_UNSET_RAW_MEM;
 732   return 0;
 733 }
 734
 735 void set_pair_stateless_reached(mc_pair_stateless_t pair){
 736
 737   if(reached_stateless(pair) == 0){
 738
 739     MC_SET_RAW_MEM;
 740     char *hash = malloc(sizeof(char)*160) ;
 741     xbt_sha((char *)&pair, hash);
 742     xbt_dynar_push(reached_pairs, &hash);
 743     MC_UNSET_RAW_MEM;
 744   }
 745
 746 }
 747
 748
 749 void MC_ddfs_stateless_init(xbt_automaton_t a){
 750
 751   XBT_DEBUG("**************************************************");
 752   XBT_DEBUG("Double-DFS stateless init");
 753   XBT_DEBUG("**************************************************");
 754
 755   mc_pair_stateless_t mc_initial_pair;
 756   mc_state_t initial_graph_state;
 757   smx_process_t process;
 758
 759   MC_wait_for_requests();
 760
 761   MC_SET_RAW_MEM;
 762
 763   initial_graph_state = MC_state_pair_new();
 764   xbt_swag_foreach(process, simix_global->process_list){
 765     if(MC_process_is_enabled(process)){
 766       MC_state_interleave_process(initial_graph_state, process);
 767     }
 768   }
 769
 770   reached_pairs = xbt_dynar_new(sizeof(char *), NULL);
 771
 772   MC_UNSET_RAW_MEM;
 773
 774   /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
 775     -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
 776
 777   unsigned int cursor = 0;
 778   //unsigned int cursor2 = 0;
 779   xbt_state_t state = NULL;
 780   //int res;
 781   //xbt_transition_t transition_succ;
 782   //xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 783   //xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 784   //mc_pair_stateless_t pair_succ;
 785
 786   /*xbt_dynar_foreach(a->states, cursor, state){
 787     if(state->type == -1){
 788       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 789         res = MC_automaton_evaluate_label(a, transition_succ->label);
 790
 791         if(res == 1){
 792
 793           MC_SET_RAW_MEM;
 794
 795           mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst);
 796           xbt_dynar_push(successors, &mc_initial_pair);
 797
 798           MC_UNSET_RAW_MEM;
 799
 800         }
 801       }
 802     }
 803   }
 804
 805   cursor = 0;
 806   cursor2 = 0;
 807
 808   xbt_dynar_foreach(a->states, cursor, state){
 809     if(state->type == -1){
 810       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 811         res = MC_automaton_evaluate_label(a, transition_succ->label);
 812
 813         if(res == 2){
 814
 815           MC_SET_RAW_MEM;
 816
 817           mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst);
 818           xbt_dynar_push(successors, &mc_initial_pair);
 819
 820           MC_UNSET_RAW_MEM;
 821
 822         }
 823       }
 824     }
 825   }
 826
 827
 828   cursor = 0;
 829
 830   if((xbt_dynar_length(successors) == 0) && (xbt_dynar_length(elses) == 0)){
 831     xbt_dynar_foreach(a->states, cursor, state){
 832       if(state->type == -1){
 833         MC_SET_RAW_MEM;
 834
 835         mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst);
 836         xbt_dynar_push(successors, &mc_initial_pair);
 837
 838         MC_UNSET_RAW_MEM;
 839       }
 840     }
 841   }
 842
 843
 844   cursor = 0;
 845   xbt_dynar_foreach(successors, cursor, pair_succ){
 846     MC_SET_RAW_MEM;
 847
 848     xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 849
 850     initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 851     MC_take_snapshot(initial_snapshot);
 852
 853     MC_UNSET_RAW_MEM;
 854
 855     if(cursor == 0){
 856       MC_ddfs_stateless(a, 0, 0);
 857     }else{
 858       MC_ddfs_stateless(a, 0, 1);
 859     }
 860   }  */
 861
 862   xbt_dynar_foreach(a->states, cursor, state){
 863     if(state->type == -1){
 864
 865       MC_SET_RAW_MEM;
 866       mc_initial_pair = new_pair_stateless(initial_graph_state, state);
 867       xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 868
 869       initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 870       MC_take_snapshot(initial_snapshot);
 871
 872       MC_UNSET_RAW_MEM;
 873
 874       if(cursor == 0){
 875         MC_ddfs_stateless(a, 0, 0);
 876       }else{
 877         MC_restore_snapshot(initial_snapshot);
 878         MC_UNSET_RAW_MEM;
 879         MC_ddfs_stateless(a, 0, 0);
 880       }
 881     }else{
 882       if(state->type == 2){
 883
 884         MC_SET_RAW_MEM;
 885         mc_initial_pair = new_pair_stateless(initial_graph_state, state);
 886         xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 887
 888         initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 889         MC_take_snapshot(initial_snapshot);
 890
 891         MC_UNSET_RAW_MEM;
 892
 893         if(cursor == 0){
 894           MC_ddfs_stateless(a, 1, 0);
 895         }else{
 896           MC_restore_snapshot(initial_snapshot);
 897           MC_UNSET_RAW_MEM;
 898           MC_ddfs_stateless(a, 1, 0);
 899         }
 900       }
 901     }
 902   }
 903
 904 }
 905
 906
 907 void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
 908
 909   smx_process_t process = NULL;
 910
 911   if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
 912     return;
 913
 914   if(replay == 1){
 915     MC_replay_liveness(mc_stack_liveness_stateless);
 916   }
 917
 918   //XBT_DEBUG("Stack size before restore %u", xbt_fifo_size(mc_stack_liveness_stateless));
 919
 920   /* Get current state */
 921   mc_pair_stateless_t current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 922
 923   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
 924   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));
 925
 926   mc_stats_pair->visited_pairs++;
 927
 928   int value;
 929   mc_state_t next_graph_state = NULL;
 930   smx_req_t req = NULL;
 931   char *req_str;
 932
 933   mc_pair_stateless_t pair_succ;
 934   xbt_transition_t transition_succ;
 935   unsigned int cursor;
 936   int res;
 937
 938   xbt_dynar_t successors;
 939
 940   mc_pair_stateless_t next_pair;
 941   //mc_snapshot_t current_snap;
 942
 943
 944   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 945
 946     //XBT_DEBUG("Interleave size %u", MC_state_interleave_size(current_pair->graph_state));
 947
 948     /* Debug information */
 949     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 950       req_str = MC_request_to_string(req, value);
 951       XBT_DEBUG("Execute: %s", req_str);
 952       xbt_free(req_str);
 953     }
 954
 955     //sleep(1);
 956
 957     MC_state_set_executed_request(current_pair->graph_state, req, value);
 958
 959     /* Answer the request */
 960     SIMIX_request_pre(req, value);
 961
 962     /* Wait for requests (schedules processes) */
 963     MC_wait_for_requests();
 964
 965
 966     /* Create the new expanded graph_state */
 967     MC_SET_RAW_MEM;
 968
 969     next_graph_state = MC_state_pair_new();
 970
 971     /* Get enabled process and insert it in the interleave set of the next graph_state */
 972     xbt_swag_foreach(process, simix_global->process_list){
 973       if(MC_process_is_enabled(process)){
 974         MC_state_interleave_process(next_graph_state, process);
 975       }
 976     }
 977
 978     successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 979
 980     MC_UNSET_RAW_MEM;
 981
 982     //xbt_dynar_reset(successors);
 983
 984     cursor = 0;
 985
 986     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 987
 988       res = MC_automaton_evaluate_label(a, transition_succ->label);
 989
 990       MC_SET_RAW_MEM;
 991
 992       if(res == 1){ // enabled transition in automaton
 993         next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
 994         xbt_dynar_push(successors, &next_pair);
 995       }
 996
 997       MC_UNSET_RAW_MEM;
 998     }
 999
1000     cursor = 0;
1001
1002     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1003
1004       res = MC_automaton_evaluate_label(a, transition_succ->label);
1005
1006       MC_SET_RAW_MEM;
1007
1008       if(res == 2){ // enabled transition in automaton
1009         next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
1010         xbt_dynar_push(successors, &next_pair);
1011       }
1012
1013       MC_UNSET_RAW_MEM;
1014     }
1015
1016
1017     if(xbt_dynar_length(successors) == 0){
1018
1019       MC_SET_RAW_MEM;
1020       next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);
1021       xbt_dynar_push(successors, &next_pair);
1022       MC_UNSET_RAW_MEM;
1023
1024     }
1025
1026     cursor = 0;
1027     //XBT_DEBUG("Successors length %lu", xbt_dynar_length(successors));
1028
1029     xbt_dynar_foreach(successors, cursor, pair_succ){
1030
1031       if((search_cycle == 1) && (reached_stateless(pair_succ) == 1)){
1032         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1033         XBT_INFO("|             ACCEPTANCE CYCLE            |");
1034         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1035         XBT_INFO("Counter-example that violates formula :");
1036         MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
1037         MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
1038         MC_print_statistics_pairs(mc_stats_pair);
1039         exit(0);
1040       }
1041
1042       mc_stats_pair->executed_transitions++;
1043
1044       MC_SET_RAW_MEM;
1045       xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
1046       MC_UNSET_RAW_MEM;
1047
1048       MC_ddfs_stateless(a, search_cycle, 0);
1049
1050       //XBT_DEBUG("Stack size %u", xbt_fifo_size(mc_stack_liveness_stateless));
1051
1052       if((search_cycle == 0) && ((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2))){
1053
1054         /*xbt_swag_foreach(process, simix_global->process_list){
1055           if(MC_process_is_enabled(process)){
1056           MC_state_interleave_process(current_pair->graph_state, process);
1057           }
1058           }*/
1059
1060         set_pair_stateless_reached(current_pair);
1061         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
1062
1063         MC_ddfs_stateless(a, 1, 1);
1064
1065         xbt_dynar_pop(reached_pairs, NULL);
1066       }
1067     }
1068
1069     if(MC_state_interleave_size(current_pair->graph_state) > 0){
1070       XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
1071       MC_replay_liveness(mc_stack_liveness_stateless);
1072     }
1073
1074   }
1075
1076
1077   MC_SET_RAW_MEM;
1078   xbt_fifo_shift(mc_stack_liveness_stateless);
1079   XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
1080   MC_UNSET_RAW_MEM;
1081
1082 }
1083