src/mc/mc_dfs.c

   1 #include "private.h"
   2 #include "unistd.h"
   3
   4 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc,
   5                                 "Logging specific to MC DFS algorithm");
   6
   7 xbt_dynar_t initial_pairs = NULL;
   8 int max_pair = 0;
   9 xbt_dynar_t visited_pairs;
  10 xbt_dynar_t reached_pairs;
  11
  12 mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
  13   mc_pairs_t p = NULL;
  14   p = xbt_new0(s_mc_pairs_t, 1);
  15   p->system_state = sn;
  16    p->automaton_state = st;
  17   p->graph_state = sg;
  18   p->num = max_pair;
  19   max_pair++;
  20   return p;
  21
  22 }
  23
  24 void set_pair_visited(mc_state_t gs, xbt_state_t as, int sc){
  25
  26   //XBT_DEBUG("New visited pair : graph=%p, automaton=%p", gs, as);
  27   MC_SET_RAW_MEM;
  28   mc_visited_pairs_t p = NULL;
  29   p = xbt_new0(s_mc_visited_pairs_t, 1);
  30   p->graph_state = gs;
  31   p->automaton_state = as;
  32   p->search_cycle = sc;
  33   xbt_dynar_push(visited_pairs, &p);
  34   //XBT_DEBUG("New visited pair , length of visited pairs : %lu", xbt_dynar_length(visited_pairs));
  35   MC_UNSET_RAW_MEM;
  36
  37   //XBT_DEBUG("New visited pair , length of visited pairs : %lu", xbt_dynar_length(visited_pairs));
  38 }
  39
  40 int reached(mc_state_t gs, xbt_state_t as ){
  41
  42   mc_reached_pairs_t rp = NULL;
  43   unsigned int c= 0;
  44   unsigned int i;
  45   int different_process;
  46
  47   MC_SET_RAW_MEM;
  48   xbt_dynar_foreach(reached_pairs, c, rp){
  49     if(rp->automaton_state == as){
  50       different_process=0;
  51       for(i=0; i < gs->max_pid; i++){
  52         if(gs->proc_status[i].state != rp->graph_state->proc_status[i].state){
  53           different_process++;
  54         }
  55       }
  56       if(different_process==0){
  57         MC_UNSET_RAW_MEM;
  58         XBT_DEBUG("Pair (graph=%p, automaton=%p(%s)) already reached (graph=%p)!", gs, as, as->id, rp->graph_state);
  59         return 1;
  60       }
  61       /* XBT_DEBUG("Pair (graph=%p, automaton=%p(%s)) already reached !", gs, as, as->id); */
  62       /* return 1; */
  63     }
  64   }
  65   MC_UNSET_RAW_MEM;
  66   return 0;
  67 }
  68
  69 void set_pair_reached(mc_state_t gs, xbt_state_t as){
  70
  71   //XBT_DEBUG("Set pair (graph=%p, automaton=%p) reached ", gs, as);
  72   //if(reached(gs, as) == 0){
  73     MC_SET_RAW_MEM;
  74     mc_reached_pairs_t p = NULL;
  75     p = xbt_new0(s_mc_reached_pairs_t, 1);
  76     p->graph_state = gs;
  77     p->automaton_state = as;
  78     xbt_dynar_push(reached_pairs, &p);
  79     XBT_DEBUG("New reached pair : graph=%p, automaton=%p(%s)", gs, as, as->id);
  80     MC_UNSET_RAW_MEM;
  81     //}
  82
  83 }
  84
  85 int visited(mc_state_t gs, xbt_state_t as, int sc){
  86   unsigned int c = 0;
  87   mc_visited_pairs_t p = NULL;
  88   unsigned int i;
  89   int different_process;
  90
  91   //XBT_DEBUG("Visited pair length : %lu", xbt_dynar_length(visited_pairs));
  92
  93   MC_SET_RAW_MEM;
  94   xbt_dynar_foreach(visited_pairs, c, p){
  95     //XBT_DEBUG("Test pair visited");
  96     //sleep(1);
  97     if((p->automaton_state == as) && (p->search_cycle == sc)){
  98       different_process=0;
  99       for(i=0; i < gs->max_pid; i++){
 100         if(gs->proc_status[i].state != p->graph_state->proc_status[i].state){
 101           different_process++;
 102         }
 103       }
 104       if(different_process==0){
 105         MC_UNSET_RAW_MEM;
 106         return 1;
 107       }
 108     }
 109   }
 110   MC_UNSET_RAW_MEM;
 111   return 0;
 112
 113 }
 114
 115 void MC_dfs_init(xbt_automaton_t a){
 116
 117    XBT_DEBUG("**************************************************");
 118    XBT_DEBUG("DFS init");
 119    XBT_DEBUG("**************************************************");
 120
 121   mc_pairs_t mc_initial_pair;
 122   mc_state_t initial_graph_state;
 123   smx_process_t process;
 124   mc_snapshot_t init_snapshot;
 125
 126   MC_wait_for_requests();
 127
 128   MC_SET_RAW_MEM;
 129
 130   init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 131
 132   initial_graph_state = MC_state_pair_new();
 133   xbt_swag_foreach(process, simix_global->process_list){
 134     if(MC_process_is_enabled(process)){
 135       MC_state_interleave_process(initial_graph_state, process);
 136     }
 137   }
 138
 139   visited_pairs = xbt_dynar_new(sizeof(mc_visited_pairs_t), NULL);
 140   reached_pairs = xbt_dynar_new(sizeof(mc_reached_pairs_t), NULL);
 141
 142   MC_take_snapshot(init_snapshot);
 143
 144   MC_UNSET_RAW_MEM;
 145
 146   /* unsigned int cursor = 0; */
 147   /* xbt_state_t state = NULL; */
 148   /* int nb_init_state = 0; */
 149
 150   /* xbt_dynar_foreach(a->states, cursor, state){ */
 151   /*   if(state->type == -1){ */
 152
 153   /*     MC_SET_RAW_MEM; */
 154   /*     mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state); */
 155
 156   /*     xbt_fifo_unshift(mc_snapshot_stack, mc_initial_pair); */
 157
 158   /*     XBT_DEBUG("**************************************************"); */
 159   /*     XBT_DEBUG("Initial state=%p ", mc_initial_pair); */
 160
 161   /*     MC_UNSET_RAW_MEM; */
 162
 163   /*     set_pair_visited(mc_initial_pair->graph_state, mc_initial_pair->automaton_state, 0); */
 164
 165   /*     if(nb_init_state == 0) */
 166   /*    MC_dfs(a, 0, 0); */
 167   /*     else */
 168   /*    MC_dfs(a, 0, 1); */
 169
 170   /*     nb_init_state++; */
 171   /*   } */
 172   /* } */
 173
 174   /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
 175     -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
 176
 177   unsigned int cursor = 0;
 178   unsigned int cursor2 = 0;
 179   xbt_state_t state = NULL;
 180   int res;
 181   xbt_transition_t transition_succ;
 182   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
 183   xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
 184   mc_pairs_t pair_succ;
 185
 186   xbt_dynar_foreach(a->states, cursor, state){
 187     if(state->type == -1){
 188       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 189         res = MC_automaton_evaluate_label(a, transition_succ->label);
 190
 191         if(res == 1){
 192
 193           MC_SET_RAW_MEM;
 194
 195           mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 196           xbt_dynar_push(successors, &mc_initial_pair);
 197
 198           MC_UNSET_RAW_MEM;
 199
 200         }else{
 201           if(res == 2){
 202
 203             MC_SET_RAW_MEM;
 204
 205             mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 206             xbt_dynar_push(elses, &mc_initial_pair);
 207
 208             MC_UNSET_RAW_MEM;
 209           }
 210         }
 211       }
 212     }
 213   }
 214
 215
 216   cursor = 0;
 217   xbt_dynar_foreach(successors, cursor, pair_succ){
 218     MC_SET_RAW_MEM;
 219
 220     xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 221
 222     XBT_DEBUG("**************************************************");
 223     XBT_DEBUG("Initial pair=%p (graph=%p, automaton=%p(%s)) ", pair_succ, pair_succ->graph_state, pair_succ->automaton_state,pair_succ->automaton_state->id );
 224
 225     MC_UNSET_RAW_MEM;
 226
 227     set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
 228
 229     if(cursor == 0){
 230       MC_dfs(a, 0, 0);
 231     }else{
 232       MC_dfs(a, 0, 1);
 233     }
 234   }
 235
 236   cursor = 0;
 237   xbt_dynar_foreach(elses, cursor, pair_succ){
 238     MC_SET_RAW_MEM;
 239
 240     xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 241
 242     XBT_DEBUG("**************************************************");
 243     XBT_DEBUG("Initial pair=%p (graph=%p, automaton=%p(%s)) ", pair_succ, pair_succ->graph_state, pair_succ->automaton_state,pair_succ->automaton_state->id );
 244
 245     MC_UNSET_RAW_MEM;
 246
 247     set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
 248
 249     if((xbt_dynar_length(successors) == 0) && (cursor == 0)){
 250       MC_dfs(a, 0, 0);
 251     }else{
 252       MC_dfs(a, 0, 1);
 253     }
 254   }
 255
 256 }
 257
 258
 259 void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
 260
 261   smx_process_t process = NULL;
 262
 263
 264   if(xbt_fifo_size(mc_snapshot_stack) == 0)
 265     return;
 266
 267   if(restore == 1){
 268     MC_restore_snapshot(((mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
 269     MC_UNSET_RAW_MEM;
 270   }
 271
 272   //XBT_DEBUG("Lpv length after restore snapshot: %lu", xbt_dynar_length(visited_pairs));
 273
 274   /* Get current state */
 275   mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 276
 277   if(restore==1){
 278     xbt_swag_foreach(process, simix_global->process_list){
 279       if(MC_process_is_enabled(process)){
 280         //XBT_DEBUG("Pid : %lu", process->pid);
 281         MC_state_interleave_process(current_pair->graph_state, process);
 282       }
 283     }
 284   }
 285
 286   XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
 287   XBT_DEBUG("State : 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));
 288   //XBT_DEBUG("Restore : %d", restore);
 289
 290   //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 291
 292   //sleep(1);
 293
 294   mc_stats_pair->visited_pairs++;
 295
 296   int value;
 297   mc_state_t next_graph_state = NULL;
 298   smx_req_t req = NULL;
 299   char *req_str;
 300
 301   mc_pairs_t pair_succ;
 302   xbt_transition_t transition_succ;
 303   unsigned int cursor;
 304   int res;
 305   //int enabled_transition = 0;
 306
 307   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
 308   xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
 309
 310   mc_pairs_t next_pair;
 311   mc_snapshot_t next_snapshot;
 312   mc_snapshot_t current_snapshot;
 313
 314
 315   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 316
 317     MC_SET_RAW_MEM;
 318     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 319     MC_take_snapshot(current_snapshot);
 320     MC_UNSET_RAW_MEM;
 321
 322
 323     /* Debug information */
 324     if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){
 325       req_str = MC_request_to_string(req, value);
 326       XBT_DEBUG("Execute: %s", req_str);
 327       xbt_free(req_str);
 328     }
 329
 330     MC_state_set_executed_request(current_pair->graph_state, req, value);
 331
 332     /* Answer the request */
 333     SIMIX_request_pre(req, value);
 334
 335     /* Wait for requests (schedules processes) */
 336     MC_wait_for_requests();
 337
 338
 339     /* Create the new expanded graph_state */
 340     MC_SET_RAW_MEM;
 341
 342     next_graph_state = MC_state_pair_new();
 343
 344     /* Get enabled process and insert it in the interleave set of the next graph_state */
 345     xbt_swag_foreach(process, simix_global->process_list){
 346       if(MC_process_is_enabled(process)){
 347         //XBT_DEBUG("Pid : %lu", process->pid);
 348         MC_state_interleave_process(next_graph_state, process);
 349       }
 350     }
 351
 352     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 353     MC_take_snapshot(next_snapshot);
 354
 355     MC_UNSET_RAW_MEM;
 356
 357     xbt_dynar_reset(successors);
 358     xbt_dynar_reset(elses);
 359
 360     cursor = 0;
 361     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 362
 363       res = MC_automaton_evaluate_label(a, transition_succ->label);
 364
 365       MC_SET_RAW_MEM;
 366       next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 367
 368       //XBT_DEBUG("Next pair : %p", next_pair);
 369
 370       if(res == 1){ // enabled transition in automaton
 371         xbt_dynar_push(successors, &next_pair);
 372         mc_stats_pair->expanded_pairs++;
 373       }else{
 374         if(res == 2){ // enabled transition in automaton
 375           xbt_dynar_push(elses, &next_pair);
 376           mc_stats_pair->expanded_pairs++;
 377         }
 378       }
 379
 380       MC_UNSET_RAW_MEM;
 381     }
 382
 383
 384     if(xbt_dynar_length(successors) == 0){
 385
 386       MC_SET_RAW_MEM;
 387       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
 388       xbt_dynar_push(successors, &next_pair);
 389       mc_stats_pair->expanded_pairs++;
 390       MC_UNSET_RAW_MEM;
 391
 392     }
 393
 394
 395     cursor = 0;
 396     xbt_dynar_foreach(successors, cursor, pair_succ){
 397
 398       //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 399
 400       if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){
 401         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 402         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 403         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 404         XBT_INFO("Counter-example that violates formula :");
 405         MC_show_snapshot_stack(mc_snapshot_stack);
 406         MC_dump_snapshot_stack(mc_snapshot_stack);
 407         MC_print_statistics_pairs(mc_stats_pair);
 408         exit(0);
 409       }
 410
 411       if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
 412
 413         //XBT_DEBUG("Unvisited pair !");
 414
 415         mc_stats_pair->executed_transitions++;
 416
 417         MC_SET_RAW_MEM;
 418         xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 419         MC_UNSET_RAW_MEM;
 420
 421         set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
 422         MC_dfs(a, search_cycle, 0);
 423
 424         if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 425
 426           MC_restore_snapshot(current_pair->system_state);
 427           MC_UNSET_RAW_MEM;
 428
 429           xbt_swag_foreach(process, simix_global->process_list){
 430             if(MC_process_is_enabled(process)){
 431               //XBT_DEBUG("Pid : %lu", process->pid);
 432               MC_state_interleave_process(current_pair->graph_state, process);
 433             }
 434           }
 435
 436           set_pair_reached(current_pair->graph_state, current_pair->automaton_state);
 437           XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
 438           MC_dfs(a, 1, 1);
 439
 440         }
 441       }
 442     }
 443
 444     cursor = 0;
 445     xbt_dynar_foreach(elses, cursor, pair_succ){
 446
 447       //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 448
 449       if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){
 450         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 451         XBT_INFO("|             ACCEPTANCE CYCLE            |");
 452         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 453         XBT_INFO("Counter-example that violates formula :");
 454         MC_show_snapshot_stack(mc_snapshot_stack);
 455         MC_dump_snapshot_stack(mc_snapshot_stack);
 456         MC_print_statistics_pairs(mc_stats_pair);
 457         exit(0);
 458       }
 459
 460       if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
 461
 462         //XBT_DEBUG("Unvisited pair !");
 463
 464         mc_stats_pair->executed_transitions++;
 465
 466         MC_SET_RAW_MEM;
 467         xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 468         MC_UNSET_RAW_MEM;
 469
 470         set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
 471         MC_dfs(a, search_cycle, 0);
 472
 473         if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 474
 475           MC_restore_snapshot(current_pair->system_state);
 476           MC_UNSET_RAW_MEM;
 477
 478           xbt_swag_foreach(process, simix_global->process_list){
 479             if(MC_process_is_enabled(process)){
 480               //XBT_DEBUG("Pid : %lu", process->pid);
 481               MC_state_interleave_process(current_pair->graph_state, process);
 482             }
 483           }
 484
 485           set_pair_reached(current_pair->graph_state, current_pair->automaton_state);
 486           XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
 487           MC_dfs(a, 1, 1);
 488
 489         }
 490       }
 491     }
 492
 493
 494     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 495       MC_restore_snapshot(current_snapshot);
 496       MC_UNSET_RAW_MEM;
 497       //XBT_DEBUG("Snapshot restored");
 498     }
 499   }
 500
 501
 502   MC_SET_RAW_MEM;
 503   //remove_pair_reached(current_pair->graph_state);
 504   xbt_fifo_shift(mc_snapshot_stack);
 505   XBT_DEBUG("State (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
 506   MC_UNSET_RAW_MEM;
 507
 508 }
 509
 510 void MC_show_snapshot_stack(xbt_fifo_t stack){
 511   int value;
 512   mc_pairs_t pair;
 513   xbt_fifo_item_t item;
 514   smx_req_t req;
 515   char *req_str = NULL;
 516
 517   for (item = xbt_fifo_get_last_item(stack);
 518        (item ? (pair = (mc_pairs_t) (xbt_fifo_get_item_content(item)))
 519         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 520     req = MC_state_get_executed_request(pair->graph_state, &value);
 521     if(req){
 522       req_str = MC_request_to_string(req, value);
 523       XBT_INFO("%s", req_str);
 524       xbt_free(req_str);
 525     }
 526   }
 527 }
 528
 529 void MC_dump_snapshot_stack(xbt_fifo_t stack){
 530   mc_pairs_t pair;
 531
 532   MC_SET_RAW_MEM;
 533   while ((pair = (mc_pairs_t) xbt_fifo_pop(stack)) != NULL)
 534     MC_pair_delete(pair);
 535   MC_UNSET_RAW_MEM;
 536 }
 537
 538 void MC_pair_delete(mc_pairs_t pair){
 539   xbt_free(pair->graph_state->proc_status);
 540   xbt_free(pair->graph_state);
 541   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 542   xbt_free(pair);
 543 }
 544
 545
 546 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 547
 548   switch(l->type){
 549   case 0 : {
 550     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 551     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 552     return (left_res || right_res);
 553     break;
 554   }
 555   case 1 : {
 556     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 557     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 558     return (left_res && right_res);
 559     break;
 560   }
 561   case 2 : {
 562     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
 563     return (!res);
 564     break;
 565   }
 566   case 3 : {
 567     unsigned int cursor = 0;
 568     xbt_propositional_symbol_t p = NULL;
 569     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
 570       if(strcmp(p->pred, l->u.predicat) == 0){
 571         int (*f)() = p->function;
 572         return (*f)();
 573       }
 574     }
 575     return -1;
 576     break;
 577   }
 578   case 4 : {
 579     return 2;
 580     break;
 581   }
 582   default :
 583     return -1;
 584   }
 585 }
 586
 587 /*void MC_dfs(xbt_automaton_t a, int search_cycle){
 588
 589   xbt_state_t current_state = (xbt_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(stack_automaton_dfs));
 590   xbt_transition_t transition_succ = NULL;
 591   xbt_state_t successor = NULL;
 592   unsigned int cursor = 0;
 593   xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
 594   int res;
 595
 596   //printf("++ current state : %s\n", current_state->id);
 597
 598   xbt_dynar_foreach(current_state->out, cursor, transition_succ){
 599     successor = transition_succ->dst;
 600     res = MC_automaton_evaluate_label(a, transition_succ->label);
 601     //printf("-- state : %s, transition_label : %d, res = %d\n", successor->id, transition_succ->label->type, res);
 602     if(res == 1){
 603       if(search_cycle == 1 && reached_dfs != NULL){
 604         if(strcmp(reached_dfs->id, successor->id) == 0){
 605           xbt_dynar_push(state_automaton_visited_dfs, &successor);
 606           printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 607           printf("Visited states : \n");
 608           unsigned int cursor2 = 0;
 609           xbt_state_t visited_state = NULL;
 610           xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
 611             printf("State : %s\n", visited_state->id);
 612           }
 613           exit(1);
 614         }
 615       }
 616       if(successor->visited == 0){
 617         successor->visited = 1;
 618         xbt_fifo_unshift(stack_automaton_dfs, successor);
 619         xbt_dynar_push(state_automaton_visited_dfs, &successor);
 620         MC_dfs(a, search_cycle);
 621         if(search_cycle == 0 && successor->type == 1){
 622           reached_dfs = successor;
 623           MC_dfs(a, 1);
 624         }
 625       }
 626     }else{
 627       if(res == 2){
 628         xbt_dynar_push(elses,&transition_succ);
 629       }
 630     }
 631   }
 632
 633   cursor = 0;
 634   xbt_dynar_foreach(elses, cursor, transition_succ){
 635    successor = transition_succ->dst;
 636    if(search_cycle == 1 && reached_dfs != NULL){
 637      if(strcmp(reached_dfs->id, successor->id) == 0){
 638        xbt_dynar_push(state_automaton_visited_dfs, &successor);
 639        printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 640        printf("Visited states : \n");
 641        unsigned int cursor2 = 0;
 642        xbt_state_t visited_state = NULL;
 643        xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
 644          printf("State : %s\n", visited_state->id);
 645        }
 646        exit(1);
 647      }
 648    }
 649    if(successor->visited == 0){
 650      successor->visited = 1;
 651      xbt_fifo_unshift(stack_automaton_dfs, successor);
 652      xbt_dynar_push(state_automaton_visited_dfs, &successor);
 653      MC_dfs(a, search_cycle);
 654      if(search_cycle == 0 && successor->type == 1){
 655        reached_dfs = successor;
 656        MC_dfs(a, 1);
 657      }
 658    }
 659   }
 660
 661   xbt_fifo_shift(stack_automaton_dfs);
 662   }*/
 663
 664
 665 /* void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ */
 666
 667
 668 /*   if(xbt_fifo_size(mc_snapshot_stack) == 0) */
 669 /*     return; */
 670
 671 /*   if(restore == 1){ */
 672 /*     MC_restore_snapshot(((mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state); */
 673 /*     MC_UNSET_RAW_MEM; */
 674 /*   } */
 675
 676
 677 /*   //XBT_DEBUG("Lpv length after restore snapshot: %lu", xbt_dynar_length(visited_pairs)); */
 678
 679 /*   /\* Get current state *\/ */
 680 /*   mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); */
 681
 682 /*   XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle); */
 683 /*   XBT_DEBUG("State : 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)); */
 684
 685 /*   //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); */
 686
 687 /*   //sleep(1); */
 688
 689 /*   smx_process_t process = NULL; */
 690 /*   int value; */
 691 /*   mc_state_t next_graph_state = NULL; */
 692 /*   smx_req_t req = NULL; */
 693 /*   char *req_str; */
 694
 695 /*   mc_pairs_t pair_succ; */
 696 /*   xbt_transition_t transition_succ; */
 697 /*   unsigned int cursor; */
 698 /*   int res; */
 699 /*   //int enabled_transition = 0; */
 700
 701 /*   xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL); */
 702 /*   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);  */
 703 /*   xbt_dynar_reset(all_successors); */
 704
 705 /*   mc_pairs_t next_pair; */
 706 /*   mc_snapshot_t next_snapshot; */
 707 /*   mc_snapshot_t current_snapshot; */
 708
 709 /*   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ */
 710
 711 /*     //XBT_DEBUG("Current pair : %p (%u interleave)", current_pair, MC_state_interleave_size(current_pair->graph_state)+1); */
 712 /*     //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs)); */
 713
 714 /*     MC_SET_RAW_MEM; */
 715 /*     current_snapshot = xbt_new0(s_mc_snapshot_t, 1); */
 716 /*     MC_take_snapshot(current_snapshot); */
 717 /*     MC_UNSET_RAW_MEM; */
 718
 719
 720 /*     /\* Debug information *\/ */
 721 /*     if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){ */
 722 /*       req_str = MC_request_to_string(req, value); */
 723 /*       XBT_DEBUG("Execute: %s", req_str); */
 724 /*       xbt_free(req_str); */
 725 /*     } */
 726
 727 /*     MC_state_set_executed_request(current_pair->graph_state, req, value); */
 728 /*     //mc_stats->executed_transitions++; */
 729
 730 /*     /\* Answer the request *\/ */
 731 /*     SIMIX_request_pre(req, value);  */
 732
 733 /*     /\* Wait for requests (schedules processes) *\/ */
 734 /*     MC_wait_for_requests(); */
 735
 736
 737 /*     /\* Create the new expanded graph_state *\/ */
 738 /*     MC_SET_RAW_MEM; */
 739
 740 /*     next_graph_state = MC_state_new(); */
 741
 742 /*     /\* Get enabled process and insert it in the interleave set of the next graph_state *\/ */
 743 /*     xbt_swag_foreach(process, simix_global->process_list){ */
 744 /*       if(MC_process_is_enabled(process)){ */
 745 /*      MC_state_interleave_process(next_graph_state, process); */
 746 /*       } */
 747 /*     } */
 748
 749 /*     next_snapshot = xbt_new0(s_mc_snapshot_t, 1); */
 750 /*     MC_take_snapshot(next_snapshot); */
 751
 752 /*     MC_UNSET_RAW_MEM; */
 753
 754 /*     xbt_dynar_reset(elses); */
 755 /*     xbt_dynar_reset(successors); */
 756
 757 /*     cursor = 0; */
 758 /*     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ */
 759
 760 /*       res = MC_automaton_evaluate_label(a, transition_succ->label); */
 761
 762 /*       MC_SET_RAW_MEM; */
 763 /*       next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); */
 764
 765 /*       //XBT_DEBUG("Next pair : %p", next_pair); */
 766
 767 /*       if(res == 1){ // enabled transition in automaton */
 768 /*      xbt_dynar_push(successors, &next_pair);    */
 769 /*      //XBT_DEBUG("New Successors length : %lu", xbt_dynar_length(successors)); */
 770 /*       }else{ */
 771 /*      if(res == 2){ */
 772 /*        xbt_dynar_push(elses, &next_pair); */
 773 /*        //XBT_DEBUG("New Elses length : %lu", xbt_dynar_length(elses)); */
 774 /*      } */
 775 /*       } */
 776
 777 /*       MC_UNSET_RAW_MEM; */
 778 /*     } */
 779
 780
 781 /*     if((xbt_dynar_length(successors) == 0) && (xbt_dynar_length(elses) == 0) ){ */
 782
 783 /*       MC_SET_RAW_MEM; */
 784 /*       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state); */
 785 /*       xbt_dynar_push(successors, &next_pair); */
 786 /*       MC_UNSET_RAW_MEM; */
 787
 788 /*     } */
 789
 790 /*     //XBT_DEBUG("Successors length : %lu", xbt_dynar_length(successors)); */
 791 /*     //XBT_DEBUG("Elses length : %lu", xbt_dynar_length(elses)); */
 792
 793 /*     if(xbt_dynar_length(successors) > 0){ */
 794
 795 /*       cursor = 0; */
 796 /*       xbt_dynar_foreach(successors, cursor, pair_succ){ */
 797 /*      MC_SET_RAW_MEM; */
 798 /*      xbt_dynar_push(all_successors, &pair_succ); */
 799 /*      MC_UNSET_RAW_MEM; */
 800 /*       } */
 801
 802 /*     }else{  */
 803
 804 /*       cursor = 0; */
 805 /*       xbt_dynar_foreach(elses, cursor, pair_succ){ */
 806 /*      MC_SET_RAW_MEM; */
 807 /*      xbt_dynar_push(all_successors, &pair_succ); */
 808 /*      MC_UNSET_RAW_MEM; */
 809 /*       } */
 810
 811 /*     }  */
 812
 813 /*     MC_restore_snapshot(current_snapshot); */
 814 /*     MC_UNSET_RAW_MEM; */
 815
 816 /*   }    */
 817
 818 /*   //XBT_DEBUG("All successors : %lu", xbt_dynar_length(all_successors)); */
 819
 820 /*   cursor = 0; */
 821
 822 /*   xbt_dynar_foreach(all_successors, cursor, pair_succ){ */
 823
 824 /*     if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){ */
 825 /*       XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); */
 826 /*       XBT_INFO("|             ACCEPTANCE CYCLE            |"); */
 827 /*       XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); */
 828 /*       XBT_INFO("Counter-example that violates formula :"); */
 829 /*       MC_show_snapshot_stack(mc_snapshot_stack); */
 830 /*       MC_dump_snapshot_stack(mc_snapshot_stack); */
 831 /*       exit(0); */
 832 /*     } */
 833
 834 /*     if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){ */
 835
 836 /*       //XBT_DEBUG("New pair in stack"); */
 837
 838 /*       MC_SET_RAW_MEM; */
 839 /*       xbt_fifo_unshift(mc_snapshot_stack, pair_succ); */
 840 /*       MC_UNSET_RAW_MEM; */
 841
 842 /*       set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle); */
 843 /*       MC_dfs(a, search_cycle, 1); */
 844
 845 /*       if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){ */
 846
 847 /*      set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);  */
 848 /*      XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); */
 849 /*      MC_dfs(a, 1, 1); */
 850
 851 /*       } */
 852 /*     }  */
 853
 854 /*   } */
 855
 856 /*   MC_SET_RAW_MEM; */
 857 /*   //remove_pair_reached(current_pair->graph_state); */
 858 /*   xbt_fifo_shift(mc_snapshot_stack); */
 859 /*   XBT_DEBUG("State (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state); */
 860 /*   MC_UNSET_RAW_MEM; */
 861
 862 /* } */