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   XBT_DEBUG("Test reached");
  64
  65   if(xbt_dynar_is_empty(reached_pairs)){
  66     return 0;
  67   }else{
  68     MC_SET_RAW_MEM;
  69
  70     mc_pair_reached_t pair = NULL;
  71     pair = xbt_new0(s_mc_pair_reached_t, 1);
  72     pair->automaton_state = a->current_state;
  73     pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
  74     pair->system_state = s;
  75
  76     /* Get values of propositional symbols */
  77     unsigned int cursor = 0;
  78     xbt_propositional_symbol_t ps = NULL;
  79     xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
  80       int (*f)() = ps->function;
  81       int res = (*f)();
  82       xbt_dynar_push_as(pair->prop_ato, int, res);
  83     }
  84
  85     cursor = 0;
  86     mc_pair_reached_t pair_test;
  87     //int (*compare_dynar)(const void*, const void*) = &propositional_symbols_compare_value;
  88     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
  89       if(automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
  90         if(propositional_symbols_compare_value(pair_test->prop_ato, pair->prop_ato) == 0){
  91           if(snapshot_compare(pair_test->system_state, pair->system_state) == 0){
  92             MC_UNSET_RAW_MEM;
  93             return 1;
  94           }
  95         }
  96       }
  97     }
  98
  99     MC_UNSET_RAW_MEM;
 100     return 0;
 101
 102   }
 103 }
 104
 105 int set_pair_reached(xbt_automaton_t a, mc_snapshot_t s){
 106
 107   if(reached(a, s) == 0){
 108
 109     MC_SET_RAW_MEM;
 110
 111     mc_pair_reached_t pair = NULL;
 112     pair = xbt_new0(s_mc_pair_reached_t, 1);
 113     pair->automaton_state = a->current_state;
 114     pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 115     pair->system_state = s;
 116
 117     /* Get values of propositional symbols */
 118     unsigned int cursor = 0;
 119     xbt_propositional_symbol_t ps = NULL;
 120     xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 121       int (*f)() = ps->function;
 122       int res = (*f)();
 123       xbt_dynar_push_as(pair->prop_ato, int, res);
 124     }
 125
 126     xbt_dynar_push(reached_pairs, &pair);
 127
 128     MC_UNSET_RAW_MEM;
 129
 130     return 1;
 131
 132   }
 133
 134   return 0;
 135 }
 136
 137 void MC_pair_delete(mc_pair_t pair){
 138   xbt_free(pair->graph_state->proc_status);
 139   xbt_free(pair->graph_state);
 140   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 141   xbt_free(pair);
 142 }
 143
 144
 145 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 146
 147   switch(l->type){
 148   case 0 : {
 149     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 150     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 151     return (left_res || right_res);
 152     break;
 153   }
 154   case 1 : {
 155     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 156     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 157     return (left_res && right_res);
 158     break;
 159   }
 160   case 2 : {
 161     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
 162     return (!res);
 163     break;
 164   }
 165   case 3 : {
 166     unsigned int cursor = 0;
 167     xbt_propositional_symbol_t p = NULL;
 168     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
 169       if(strcmp(p->pred, l->u.predicat) == 0){
 170         int (*f)() = p->function;
 171         return (*f)();
 172       }
 173     }
 174     return -1;
 175     break;
 176   }
 177   case 4 : {
 178     return 2;
 179     break;
 180   }
 181   default :
 182     return -1;
 183   }
 184 }
 185
 186
 187
 188
 189
 190 /********************* Double-DFS stateless *******************/
 191
 192 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 193   xbt_free(pair->graph_state->proc_status);
 194   xbt_free(pair->graph_state);
 195   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 196   xbt_free(pair);
 197 }
 198
 199 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
 200   mc_pair_stateless_t p = NULL;
 201   p = xbt_new0(s_mc_pair_stateless_t, 1);
 202   p->automaton_state = st;
 203   p->graph_state = sg;
 204   mc_stats_pair->expanded_pairs++;
 205   return p;
 206 }
 207
 208
 209
 210 void MC_ddfs_stateless_init(xbt_automaton_t a){
 211
 212   XBT_DEBUG("**************************************************");
 213   XBT_DEBUG("Double-DFS stateless init");
 214   XBT_DEBUG("**************************************************");
 215
 216   mc_pair_stateless_t mc_initial_pair = NULL;
 217   mc_state_t initial_graph_state = NULL;
 218   smx_process_t process;
 219
 220   MC_wait_for_requests();
 221
 222   MC_SET_RAW_MEM;
 223   initial_graph_state = MC_state_pair_new();
 224   xbt_swag_foreach(process, simix_global->process_list){
 225     if(MC_process_is_enabled(process)){
 226       MC_state_interleave_process(initial_graph_state, process);
 227     }
 228   }
 229
 230   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
 231
 232   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 233   MC_take_snapshot(initial_snapshot);
 234
 235   MC_UNSET_RAW_MEM;
 236
 237   unsigned int cursor = 0;
 238   xbt_state_t state;
 239
 240   xbt_dynar_foreach(a->states, cursor, state){
 241     if(state->type == -1){
 242
 243       MC_SET_RAW_MEM;
 244       mc_initial_pair = new_pair_stateless(initial_graph_state, state);
 245       xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 246       MC_UNSET_RAW_MEM;
 247
 248       if(cursor == 0){
 249         MC_ddfs_stateless(a, 0, 0);
 250       }else{
 251         MC_restore_snapshot(initial_snapshot);
 252         MC_UNSET_RAW_MEM;
 253         MC_ddfs_stateless(a, 0, 0);
 254       }
 255     }else{
 256       if(state->type == 2){
 257
 258         MC_SET_RAW_MEM;
 259         mc_initial_pair = new_pair_stateless(initial_graph_state, state);
 260         xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 261         MC_UNSET_RAW_MEM;
 262
 263         if(cursor == 0){
 264           MC_ddfs_stateless(a, 1, 0);
 265         }else{
 266           MC_restore_snapshot(initial_snapshot);
 267           MC_UNSET_RAW_MEM;
 268           MC_ddfs_stateless(a, 1, 0);
 269         }
 270       }
 271     }
 272   }
 273
 274 }
 275
 276
 277 void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
 278
 279   smx_process_t process;
 280   mc_pair_stateless_t current_pair = NULL;
 281
 282   if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
 283     return;
 284
 285   if(replay == 1){
 286     MC_replay_liveness(mc_stack_liveness_stateless);
 287     current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 288     xbt_swag_foreach(process, simix_global->process_list){
 289       if(MC_process_is_enabled(process)){
 290         MC_state_interleave_process(current_pair->graph_state, process);
 291       }
 292     }
 293   }
 294
 295   /* Get current pair */
 296   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 297
 298   /* Update current state in buchi automaton */
 299   a->current_state = current_pair->automaton_state;
 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   mc_stats_pair->visited_pairs++;
 306
 307   int value;
 308   mc_state_t next_graph_state = NULL;
 309   smx_req_t req = NULL;
 310   char *req_str;
 311
 312   xbt_transition_t transition_succ;
 313   unsigned int cursor = 0;
 314   int res;
 315
 316   mc_pair_stateless_t next_pair = NULL;
 317   mc_pair_stateless_t pair_succ;
 318   mc_snapshot_t next_snapshot = NULL;
 319   mc_snapshot_t current_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     MC_SET_RAW_MEM;
 330     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 331     MC_take_snapshot(current_snapshot);
 332     MC_UNSET_RAW_MEM;
 333
 334     /* Debug information */
 335     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 336       req_str = MC_request_to_string(req, value);
 337       XBT_DEBUG("Execute: %s", req_str);
 338       xbt_free(req_str);
 339     }
 340
 341     //sleep(1);
 342
 343     MC_state_set_executed_request(current_pair->graph_state, req, value);
 344
 345     /* Answer the request */
 346     SIMIX_request_pre(req, value);
 347
 348     /* Wait for requests (schedules processes) */
 349     MC_wait_for_requests();
 350
 351
 352     MC_SET_RAW_MEM;
 353
 354     /* Create the new expanded graph_state */
 355     next_graph_state = MC_state_pair_new();
 356
 357     /* Get enabled process and insert it in the interleave set of the next graph_state */
 358     xbt_swag_foreach(process, simix_global->process_list){
 359       if(MC_process_is_enabled(process)){
 360         MC_state_interleave_process(next_graph_state, process);
 361       }
 362     }
 363
 364     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 365     MC_take_snapshot(next_snapshot);
 366
 367     xbt_dynar_reset(successors);
 368
 369     if(snapshot_compare(current_snapshot,next_snapshot)){
 370       XBT_DEBUG("Different snapshot");
 371       //sleep(2);
 372
 373     }
 374
 375     MC_UNSET_RAW_MEM;
 376
 377
 378     cursor= 0;
 379     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 380
 381       res = MC_automaton_evaluate_label(a, transition_succ->label);
 382
 383       if(res == 1){ // enabled transition in automaton
 384         MC_SET_RAW_MEM;
 385         next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
 386         xbt_dynar_push(successors, &next_pair);
 387         MC_UNSET_RAW_MEM;
 388       }
 389
 390     }
 391
 392     cursor = 0;
 393
 394     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 395
 396       res = MC_automaton_evaluate_label(a, transition_succ->label);
 397
 398       if(res == 2){ // true transition in automaton
 399         MC_SET_RAW_MEM;
 400         next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
 401         xbt_dynar_push(successors, &next_pair);
 402         MC_UNSET_RAW_MEM;
 403       }
 404
 405     }
 406
 407
 408     if(xbt_dynar_length(successors) == 0){
 409       MC_SET_RAW_MEM;
 410       next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);
 411       xbt_dynar_push(successors, &next_pair);
 412       MC_UNSET_RAW_MEM;
 413     }
 414
 415     cursor = 0;
 416
 417     xbt_dynar_foreach(successors, cursor, pair_succ){
 418
 419       if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){
 420         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 421         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 422         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 423         XBT_INFO("Counter-example that violates formula :");
 424         MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 425         MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 426         MC_print_statistics_pairs(mc_stats_pair);
 427         exit(0);
 428       }
 429
 430       MC_SET_RAW_MEM;
 431       xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 432       MC_UNSET_RAW_MEM;
 433
 434       MC_ddfs_stateless(a, search_cycle, 0);
 435
 436
 437       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 438
 439         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);
 440         int res = set_pair_reached(a, next_snapshot);
 441
 442         MC_SET_RAW_MEM;
 443         xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 444         MC_UNSET_RAW_MEM;
 445
 446         MC_ddfs_stateless(a, 1, 1);
 447
 448         if(res){
 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
 683       if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){
 684         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 685         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 686         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 687         XBT_INFO("Counter-example that violates formula :");
 688         MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
 689         MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
 690         MC_print_statistics_pairs(mc_stats_pair);
 691         exit(0);
 692       }
 693
 694       //mc_stats_pair->executed_transitions++;
 695
 696       MC_SET_RAW_MEM;
 697       xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 698       MC_UNSET_RAW_MEM;
 699
 700       MC_ddfs_stateful(a, search_cycle, 0);
 701
 702
 703       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 704
 705         int res = set_pair_reached(a, next_snapshot);
 706         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 707
 708         MC_SET_RAW_MEM;
 709         xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 710         MC_UNSET_RAW_MEM;
 711
 712         MC_ddfs_stateful(a, 1, 1);
 713
 714         if(res){
 715           MC_SET_RAW_MEM;
 716           xbt_dynar_pop(reached_pairs, NULL);
 717           MC_UNSET_RAW_MEM;
 718         }
 719       }
 720
 721     }
 722
 723     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 724       XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateful));
 725       MC_restore_snapshot(current_snapshot);
 726       MC_UNSET_RAW_MEM;
 727     }
 728
 729   }
 730
 731
 732   MC_SET_RAW_MEM;
 733   xbt_fifo_shift(mc_stack_liveness_stateful);
 734   XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
 735   MC_UNSET_RAW_MEM;
 736
 737 }