src/mc/mc_liveness.c

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