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_state_t st){
 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(automaton->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);
 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_state_t st){
 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);
 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(automaton->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_state_t st, int sc){
 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(automaton->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);
 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_state_t st, int sc){
 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);
 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(automaton->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_exp_label_t l){
 307
 308   switch(l->type){
 309   case 0 : {
 310     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 311     int right_res = MC_automaton_evaluate_label(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(l->u.or_and.left_exp);
 317     int right_res = MC_automaton_evaluate_label(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(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(automaton->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(){
 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);
 397
 398   MC_UNSET_RAW_MEM;
 399
 400   unsigned int cursor = 0;
 401   xbt_state_t state;
 402
 403   xbt_dynar_foreach(automaton->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(0);
 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(state);
 427
 428         if(cursor != 0){
 429           MC_restore_snapshot(initial_snapshot_liveness);
 430           MC_UNSET_RAW_MEM;
 431         }
 432
 433         MC_ddfs_stateless(1);
 434
 435       }
 436     }
 437   }
 438
 439 }
 440
 441
 442 void MC_ddfs_stateless(int search_cycle){
 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
 451   /* Get current pair */
 452   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 453
 454   /* Update current state in buchi automaton */
 455   automaton->current_state = current_pair->automaton_state;
 456
 457
 458   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
 459   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));
 460
 461   mc_stats_pair->visited_pairs++;
 462
 463   //sleep(1);
 464
 465   int value;
 466   mc_state_t next_graph_state = NULL;
 467   smx_req_t req = NULL;
 468   char *req_str;
 469
 470   xbt_transition_t transition_succ;
 471   unsigned int cursor = 0;
 472   int res;
 473
 474   mc_pair_stateless_t next_pair = NULL;
 475   mc_pair_stateless_t pair_succ;
 476
 477   if(xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS){
 478
 479     set_pair_visited(current_pair->automaton_state, search_cycle);
 480
 481     XBT_DEBUG("Visited pairs : %d", xbt_fifo_size(visited_pairs));
 482
 483     if(current_pair->requests > 0){
 484
 485       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 486
 487         /* Debug information */
 488         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 489           req_str = MC_request_to_string(req, value);
 490           XBT_DEBUG("Execute: %s", req_str);
 491           xbt_free(req_str);
 492         }
 493
 494         MC_state_set_executed_request(current_pair->graph_state, req, value);
 495
 496         /* Answer the request */
 497         SIMIX_request_pre(req, value);
 498
 499         /* Wait for requests (schedules processes) */
 500         MC_wait_for_requests();
 501
 502
 503         MC_SET_RAW_MEM;
 504
 505         /* Create the new expanded graph_state */
 506         next_graph_state = MC_state_pair_new();
 507
 508         /* Get enabled process and insert it in the interleave set of the next graph_state */
 509         xbt_swag_foreach(process, simix_global->process_list){
 510           if(MC_process_is_enabled(process)){
 511             MC_state_interleave_process(next_graph_state, process);
 512           }
 513         }
 514
 515         xbt_dynar_reset(successors);
 516
 517         MC_UNSET_RAW_MEM;
 518
 519
 520         cursor= 0;
 521         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 522
 523           res = MC_automaton_evaluate_label(transition_succ->label);
 524
 525           if(res == 1){ // enabled transition in automaton
 526             MC_SET_RAW_MEM;
 527             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 528             xbt_dynar_push(successors, &next_pair);
 529             MC_UNSET_RAW_MEM;
 530           }
 531
 532         }
 533
 534         cursor = 0;
 535
 536         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 537
 538           res = MC_automaton_evaluate_label(transition_succ->label);
 539
 540           if(res == 2){ // true transition in automaton
 541             MC_SET_RAW_MEM;
 542             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 543             xbt_dynar_push(successors, &next_pair);
 544             MC_UNSET_RAW_MEM;
 545           }
 546
 547         }
 548
 549         cursor = 0;
 550
 551         xbt_dynar_foreach(successors, cursor, pair_succ){
 552
 553           if(!visited(pair_succ->automaton_state, search_cycle)){
 554
 555             if(search_cycle == 1){
 556
 557               if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 558
 559                 if(reached(pair_succ->automaton_state) == 1){
 560
 561                   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));
 562
 563                   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 564                   XBT_INFO("|             ACCEPTANCE CYCLE            |");
 565                   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 566                   XBT_INFO("Counter-example that violates formula :");
 567                   MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 568                   MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 569                   MC_print_statistics_pairs(mc_stats_pair);
 570                   exit(0);
 571
 572                 }else{
 573
 574                   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);
 575
 576                   set_pair_reached(pair_succ->automaton_state);
 577
 578                   XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs));
 579
 580                 }
 581
 582               }
 583
 584             }else{
 585
 586               if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 587
 588                 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);
 589
 590                 set_pair_reached(pair_succ->automaton_state);
 591
 592                 search_cycle = 1;
 593
 594                 XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs));
 595
 596               }
 597
 598             }
 599
 600             MC_SET_RAW_MEM;
 601             xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 602             MC_UNSET_RAW_MEM;
 603
 604             MC_ddfs_stateless(search_cycle);
 605
 606             /* Restore system before checking others successors */
 607             if(cursor != (xbt_dynar_length(successors) - 1))
 608               MC_replay_liveness(mc_stack_liveness_stateless, 1);
 609
 610           }else{
 611
 612             XBT_DEBUG("Next pair already visited");
 613
 614             if(search_cycle == 1){
 615
 616               if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 617
 618                 if(reached(pair_succ->automaton_state) == 1){
 619
 620                   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));
 621
 622                   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 623                   XBT_INFO("|             ACCEPTANCE CYCLE            |");
 624                   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 625                   XBT_INFO("Counter-example that violates formula :");
 626                   MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 627                   MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 628                   MC_print_statistics_pairs(mc_stats_pair);
 629                   exit(0);
 630
 631                 }
 632
 633               }
 634             }
 635
 636           }
 637         }
 638
 639         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 640           XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
 641           MC_replay_liveness(mc_stack_liveness_stateless, 0);
 642         }
 643       }
 644
 645
 646     }else{  /*No request to execute, search evolution in Büchi automaton */
 647
 648       MC_SET_RAW_MEM;
 649
 650       /* Create the new expanded graph_state */
 651       next_graph_state = MC_state_pair_new();
 652
 653       xbt_dynar_reset(successors);
 654
 655       MC_UNSET_RAW_MEM;
 656
 657
 658       cursor= 0;
 659       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 660
 661         res = MC_automaton_evaluate_label(transition_succ->label);
 662
 663         if(res == 1){ // enabled transition in automaton
 664           MC_SET_RAW_MEM;
 665           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 666           xbt_dynar_push(successors, &next_pair);
 667           MC_UNSET_RAW_MEM;
 668         }
 669
 670       }
 671
 672       cursor = 0;
 673
 674       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 675
 676         res = MC_automaton_evaluate_label(transition_succ->label);
 677
 678         if(res == 2){ // true transition in automaton
 679           MC_SET_RAW_MEM;
 680           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 681           xbt_dynar_push(successors, &next_pair);
 682           MC_UNSET_RAW_MEM;
 683         }
 684
 685       }
 686
 687       cursor = 0;
 688
 689       xbt_dynar_foreach(successors, cursor, pair_succ){
 690
 691         if(!visited(pair_succ->automaton_state, search_cycle)){
 692
 693           if(search_cycle == 1){
 694
 695             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 696
 697               if(reached(pair_succ->automaton_state) == 1){
 698
 699                 XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1);
 700
 701                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 702                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 703                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 704                 XBT_INFO("Counter-example that violates formula :");
 705                 MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 706                 MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 707                 MC_print_statistics_pairs(mc_stats_pair);
 708                 exit(0);
 709
 710               }else{
 711
 712                 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);
 713
 714                 set_pair_reached(pair_succ->automaton_state);
 715
 716                 XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs));
 717
 718               }
 719
 720             }
 721
 722           }else{
 723
 724             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (xbt_fifo_size(mc_stack_liveness_stateless) < (MAX_DEPTH_LIVENESS - 1))){
 725
 726               set_pair_reached(pair_succ->automaton_state);
 727
 728               search_cycle = 1;
 729
 730               XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs));
 731
 732             }
 733
 734           }
 735
 736           MC_SET_RAW_MEM;
 737           xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 738           MC_UNSET_RAW_MEM;
 739
 740           MC_ddfs_stateless(search_cycle);
 741
 742           /* Restore system before checking others successors */
 743           if(cursor != xbt_dynar_length(successors) - 1)
 744             MC_replay_liveness(mc_stack_liveness_stateless, 1);
 745
 746         }else{
 747
 748           XBT_DEBUG("Next pair already visited");
 749
 750           if(search_cycle == 1){
 751
 752             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 753
 754               if(reached(pair_succ->automaton_state) == 1){
 755
 756                 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));
 757
 758                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 759                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 760                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 761                 XBT_INFO("Counter-example that violates formula :");
 762                 MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 763                 MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 764                 MC_print_statistics_pairs(mc_stats_pair);
 765                 exit(0);
 766
 767               }
 768
 769             }
 770
 771           }
 772         }
 773
 774       }
 775
 776     }
 777
 778   }else{
 779
 780     XBT_DEBUG("Max depth reached");
 781
 782   }
 783
 784   if(xbt_fifo_size(mc_stack_liveness_stateless) == MAX_DEPTH_LIVENESS ){
 785     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) );
 786   }else{
 787     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) );
 788   }
 789
 790
 791   MC_SET_RAW_MEM;
 792   xbt_fifo_shift(mc_stack_liveness_stateless);
 793   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 794     xbt_fifo_shift(reached_pairs);
 795   }
 796   MC_UNSET_RAW_MEM;
 797
 798
 799
 800 }
 801