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, interleave=%d) already reached (graph=%p)!", gs, as, MC_state_interleave_size(gs), 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_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 elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
 183   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
 184   //  int enabled_transition = 0;
 185   mc_pairs_t pair_succ;
 186
 187   xbt_dynar_foreach(a->states, cursor, state){
 188     if(state->type == -1){
 189       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 190         res = MC_automaton_evaluate_label(a, transition_succ->label);
 191
 192         if(res == 1){
 193
 194           MC_SET_RAW_MEM;
 195
 196           mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 197           xbt_dynar_push(successors, &mc_initial_pair);
 198
 199           //XBT_DEBUG("New initial successor");
 200
 201           MC_UNSET_RAW_MEM;
 202
 203         }else{
 204           if(res == 2){
 205
 206             MC_SET_RAW_MEM;
 207
 208             mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 209             xbt_dynar_push(elses, &mc_initial_pair);
 210
 211             //XBT_DEBUG("New initial successor");
 212
 213             MC_UNSET_RAW_MEM;
 214           }
 215         }
 216       }
 217     }
 218   }
 219
 220   if(xbt_dynar_length(successors) > 0){
 221
 222     cursor = 0;
 223     xbt_dynar_foreach(successors, cursor, pair_succ){
 224       MC_SET_RAW_MEM;
 225
 226       xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 227
 228       XBT_DEBUG("**************************************************");
 229       XBT_DEBUG("Initial state=%p ", pair_succ);
 230
 231       MC_UNSET_RAW_MEM;
 232
 233       set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
 234
 235       if(cursor == 0){
 236         MC_dfs(a, 0, 0);
 237         if(pair_succ->automaton_state->type == 1){
 238           set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);
 239           MC_dfs(a, 1, 0);
 240         }
 241       }else{
 242         MC_dfs(a, 0, 1);
 243         if(pair_succ->automaton_state->type == 1){
 244           MC_dfs(a, 1, 1);
 245         }
 246       }
 247
 248       /* if(cursor == 0) */
 249       /*        MC_dfs(a, 0, 0); */
 250       /* else */
 251       /*        MC_dfs(a, 0, 1); */
 252
 253     }
 254
 255   }
 256
 257   if(xbt_dynar_length(elses) > 0){
 258     cursor = 0;
 259     xbt_dynar_foreach(elses, cursor, pair_succ){
 260       MC_SET_RAW_MEM;
 261
 262       xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 263
 264       XBT_DEBUG("**************************************************");
 265       XBT_DEBUG("Initial state=%p ", pair_succ);
 266
 267       MC_UNSET_RAW_MEM;
 268
 269       set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
 270
 271       if(cursor == 0){
 272         MC_dfs(a, 0, 0);
 273         if(pair_succ->automaton_state->type == 1){
 274           set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);
 275           MC_dfs(a, 1, 0);
 276         }
 277       }else{
 278         MC_dfs(a, 0, 1);
 279         if(pair_succ->automaton_state->type == 1){
 280           MC_dfs(a, 1, 1);
 281         }
 282       }
 283
 284       /* if(cursor == 0) */
 285       /*   MC_dfs(a, 0, 0); */
 286       /* else */
 287       /*   MC_dfs(a, 0, 1); */
 288
 289
 290     }
 291   }
 292
 293 }
 294
 295
 296 void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
 297
 298   smx_process_t process = NULL;
 299
 300
 301   if(xbt_fifo_size(mc_snapshot_stack) == 0)
 302     return;
 303
 304   if(restore == 1){
 305     MC_restore_snapshot(((mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
 306     MC_UNSET_RAW_MEM;
 307   }
 308
 309   //XBT_DEBUG("Lpv length after restore snapshot: %lu", xbt_dynar_length(visited_pairs));
 310
 311   /* Get current state */
 312   mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 313
 314   if(restore==1){
 315     xbt_swag_foreach(process, simix_global->process_list){
 316       if(MC_process_is_enabled(process)){
 317         //XBT_DEBUG("Pid : %lu", process->pid);
 318         MC_state_interleave_process(current_pair->graph_state, process);
 319       }
 320     }
 321   }
 322
 323   XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
 324   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));
 325   //XBT_DEBUG("Restore : %d", restore);
 326
 327   //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 328
 329   //sleep(1);
 330
 331   int value;
 332   mc_state_t next_graph_state = NULL;
 333   smx_req_t req = NULL;
 334   char *req_str;
 335
 336   mc_pairs_t pair_succ;
 337   xbt_transition_t transition_succ;
 338   unsigned int cursor;
 339   int res;
 340   //int enabled_transition = 0;
 341
 342   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
 343
 344   mc_pairs_t next_pair;
 345   mc_snapshot_t next_snapshot;
 346   mc_snapshot_t current_snapshot;
 347
 348
 349   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 350
 351     MC_SET_RAW_MEM;
 352     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 353     MC_take_snapshot(current_snapshot);
 354     MC_UNSET_RAW_MEM;
 355
 356
 357     /* Debug information */
 358     if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){
 359       req_str = MC_request_to_string(req, value);
 360       XBT_DEBUG("Execute: %s", req_str);
 361       xbt_free(req_str);
 362     }
 363
 364     MC_state_set_executed_request(current_pair->graph_state, req, value);
 365     //mc_stats->executed_transitions++;
 366
 367     /* Answer the request */
 368     SIMIX_request_pre(req, value);
 369
 370     /* Wait for requests (schedules processes) */
 371     MC_wait_for_requests();
 372
 373
 374     /* Create the new expanded graph_state */
 375     MC_SET_RAW_MEM;
 376
 377     next_graph_state = MC_state_new();
 378
 379     /* Get enabled process and insert it in the interleave set of the next graph_state */
 380     xbt_swag_foreach(process, simix_global->process_list){
 381       if(MC_process_is_enabled(process)){
 382         //XBT_DEBUG("Pid : %lu", process->pid);
 383         MC_state_interleave_process(next_graph_state, process);
 384       }
 385     }
 386
 387     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 388     MC_take_snapshot(next_snapshot);
 389
 390     MC_UNSET_RAW_MEM;
 391
 392     xbt_dynar_reset(successors);
 393
 394     cursor = 0;
 395     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 396
 397       res = MC_automaton_evaluate_label(a, transition_succ->label);
 398
 399       MC_SET_RAW_MEM;
 400       next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 401
 402       //XBT_DEBUG("Next pair : %p", next_pair);
 403
 404       if((res == 1) || (res == 2)){ // enabled transition in automaton
 405         xbt_dynar_push(successors, &next_pair);
 406       }
 407
 408       MC_UNSET_RAW_MEM;
 409     }
 410
 411
 412     if(xbt_dynar_length(successors) == 0){
 413
 414       MC_SET_RAW_MEM;
 415       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
 416       xbt_dynar_push(successors, &next_pair);
 417       MC_UNSET_RAW_MEM;
 418
 419     }
 420
 421     // XBT_DEBUG("Successors length : %lu", xbt_dynar_length(successors));
 422     //XBT_DEBUG("Elses length : %lu", xbt_dynar_length(elses));
 423
 424     if(xbt_dynar_length(successors) >0){
 425
 426       cursor = 0;
 427       xbt_dynar_foreach(successors, cursor, pair_succ){
 428
 429         //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 430
 431         if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){
 432           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 433           XBT_INFO("|             ACCEPTANCE CYCLE            |");
 434           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 435           XBT_INFO("Counter-example that violates formula :");
 436           MC_show_snapshot_stack(mc_snapshot_stack);
 437           MC_dump_snapshot_stack(mc_snapshot_stack);
 438           exit(0);
 439         }
 440
 441         if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
 442
 443           //XBT_DEBUG("Unvisited pair !");
 444
 445           MC_SET_RAW_MEM;
 446           xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 447           MC_UNSET_RAW_MEM;
 448
 449           set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
 450           MC_dfs(a, search_cycle, 0);
 451
 452           if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 453
 454             MC_restore_snapshot(current_pair->system_state);
 455             MC_UNSET_RAW_MEM;
 456
 457             xbt_swag_foreach(process, simix_global->process_list){
 458               if(MC_process_is_enabled(process)){
 459                 //XBT_DEBUG("Pid : %lu", process->pid);
 460                 MC_state_interleave_process(current_pair->graph_state, process);
 461               }
 462             }
 463
 464             set_pair_reached(current_pair->graph_state, current_pair->automaton_state);
 465             XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
 466             MC_dfs(a, 1, 1);
 467
 468           }
 469         }
 470       }
 471
 472     }
 473
 474
 475     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 476       MC_restore_snapshot(current_snapshot);
 477       MC_UNSET_RAW_MEM;
 478       //XBT_DEBUG("Snapshot restored");
 479     }
 480   }
 481
 482
 483   MC_SET_RAW_MEM;
 484   //remove_pair_reached(current_pair->graph_state);
 485   xbt_fifo_shift(mc_snapshot_stack);
 486   XBT_DEBUG("State (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
 487   MC_UNSET_RAW_MEM;
 488
 489 }
 490
 491 void MC_show_snapshot_stack(xbt_fifo_t stack){
 492   int value;
 493   mc_pairs_t pair;
 494   xbt_fifo_item_t item;
 495   smx_req_t req;
 496   char *req_str = NULL;
 497
 498   for (item = xbt_fifo_get_last_item(stack);
 499        (item ? (pair = (mc_pairs_t) (xbt_fifo_get_item_content(item)))
 500         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 501     req = MC_state_get_executed_request(pair->graph_state, &value);
 502     if(req){
 503       req_str = MC_request_to_string(req, value);
 504       XBT_INFO("%s", req_str);
 505       xbt_free(req_str);
 506     }
 507   }
 508 }
 509
 510 void MC_dump_snapshot_stack(xbt_fifo_t stack){
 511   mc_pairs_t pair;
 512
 513   MC_SET_RAW_MEM;
 514   while ((pair = (mc_pairs_t) xbt_fifo_pop(stack)) != NULL)
 515     MC_pair_delete(pair);
 516   MC_UNSET_RAW_MEM;
 517 }
 518
 519 void MC_pair_delete(mc_pairs_t pair){
 520   xbt_free(pair->graph_state->proc_status);
 521   xbt_free(pair->graph_state);
 522   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 523   xbt_free(pair);
 524 }
 525
 526
 527 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 528
 529   switch(l->type){
 530   case 0 : {
 531     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 532     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 533     return (left_res || right_res);
 534     break;
 535   }
 536   case 1 : {
 537     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 538     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 539     return (left_res && right_res);
 540     break;
 541   }
 542   case 2 : {
 543     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
 544     return (!res);
 545     break;
 546   }
 547   case 3 : {
 548     unsigned int cursor = 0;
 549     xbt_propositional_symbol_t p = NULL;
 550     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
 551       if(strcmp(p->pred, l->u.predicat) == 0){
 552         int (*f)() = p->function;
 553         return (*f)();
 554       }
 555     }
 556     return -1;
 557     break;
 558   }
 559   case 4 : {
 560     return 2;
 561     break;
 562   }
 563   default :
 564     return -1;
 565   }
 566 }
 567
 568 /*void MC_dfs(xbt_automaton_t a, int search_cycle){
 569
 570   xbt_state_t current_state = (xbt_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(stack_automaton_dfs));
 571   xbt_transition_t transition_succ = NULL;
 572   xbt_state_t successor = NULL;
 573   unsigned int cursor = 0;
 574   xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
 575   int res;
 576
 577   //printf("++ current state : %s\n", current_state->id);
 578
 579   xbt_dynar_foreach(current_state->out, cursor, transition_succ){
 580     successor = transition_succ->dst;
 581     res = MC_automaton_evaluate_label(a, transition_succ->label);
 582     //printf("-- state : %s, transition_label : %d, res = %d\n", successor->id, transition_succ->label->type, res);
 583     if(res == 1){
 584       if(search_cycle == 1 && reached_dfs != NULL){
 585         if(strcmp(reached_dfs->id, successor->id) == 0){
 586           xbt_dynar_push(state_automaton_visited_dfs, &successor);
 587           printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 588           printf("Visited states : \n");
 589           unsigned int cursor2 = 0;
 590           xbt_state_t visited_state = NULL;
 591           xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
 592             printf("State : %s\n", visited_state->id);
 593           }
 594           exit(1);
 595         }
 596       }
 597       if(successor->visited == 0){
 598         successor->visited = 1;
 599         xbt_fifo_unshift(stack_automaton_dfs, successor);
 600         xbt_dynar_push(state_automaton_visited_dfs, &successor);
 601         MC_dfs(a, search_cycle);
 602         if(search_cycle == 0 && successor->type == 1){
 603           reached_dfs = successor;
 604           MC_dfs(a, 1);
 605         }
 606       }
 607     }else{
 608       if(res == 2){
 609         xbt_dynar_push(elses,&transition_succ);
 610       }
 611     }
 612   }
 613
 614   cursor = 0;
 615   xbt_dynar_foreach(elses, cursor, transition_succ){
 616    successor = transition_succ->dst;
 617    if(search_cycle == 1 && reached_dfs != NULL){
 618      if(strcmp(reached_dfs->id, successor->id) == 0){
 619        xbt_dynar_push(state_automaton_visited_dfs, &successor);
 620        printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 621        printf("Visited states : \n");
 622        unsigned int cursor2 = 0;
 623        xbt_state_t visited_state = NULL;
 624        xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
 625          printf("State : %s\n", visited_state->id);
 626        }
 627        exit(1);
 628      }
 629    }
 630    if(successor->visited == 0){
 631      successor->visited = 1;
 632      xbt_fifo_unshift(stack_automaton_dfs, successor);
 633      xbt_dynar_push(state_automaton_visited_dfs, &successor);
 634      MC_dfs(a, search_cycle);
 635      if(search_cycle == 0 && successor->type == 1){
 636        reached_dfs = successor;
 637        MC_dfs(a, 1);
 638      }
 639    }
 640   }
 641
 642   xbt_fifo_shift(stack_automaton_dfs);
 643   }*/
 644
 645
 646 /* void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ */
 647
 648
 649 /*   if(xbt_fifo_size(mc_snapshot_stack) == 0) */
 650 /*     return; */
 651
 652 /*   if(restore == 1){ */
 653 /*     MC_restore_snapshot(((mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state); */
 654 /*     MC_UNSET_RAW_MEM; */
 655 /*   } */
 656
 657
 658 /*   //XBT_DEBUG("Lpv length after restore snapshot: %lu", xbt_dynar_length(visited_pairs)); */
 659
 660 /*   /\* Get current state *\/ */
 661 /*   mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); */
 662
 663 /*   XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle); */
 664 /*   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)); */
 665
 666 /*   //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); */
 667
 668 /*   //sleep(1); */
 669
 670 /*   smx_process_t process = NULL; */
 671 /*   int value; */
 672 /*   mc_state_t next_graph_state = NULL; */
 673 /*   smx_req_t req = NULL; */
 674 /*   char *req_str; */
 675
 676 /*   mc_pairs_t pair_succ; */
 677 /*   xbt_transition_t transition_succ; */
 678 /*   unsigned int cursor; */
 679 /*   int res; */
 680 /*   //int enabled_transition = 0; */
 681
 682 /*   xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL); */
 683 /*   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);  */
 684 /*   xbt_dynar_reset(all_successors); */
 685
 686 /*   mc_pairs_t next_pair; */
 687 /*   mc_snapshot_t next_snapshot; */
 688 /*   mc_snapshot_t current_snapshot; */
 689
 690 /*   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ */
 691
 692 /*     //XBT_DEBUG("Current pair : %p (%u interleave)", current_pair, MC_state_interleave_size(current_pair->graph_state)+1); */
 693 /*     //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs)); */
 694
 695 /*     MC_SET_RAW_MEM; */
 696 /*     current_snapshot = xbt_new0(s_mc_snapshot_t, 1); */
 697 /*     MC_take_snapshot(current_snapshot); */
 698 /*     MC_UNSET_RAW_MEM; */
 699
 700
 701 /*     /\* Debug information *\/ */
 702 /*     if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){ */
 703 /*       req_str = MC_request_to_string(req, value); */
 704 /*       XBT_DEBUG("Execute: %s", req_str); */
 705 /*       xbt_free(req_str); */
 706 /*     } */
 707
 708 /*     MC_state_set_executed_request(current_pair->graph_state, req, value); */
 709 /*     //mc_stats->executed_transitions++; */
 710
 711 /*     /\* Answer the request *\/ */
 712 /*     SIMIX_request_pre(req, value);  */
 713
 714 /*     /\* Wait for requests (schedules processes) *\/ */
 715 /*     MC_wait_for_requests(); */
 716
 717
 718 /*     /\* Create the new expanded graph_state *\/ */
 719 /*     MC_SET_RAW_MEM; */
 720
 721 /*     next_graph_state = MC_state_new(); */
 722
 723 /*     /\* Get enabled process and insert it in the interleave set of the next graph_state *\/ */
 724 /*     xbt_swag_foreach(process, simix_global->process_list){ */
 725 /*       if(MC_process_is_enabled(process)){ */
 726 /*      MC_state_interleave_process(next_graph_state, process); */
 727 /*       } */
 728 /*     } */
 729
 730 /*     next_snapshot = xbt_new0(s_mc_snapshot_t, 1); */
 731 /*     MC_take_snapshot(next_snapshot); */
 732
 733 /*     MC_UNSET_RAW_MEM; */
 734
 735 /*     xbt_dynar_reset(elses); */
 736 /*     xbt_dynar_reset(successors); */
 737
 738 /*     cursor = 0; */
 739 /*     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ */
 740
 741 /*       res = MC_automaton_evaluate_label(a, transition_succ->label); */
 742
 743 /*       MC_SET_RAW_MEM; */
 744 /*       next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); */
 745
 746 /*       //XBT_DEBUG("Next pair : %p", next_pair); */
 747
 748 /*       if(res == 1){ // enabled transition in automaton */
 749 /*      xbt_dynar_push(successors, &next_pair);    */
 750 /*      //XBT_DEBUG("New Successors length : %lu", xbt_dynar_length(successors)); */
 751 /*       }else{ */
 752 /*      if(res == 2){ */
 753 /*        xbt_dynar_push(elses, &next_pair); */
 754 /*        //XBT_DEBUG("New Elses length : %lu", xbt_dynar_length(elses)); */
 755 /*      } */
 756 /*       } */
 757
 758 /*       MC_UNSET_RAW_MEM; */
 759 /*     } */
 760
 761
 762 /*     if((xbt_dynar_length(successors) == 0) && (xbt_dynar_length(elses) == 0) ){ */
 763
 764 /*       MC_SET_RAW_MEM; */
 765 /*       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state); */
 766 /*       xbt_dynar_push(successors, &next_pair); */
 767 /*       MC_UNSET_RAW_MEM; */
 768
 769 /*     } */
 770
 771 /*     //XBT_DEBUG("Successors length : %lu", xbt_dynar_length(successors)); */
 772 /*     //XBT_DEBUG("Elses length : %lu", xbt_dynar_length(elses)); */
 773
 774 /*     if(xbt_dynar_length(successors) > 0){ */
 775
 776 /*       cursor = 0; */
 777 /*       xbt_dynar_foreach(successors, cursor, pair_succ){ */
 778 /*      MC_SET_RAW_MEM; */
 779 /*      xbt_dynar_push(all_successors, &pair_succ); */
 780 /*      MC_UNSET_RAW_MEM; */
 781 /*       } */
 782
 783 /*     }else{  */
 784
 785 /*       cursor = 0; */
 786 /*       xbt_dynar_foreach(elses, cursor, pair_succ){ */
 787 /*      MC_SET_RAW_MEM; */
 788 /*      xbt_dynar_push(all_successors, &pair_succ); */
 789 /*      MC_UNSET_RAW_MEM; */
 790 /*       } */
 791
 792 /*     }  */
 793
 794 /*     MC_restore_snapshot(current_snapshot); */
 795 /*     MC_UNSET_RAW_MEM; */
 796
 797 /*   }    */
 798
 799 /*   //XBT_DEBUG("All successors : %lu", xbt_dynar_length(all_successors)); */
 800
 801 /*   cursor = 0; */
 802
 803 /*   xbt_dynar_foreach(all_successors, cursor, pair_succ){ */
 804
 805 /*     if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){ */
 806 /*       XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); */
 807 /*       XBT_INFO("|             ACCEPTANCE CYCLE            |"); */
 808 /*       XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); */
 809 /*       XBT_INFO("Counter-example that violates formula :"); */
 810 /*       MC_show_snapshot_stack(mc_snapshot_stack); */
 811 /*       MC_dump_snapshot_stack(mc_snapshot_stack); */
 812 /*       exit(0); */
 813 /*     } */
 814
 815 /*     if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){ */
 816
 817 /*       //XBT_DEBUG("New pair in stack"); */
 818
 819 /*       MC_SET_RAW_MEM; */
 820 /*       xbt_fifo_unshift(mc_snapshot_stack, pair_succ); */
 821 /*       MC_UNSET_RAW_MEM; */
 822
 823 /*       set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle); */
 824 /*       MC_dfs(a, search_cycle, 1); */
 825
 826 /*       if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){ */
 827
 828 /*      set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);  */
 829 /*      XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); */
 830 /*      MC_dfs(a, 1, 1); */
 831
 832 /*       } */
 833 /*     }  */
 834
 835 /*   } */
 836
 837 /*   MC_SET_RAW_MEM; */
 838 /*   //remove_pair_reached(current_pair->graph_state); */
 839 /*   xbt_fifo_shift(mc_snapshot_stack); */
 840 /*   XBT_DEBUG("State (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state); */
 841 /*   MC_UNSET_RAW_MEM; */
 842
 843 /* } */