src/mc/mc_dpor.c

   1 /* Copyright (c) 2008 Martin Quinson, Cristian Rosa.
   2    All rights reserved.                                          */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include "private.h"
   8
   9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
  10                                 "Logging specific to MC DPOR exploration");
  11
  12 /**
  13  *  \brief Initialize the DPOR exploration algorithm
  14  */
  15 void MC_dpor_init()
  16 {
  17   mc_state_t initial_state = NULL;
  18   smx_process_t process;
  19
  20   /* Create the initial state and push it into the exploration stack */
  21   MC_SET_RAW_MEM;
  22   initial_state = MC_state_new();
  23   xbt_fifo_unshift(mc_stack, initial_state);
  24   MC_UNSET_RAW_MEM;
  25
  26   XBT_DEBUG("**************************************************");
  27   XBT_DEBUG("Initial state");
  28
  29   /* Wait for requests (schedules processes) */
  30   MC_wait_for_requests();
  31
  32   MC_SET_RAW_MEM;
  33   /* Get an enabled process and insert it in the interleave set of the initial state */
  34   xbt_swag_foreach(process, simix_global->process_list){
  35     if(MC_process_is_enabled(process)){
  36       MC_state_interleave_process(initial_state, process);
  37       break;
  38     }
  39   }
  40   MC_UNSET_RAW_MEM;
  41
  42   /* FIXME: Update Statistics
  43   mc_stats->state_size +=
  44       xbt_setset_set_size(initial_state->enabled_transitions); */
  45 }
  46
  47
  48 /**
  49  *      \brief Perform the model-checking operation using a depth-first search exploration
  50  *         with Dynamic Partial Order Reductions
  51  */
  52 void MC_dpor(void)
  53 {
  54   char *req_str;
  55   int value;
  56   smx_req_t req = NULL, prev_req = NULL;
  57   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
  58   smx_process_t process = NULL;
  59   xbt_fifo_item_t item = NULL;
  60
  61   while (xbt_fifo_size(mc_stack) > 0) {
  62
  63     /* Get current state */
  64     state = (mc_state_t)
  65       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
  66
  67     XBT_DEBUG("**************************************************");
  68     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
  69            xbt_fifo_size(mc_stack), state,
  70            MC_state_interleave_size(state));
  71
  72     /* Update statistics */
  73     mc_stats->visited_states++;
  74
  75     /* If there are processes to interleave and the maximum depth has not been reached
  76        then perform one step of the exploration algorithm */
  77     if (xbt_fifo_size(mc_stack) < MAX_DEPTH &&
  78         (req = MC_state_get_request(state, &value))) {
  79
  80       /* Debug information */
  81       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
  82         req_str = MC_request_to_string(req, value);
  83         XBT_DEBUG("Execute: %s", req_str);
  84         xbt_free(req_str);
  85       }
  86
  87       MC_state_set_executed_request(state, req, value);
  88       mc_stats->executed_transitions++;
  89
  90       /* Answer the request */
  91       SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
  92
  93       /* Wait for requests (schedules processes) */
  94       MC_wait_for_requests();
  95
  96       /* Create the new expanded state */
  97       MC_SET_RAW_MEM;
  98       next_state = MC_state_new();
  99       xbt_fifo_unshift(mc_stack, next_state);
 100
 101       /* Get an enabled process and insert it in the interleave set of the next state */
 102       xbt_swag_foreach(process, simix_global->process_list){
 103         if(MC_process_is_enabled(process)){
 104           MC_state_interleave_process(next_state, process);
 105           break;
 106         }
 107       }
 108       MC_UNSET_RAW_MEM;
 109
 110       /* FIXME: Update Statistics
 111       mc_stats->state_size +=
 112           xbt_setset_set_size(next_state->enabled_transitions);*/
 113
 114       /* Let's loop again */
 115
 116       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 117     } else {
 118       XBT_DEBUG("There are no more processes to interleave.");
 119
 120       /* Trash the current state, no longer needed */
 121       MC_SET_RAW_MEM;
 122       xbt_fifo_shift(mc_stack);
 123       MC_state_delete(state);
 124       MC_UNSET_RAW_MEM;
 125
 126       /* Check for deadlocks */
 127       if(MC_deadlock_check()){
 128         MC_show_deadlock(NULL);
 129         return;
 130       }
 131
 132       MC_SET_RAW_MEM;
 133       /* Traverse the stack backwards until a state with a non empty interleave
 134          set is found, deleting all the states that have it empty in the way.
 135          For each deleted state, check if the request that has generated it
 136          (from it's predecesor state), depends on any other previous request
 137          executed before it. If it does then add it to the interleave set of the
 138          state that executed that previous request. */
 139       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
 140         req = MC_state_get_internal_request(state);
 141         xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
 142           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
 143             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 144               XBT_DEBUG("Dependent Transitions:");
 145               prev_req = MC_state_get_executed_request(prev_state, &value);
 146               req_str = MC_request_to_string(prev_req, value);
 147               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
 148               xbt_free(req_str);
 149               prev_req = MC_state_get_executed_request(state, &value);
 150               req_str = MC_request_to_string(prev_req, value);
 151               XBT_DEBUG("%s (state=%p)", req_str, state);
 152               xbt_free(req_str);
 153             }
 154
 155             if(!MC_state_process_is_done(prev_state, req->issuer))
 156               MC_state_interleave_process(prev_state, req->issuer);
 157             else
 158               XBT_DEBUG("Process %p is in done set", req->issuer);
 159
 160             break;
 161           }
 162         }
 163         if (MC_state_interleave_size(state)) {
 164           /* We found a back-tracking point, let's loop */
 165           xbt_fifo_unshift(mc_stack, state);
 166           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
 167           MC_UNSET_RAW_MEM;
 168           MC_replay(mc_stack);
 169           break;
 170         } else {
 171           MC_state_delete(state);
 172         }
 173       }
 174       MC_UNSET_RAW_MEM;
 175     }
 176   }
 177   MC_UNSET_RAW_MEM;
 178   return;
 179 }
 180
 181
 182 /********************* DPOR without replay *********************/
 183
 184 mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs){
 185   mc_state_ws_t sws = NULL;
 186   sws = xbt_new0(s_mc_state_ws_t, 1);
 187   sws->system_state = s;
 188   sws->graph_state = gs;
 189   return sws;
 190 }
 191
 192 void MC_dpor_with_restore_snapshot_init(){
 193
 194   XBT_DEBUG("**************************************************");
 195   XBT_DEBUG("DPOR (with restore snapshot) init");
 196   XBT_DEBUG("**************************************************");
 197
 198   mc_state_t initial_graph_state;
 199   smx_process_t process;
 200   mc_snapshot_t initial_system_snapshot;
 201   mc_state_ws_t initial_state ;
 202
 203   MC_wait_for_requests();
 204
 205   MC_SET_RAW_MEM;
 206
 207   initial_system_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 208
 209   initial_graph_state = MC_state_new();
 210   xbt_swag_foreach(process, simix_global->process_list){
 211     if(MC_process_is_enabled(process)){
 212       MC_state_interleave_process(initial_graph_state, process);
 213       break;
 214     }
 215   }
 216
 217   MC_take_snapshot(initial_system_snapshot);
 218
 219   initial_state = new_state_ws(initial_system_snapshot, initial_graph_state);
 220   xbt_fifo_unshift(mc_snapshot_stack, initial_state);
 221
 222   MC_UNSET_RAW_MEM;
 223
 224   MC_dpor_with_restore_snapshot();
 225
 226 }
 227
 228 void MC_dpor_with_restore_snapshot(){
 229
 230   smx_process_t process = NULL;
 231
 232   if(xbt_fifo_size(mc_snapshot_stack) == 0)
 233     return;
 234
 235   int value;
 236   mc_state_t next_graph_state = NULL;
 237   smx_req_t req = NULL, prev_req = NULL;
 238   char *req_str;
 239   xbt_fifo_item_t item = NULL;
 240
 241   mc_snapshot_t next_snapshot;
 242   mc_state_ws_t current_state;
 243   mc_state_ws_t prev_state;
 244   mc_state_ws_t next_state;
 245
 246   while(xbt_fifo_size(mc_snapshot_stack) > 0){
 247
 248     current_state = (mc_state_ws_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 249
 250
 251     XBT_DEBUG("**************************************************");
 252     XBT_DEBUG("Depth : %d, State : %p , %u interleave", xbt_fifo_size(mc_snapshot_stack),current_state, MC_state_interleave_size(current_state->graph_state));
 253
 254
 255     if((xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH) && (req = MC_state_get_request(current_state->graph_state, &value))){
 256
 257       /* Debug information */
 258       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 259         req_str = MC_request_to_string(req, value);
 260         XBT_DEBUG("Execute: %s", req_str);
 261         xbt_free(req_str);
 262       }
 263
 264       MC_state_set_executed_request(current_state->graph_state, req, value);
 265
 266       /* Answer the request */
 267       SIMIX_request_pre(req, value);
 268
 269       /* Wait for requests (schedules processes) */
 270       MC_wait_for_requests();
 271
 272       /* Create the new expanded graph_state */
 273       MC_SET_RAW_MEM;
 274
 275       next_graph_state = MC_state_new();
 276
 277       /* Get an enabled process and insert it in the interleave set of the next graph_state */
 278       xbt_swag_foreach(process, simix_global->process_list){
 279         if(MC_process_is_enabled(process)){
 280           MC_state_interleave_process(next_graph_state, process);
 281           break;
 282         }
 283       }
 284
 285       next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 286       MC_take_snapshot(next_snapshot);
 287
 288       next_state = new_state_ws(next_snapshot, next_graph_state);
 289       xbt_fifo_unshift(mc_snapshot_stack, next_state);
 290
 291       MC_UNSET_RAW_MEM;
 292
 293     }else{
 294       XBT_DEBUG("There are no more processes to interleave.");
 295
 296       /* Trash the current state, no longer needed */
 297       MC_SET_RAW_MEM;
 298       xbt_fifo_shift(mc_snapshot_stack);
 299       MC_UNSET_RAW_MEM;
 300
 301       while((current_state = xbt_fifo_shift(mc_snapshot_stack)) != NULL){
 302         req = MC_state_get_internal_request(current_state->graph_state);
 303         xbt_fifo_foreach(mc_snapshot_stack, item, prev_state, mc_state_ws_t) {
 304           if(MC_request_depend(req, MC_state_get_internal_request(prev_state->graph_state))){
 305             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 306               XBT_DEBUG("Dependent Transitions:");
 307               prev_req = MC_state_get_executed_request(prev_state->graph_state, &value);
 308               req_str = MC_request_to_string(prev_req, value);
 309               XBT_DEBUG("%s (state=%p)", req_str, prev_state->graph_state);
 310               xbt_free(req_str);
 311               prev_req = MC_state_get_executed_request(current_state->graph_state, &value);
 312               req_str = MC_request_to_string(prev_req, value);
 313               XBT_DEBUG("%s (state=%p)", req_str, current_state->graph_state);
 314               xbt_free(req_str);
 315             }
 316
 317             if(!MC_state_process_is_done(prev_state->graph_state, req->issuer)){
 318               MC_state_interleave_process(prev_state->graph_state, req->issuer);
 319
 320             } else {
 321               XBT_DEBUG("Process %p is in done set", req->issuer);
 322             }
 323
 324             break;
 325           }
 326         }
 327
 328         if(MC_state_interleave_size(current_state->graph_state)){
 329           MC_restore_snapshot(current_state->system_state);
 330           xbt_fifo_unshift(mc_snapshot_stack, current_state);
 331           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));
 332           MC_UNSET_RAW_MEM;
 333           break;
 334         }
 335       }
 336
 337       MC_UNSET_RAW_MEM;
 338
 339     }
 340   }
 341   MC_UNSET_RAW_MEM;
 342   return;
 343 }
 344
 345
 346
 347 /************ DPOR 2 (invisible and independant transitions) ************/
 348
 349 xbt_dynar_t reached_pairs_prop;
 350 xbt_dynar_t visible_transitions;
 351 xbt_dynar_t enabled_processes;
 352
 353 mc_prop_ato_t new_proposition(char* id, int value){
 354   mc_prop_ato_t prop = NULL;
 355   prop = xbt_new0(s_mc_prop_ato_t, 1);
 356   prop->id = strdup(id);
 357   prop->value = value;
 358   return prop;
 359 }
 360
 361 mc_pair_prop_t new_pair_prop(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
 362   mc_pair_prop_t pair = NULL;
 363   pair = xbt_new0(s_mc_pair_prop_t, 1);
 364   pair->system_state = sn;
 365   pair->automaton_state = st;
 366   pair->graph_state = sg;
 367   pair->propositions = xbt_dynar_new(sizeof(mc_prop_ato_t), NULL);
 368   pair->fully_expanded = 0;
 369   pair->interleave = 0;
 370   mc_stats_pair->expanded_pairs++;
 371   return pair;
 372 }
 373
 374 int reached_prop(mc_pair_prop_t pair){
 375
 376   char* hash_reached = malloc(sizeof(char)*160);
 377   unsigned int c= 0;
 378
 379   MC_SET_RAW_MEM;
 380   char *hash = malloc(sizeof(char)*160);
 381   xbt_sha((char *)&pair, hash);
 382   xbt_dynar_foreach(reached_pairs_prop, c, hash_reached){
 383     if(strcmp(hash, hash_reached) == 0){
 384       MC_UNSET_RAW_MEM;
 385       return 1;
 386     }
 387   }
 388
 389   MC_UNSET_RAW_MEM;
 390   return 0;
 391 }
 392
 393 void set_pair_prop_reached(mc_pair_prop_t pair){
 394
 395   if(reached_prop(pair) == 0){
 396     MC_SET_RAW_MEM;
 397     char *hash = malloc(sizeof(char)*160) ;
 398     xbt_sha((char *)&pair, hash);
 399     xbt_dynar_push(reached_pairs_prop, &hash);
 400     MC_UNSET_RAW_MEM;
 401   }
 402
 403 }
 404
 405 int invisible(mc_pair_prop_t p, mc_pair_prop_t np){
 406   mc_prop_ato_t prop1;
 407   mc_prop_ato_t prop2;
 408   int i;
 409   for(i=0;i<xbt_dynar_length(p->propositions); i++){
 410     prop1 = xbt_dynar_get_as(p->propositions, i, mc_prop_ato_t);
 411     prop2 = xbt_dynar_get_as(np->propositions, i, mc_prop_ato_t);
 412     //XBT_DEBUG("test invisible : prop 1 = %s : %d / prop 2 = %s : %d", prop1->id, prop1->value, prop2->id, prop2->value);
 413     if(prop1->value != prop2->value)
 414           return 0;
 415   }
 416   return 1;
 417
 418 }
 419
 420 void set_fully_expanded(mc_pair_prop_t pair){
 421   pair->fully_expanded = 1;
 422 }
 423
 424 void MC_dpor2_init(xbt_automaton_t a)
 425 {
 426   mc_pair_prop_t initial_pair = NULL;
 427   mc_state_t initial_graph_state = NULL;
 428   mc_snapshot_t initial_system_state = NULL;
 429   xbt_state_t initial_automaton_state = NULL;
 430
 431
 432   MC_SET_RAW_MEM;
 433   initial_graph_state = MC_state_new();
 434   MC_UNSET_RAW_MEM;
 435
 436   /* Wait for requests (schedules processes) */
 437   MC_wait_for_requests();
 438
 439   unsigned int cursor = 0;
 440   unsigned int cursor2 = 0;
 441   xbt_state_t automaton_state = NULL;
 442   int res;
 443   xbt_transition_t transition_succ;
 444
 445   xbt_dynar_foreach(a->states, cursor, automaton_state){
 446     if(automaton_state->type == -1){
 447       xbt_dynar_foreach(automaton_state->out, cursor2, transition_succ){
 448         res = MC_automaton_evaluate_label(a, transition_succ->label);
 449         if((res == 1) || (res == 2)){
 450           initial_automaton_state = transition_succ->dst;
 451           break;
 452         }
 453       }
 454     }
 455
 456     if(xbt_fifo_size(mc_snapshot_stack) > 0)
 457       break;
 458   }
 459
 460   if(xbt_fifo_size(mc_snapshot_stack) == 0){
 461     cursor = 0;
 462     xbt_dynar_foreach(a->states, cursor, automaton_state){
 463       if(automaton_state->type == -1){
 464         initial_automaton_state = automaton_state;
 465         break;
 466       }
 467     }
 468   }
 469
 470   reached_pairs_prop = xbt_dynar_new(sizeof(char *), NULL);
 471   visible_transitions = xbt_dynar_new(sizeof(s_smx_req_t), NULL);
 472   enabled_processes = xbt_dynar_new(sizeof(smx_process_t), NULL);
 473
 474   MC_SET_RAW_MEM;
 475   initial_system_state = xbt_new0(s_mc_snapshot_t, 1);
 476   MC_take_snapshot(initial_system_state);
 477   initial_pair = new_pair_prop(initial_system_state, initial_graph_state, initial_automaton_state);
 478   cursor = 0;
 479   xbt_propositional_symbol_t ps;
 480   xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 481     int (*f)() = ps->function;
 482     int val = (*f)();
 483     mc_prop_ato_t pa = new_proposition(ps->pred, val);
 484     xbt_dynar_push(initial_pair->propositions, &pa);
 485   }
 486   xbt_fifo_unshift(mc_snapshot_stack, initial_pair);
 487   MC_UNSET_RAW_MEM;
 488
 489
 490   XBT_DEBUG("**************************************************");
 491   XBT_DEBUG("Initial pair");
 492
 493   MC_dpor2(a, 0);
 494
 495 }
 496
 497
 498 void MC_dpor2(xbt_automaton_t a, int search_cycle)
 499 {
 500   char *req_str;
 501   int value;
 502   smx_req_t req = NULL, prev_req = NULL;
 503   mc_state_t next_graph_state = NULL;
 504   mc_snapshot_t next_system_state = NULL;
 505   xbt_state_t next_automaton_state = NULL;
 506   xbt_transition_t transition_succ;
 507   unsigned int cursor;
 508   int res;
 509   mc_pair_prop_t pair = NULL, next_pair = NULL, prev_pair = NULL;
 510   smx_process_t process = NULL;
 511   xbt_fifo_item_t item = NULL;
 512   int d;
 513
 514
 515   while (xbt_fifo_size(mc_snapshot_stack) > 0) {
 516
 517     /* Get current pair */
 518     pair = (mc_pair_prop_t)
 519       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 520
 521     XBT_DEBUG("**************************************************");
 522     XBT_DEBUG("Exploration depth=%d (pair=%p) (%d interleave)",
 523               xbt_fifo_size(mc_snapshot_stack), pair, MC_state_interleave_size(pair->graph_state));
 524
 525     if(MC_state_interleave_size(pair->graph_state) == 0){
 526
 527       xbt_dynar_reset(enabled_processes);
 528
 529       MC_SET_RAW_MEM;
 530
 531       xbt_swag_foreach(process, simix_global->process_list){
 532         if(MC_process_is_enabled(process)){
 533           xbt_dynar_push(enabled_processes, &process);
 534           //XBT_DEBUG("Process : pid=%lu",process->pid);
 535         }
 536       }
 537
 538       XBT_DEBUG("Enabled processes before pop : %lu", xbt_dynar_length(enabled_processes));
 539
 540       XBT_DEBUG("Processes already interleaved : %d", pair->interleave);
 541
 542       if(xbt_dynar_length(enabled_processes) > 0){
 543         for(d=0;d<pair->interleave;d++){
 544           xbt_dynar_shift(enabled_processes, NULL);
 545         }
 546       }
 547
 548       XBT_DEBUG("Enabled processes after pop : %lu", xbt_dynar_length(enabled_processes));
 549
 550       if(pair->fully_expanded == 0){
 551         if(xbt_dynar_length(enabled_processes) > 0){
 552           MC_state_interleave_process(pair->graph_state, xbt_dynar_get_as(enabled_processes, 0, smx_process_t));
 553           //XBT_DEBUG("Interleave process");
 554         }
 555       }
 556
 557       MC_UNSET_RAW_MEM;
 558
 559     }
 560
 561
 562     /* Update statistics */
 563     mc_stats_pair->visited_pairs++;
 564     //sleep(1);
 565
 566     /*cursor = 0;
 567     mc_prop_ato_t pato;
 568     xbt_dynar_foreach(pair->propositions, cursor, pato){
 569       XBT_DEBUG("%s : %d", pato->id, pato->value);
 570       }*/
 571
 572     /* Test acceptance pair and acceptance cycle*/
 573
 574     if(pair->automaton_state->type == 1){
 575       if(search_cycle == 0){
 576         set_pair_prop_reached(pair);
 577         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair->graph_state, pair->automaton_state, pair->automaton_state->id);
 578       }else{
 579         if(reached_prop(pair) == 1){
 580           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 581           XBT_INFO("|             ACCEPTANCE CYCLE            |");
 582           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 583           XBT_INFO("Counter-example that violates formula :");
 584           MC_show_snapshot_stack(mc_snapshot_stack);
 585           MC_dump_snapshot_stack(mc_snapshot_stack);
 586           MC_print_statistics_pairs(mc_stats_pair);
 587           exit(0);
 588         }
 589       }
 590     }
 591
 592     /* If there are processes to interleave and the maximum depth has not been reached
 593        then perform one step of the exploration algorithm */
 594     if (xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH &&
 595         (req = MC_state_get_request(pair->graph_state, &value))) {
 596
 597       /* Debug information */
 598       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 599         req_str = MC_request_to_string(req, value);
 600         XBT_DEBUG("Execute: %s", req_str);
 601         xbt_free(req_str);
 602       }
 603
 604       MC_state_set_executed_request(pair->graph_state, req, value);
 605       //mc_stats_pairs->executed_transitions++;
 606
 607       /* Answer the request */
 608       SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
 609
 610       /* Wait for requests (schedules processes) */
 611       MC_wait_for_requests();
 612
 613       /* Create the new expanded state */
 614       MC_SET_RAW_MEM;
 615
 616       pair->interleave++;
 617       //XBT_DEBUG("Process interleaved in pair %p : %u", pair, MC_state_interleave_size(pair->graph_state));
 618       //xbt_dynar_pop(enabled_processes, NULL);
 619
 620       next_graph_state = MC_state_new();
 621
 622       next_system_state = xbt_new0(s_mc_snapshot_t, 1);
 623       MC_take_snapshot(next_system_state);
 624       MC_UNSET_RAW_MEM;
 625
 626       cursor = 0;
 627       xbt_dynar_foreach(pair->automaton_state->out, cursor, transition_succ){
 628         res = MC_automaton_evaluate_label(a, transition_succ->label);
 629         if((res == 1) || (res == 2)){ // enabled transition in automaton
 630           next_automaton_state = transition_succ->dst;
 631           break;
 632         }
 633       }
 634
 635       if(next_automaton_state == NULL){
 636         next_automaton_state = pair->automaton_state;
 637       }
 638
 639       MC_SET_RAW_MEM;
 640
 641       next_pair = new_pair_prop(next_system_state, next_graph_state, next_automaton_state);
 642       cursor = 0;
 643       xbt_propositional_symbol_t ps;
 644       xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 645         int (*f)() = ps->function;
 646         int val = (*f)();
 647         mc_prop_ato_t pa = new_proposition(ps->pred, val);
 648         xbt_dynar_push(next_pair->propositions, &pa);
 649         //XBT_DEBUG("%s : %d", pa->id, pa->value);
 650       }
 651       xbt_fifo_unshift(mc_snapshot_stack, next_pair);
 652
 653       cursor = 0;
 654       if((invisible(pair, next_pair) == 0) && (pair->fully_expanded == 0)){
 655         set_fully_expanded(pair);
 656         if(xbt_dynar_length(enabled_processes) > 1){ // Si 1 seul process activé, déjà exécuté juste avant donc état complètement étudié
 657           xbt_dynar_foreach(enabled_processes, cursor, process){
 658             MC_state_interleave_process(pair->graph_state, process);
 659           }
 660         }
 661         XBT_DEBUG("Pair %p fully expanded (%u interleave)", pair, MC_state_interleave_size(pair->graph_state));
 662       }
 663
 664       MC_UNSET_RAW_MEM;
 665
 666
 667       /* Let's loop again */
 668
 669       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 670     } else {
 671       XBT_DEBUG("There are no more processes to interleave.");
 672
 673       /* Trash the current state, no longer needed */
 674       MC_SET_RAW_MEM;
 675       xbt_fifo_shift(mc_snapshot_stack);
 676       //MC_state_delete(state);
 677       MC_UNSET_RAW_MEM;
 678
 679       /* Check for deadlocks */
 680       if(MC_deadlock_check()){
 681         MC_show_deadlock(NULL);
 682         return;
 683       }
 684
 685       MC_SET_RAW_MEM;
 686       /* Traverse the stack backwards until a state with a non empty interleave
 687          set is found, deleting all the states that have it empty in the way.
 688          For each deleted state, check if the request that has generated it
 689          (from it's predecesor state), depends on any other previous request
 690          executed before it. If it does then add it to the interleave set of the
 691          state that executed that previous request. */
 692       while ((pair = xbt_fifo_shift(mc_snapshot_stack)) != NULL) {
 693         req = MC_state_get_internal_request(pair->graph_state);
 694         xbt_fifo_foreach(mc_snapshot_stack, item, prev_pair, mc_pair_prop_t) {
 695           if(MC_request_depend(req, MC_state_get_internal_request(prev_pair->graph_state))){
 696             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 697               XBT_DEBUG("Dependent Transitions:");
 698               prev_req = MC_state_get_executed_request(prev_pair->graph_state, &value);
 699               req_str = MC_request_to_string(prev_req, value);
 700               XBT_DEBUG("%s (pair=%p)", req_str, prev_pair);
 701               xbt_free(req_str);
 702               prev_req = MC_state_get_executed_request(pair->graph_state, &value);
 703               req_str = MC_request_to_string(prev_req, value);
 704               XBT_DEBUG("%s (pair=%p)", req_str, pair);
 705               xbt_free(req_str);
 706             }
 707
 708             if(prev_pair->fully_expanded == 0){
 709               if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer)){
 710                 MC_state_interleave_process(prev_pair->graph_state, req->issuer);
 711                 XBT_DEBUG("Process %p (%lu) interleaved in pair %p", req->issuer, req->issuer->pid, prev_pair);
 712               }else{
 713                 XBT_DEBUG("Process %p (%lu) is in done set", req->issuer, req->issuer->pid);
 714               }
 715             }
 716
 717             break;
 718           }
 719         }
 720
 721
 722         if (MC_state_interleave_size(pair->graph_state) > 0) {
 723           /* We found a back-tracking point, let's loop */
 724           MC_restore_snapshot(pair->system_state);
 725           xbt_fifo_unshift(mc_snapshot_stack, pair);
 726           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));
 727           MC_UNSET_RAW_MEM;
 728           break;
 729         } else {
 730           //MC_state_delete(state);
 731         }
 732       }
 733       MC_UNSET_RAW_MEM;
 734     }
 735   }
 736   MC_UNSET_RAW_MEM;
 737   return;
 738 }