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) || (res == 2)){
 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
 213   if(xbt_dynar_length(successors) == 0){
 214     xbt_dynar_foreach(a->states, cursor, state){
 215       if(state->type == -1){
 216         MC_SET_RAW_MEM;
 217
 218         mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 219         xbt_dynar_push(successors, &mc_initial_pair);
 220
 221         MC_UNSET_RAW_MEM;
 222       }
 223     }
 224   }
 225
 226   cursor = 0;
 227   xbt_dynar_foreach(successors, cursor, pair_succ){
 228     MC_SET_RAW_MEM;
 229
 230     xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 231     set_pair_visited(pair_succ, 0);
 232
 233     MC_UNSET_RAW_MEM;
 234
 235     if(cursor == 0){
 236       MC_vddfs_stateful(a, 0, 0);
 237     }else{
 238       MC_vddfs_stateful(a, 0, 1);
 239     }
 240   }
 241 }
 242
 243
 244 void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 245
 246   smx_process_t process = NULL;
 247
 248
 249   if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
 250     return;
 251
 252   if(restore == 1){
 253     MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state);
 254     MC_UNSET_RAW_MEM;
 255   }
 256
 257
 258   /* Get current state */
 259   mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 260
 261   if(restore==1){
 262     xbt_swag_foreach(process, simix_global->process_list){
 263       if(MC_process_is_enabled(process)){
 264         MC_state_interleave_process(current_pair->graph_state, process);
 265       }
 266     }
 267   }
 268
 269   XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
 270   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));
 271
 272
 273   mc_stats_pair->visited_pairs++;
 274
 275   int value;
 276   mc_state_t next_graph_state = NULL;
 277   smx_req_t req = NULL;
 278   char *req_str;
 279
 280   mc_pair_t pair_succ;
 281   xbt_transition_t transition_succ;
 282   unsigned int cursor;
 283   int res;
 284
 285   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 286
 287   mc_pair_t next_pair;
 288   mc_snapshot_t next_snapshot;
 289   mc_snapshot_t current_snapshot;
 290
 291
 292   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 293
 294     MC_SET_RAW_MEM;
 295     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 296     MC_take_snapshot(current_snapshot);
 297     MC_UNSET_RAW_MEM;
 298
 299
 300     /* Debug information */
 301     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 302       req_str = MC_request_to_string(req, value);
 303       XBT_DEBUG("Execute: %s", req_str);
 304       xbt_free(req_str);
 305     }
 306
 307     MC_state_set_executed_request(current_pair->graph_state, req, value);
 308
 309     /* Answer the request */
 310     SIMIX_request_pre(req, value);
 311
 312     /* Wait for requests (schedules processes) */
 313     MC_wait_for_requests();
 314
 315
 316     /* Create the new expanded graph_state */
 317     MC_SET_RAW_MEM;
 318
 319     next_graph_state = MC_state_pair_new();
 320
 321     /* Get enabled process and insert it in the interleave set of the next graph_state */
 322     xbt_swag_foreach(process, simix_global->process_list){
 323       if(MC_process_is_enabled(process)){
 324         MC_state_interleave_process(next_graph_state, process);
 325       }
 326     }
 327
 328     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 329     MC_take_snapshot(next_snapshot);
 330
 331     MC_UNSET_RAW_MEM;
 332
 333     xbt_dynar_reset(successors);
 334
 335     cursor = 0;
 336     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 337
 338       res = MC_automaton_evaluate_label(a, transition_succ->label);
 339
 340       MC_SET_RAW_MEM;
 341
 342       if((res == 1) || (res == 2)){ // enabled transition in automaton
 343         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 344         xbt_dynar_push(successors, &next_pair);
 345       }
 346
 347       MC_UNSET_RAW_MEM;
 348     }
 349
 350
 351     if(xbt_dynar_length(successors) == 0){
 352
 353       MC_SET_RAW_MEM;
 354       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
 355       xbt_dynar_push(successors, &next_pair);
 356       MC_UNSET_RAW_MEM;
 357
 358     }
 359
 360
 361     cursor = 0;
 362     xbt_dynar_foreach(successors, cursor, pair_succ){
 363
 364       //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 365
 366       if((search_cycle == 1) && (reached(pair_succ) == 1)){
 367         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 368         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 369         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 370         XBT_INFO("Counter-example that violates formula :");
 371         MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
 372         MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
 373         MC_print_statistics_pairs(mc_stats_pair);
 374         exit(0);
 375       }
 376
 377       if(visited(pair_succ, search_cycle) == 0){
 378
 379         mc_stats_pair->executed_transitions++;
 380
 381         MC_SET_RAW_MEM;
 382         xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 383         set_pair_visited(pair_succ, search_cycle);
 384         MC_UNSET_RAW_MEM;
 385
 386         MC_vddfs_stateful(a, search_cycle, 0);
 387
 388         if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 389
 390           MC_restore_snapshot(current_pair->system_state);
 391           MC_UNSET_RAW_MEM;
 392
 393           xbt_swag_foreach(process, simix_global->process_list){
 394             if(MC_process_is_enabled(process)){
 395               MC_state_interleave_process(current_pair->graph_state, process);
 396             }
 397           }
 398
 399           set_pair_reached(current_pair);
 400           XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
 401           MC_vddfs_stateful(a, 1, 1);
 402
 403         }
 404       }else{
 405
 406         XBT_DEBUG("Pair already visited !");
 407
 408       }
 409     }
 410
 411
 412     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 413       MC_restore_snapshot(current_snapshot);
 414       MC_UNSET_RAW_MEM;
 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 snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
 422   MC_UNSET_RAW_MEM;
 423
 424 }
 425
 426
 427
 428 /********************* Double-DFS stateful without visited state *******************/
 429
 430
 431 void MC_ddfs_stateful_init(xbt_automaton_t a){
 432
 433   XBT_DEBUG("**************************************************");
 434   XBT_DEBUG("Double-DFS stateful without visited state init");
 435   XBT_DEBUG("**************************************************");
 436
 437   mc_pair_t mc_initial_pair;
 438   mc_state_t initial_graph_state;
 439   smx_process_t process;
 440   mc_snapshot_t init_snapshot;
 441
 442   MC_wait_for_requests();
 443
 444   MC_SET_RAW_MEM;
 445
 446   init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 447
 448   initial_graph_state = MC_state_pair_new();
 449   xbt_swag_foreach(process, simix_global->process_list){
 450     if(MC_process_is_enabled(process)){
 451       MC_state_interleave_process(initial_graph_state, process);
 452     }
 453   }
 454
 455   reached_pairs = xbt_dynar_new(sizeof(char *), NULL);
 456
 457   MC_take_snapshot(init_snapshot);
 458
 459   MC_UNSET_RAW_MEM;
 460
 461   /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
 462     -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
 463
 464   unsigned int cursor = 0;
 465   unsigned int cursor2 = 0;
 466   xbt_state_t state = NULL;
 467   int res;
 468   xbt_transition_t transition_succ;
 469   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 470   mc_pair_t pair_succ;
 471
 472   xbt_dynar_foreach(a->states, cursor, state){
 473     if(state->type == -1){
 474       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 475         res = MC_automaton_evaluate_label(a, transition_succ->label);
 476
 477         if((res == 1) || (res == 2)){
 478
 479           MC_SET_RAW_MEM;
 480
 481           mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 482           xbt_dynar_push(successors, &mc_initial_pair);
 483
 484           MC_UNSET_RAW_MEM;
 485
 486         }
 487       }
 488     }
 489   }
 490
 491   cursor = 0;
 492
 493   if(xbt_dynar_length(successors) == 0){
 494     xbt_dynar_foreach(a->states, cursor, state){
 495       if(state->type == -1){
 496         MC_SET_RAW_MEM;
 497
 498         mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 499         xbt_dynar_push(successors, &mc_initial_pair);
 500
 501         MC_UNSET_RAW_MEM;
 502       }
 503     }
 504   }
 505
 506   cursor = 0;
 507   xbt_dynar_foreach(successors, cursor, pair_succ){
 508     MC_SET_RAW_MEM;
 509
 510     xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 511
 512     MC_UNSET_RAW_MEM;
 513
 514     if(cursor == 0){
 515       MC_ddfs_stateful(a, 0, 0);
 516     }else{
 517       MC_ddfs_stateful(a, 0, 1);
 518     }
 519   }
 520 }
 521
 522
 523 void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 524
 525   smx_process_t process = NULL;
 526
 527
 528   if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
 529     return;
 530
 531   if(restore == 1){
 532     MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state);
 533     MC_UNSET_RAW_MEM;
 534   }
 535
 536
 537   /* Get current state */
 538   mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 539
 540   if(restore==1){
 541     xbt_swag_foreach(process, simix_global->process_list){
 542       if(MC_process_is_enabled(process)){
 543         MC_state_interleave_process(current_pair->graph_state, process);
 544       }
 545     }
 546   }
 547
 548   XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
 549   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));
 550
 551
 552   mc_stats_pair->visited_pairs++;
 553
 554   int value;
 555   mc_state_t next_graph_state = NULL;
 556   smx_req_t req = NULL;
 557   char *req_str;
 558
 559   mc_pair_t pair_succ;
 560   xbt_transition_t transition_succ;
 561   unsigned int cursor;
 562   int res;
 563
 564   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 565
 566   mc_pair_t next_pair;
 567   mc_snapshot_t next_snapshot;
 568   mc_snapshot_t current_snapshot;
 569
 570
 571   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 572
 573     MC_SET_RAW_MEM;
 574     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 575     MC_take_snapshot(current_snapshot);
 576     MC_UNSET_RAW_MEM;
 577
 578
 579     /* Debug information */
 580     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 581       req_str = MC_request_to_string(req, value);
 582       XBT_DEBUG("Execute: %s", req_str);
 583       xbt_free(req_str);
 584     }
 585
 586     MC_state_set_executed_request(current_pair->graph_state, req, value);
 587
 588     /* Answer the request */
 589     SIMIX_request_pre(req, value);
 590
 591     /* Wait for requests (schedules processes) */
 592     MC_wait_for_requests();
 593
 594
 595     /* Create the new expanded graph_state */
 596     MC_SET_RAW_MEM;
 597
 598     next_graph_state = MC_state_pair_new();
 599
 600     /* Get enabled process and insert it in the interleave set of the next graph_state */
 601     xbt_swag_foreach(process, simix_global->process_list){
 602       if(MC_process_is_enabled(process)){
 603         MC_state_interleave_process(next_graph_state, process);
 604       }
 605     }
 606
 607     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 608     MC_take_snapshot(next_snapshot);
 609
 610     MC_UNSET_RAW_MEM;
 611
 612     xbt_dynar_reset(successors);
 613
 614     cursor = 0;
 615     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 616
 617       res = MC_automaton_evaluate_label(a, transition_succ->label);
 618
 619       MC_SET_RAW_MEM;
 620
 621       if((res == 1) || (res == 2)){ // enabled transition in automaton
 622         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 623         xbt_dynar_push(successors, &next_pair);
 624       }
 625
 626       MC_UNSET_RAW_MEM;
 627     }
 628
 629
 630     if(xbt_dynar_length(successors) == 0){
 631
 632       MC_SET_RAW_MEM;
 633       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
 634       xbt_dynar_push(successors, &next_pair);
 635       MC_UNSET_RAW_MEM;
 636
 637     }
 638
 639
 640     cursor = 0;
 641     xbt_dynar_foreach(successors, cursor, pair_succ){
 642
 643       //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 644
 645       if((search_cycle == 1) && (reached(pair_succ) == 1)){
 646         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 647         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 648         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 649         XBT_INFO("Counter-example that violates formula :");
 650         MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
 651         MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
 652         MC_print_statistics_pairs(mc_stats_pair);
 653         exit(0);
 654       }
 655
 656       mc_stats_pair->executed_transitions++;
 657
 658       MC_SET_RAW_MEM;
 659       xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 660       MC_UNSET_RAW_MEM;
 661
 662       MC_ddfs_stateful(a, search_cycle, 0);
 663
 664       if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 665
 666         MC_restore_snapshot(current_pair->system_state);
 667         MC_UNSET_RAW_MEM;
 668
 669         xbt_swag_foreach(process, simix_global->process_list){
 670           if(MC_process_is_enabled(process)){
 671             MC_state_interleave_process(current_pair->graph_state, process);
 672           }
 673         }
 674
 675         set_pair_reached(current_pair);
 676         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
 677         MC_ddfs_stateful(a, 1, 1);
 678
 679       }
 680     }
 681
 682
 683     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 684       MC_restore_snapshot(current_snapshot);
 685       MC_UNSET_RAW_MEM;
 686     }
 687   }
 688
 689
 690   MC_SET_RAW_MEM;
 691   xbt_fifo_shift(mc_stack_liveness_stateful);
 692   XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
 693   MC_UNSET_RAW_MEM;
 694
 695 }
 696
 697
 698
 699 /********************* Double-DFS stateless *******************/
 700
 701 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 702   xbt_free(pair->graph_state->proc_status);
 703   xbt_free(pair->graph_state);
 704   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 705   xbt_free(pair);
 706 }
 707
 708 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
 709   mc_pair_stateless_t p = NULL;
 710   p = xbt_new0(s_mc_pair_stateless_t, 1);
 711   p->automaton_state = st;
 712   p->graph_state = sg;
 713   mc_stats_pair->expanded_pairs++;
 714   return p;
 715 }
 716
 717
 718 int reached_stateless(mc_pair_stateless_t pair){
 719
 720   char* hash_reached = malloc(sizeof(char)*160);
 721   unsigned int c= 0;
 722
 723   MC_SET_RAW_MEM;
 724   char *hash = malloc(sizeof(char)*160);
 725   xbt_sha((char *)&pair, hash);
 726   xbt_dynar_foreach(reached_pairs, c, hash_reached){
 727     if(strcmp(hash, hash_reached) == 0){
 728       MC_UNSET_RAW_MEM;
 729       return 1;
 730     }
 731   }
 732
 733   MC_UNSET_RAW_MEM;
 734   return 0;
 735 }
 736
 737 void set_pair_stateless_reached(mc_pair_stateless_t pair){
 738
 739   if(reached_stateless(pair) == 0){
 740     MC_SET_RAW_MEM;
 741     char *hash = malloc(sizeof(char)*160) ;
 742     xbt_sha((char *)&pair, hash);
 743     xbt_dynar_push(reached_pairs, &hash);
 744     MC_UNSET_RAW_MEM;
 745   }
 746
 747 }
 748
 749
 750 void MC_ddfs_stateless_init(xbt_automaton_t a){
 751
 752   XBT_DEBUG("**************************************************");
 753   XBT_DEBUG("Double-DFS stateless init");
 754   XBT_DEBUG("**************************************************");
 755
 756   mc_pair_stateless_t mc_initial_pair;
 757   mc_state_t initial_graph_state;
 758   smx_process_t process;
 759
 760   MC_wait_for_requests();
 761
 762   MC_SET_RAW_MEM;
 763
 764   initial_graph_state = MC_state_pair_new();
 765   xbt_swag_foreach(process, simix_global->process_list){
 766     if(MC_process_is_enabled(process)){
 767       MC_state_interleave_process(initial_graph_state, process);
 768     }
 769   }
 770
 771   reached_pairs = xbt_dynar_new(sizeof(char *), NULL);
 772
 773   MC_UNSET_RAW_MEM;
 774
 775   /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
 776     -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
 777
 778   unsigned int cursor = 0;
 779   unsigned int cursor2 = 0;
 780   xbt_state_t state = NULL;
 781   int res;
 782   xbt_transition_t transition_succ;
 783   xbt_dynar_t successors = 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) || (res == 2)){
 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
 807   if(xbt_dynar_length(successors) == 0){
 808     xbt_dynar_foreach(a->states, cursor, state){
 809       if(state->type == -1){
 810         MC_SET_RAW_MEM;
 811
 812         mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst);
 813         xbt_dynar_push(successors, &mc_initial_pair);
 814
 815         MC_UNSET_RAW_MEM;
 816       }
 817     }
 818   }
 819
 820   cursor = 0;
 821   xbt_dynar_foreach(successors, cursor, pair_succ){
 822     MC_SET_RAW_MEM;
 823
 824     xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 825
 826     /* Save the initial state */
 827     initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 828     MC_take_snapshot(initial_snapshot);
 829
 830     MC_UNSET_RAW_MEM;
 831
 832     if(cursor == 0){
 833       MC_ddfs_stateless(a, 0, 0);
 834     }else{
 835       MC_ddfs_stateless(a, 0, 1);
 836     }
 837   }
 838 }
 839
 840
 841 void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
 842
 843  smx_process_t process = NULL;
 844
 845
 846   if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
 847     return;
 848
 849   /* Get current state */
 850   mc_pair_stateless_t current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 851
 852   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
 853   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));
 854
 855
 856   mc_stats_pair->visited_pairs++;
 857
 858   int value;
 859   mc_state_t next_graph_state = NULL;
 860   smx_req_t req = NULL;
 861   char *req_str;
 862
 863   mc_pair_stateless_t pair_succ;
 864   xbt_transition_t transition_succ;
 865   unsigned int cursor;
 866   int res;
 867
 868   xbt_dynar_t successors;
 869
 870   mc_pair_stateless_t next_pair;
 871
 872   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 873
 874     //XBT_DEBUG("Interleave size %u", MC_state_interleave_size(current_pair->graph_state));
 875
 876     /* Debug information */
 877     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 878       req_str = MC_request_to_string(req, value);
 879       XBT_DEBUG("Execute: %s", req_str);
 880       xbt_free(req_str);
 881     }
 882
 883     //sleep(1);
 884
 885     MC_state_set_executed_request(current_pair->graph_state, req, value);
 886
 887     /* Answer the request */
 888     SIMIX_request_pre(req, value);
 889
 890     /* Wait for requests (schedules processes) */
 891     MC_wait_for_requests();
 892
 893
 894     /* Create the new expanded graph_state */
 895     MC_SET_RAW_MEM;
 896
 897     next_graph_state = MC_state_pair_new();
 898
 899     /* Get enabled process and insert it in the interleave set of the next graph_state */
 900     xbt_swag_foreach(process, simix_global->process_list){
 901       if(MC_process_is_enabled(process)){
 902         MC_state_interleave_process(next_graph_state, process);
 903       }
 904     }
 905
 906     successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 907
 908     MC_UNSET_RAW_MEM;
 909
 910     //xbt_dynar_reset(successors);
 911
 912     cursor = 0;
 913
 914     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 915
 916       res = MC_automaton_evaluate_label(a, transition_succ->label);
 917
 918       MC_SET_RAW_MEM;
 919
 920       if((res == 1) || (res == 2)){ // enabled transition in automaton
 921         next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
 922         xbt_dynar_push(successors, &next_pair);
 923       }
 924
 925       MC_UNSET_RAW_MEM;
 926     }
 927
 928
 929     if(xbt_dynar_length(successors) == 0){
 930
 931       MC_SET_RAW_MEM;
 932       next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);
 933       xbt_dynar_push(successors, &next_pair);
 934       MC_UNSET_RAW_MEM;
 935
 936     }
 937
 938     cursor = 0;
 939
 940     xbt_dynar_foreach(successors, cursor, pair_succ){
 941
 942       if((search_cycle == 1) && (reached_stateless(pair_succ) == 1)){
 943         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 944         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 945         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 946         XBT_INFO("Counter-example that violates formula :");
 947         MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 948         MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 949         MC_print_statistics_pairs(mc_stats_pair);
 950         exit(0);
 951       }
 952
 953       mc_stats_pair->executed_transitions++;
 954
 955       MC_SET_RAW_MEM;
 956       xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 957       MC_UNSET_RAW_MEM;
 958
 959
 960
 961       MC_ddfs_stateless(a, search_cycle, 0);
 962
 963       if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 964
 965         set_pair_stateless_reached(current_pair);
 966         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
 967         MC_replay_liveness(mc_stack_liveness_stateless);
 968         MC_ddfs_stateless(a, 1, 1);
 969
 970       }
 971     }
 972
 973     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 974       XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
 975       MC_replay_liveness(mc_stack_liveness_stateless);
 976     }
 977   }
 978
 979
 980   MC_SET_RAW_MEM;
 981   xbt_fifo_shift(mc_stack_liveness_stateless);
 982   XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
 983   MC_UNSET_RAW_MEM;
 984
 985 }
 986