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