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