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