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