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   /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
 182     -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
 183
 184   unsigned int cursor = 0;
 185   //unsigned int cursor2 = 0;
 186   xbt_state_t state = NULL;
 187   //int res;
 188   //xbt_transition_t transition_succ;
 189   //xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 190   //mc_pair_t pair_succ;
 191
 192   /* xbt_dynar_foreach(a->states, cursor, state){
 193     if(state->type == -1){
 194       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 195         res = MC_automaton_evaluate_label(a, transition_succ->label);
 196
 197         if(res == 1){
 198
 199           MC_SET_RAW_MEM;
 200
 201           mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 202           xbt_dynar_push(successors, &mc_initial_pair);
 203
 204           MC_UNSET_RAW_MEM;
 205
 206         }
 207       }
 208     }
 209   }
 210
 211   cursor = 0;
 212   cursor2 = 0;
 213
 214   xbt_dynar_foreach(a->states, cursor, state){
 215     if(state->type == -1){
 216       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 217         res = MC_automaton_evaluate_label(a, transition_succ->label);
 218
 219         if(res == 2){
 220
 221           MC_SET_RAW_MEM;
 222
 223           mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 224           xbt_dynar_push(successors, &mc_initial_pair);
 225
 226           MC_UNSET_RAW_MEM;
 227
 228         }
 229       }
 230     }
 231   }
 232
 233   cursor = 0;
 234
 235   if(xbt_dynar_length(successors) == 0){
 236     xbt_dynar_foreach(a->states, cursor, state){
 237       if(state->type == -1){
 238         MC_SET_RAW_MEM;
 239
 240         mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 241         xbt_dynar_push(successors, &mc_initial_pair);
 242
 243         MC_UNSET_RAW_MEM;
 244       }
 245     }
 246   }
 247
 248   cursor = 0;
 249   xbt_dynar_foreach(successors, cursor, pair_succ){
 250     MC_SET_RAW_MEM;
 251
 252     xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 253
 254     MC_UNSET_RAW_MEM;
 255
 256     if(cursor == 0){
 257       MC_vddfs_stateful(a, 0, 0);
 258     }else{
 259       MC_vddfs_stateful(a, 0, 1);
 260     }
 261   } */
 262
 263   cursor = 0;
 264   xbt_dynar_foreach(a->states, cursor, state){
 265     if(state->type == -1){
 266
 267       MC_SET_RAW_MEM;
 268       mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
 269       xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
 270       MC_UNSET_RAW_MEM;
 271
 272       if(cursor == 0){
 273         MC_vddfs_stateful(a, 0, 0);
 274       }else{
 275         MC_vddfs_stateful(a, 0, 1);
 276       }
 277     }
 278   }
 279 }
 280
 281
 282 void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 283
 284   smx_process_t process = NULL;
 285
 286
 287   if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
 288     return;
 289
 290   if(restore == 1){
 291     MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state);
 292     MC_UNSET_RAW_MEM;
 293   }
 294
 295
 296   /* Get current state */
 297   mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 298
 299   if(restore==1){
 300     xbt_swag_foreach(process, simix_global->process_list){
 301       if(MC_process_is_enabled(process)){
 302         MC_state_interleave_process(current_pair->graph_state, process);
 303       }
 304     }
 305   }
 306
 307   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle);
 308   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));
 309
 310
 311   mc_stats_pair->visited_pairs++;
 312
 313   int value;
 314   mc_state_t next_graph_state = NULL;
 315   smx_req_t req = NULL;
 316   char *req_str;
 317
 318   mc_pair_t pair_succ;
 319   xbt_transition_t transition_succ;
 320   unsigned int cursor;
 321   int res;
 322
 323   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 324
 325   mc_pair_t next_pair;
 326   mc_snapshot_t next_snapshot;
 327   mc_snapshot_t current_snapshot;
 328
 329
 330   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 331
 332     MC_SET_RAW_MEM;
 333     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 334     MC_take_snapshot(current_snapshot);
 335     MC_UNSET_RAW_MEM;
 336
 337
 338     /* Debug information */
 339     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 340       req_str = MC_request_to_string(req, value);
 341       XBT_DEBUG("Execute: %s", req_str);
 342       xbt_free(req_str);
 343     }
 344
 345     MC_state_set_executed_request(current_pair->graph_state, req, value);
 346
 347     /* Answer the request */
 348     SIMIX_request_pre(req, value);
 349
 350     /* Wait for requests (schedules processes) */
 351     MC_wait_for_requests();
 352
 353
 354     /* Create the new expanded graph_state */
 355     MC_SET_RAW_MEM;
 356
 357     next_graph_state = MC_state_pair_new();
 358
 359     /* Get enabled process and insert it in the interleave set of the next graph_state */
 360     xbt_swag_foreach(process, simix_global->process_list){
 361       if(MC_process_is_enabled(process)){
 362         MC_state_interleave_process(next_graph_state, process);
 363       }
 364     }
 365
 366     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 367     MC_take_snapshot(next_snapshot);
 368
 369     MC_UNSET_RAW_MEM;
 370
 371     xbt_dynar_reset(successors);
 372
 373     cursor = 0;
 374     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 375
 376       res = MC_automaton_evaluate_label(a, transition_succ->label);
 377
 378       MC_SET_RAW_MEM;
 379
 380       if(res == 1){
 381         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 382         xbt_dynar_push(successors, &next_pair);
 383       }
 384
 385       MC_UNSET_RAW_MEM;
 386     }
 387
 388     cursor = 0;
 389     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 390
 391       res = MC_automaton_evaluate_label(a, transition_succ->label);
 392
 393       MC_SET_RAW_MEM;
 394
 395       if(res == 2){
 396         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 397         xbt_dynar_push(successors, &next_pair);
 398       }
 399
 400       MC_UNSET_RAW_MEM;
 401     }
 402
 403
 404
 405     if(xbt_dynar_length(successors) == 0){
 406
 407       MC_SET_RAW_MEM;
 408       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
 409       xbt_dynar_push(successors, &next_pair);
 410       MC_UNSET_RAW_MEM;
 411
 412     }
 413
 414
 415     //XBT_DEBUG("Successors length %lu", xbt_dynar_length(successors));
 416
 417     cursor = 0;
 418     xbt_dynar_foreach(successors, cursor, pair_succ){
 419
 420       //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 421
 422       if((search_cycle == 1) && (reached(pair_succ) == 1)){
 423         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 424         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 425         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 426         XBT_INFO("Counter-example that violates formula :");
 427         MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
 428         MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
 429         MC_print_statistics_pairs(mc_stats_pair);
 430         exit(0);
 431       }
 432
 433       if(visited(pair_succ, search_cycle) == 0){
 434
 435         mc_stats_pair->executed_transitions++;
 436
 437         MC_SET_RAW_MEM;
 438         xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 439         set_pair_visited(pair_succ, search_cycle);
 440         //XBT_DEBUG("New pair (graph=%p, automaton=%p) in stack", pair_succ->graph_state, pair_succ->automaton_state);
 441         MC_UNSET_RAW_MEM;
 442
 443         MC_vddfs_stateful(a, search_cycle, 0);
 444
 445         //XBT_DEBUG("Pair (graph=%p, automaton=%p) expanded", pair_succ->graph_state, pair_succ->automaton_state);
 446
 447       }else{
 448
 449         XBT_DEBUG("Pair already visited !");
 450
 451       }
 452     }
 453
 454     if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 455
 456       /*MC_restore_snapshot(current_pair->system_state);
 457         MC_UNSET_RAW_MEM;
 458
 459         xbt_swag_foreach(process, simix_global->process_list){
 460         if(MC_process_is_enabled(process)){
 461         MC_state_interleave_process(current_pair->graph_state, process);
 462         }
 463         }*/
 464
 465       set_pair_reached(current_pair);
 466       XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
 467       MC_vddfs_stateful(a, 1, 1);
 468
 469     }
 470
 471
 472
 473     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 474       MC_restore_snapshot(current_snapshot);
 475       MC_UNSET_RAW_MEM;
 476     }
 477   }
 478
 479
 480   MC_SET_RAW_MEM;
 481   mc_pair_t top_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 482   if((top_pair->graph_state == current_pair->graph_state) && (top_pair->automaton_state == current_pair->automaton_state)){
 483     xbt_fifo_shift(mc_stack_liveness_stateful);
 484     XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
 485   }
 486   MC_UNSET_RAW_MEM;
 487
 488
 489
 490 }
 491
 492
 493
 494 /********************* Double-DFS stateful without visited state *******************/
 495
 496
 497 void MC_ddfs_stateful_init(xbt_automaton_t a){
 498
 499   XBT_DEBUG("**************************************************");
 500   XBT_DEBUG("Double-DFS stateful without visited state init");
 501   XBT_DEBUG("**************************************************");
 502
 503   mc_pair_t mc_initial_pair;
 504   mc_state_t initial_graph_state;
 505   smx_process_t process;
 506   mc_snapshot_t init_snapshot;
 507
 508   MC_wait_for_requests();
 509
 510   MC_SET_RAW_MEM;
 511
 512   init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 513
 514   initial_graph_state = MC_state_pair_new();
 515   xbt_swag_foreach(process, simix_global->process_list){
 516     if(MC_process_is_enabled(process)){
 517       MC_state_interleave_process(initial_graph_state, process);
 518     }
 519   }
 520
 521   reached_pairs = xbt_dynar_new(sizeof(char *), NULL);
 522
 523   MC_take_snapshot(init_snapshot);
 524
 525   MC_UNSET_RAW_MEM;
 526
 527   /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
 528     -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
 529
 530   unsigned int cursor = 0;
 531   //unsigned int cursor2 = 0;
 532   xbt_state_t state = NULL;
 533   //int res;
 534   //xbt_transition_t transition_succ;
 535   //xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 536   //mc_pair_t pair_succ;
 537
 538   /*xbt_dynar_foreach(a->states, cursor, state){
 539     if(state->type == -1){
 540       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 541         res = MC_automaton_evaluate_label(a, transition_succ->label);
 542
 543         if(res == 1){
 544
 545           MC_SET_RAW_MEM;
 546
 547           mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 548           xbt_dynar_push(successors, &mc_initial_pair);
 549
 550           MC_UNSET_RAW_MEM;
 551
 552         }
 553       }
 554     }
 555   }
 556
 557   cursor = 0;
 558   cursor2 = 0;
 559
 560   xbt_dynar_foreach(a->states, cursor, state){
 561     if(state->type == -1){
 562       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 563         res = MC_automaton_evaluate_label(a, transition_succ->label);
 564
 565         if(res == 2){
 566
 567           MC_SET_RAW_MEM;
 568
 569           mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 570           xbt_dynar_push(successors, &mc_initial_pair);
 571
 572           MC_UNSET_RAW_MEM;
 573
 574         }
 575       }
 576     }
 577   }
 578
 579   cursor = 0;
 580
 581   if(xbt_dynar_length(successors) == 0){
 582     xbt_dynar_foreach(a->states, cursor, state){
 583       if(state->type == -1){
 584         MC_SET_RAW_MEM;
 585
 586         mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 587         xbt_dynar_push(successors, &mc_initial_pair);
 588
 589         MC_UNSET_RAW_MEM;
 590       }
 591     }
 592     }*/
 593
 594   cursor = 0;
 595   xbt_dynar_foreach(a->states, cursor, state){
 596     if(state->type == -1){
 597
 598       MC_SET_RAW_MEM;
 599       mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
 600       xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
 601       MC_UNSET_RAW_MEM;
 602
 603       if(cursor == 0){
 604         MC_ddfs_stateful(a, 0, 0);
 605       }else{
 606         MC_ddfs_stateful(a, 0, 1);
 607       }
 608     }
 609   }
 610 }
 611
 612
 613 void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 614
 615   smx_process_t process = NULL;
 616
 617
 618   if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
 619     return;
 620
 621   if(restore == 1){
 622     MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state);
 623     MC_UNSET_RAW_MEM;
 624   }
 625
 626
 627   /* Get current state */
 628   mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 629
 630   if(restore==1){
 631     xbt_swag_foreach(process, simix_global->process_list){
 632       if(MC_process_is_enabled(process)){
 633         MC_state_interleave_process(current_pair->graph_state, process);
 634       }
 635     }
 636   }
 637
 638   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle);
 639   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));
 640
 641   mc_stats_pair->visited_pairs++;
 642
 643   int value;
 644   mc_state_t next_graph_state = NULL;
 645   smx_req_t req = NULL;
 646   char *req_str;
 647
 648   mc_pair_t pair_succ;
 649   xbt_transition_t transition_succ;
 650   unsigned int cursor;
 651   int res;
 652
 653   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 654
 655   mc_pair_t next_pair;
 656   mc_snapshot_t next_snapshot;
 657   mc_snapshot_t current_snapshot;
 658
 659
 660   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 661
 662     MC_SET_RAW_MEM;
 663     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 664     MC_take_snapshot(current_snapshot);
 665     MC_UNSET_RAW_MEM;
 666
 667
 668     /* Debug information */
 669     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 670       req_str = MC_request_to_string(req, value);
 671       XBT_DEBUG("%u Execute: %s", search_cycle, req_str);
 672       xbt_free(req_str);
 673     }
 674
 675     MC_state_set_executed_request(current_pair->graph_state, req, value);
 676
 677     /* Answer the request */
 678     SIMIX_request_pre(req, value);
 679
 680     /* Wait for requests (schedules processes) */
 681     MC_wait_for_requests();
 682
 683
 684     /* Create the new expanded graph_state */
 685     MC_SET_RAW_MEM;
 686
 687     next_graph_state = MC_state_pair_new();
 688
 689     /* Get enabled process and insert it in the interleave set of the next graph_state */
 690     xbt_swag_foreach(process, simix_global->process_list){
 691       if(MC_process_is_enabled(process)){
 692         MC_state_interleave_process(next_graph_state, process);
 693       }
 694     }
 695
 696     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 697     MC_take_snapshot(next_snapshot);
 698
 699     MC_UNSET_RAW_MEM;
 700
 701     xbt_dynar_reset(successors);
 702
 703     cursor = 0;
 704     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 705
 706       res = MC_automaton_evaluate_label(a, transition_succ->label);
 707
 708       MC_SET_RAW_MEM;
 709
 710       if(res == 1){ // enabled transition in automaton
 711         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 712         xbt_dynar_push(successors, &next_pair);
 713       }
 714
 715       MC_UNSET_RAW_MEM;
 716     }
 717
 718     cursor = 0;
 719     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 720
 721       res = MC_automaton_evaluate_label(a, transition_succ->label);
 722
 723       MC_SET_RAW_MEM;
 724
 725       if(res == 2){ // enabled transition in automaton
 726         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 727         xbt_dynar_push(successors, &next_pair);
 728       }
 729
 730       MC_UNSET_RAW_MEM;
 731     }
 732
 733
 734     if(xbt_dynar_length(successors) == 0){
 735
 736       MC_SET_RAW_MEM;
 737       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
 738       xbt_dynar_push(successors, &next_pair);
 739       MC_UNSET_RAW_MEM;
 740
 741     }
 742
 743     //XBT_DEBUG("Successors in automaton %lu", xbt_dynar_length(successors));
 744
 745     cursor = 0;
 746     xbt_dynar_foreach(successors, cursor, pair_succ){
 747
 748       //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 749
 750       if((search_cycle == 1) && (reached(pair_succ) == 1)){
 751         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 752         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 753         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 754         XBT_INFO("Counter-example that violates formula :");
 755         MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
 756         MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
 757         MC_print_statistics_pairs(mc_stats_pair);
 758         exit(0);
 759       }
 760
 761       mc_stats_pair->executed_transitions++;
 762
 763       MC_SET_RAW_MEM;
 764       xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 765       MC_UNSET_RAW_MEM;
 766
 767       MC_ddfs_stateful(a, search_cycle, 0);
 768     }
 769
 770     if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 771
 772         set_pair_reached(current_pair);
 773         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
 774
 775         /*MC_restore_snapshot(current_pair->system_state);
 776         MC_UNSET_RAW_MEM;
 777
 778         xbt_swag_foreach(process, simix_global->process_list){
 779           if(MC_process_is_enabled(process)){
 780             MC_state_interleave_process(current_pair->graph_state, process);
 781           }
 782         }
 783
 784         mc_pair_t top_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 785         if((top_pair->graph_state != current_pair->graph_state) || (top_pair->automaton_state != current_pair->automaton_state)){
 786           MC_SET_RAW_MEM;
 787           xbt_fifo_unshift(mc_stack_liveness_stateful, current_pair);
 788           MC_UNSET_RAW_MEM;
 789           }*/
 790
 791         MC_ddfs_stateful(a, 1, 1);
 792
 793     }
 794
 795
 796     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 797       MC_restore_snapshot(current_snapshot);
 798       MC_UNSET_RAW_MEM;
 799     }
 800
 801   }
 802
 803
 804   MC_SET_RAW_MEM;
 805   mc_pair_t top_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 806   if((top_pair->graph_state == current_pair->graph_state) && (top_pair->automaton_state == current_pair->automaton_state)){
 807     xbt_fifo_shift(mc_stack_liveness_stateful);
 808     XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
 809   }
 810   MC_UNSET_RAW_MEM;
 811
 812 }
 813
 814
 815
 816 /********************* Double-DFS stateless *******************/
 817
 818 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 819   xbt_free(pair->graph_state->proc_status);
 820   xbt_free(pair->graph_state);
 821   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 822   xbt_free(pair);
 823 }
 824
 825 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
 826   mc_pair_stateless_t p = NULL;
 827   p = xbt_new0(s_mc_pair_stateless_t, 1);
 828   p->automaton_state = st;
 829   p->graph_state = sg;
 830   mc_stats_pair->expanded_pairs++;
 831   return p;
 832 }
 833
 834
 835 int reached_stateless(mc_pair_stateless_t pair){
 836
 837   char* hash_reached = malloc(sizeof(char)*160);
 838   unsigned int c= 0;
 839
 840   MC_SET_RAW_MEM;
 841   char *hash = malloc(sizeof(char)*160);
 842   xbt_sha((char *)&pair, hash);
 843   xbt_dynar_foreach(reached_pairs, c, hash_reached){
 844     if(strcmp(hash, hash_reached) == 0){
 845       MC_UNSET_RAW_MEM;
 846       return 1;
 847     }
 848   }
 849
 850   MC_UNSET_RAW_MEM;
 851   return 0;
 852 }
 853
 854 void set_pair_stateless_reached(mc_pair_stateless_t pair){
 855
 856   if(reached_stateless(pair) == 0){
 857
 858     MC_SET_RAW_MEM;
 859     char *hash = malloc(sizeof(char)*160) ;
 860     xbt_sha((char *)&pair, hash);
 861     xbt_dynar_push(reached_pairs, &hash);
 862     MC_UNSET_RAW_MEM;
 863   }
 864
 865 }
 866
 867
 868 void MC_ddfs_stateless_init(xbt_automaton_t a){
 869
 870   XBT_DEBUG("**************************************************");
 871   XBT_DEBUG("Double-DFS stateless init");
 872   XBT_DEBUG("**************************************************");
 873
 874   mc_pair_stateless_t mc_initial_pair;
 875   mc_state_t initial_graph_state;
 876   smx_process_t process;
 877
 878   MC_wait_for_requests();
 879
 880   MC_SET_RAW_MEM;
 881
 882   initial_graph_state = MC_state_pair_new();
 883   xbt_swag_foreach(process, simix_global->process_list){
 884     if(MC_process_is_enabled(process)){
 885       MC_state_interleave_process(initial_graph_state, process);
 886     }
 887   }
 888
 889   reached_pairs = xbt_dynar_new(sizeof(char *), NULL);
 890
 891   MC_UNSET_RAW_MEM;
 892
 893   /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
 894     -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
 895
 896   unsigned int cursor = 0;
 897   //unsigned int cursor2 = 0;
 898   xbt_state_t state = NULL;
 899   //int res;
 900   //xbt_transition_t transition_succ;
 901   //xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 902   //xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 903   //mc_pair_stateless_t pair_succ;
 904
 905   /*xbt_dynar_foreach(a->states, cursor, state){
 906     if(state->type == -1){
 907       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 908         res = MC_automaton_evaluate_label(a, transition_succ->label);
 909
 910         if(res == 1){
 911
 912           MC_SET_RAW_MEM;
 913
 914           mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst);
 915           xbt_dynar_push(successors, &mc_initial_pair);
 916
 917           MC_UNSET_RAW_MEM;
 918
 919         }
 920       }
 921     }
 922   }
 923
 924   cursor = 0;
 925   cursor2 = 0;
 926
 927   xbt_dynar_foreach(a->states, cursor, state){
 928     if(state->type == -1){
 929       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 930         res = MC_automaton_evaluate_label(a, transition_succ->label);
 931
 932         if(res == 2){
 933
 934           MC_SET_RAW_MEM;
 935
 936           mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst);
 937           xbt_dynar_push(successors, &mc_initial_pair);
 938
 939           MC_UNSET_RAW_MEM;
 940
 941         }
 942       }
 943     }
 944   }
 945
 946
 947   cursor = 0;
 948
 949   if((xbt_dynar_length(successors) == 0) && (xbt_dynar_length(elses) == 0)){
 950     xbt_dynar_foreach(a->states, cursor, state){
 951       if(state->type == -1){
 952         MC_SET_RAW_MEM;
 953
 954         mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst);
 955         xbt_dynar_push(successors, &mc_initial_pair);
 956
 957         MC_UNSET_RAW_MEM;
 958       }
 959     }
 960   }
 961
 962
 963   cursor = 0;
 964   xbt_dynar_foreach(successors, cursor, pair_succ){
 965     MC_SET_RAW_MEM;
 966
 967     xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 968
 969     initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 970     MC_take_snapshot(initial_snapshot);
 971
 972     MC_UNSET_RAW_MEM;
 973
 974     if(cursor == 0){
 975       MC_ddfs_stateless(a, 0, 0);
 976     }else{
 977       MC_ddfs_stateless(a, 0, 1);
 978     }
 979   }  */
 980
 981   xbt_dynar_foreach(a->states, cursor, state){
 982     if(state->type == -1){
 983
 984       MC_SET_RAW_MEM;
 985       mc_initial_pair = new_pair_stateless(initial_graph_state, state);
 986       xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 987
 988       initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 989       MC_take_snapshot(initial_snapshot);
 990
 991       MC_UNSET_RAW_MEM;
 992
 993       if(cursor == 0){
 994         MC_ddfs_stateless(a, 0);
 995       }else{
 996         MC_restore_snapshot(initial_snapshot);
 997         MC_UNSET_RAW_MEM;
 998         MC_ddfs_stateless(a, 0);
 999       }
1000     }
1001   }
1002 }
1003
1004
1005 void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle){
1006
1007   smx_process_t process = NULL;
1008
1009   if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
1010     return;
1011
1012   //XBT_DEBUG("Stack size before restore %u", xbt_fifo_size(mc_stack_liveness_stateless));
1013
1014   /* Get current state */
1015   mc_pair_stateless_t current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
1016
1017   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
1018   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));
1019
1020   mc_stats_pair->visited_pairs++;
1021
1022   int value;
1023   mc_state_t next_graph_state = NULL;
1024   smx_req_t req = NULL;
1025   char *req_str;
1026
1027   mc_pair_stateless_t pair_succ;
1028   xbt_transition_t transition_succ;
1029   unsigned int cursor;
1030   int res;
1031
1032   xbt_dynar_t successors;
1033
1034   mc_pair_stateless_t next_pair;
1035   mc_snapshot_t current_snap;
1036
1037
1038   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
1039
1040     MC_SET_RAW_MEM;
1041     current_snap = xbt_new0(s_mc_snapshot_t, 1);
1042     MC_take_snapshot(current_snap);
1043     MC_UNSET_RAW_MEM;
1044
1045     //XBT_DEBUG("Interleave size %u", MC_state_interleave_size(current_pair->graph_state));
1046
1047     /* Debug information */
1048     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
1049       req_str = MC_request_to_string(req, value);
1050       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));
1051       XBT_DEBUG("Execute: %s", req_str);
1052       xbt_free(req_str);
1053     }
1054
1055     //sleep(1);
1056
1057     MC_state_set_executed_request(current_pair->graph_state, req, value);
1058
1059     /* Answer the request */
1060     SIMIX_request_pre(req, value);
1061
1062     /* Wait for requests (schedules processes) */
1063     MC_wait_for_requests();
1064
1065
1066     /* Create the new expanded graph_state */
1067     MC_SET_RAW_MEM;
1068
1069     next_graph_state = MC_state_pair_new();
1070
1071     /* Get enabled process and insert it in the interleave set of the next graph_state */
1072     xbt_swag_foreach(process, simix_global->process_list){
1073       if(MC_process_is_enabled(process)){
1074         MC_state_interleave_process(next_graph_state, process);
1075       }
1076     }
1077
1078     successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
1079
1080     MC_UNSET_RAW_MEM;
1081
1082     //xbt_dynar_reset(successors);
1083
1084     cursor = 0;
1085
1086     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1087
1088       res = MC_automaton_evaluate_label(a, transition_succ->label);
1089
1090       MC_SET_RAW_MEM;
1091
1092       if(res == 1){ // enabled transition in automaton
1093         next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
1094         xbt_dynar_push(successors, &next_pair);
1095       }
1096
1097       MC_UNSET_RAW_MEM;
1098     }
1099
1100     cursor = 0;
1101
1102     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1103
1104       res = MC_automaton_evaluate_label(a, transition_succ->label);
1105
1106       MC_SET_RAW_MEM;
1107
1108       if(res == 2){ // enabled transition in automaton
1109         next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
1110         xbt_dynar_push(successors, &next_pair);
1111       }
1112
1113       MC_UNSET_RAW_MEM;
1114     }
1115
1116
1117     if(xbt_dynar_length(successors) == 0){
1118
1119       MC_SET_RAW_MEM;
1120       next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);
1121       xbt_dynar_push(successors, &next_pair);
1122       MC_UNSET_RAW_MEM;
1123
1124     }
1125
1126     cursor = 0;
1127     //XBT_DEBUG("Successors length %lu", xbt_dynar_length(successors));
1128
1129     xbt_dynar_foreach(successors, cursor, pair_succ){
1130
1131       if((search_cycle == 1) && (reached_stateless(pair_succ) == 1)){
1132         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1133         XBT_INFO("|             ACCEPTANCE CYCLE            |");
1134         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1135         XBT_INFO("Counter-example that violates formula :");
1136         MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
1137         MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
1138         MC_print_statistics_pairs(mc_stats_pair);
1139         exit(0);
1140       }
1141
1142       mc_stats_pair->executed_transitions++;
1143
1144       MC_SET_RAW_MEM;
1145       xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
1146       MC_UNSET_RAW_MEM;
1147
1148       MC_ddfs_stateless(a, search_cycle);
1149
1150       //XBT_DEBUG("Stack size %u", xbt_fifo_size(mc_stack_liveness_stateless));
1151     }
1152
1153     //xbt_dynar_reset(successors);
1154
1155     if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
1156
1157         set_pair_stateless_reached(current_pair);
1158         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
1159         MC_restore_snapshot(current_snap);
1160         MC_UNSET_RAW_MEM;
1161
1162         xbt_swag_foreach(process, simix_global->process_list){
1163           if(MC_process_is_enabled(process)){
1164             MC_state_interleave_process(current_pair->graph_state, process);
1165           }
1166         }
1167
1168         MC_ddfs_stateless(a, 1);
1169     }
1170
1171     if(MC_state_interleave_size(current_pair->graph_state) > 0){
1172       //XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
1173       //MC_replay_liveness(mc_stack_liveness_stateless);
1174       MC_restore_snapshot(current_snap);
1175       MC_UNSET_RAW_MEM;
1176     }
1177
1178   }
1179
1180
1181   MC_SET_RAW_MEM;
1182   mc_pair_stateless_t top_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
1183   if((top_pair->graph_state == current_pair->graph_state) && (top_pair->automaton_state == current_pair->automaton_state)){
1184     xbt_fifo_shift(mc_stack_liveness_stateless);
1185     XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
1186   }
1187   MC_UNSET_RAW_MEM;
1188   //XBT_DEBUG("Stack size after shift %u", xbt_fifo_size(mc_stack_liveness_stateless));
1189
1190 }
1191