src/mc/mc_liveness.c

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