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;
  86
  87     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
  88       if(automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
  89         if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, compare_dynar) == 0){
  90           if(snapshot_compare(pair_test->system_state, pair->system_state) == 0){
  91             MC_UNSET_RAW_MEM;
  92             return 1;
  93           }
  94         }
  95       }
  96     }
  97
  98     MC_UNSET_RAW_MEM;
  99     return 0;
 100
 101   }
 102 }
 103
 104 int set_pair_reached(xbt_automaton_t a, mc_snapshot_t s){
 105
 106   if(reached(a, s) == 0){
 107
 108     MC_SET_RAW_MEM;
 109
 110     mc_pair_reached_t pair = NULL;
 111     pair = xbt_new0(s_mc_pair_reached_t, 1);
 112     pair->automaton_state = a->current_state;
 113     pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 114     pair->system_state = s;
 115
 116     /* Get values of propositional symbols */
 117     unsigned int cursor = 0;
 118     xbt_propositional_symbol_t ps = NULL;
 119     xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 120       int (*f)() = ps->function;
 121       int res = (*f)();
 122       xbt_dynar_push(pair->prop_ato, &res);
 123     }
 124
 125     xbt_dynar_push(reached_pairs, &pair);
 126
 127     MC_UNSET_RAW_MEM;
 128
 129     return 1;
 130
 131   }
 132
 133   return 0;
 134 }
 135
 136 void MC_pair_delete(mc_pair_t pair){
 137   xbt_free(pair->graph_state->proc_status);
 138   xbt_free(pair->graph_state);
 139   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 140   xbt_free(pair);
 141 }
 142
 143
 144 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 145
 146   switch(l->type){
 147   case 0 : {
 148     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 149     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 150     return (left_res || right_res);
 151     break;
 152   }
 153   case 1 : {
 154     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 155     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 156     return (left_res && right_res);
 157     break;
 158   }
 159   case 2 : {
 160     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
 161     return (!res);
 162     break;
 163   }
 164   case 3 : {
 165     unsigned int cursor = 0;
 166     xbt_propositional_symbol_t p = NULL;
 167     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
 168       if(strcmp(p->pred, l->u.predicat) == 0){
 169         int (*f)() = p->function;
 170         return (*f)();
 171       }
 172     }
 173     return -1;
 174     break;
 175   }
 176   case 4 : {
 177     return 2;
 178     break;
 179   }
 180   default :
 181     return -1;
 182   }
 183 }
 184
 185
 186
 187
 188
 189 /********************* Double-DFS stateless *******************/
 190
 191 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 192   xbt_free(pair->graph_state->proc_status);
 193   xbt_free(pair->graph_state);
 194   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 195   xbt_free(pair);
 196 }
 197
 198 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
 199   mc_pair_stateless_t p = NULL;
 200   p = xbt_new0(s_mc_pair_stateless_t, 1);
 201   p->automaton_state = st;
 202   p->graph_state = sg;
 203   mc_stats_pair->expanded_pairs++;
 204   return p;
 205 }
 206
 207
 208
 209 void MC_ddfs_stateless_init(xbt_automaton_t a){
 210
 211   XBT_DEBUG("**************************************************");
 212   XBT_DEBUG("Double-DFS stateless init");
 213   XBT_DEBUG("**************************************************");
 214
 215   mc_pair_stateless_t mc_initial_pair = NULL;
 216   mc_state_t initial_graph_state = NULL;
 217   smx_process_t process;
 218
 219   MC_wait_for_requests();
 220
 221   MC_SET_RAW_MEM;
 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
 231   initial_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   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
 301   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));
 302
 303
 304   mc_stats_pair->visited_pairs++;
 305
 306   int value;
 307   mc_state_t next_graph_state = NULL;
 308   smx_req_t req = NULL;
 309   char *req_str;
 310
 311   xbt_transition_t transition_succ;
 312   unsigned int cursor = 0;
 313   int res;
 314
 315   mc_pair_stateless_t next_pair = NULL;
 316   mc_pair_stateless_t pair_succ;
 317   mc_snapshot_t next_snapshot = NULL;
 318   mc_snapshot_t current_snapshot = NULL;
 319
 320   xbt_dynar_t successors = NULL;
 321
 322   MC_SET_RAW_MEM;
 323   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 324   MC_UNSET_RAW_MEM;
 325
 326   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 327
 328     MC_SET_RAW_MEM;
 329     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 330     MC_take_snapshot(current_snapshot);
 331     MC_UNSET_RAW_MEM;
 332
 333     /* Debug information */
 334     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 335       req_str = MC_request_to_string(req, value);
 336       XBT_DEBUG("Execute: %s", req_str);
 337       xbt_free(req_str);
 338     }
 339
 340     //sleep(1);
 341
 342     MC_state_set_executed_request(current_pair->graph_state, req, value);
 343
 344     /* Answer the request */
 345     SIMIX_request_pre(req, value);
 346
 347     /* Wait for requests (schedules processes) */
 348     MC_wait_for_requests();
 349
 350
 351     MC_SET_RAW_MEM;
 352
 353     /* Create the new expanded graph_state */
 354     next_graph_state = MC_state_pair_new();
 355
 356     /* Get enabled process and insert it in the interleave set of the next graph_state */
 357     xbt_swag_foreach(process, simix_global->process_list){
 358       if(MC_process_is_enabled(process)){
 359         MC_state_interleave_process(next_graph_state, process);
 360       }
 361     }
 362
 363     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 364     MC_take_snapshot(next_snapshot);
 365
 366     xbt_dynar_reset(successors);
 367
 368     if(snapshot_compare(current_snapshot,next_snapshot)){
 369       XBT_DEBUG("Different snapshot");
 370       //sleep(2);
 371
 372     }
 373
 374     MC_UNSET_RAW_MEM;
 375
 376
 377     cursor= 0;
 378     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 379
 380       res = MC_automaton_evaluate_label(a, transition_succ->label);
 381
 382       if(res == 1){ // enabled transition in automaton
 383         MC_SET_RAW_MEM;
 384         next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
 385         xbt_dynar_push(successors, &next_pair);
 386         MC_UNSET_RAW_MEM;
 387       }
 388
 389     }
 390
 391     cursor = 0;
 392
 393     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 394
 395       res = MC_automaton_evaluate_label(a, transition_succ->label);
 396
 397       if(res == 2){ // true transition in automaton
 398         MC_SET_RAW_MEM;
 399         next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
 400         xbt_dynar_push(successors, &next_pair);
 401         MC_UNSET_RAW_MEM;
 402       }
 403
 404     }
 405
 406
 407     if(xbt_dynar_length(successors) == 0){
 408       MC_SET_RAW_MEM;
 409       next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);
 410       xbt_dynar_push(successors, &next_pair);
 411       MC_UNSET_RAW_MEM;
 412     }
 413
 414     cursor = 0;
 415
 416     xbt_dynar_foreach(successors, cursor, pair_succ){
 417
 418       if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){
 419         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 420         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 421         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 422         XBT_INFO("Counter-example that violates formula :");
 423         MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 424         MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 425         MC_print_statistics_pairs(mc_stats_pair);
 426         exit(0);
 427       }
 428
 429       MC_SET_RAW_MEM;
 430       xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 431       MC_UNSET_RAW_MEM;
 432
 433       MC_ddfs_stateless(a, search_cycle, 0);
 434
 435
 436       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 437
 438         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);
 439         int res = set_pair_reached(a, next_snapshot);
 440
 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         if(res){
 448           MC_SET_RAW_MEM;
 449           xbt_dynar_pop(reached_pairs, NULL);
 450           MC_UNSET_RAW_MEM;
 451         }
 452       }
 453     }
 454
 455     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 456       XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
 457       MC_replay_liveness(mc_stack_liveness_stateless);
 458     }
 459
 460   }
 461
 462   MC_SET_RAW_MEM;
 463   xbt_fifo_shift(mc_stack_liveness_stateless);
 464   XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
 465   MC_UNSET_RAW_MEM;
 466
 467 }
 468
 469 /********************* Double-DFS stateful without visited state *******************/
 470
 471
 472 void MC_ddfs_stateful_init(xbt_automaton_t a){
 473
 474   XBT_DEBUG("**************************************************");
 475   XBT_DEBUG("Double-DFS stateful without visited state init");
 476   XBT_DEBUG("**************************************************");
 477
 478   mc_pair_t mc_initial_pair;
 479   mc_state_t initial_graph_state;
 480   smx_process_t process;
 481   mc_snapshot_t init_snapshot;
 482
 483   MC_wait_for_requests();
 484
 485   MC_SET_RAW_MEM;
 486
 487   init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 488
 489   initial_graph_state = MC_state_pair_new();
 490   xbt_swag_foreach(process, simix_global->process_list){
 491     if(MC_process_is_enabled(process)){
 492       MC_state_interleave_process(initial_graph_state, process);
 493     }
 494   }
 495
 496   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
 497
 498   MC_take_snapshot(init_snapshot);
 499
 500   MC_UNSET_RAW_MEM;
 501
 502   unsigned int cursor = 0;
 503   xbt_state_t state = NULL;
 504
 505   xbt_dynar_foreach(a->states, cursor, state){
 506     if(state->type == -1){
 507
 508       MC_SET_RAW_MEM;
 509       mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
 510       xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
 511       MC_UNSET_RAW_MEM;
 512
 513       if(cursor == 0){
 514         MC_ddfs_stateful(a, 0, 0);
 515       }else{
 516         MC_restore_snapshot(init_snapshot);
 517         MC_UNSET_RAW_MEM;
 518         MC_ddfs_stateful(a, 0, 0);
 519       }
 520     }else{
 521        if(state->type == 2){
 522
 523          MC_SET_RAW_MEM;
 524          mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
 525          xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
 526          MC_UNSET_RAW_MEM;
 527
 528          if(cursor == 0){
 529            MC_ddfs_stateful(a, 1, 0);
 530          }else{
 531            MC_restore_snapshot(init_snapshot);
 532            MC_UNSET_RAW_MEM;
 533            MC_ddfs_stateful(a, 1, 0);
 534          }
 535        }
 536     }
 537   }
 538 }
 539
 540
 541 void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 542
 543   smx_process_t process = NULL;
 544   mc_pair_t current_pair = NULL;
 545
 546   if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
 547     return;
 548
 549   if(restore == 1){
 550     current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 551     MC_restore_snapshot(current_pair->system_state);
 552     xbt_swag_foreach(process, simix_global->process_list){
 553       if(MC_process_is_enabled(process)){
 554         MC_state_interleave_process(current_pair->graph_state, process);
 555       }
 556     }
 557     MC_UNSET_RAW_MEM;
 558   }
 559
 560   /* Get current state */
 561   current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
 562
 563
 564   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle);
 565   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));
 566
 567   a->current_state = current_pair->automaton_state;
 568
 569   mc_stats_pair->visited_pairs++;
 570
 571   int value;
 572   mc_state_t next_graph_state = NULL;
 573   smx_req_t req = NULL;
 574   char *req_str;
 575
 576   mc_pair_t pair_succ;
 577   xbt_transition_t transition_succ;
 578   unsigned int cursor;
 579   int res;
 580
 581   xbt_dynar_t successors = NULL;
 582
 583   mc_pair_t next_pair = NULL;
 584   mc_snapshot_t next_snapshot = NULL;
 585   mc_snapshot_t current_snapshot = NULL;
 586
 587   //sleep(1);
 588   MC_SET_RAW_MEM;
 589   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 590   MC_UNSET_RAW_MEM;
 591
 592   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 593
 594     MC_SET_RAW_MEM;
 595     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 596     MC_take_snapshot(current_snapshot);
 597     MC_UNSET_RAW_MEM;
 598
 599
 600     /* Debug information */
 601     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 602       req_str = MC_request_to_string(req, value);
 603       XBT_DEBUG("Execute: %s", req_str);
 604       xbt_free(req_str);
 605     }
 606
 607     MC_state_set_executed_request(current_pair->graph_state, req, value);
 608
 609     /* Answer the request */
 610     SIMIX_request_pre(req, value);
 611
 612     /* Wait for requests (schedules processes) */
 613     MC_wait_for_requests();
 614
 615
 616     /* Create the new expanded graph_state */
 617     MC_SET_RAW_MEM;
 618
 619     next_graph_state = MC_state_pair_new();
 620
 621     /* Get enabled process and insert it in the interleave set of the next graph_state */
 622     xbt_swag_foreach(process, simix_global->process_list){
 623       if(MC_process_is_enabled(process)){
 624         MC_state_interleave_process(next_graph_state, process);
 625       }
 626     }
 627
 628     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 629     MC_take_snapshot(next_snapshot);
 630
 631     xbt_dynar_reset(successors);
 632
 633     MC_UNSET_RAW_MEM;
 634
 635
 636     cursor = 0;
 637     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 638
 639       res = MC_automaton_evaluate_label(a, transition_succ->label);
 640
 641       if(res == 1){ // enabled transition in automaton
 642         MC_SET_RAW_MEM;
 643         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 644         xbt_dynar_push(successors, &next_pair);
 645         MC_UNSET_RAW_MEM;
 646       }
 647
 648     }
 649
 650     cursor = 0;
 651     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 652
 653       res = MC_automaton_evaluate_label(a, transition_succ->label);
 654
 655       if(res == 2){ // transition always enabled in automaton
 656         MC_SET_RAW_MEM;
 657         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 658         xbt_dynar_push(successors, &next_pair);
 659         MC_UNSET_RAW_MEM;
 660       }
 661
 662
 663     }
 664
 665
 666     if(xbt_dynar_length(successors) == 0){
 667
 668       MC_SET_RAW_MEM;
 669       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
 670       xbt_dynar_push(successors, &next_pair);
 671       MC_UNSET_RAW_MEM;
 672
 673     }
 674
 675     //XBT_DEBUG("Successors in automaton %lu", xbt_dynar_length(successors));
 676
 677     cursor = 0;
 678     xbt_dynar_foreach(successors, cursor, pair_succ){
 679
 680       //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 681
 682       if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){
 683         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 684         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 685         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 686         XBT_INFO("Counter-example that violates formula :");
 687         MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
 688         MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
 689         MC_print_statistics_pairs(mc_stats_pair);
 690         exit(0);
 691       }
 692
 693       //mc_stats_pair->executed_transitions++;
 694
 695       MC_SET_RAW_MEM;
 696       xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 697       MC_UNSET_RAW_MEM;
 698
 699       MC_ddfs_stateful(a, search_cycle, 0);
 700
 701
 702       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 703
 704         int res = set_pair_reached(a, next_snapshot);
 705         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 706
 707         MC_SET_RAW_MEM;
 708         xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 709         MC_UNSET_RAW_MEM;
 710
 711         MC_ddfs_stateful(a, 1, 1);
 712
 713         if(res){
 714           MC_SET_RAW_MEM;
 715           xbt_dynar_pop(reached_pairs, NULL);
 716           MC_UNSET_RAW_MEM;
 717         }
 718       }
 719
 720     }
 721
 722     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 723       XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateful));
 724       MC_restore_snapshot(current_snapshot);
 725       MC_UNSET_RAW_MEM;
 726     }
 727
 728   }
 729
 730
 731   MC_SET_RAW_MEM;
 732   xbt_fifo_shift(mc_stack_liveness_stateful);
 733   XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
 734   MC_UNSET_RAW_MEM;
 735
 736 }