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_dynar_t successors = NULL;
  10
  11 //mc_snapshot_t snapshot;
  12
  13 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
  14
  15   //XBT_DEBUG("Compare snapshot");
  16
  17   if(s1->num_reg != s2->num_reg){
  18     XBT_DEBUG("Different num_reg (s1 = %d, s2 = %d)", s1->num_reg, s2->num_reg);
  19     return 1;
  20   }
  21
  22   //XBT_DEBUG("Num reg : %d", s1->num_reg);
  23
  24   int i;
  25   int errors = 0;
  26
  27   for(i=0 ; i< s1->num_reg ; i++){
  28
  29     if(s1->regions[i]->type != s2->regions[i]->type){
  30       //XBT_DEBUG("Different type of region");
  31       return 1;
  32     }
  33
  34     switch(s1->regions[i]->type){
  35     case 0:
  36       //XBT_DEBUG("Region : heap");
  37       if(s1->regions[i]->size != s2->regions[i]->size){
  38         //XBT_DEBUG("Different size of heap (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
  39         return 1;
  40       }
  41       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
  42         //XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
  43       return 1;
  44       }
  45       if(mmalloc_compare_heap(s1->regions[i]->start_addr, s2->regions[i]->start_addr)){
  46         //XBT_DEBUG("Different heap (mmalloc_compare)");
  47         errors++;
  48       }
  49       break;
  50     case 1 :
  51       //XBT_DEBUG("Region : libsimgrid");
  52       if(s1->regions[i]->size != s2->regions[i]->size){
  53         //XBT_DEBUG("Different size of libsimgrid (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
  54         return 1;
  55       }
  56       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
  57         //XBT_DEBUG("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
  58       return 1;
  59       }
  60       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
  61         //XBT_DEBUG("Different memcmp for data in libsimgrid");
  62         errors++;
  63       }
  64       break;
  65     case 2:
  66       //XBT_DEBUG("Region : program");
  67       if(s1->regions[i]->size != s2->regions[i]->size){
  68         //XBT_DEBUG("Different size of program (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
  69         return 1;
  70       }
  71       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
  72         //XBT_DEBUG("Different start addr of program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
  73         return 1;
  74       }
  75       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
  76         //XBT_DEBUG("Different memcmp for data in program");
  77         errors++;
  78       }
  79       break;
  80     case 3:
  81       //XBT_DEBUG("Region : stack");
  82       if(s1->regions[i]->size != s2->regions[i]->size){
  83         //XBT_DEBUG("Different size of stack (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
  84         return 1;
  85       }
  86       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
  87         //XBT_DEBUG("Different start addr of stack (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
  88         return 1;
  89       }
  90       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
  91         //XBT_DEBUG("Different memcmp for data in stack");
  92         errors++;
  93       }
  94       break;
  95     }
  96   }
  97
  98   return (errors>0);
  99
 100 }
 101
 102 int reached(xbt_automaton_t a, xbt_state_t st, char *prgm){
 103
 104
 105   if(xbt_fifo_size(reached_pairs) == 0){
 106
 107     return 0;
 108
 109   }else{
 110
 111     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 112
 113     /* Get values of propositional symbols */
 114     unsigned int cursor = 0;
 115     xbt_propositional_symbol_t ps = NULL;
 116     xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 117       int (*f)() = ps->function;
 118       int res = (*f)();
 119       xbt_dynar_push_as(prop_ato, int, res);
 120     }
 121
 122     MC_SET_RAW_MEM;
 123     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 124     MC_take_snapshot_liveness(sn, prgm);
 125     MC_UNSET_RAW_MEM;
 126
 127     int i=0;
 128     xbt_fifo_item_t item = xbt_fifo_get_first_item(reached_pairs);
 129     mc_pair_reached_t pair_test = NULL;
 130
 131     while(i < xbt_fifo_size(reached_pairs)){
 132
 133       pair_test = (mc_pair_reached_t) xbt_fifo_get_item_content(item);
 134
 135       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 136         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 137           if(snapshot_compare(sn, pair_test->system_state) == 0){
 138             MC_SET_RAW_MEM;
 139             MC_free_snapshot(sn);
 140             MC_UNSET_RAW_MEM;
 141             return 1;
 142           }
 143         }
 144       }
 145
 146       item = xbt_fifo_get_next_item(item);
 147
 148       i++;
 149
 150     }
 151
 152     MC_SET_RAW_MEM;
 153     MC_free_snapshot(sn);
 154     MC_UNSET_RAW_MEM;
 155     return 0;
 156
 157   }
 158 }
 159
 160 void set_pair_reached(xbt_automaton_t a, xbt_state_t st, char *prgm){
 161
 162
 163   MC_SET_RAW_MEM;
 164
 165   mc_pair_reached_t pair = NULL;
 166   pair = xbt_new0(s_mc_pair_reached_t, 1);
 167   pair->automaton_state = st;
 168   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 169   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 170   MC_take_snapshot_liveness(pair->system_state, prgm);
 171
 172   /* Get values of propositional symbols */
 173   unsigned int cursor = 0;
 174   xbt_propositional_symbol_t ps = NULL;
 175   xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 176     int (*f)() = ps->function;
 177     int 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
 188 int visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){
 189
 190
 191   if(xbt_fifo_size(visited_pairs) == 0){
 192
 193     return 0;
 194
 195   }else{
 196
 197     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 198
 199     /* Get values of propositional symbols */
 200     unsigned int cursor = 0;
 201     xbt_propositional_symbol_t ps = NULL;
 202     xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 203       int (*f)() = ps->function;
 204       int res = (*f)();
 205       xbt_dynar_push_as(prop_ato, int, res);
 206     }
 207
 208     MC_SET_RAW_MEM;
 209     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 210     MC_take_snapshot_liveness(sn, prgm);
 211     MC_UNSET_RAW_MEM;
 212
 213
 214     int i=0;
 215     xbt_fifo_item_t item = xbt_fifo_get_first_item(visited_pairs);
 216     mc_pair_visited_t pair_test = NULL;
 217
 218     while(i < xbt_fifo_size(visited_pairs)){
 219
 220       pair_test = (mc_pair_visited_t) xbt_fifo_get_item_content(item);
 221
 222       if(pair_test->search_cycle == sc) {
 223         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 224           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 225             if(snapshot_compare(sn, pair_test->system_state) == 0){
 226               MC_SET_RAW_MEM;
 227               MC_free_snapshot(sn);
 228               MC_UNSET_RAW_MEM;
 229               return 1;
 230             }
 231           }
 232         }
 233       }
 234
 235       item = xbt_fifo_get_next_item(item);
 236
 237       i++;
 238
 239     }
 240
 241     MC_SET_RAW_MEM;
 242     MC_free_snapshot(sn);
 243     MC_UNSET_RAW_MEM;
 244     return 0;
 245
 246   }
 247 }
 248
 249 void set_pair_visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){
 250
 251
 252   MC_SET_RAW_MEM;
 253
 254   mc_pair_visited_t pair = NULL;
 255   pair = xbt_new0(s_mc_pair_visited_t, 1);
 256   pair->automaton_state = st;
 257   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 258   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 259   MC_take_snapshot_liveness(pair->system_state, prgm);
 260   pair->search_cycle = sc;
 261
 262   /* Get values of propositional symbols */
 263   unsigned int cursor = 0;
 264   xbt_propositional_symbol_t ps = NULL;
 265   xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 266     int (*f)() = ps->function;
 267     int res = (*f)();
 268     xbt_dynar_push_as(pair->prop_ato, int, res);
 269   }
 270
 271   xbt_fifo_unshift(visited_pairs, pair);
 272
 273   MC_UNSET_RAW_MEM;
 274
 275
 276 }
 277
 278 void MC_pair_delete(mc_pair_t pair){
 279   xbt_free(pair->graph_state->proc_status);
 280   xbt_free(pair->graph_state);
 281   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 282   xbt_free(pair);
 283 }
 284
 285
 286
 287 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 288
 289   switch(l->type){
 290   case 0 : {
 291     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 292     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 293     return (left_res || right_res);
 294     break;
 295   }
 296   case 1 : {
 297     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 298     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 299     return (left_res && right_res);
 300     break;
 301   }
 302   case 2 : {
 303     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
 304     return (!res);
 305     break;
 306   }
 307   case 3 : {
 308     unsigned int cursor = 0;
 309     xbt_propositional_symbol_t p = NULL;
 310     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
 311       if(strcmp(p->pred, l->u.predicat) == 0){
 312         int (*f)() = p->function;
 313         return (*f)();
 314       }
 315     }
 316     return -1;
 317     break;
 318   }
 319   case 4 : {
 320     return 2;
 321     break;
 322   }
 323   default :
 324     return -1;
 325   }
 326 }
 327
 328
 329
 330
 331
 332 /********************* Double-DFS stateless *******************/
 333
 334 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 335   xbt_free(pair->graph_state->proc_status);
 336   xbt_free(pair->graph_state);
 337   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 338   xbt_free(pair);
 339 }
 340
 341 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 342   mc_pair_stateless_t p = NULL;
 343   p = xbt_new0(s_mc_pair_stateless_t, 1);
 344   p->automaton_state = st;
 345   p->graph_state = sg;
 346   p->requests = r;
 347   mc_stats_pair->expanded_pairs++;
 348   return p;
 349 }
 350
 351 void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){
 352
 353   XBT_DEBUG("**************************************************");
 354   XBT_DEBUG("Double-DFS stateless init");
 355   XBT_DEBUG("**************************************************");
 356
 357   mc_pair_stateless_t mc_initial_pair = NULL;
 358   mc_state_t initial_graph_state = NULL;
 359   smx_process_t process;
 360
 361   MC_wait_for_requests();
 362
 363   MC_SET_RAW_MEM;
 364
 365   initial_graph_state = MC_state_pair_new();
 366   xbt_swag_foreach(process, simix_global->process_list){
 367     if(MC_process_is_enabled(process)){
 368       MC_state_interleave_process(initial_graph_state, process);
 369     }
 370   }
 371
 372   reached_pairs = xbt_fifo_new();
 373   visited_pairs = xbt_fifo_new();
 374   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 375
 376   /* Save the initial state */
 377   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
 378   MC_take_snapshot_liveness(initial_snapshot_liveness, prgm);
 379
 380   MC_UNSET_RAW_MEM;
 381
 382   unsigned int cursor = 0;
 383   xbt_state_t state;
 384
 385   xbt_dynar_foreach(a->states, cursor, state){
 386     if(state->type == -1){
 387
 388       MC_SET_RAW_MEM;
 389       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 390       xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 391       MC_UNSET_RAW_MEM;
 392
 393       if(cursor != 0){
 394         MC_restore_snapshot(initial_snapshot_liveness);
 395         MC_UNSET_RAW_MEM;
 396       }
 397
 398       MC_ddfs_stateless(a, 0, 0, prgm);
 399
 400     }else{
 401       if(state->type == 2){
 402
 403         MC_SET_RAW_MEM;
 404         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 405         xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 406         MC_UNSET_RAW_MEM;
 407
 408         set_pair_reached(a, state, prgm);
 409
 410         if(cursor != 0){
 411           MC_restore_snapshot(initial_snapshot_liveness);
 412           MC_UNSET_RAW_MEM;
 413         }
 414
 415         MC_ddfs_stateless(a, 1, 0, prgm);
 416
 417       }
 418     }
 419   }
 420
 421 }
 422
 423
 424 void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *prgm){
 425
 426   smx_process_t process;
 427   mc_pair_stateless_t current_pair = NULL;
 428
 429   //mc_snapshot_t current_snapshot = NULL;
 430
 431   if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
 432     return;
 433
 434   if(replay == 1){
 435     MC_replay_liveness(mc_stack_liveness_stateless, 0);
 436     current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 437     xbt_swag_foreach(process, simix_global->process_list){
 438       if(MC_process_is_enabled(process)){
 439         MC_state_interleave_process(current_pair->graph_state, process);
 440       }
 441     }
 442   }
 443
 444   /* Get current pair */
 445   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 446
 447   /* Update current state in buchi automaton */
 448   a->current_state = current_pair->automaton_state;
 449
 450
 451   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
 452   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));
 453
 454   mc_stats_pair->visited_pairs++;
 455
 456   //sleep(1);
 457
 458   int value;
 459   mc_state_t next_graph_state = NULL;
 460   smx_req_t req = NULL;
 461   char *req_str;
 462
 463   xbt_transition_t transition_succ;
 464   unsigned int cursor = 0;
 465   int res;
 466
 467   mc_pair_stateless_t next_pair = NULL;
 468   mc_pair_stateless_t pair_succ;
 469
 470   if(xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS){
 471
 472     set_pair_visited(a, current_pair->automaton_state, search_cycle, prgm);
 473
 474     if(current_pair->requests > 0){
 475
 476       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 477
 478         /* Debug information */
 479         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 480           req_str = MC_request_to_string(req, value);
 481           XBT_DEBUG("Execute: %s", req_str);
 482           xbt_free(req_str);
 483         }
 484
 485         MC_state_set_executed_request(current_pair->graph_state, req, value);
 486
 487         /* Answer the request */
 488         SIMIX_request_pre(req, value);
 489
 490         /* Wait for requests (schedules processes) */
 491         MC_wait_for_requests();
 492
 493
 494         MC_SET_RAW_MEM;
 495
 496         /* Create the new expanded graph_state */
 497         next_graph_state = MC_state_pair_new();
 498
 499         /* Get enabled process and insert it in the interleave set of the next graph_state */
 500         xbt_swag_foreach(process, simix_global->process_list){
 501           if(MC_process_is_enabled(process)){
 502             MC_state_interleave_process(next_graph_state, process);
 503           }
 504         }
 505
 506         xbt_dynar_reset(successors);
 507
 508         MC_UNSET_RAW_MEM;
 509
 510
 511         cursor= 0;
 512         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 513
 514           res = MC_automaton_evaluate_label(a, transition_succ->label);
 515
 516           if(res == 1){ // enabled transition in automaton
 517             MC_SET_RAW_MEM;
 518             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 519             xbt_dynar_push(successors, &next_pair);
 520             MC_UNSET_RAW_MEM;
 521           }
 522
 523         }
 524
 525         cursor = 0;
 526
 527         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 528
 529           res = MC_automaton_evaluate_label(a, transition_succ->label);
 530
 531           if(res == 2){ // true transition in automaton
 532             MC_SET_RAW_MEM;
 533             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 534             xbt_dynar_push(successors, &next_pair);
 535             MC_UNSET_RAW_MEM;
 536           }
 537
 538         }
 539
 540         cursor = 0;
 541
 542         xbt_dynar_foreach(successors, cursor, pair_succ){
 543
 544           if(!visited(a, pair_succ->automaton_state, search_cycle, prgm)){
 545
 546             if(search_cycle == 1){
 547
 548               if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 549
 550                 if(reached(a, pair_succ->automaton_state, prgm) == 1){
 551
 552                   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));
 553
 554                   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 555                   XBT_INFO("|             ACCEPTANCE CYCLE            |");
 556                   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 557                   XBT_INFO("Counter-example that violates formula :");
 558                   MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 559                   MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 560                   MC_print_statistics_pairs(mc_stats_pair);
 561                   exit(0);
 562
 563                 }else{
 564
 565                   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);
 566
 567                   set_pair_reached(a, pair_succ->automaton_state, prgm);
 568
 569                 }
 570
 571               }
 572
 573             }else{
 574
 575               if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 576
 577                 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);
 578
 579                 set_pair_reached(a, pair_succ->automaton_state, prgm);
 580
 581                 search_cycle = 1;
 582
 583               }
 584
 585             }
 586
 587             MC_SET_RAW_MEM;
 588             xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 589             MC_UNSET_RAW_MEM;
 590
 591             MC_ddfs_stateless(a, search_cycle, 0, prgm);
 592
 593             /* Restore system before checking others successors */
 594             if(cursor != (xbt_dynar_length(successors) - 1))
 595               MC_replay_liveness(mc_stack_liveness_stateless, 1);
 596
 597           }else{
 598
 599             XBT_DEBUG("Next pair already visited");
 600
 601           }
 602         }
 603
 604         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 605           XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
 606           MC_replay_liveness(mc_stack_liveness_stateless, 0);
 607         }
 608       }
 609
 610
 611     }else{  /*No request to execute, search evolution in Büchi automaton */
 612
 613       MC_SET_RAW_MEM;
 614
 615       /* Create the new expanded graph_state */
 616       next_graph_state = MC_state_pair_new();
 617
 618       xbt_dynar_reset(successors);
 619
 620       MC_UNSET_RAW_MEM;
 621
 622
 623       cursor= 0;
 624       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 625
 626         res = MC_automaton_evaluate_label(a, transition_succ->label);
 627
 628         if(res == 1){ // enabled transition in automaton
 629           MC_SET_RAW_MEM;
 630           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 631           xbt_dynar_push(successors, &next_pair);
 632           MC_UNSET_RAW_MEM;
 633         }
 634
 635       }
 636
 637       cursor = 0;
 638
 639       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 640
 641         res = MC_automaton_evaluate_label(a, transition_succ->label);
 642
 643         if(res == 2){ // true transition in automaton
 644           MC_SET_RAW_MEM;
 645           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 646           xbt_dynar_push(successors, &next_pair);
 647           MC_UNSET_RAW_MEM;
 648         }
 649
 650       }
 651
 652       cursor = 0;
 653
 654       xbt_dynar_foreach(successors, cursor, pair_succ){
 655
 656         if(!visited(a, pair_succ->automaton_state, search_cycle, prgm)){
 657
 658           if(search_cycle == 1){
 659
 660             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 661
 662               if(reached(a, pair_succ->automaton_state, prgm) == 1){
 663
 664                 XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1);
 665
 666                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 667                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 668                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 669                 XBT_INFO("Counter-example that violates formula :");
 670                 MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 671                 MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 672                 MC_print_statistics_pairs(mc_stats_pair);
 673                 exit(0);
 674
 675               }else{
 676
 677                 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);
 678
 679                 set_pair_reached(a, pair_succ->automaton_state, prgm);
 680
 681               }
 682
 683             }
 684
 685           }else{
 686
 687             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (xbt_fifo_size(mc_stack_liveness_stateless) < (MAX_DEPTH_LIVENESS - 1))){
 688
 689               set_pair_reached(a, pair_succ->automaton_state, prgm);
 690
 691               search_cycle = 1;
 692
 693             }
 694
 695           }
 696
 697           MC_SET_RAW_MEM;
 698           xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 699           MC_UNSET_RAW_MEM;
 700
 701           MC_ddfs_stateless(a, search_cycle, 0, prgm);
 702
 703           /* Restore system before checking others successors */
 704           if(cursor != xbt_dynar_length(successors) - 1)
 705             MC_replay_liveness(mc_stack_liveness_stateless, 1);
 706
 707         }else{
 708
 709           XBT_DEBUG("Next pair already visited");
 710
 711         }
 712
 713       }
 714
 715     }
 716
 717   }else{
 718
 719     XBT_DEBUG("Max depth reached");
 720
 721   }
 722
 723   if(xbt_fifo_size(mc_stack_liveness_stateless) == MAX_DEPTH_LIVENESS ){
 724     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) );
 725   }else{
 726     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) );
 727   }
 728
 729
 730   MC_SET_RAW_MEM;
 731   xbt_fifo_shift(mc_stack_liveness_stateless);
 732   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 733     xbt_fifo_shift(reached_pairs);
 734   }
 735   MC_UNSET_RAW_MEM;
 736
 737
 738 }
 739