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_stateful_init(){
 193
 194   XBT_DEBUG("**************************************************");
 195   XBT_DEBUG("DPOR (stateful) 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 }
 225
 226 void MC_dpor_stateful(){
 227
 228   smx_process_t process = NULL;
 229
 230   if(xbt_fifo_size(mc_snapshot_stack) == 0)
 231     return;
 232
 233   int value;
 234   mc_state_t next_graph_state = NULL;
 235   smx_req_t req = NULL, prev_req = NULL;
 236   char *req_str;
 237   xbt_fifo_item_t item = NULL;
 238
 239   mc_snapshot_t next_snapshot;
 240   mc_state_ws_t current_state;
 241   mc_state_ws_t prev_state;
 242   mc_state_ws_t next_state;
 243
 244   while(xbt_fifo_size(mc_snapshot_stack) > 0){
 245
 246     current_state = (mc_state_ws_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 247
 248
 249     XBT_DEBUG("**************************************************");
 250     XBT_DEBUG("Depth : %d, State : %p , %u interleave", xbt_fifo_size(mc_snapshot_stack),current_state, MC_state_interleave_size(current_state->graph_state));
 251
 252     mc_stats->visited_states++;
 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       mc_stats->executed_transitions++;
 266
 267       /* Answer the request */
 268       SIMIX_request_pre(req, value);
 269
 270       /* Wait for requests (schedules processes) */
 271       MC_wait_for_requests();
 272
 273       /* Create the new expanded graph_state */
 274       MC_SET_RAW_MEM;
 275
 276       next_graph_state = MC_state_new();
 277
 278       /* Get an enabled process and insert it in the interleave set of the next graph_state */
 279       xbt_swag_foreach(process, simix_global->process_list){
 280         if(MC_process_is_enabled(process)){
 281           MC_state_interleave_process(next_graph_state, process);
 282           break;
 283         }
 284       }
 285
 286       next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 287       MC_take_snapshot(next_snapshot);
 288
 289       next_state = new_state_ws(next_snapshot, next_graph_state);
 290       xbt_fifo_unshift(mc_snapshot_stack, next_state);
 291
 292       MC_UNSET_RAW_MEM;
 293
 294     }else{
 295       XBT_DEBUG("There are no more processes to interleave.");
 296
 297       /* Trash the current state, no longer needed */
 298       MC_SET_RAW_MEM;
 299       xbt_fifo_shift(mc_snapshot_stack);
 300       MC_UNSET_RAW_MEM;
 301
 302       /* Check for deadlocks */
 303       if(MC_deadlock_check()){
 304         MC_show_deadlock_stateful(NULL);
 305         return;
 306       }
 307
 308       MC_SET_RAW_MEM;
 309       while((current_state = xbt_fifo_shift(mc_snapshot_stack)) != NULL){
 310         req = MC_state_get_internal_request(current_state->graph_state);
 311         xbt_fifo_foreach(mc_snapshot_stack, item, prev_state, mc_state_ws_t) {
 312           if(MC_request_depend(req, MC_state_get_internal_request(prev_state->graph_state))){
 313             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 314               XBT_DEBUG("Dependent Transitions:");
 315               prev_req = MC_state_get_executed_request(prev_state->graph_state, &value);
 316               req_str = MC_request_to_string(prev_req, value);
 317               XBT_DEBUG("%s (state=%p)", req_str, prev_state->graph_state);
 318               xbt_free(req_str);
 319               prev_req = MC_state_get_executed_request(current_state->graph_state, &value);
 320               req_str = MC_request_to_string(prev_req, value);
 321               XBT_DEBUG("%s (state=%p)", req_str, current_state->graph_state);
 322               xbt_free(req_str);
 323             }
 324
 325             if(!MC_state_process_is_done(prev_state->graph_state, req->issuer)){
 326               MC_state_interleave_process(prev_state->graph_state, req->issuer);
 327
 328             } else {
 329               XBT_DEBUG("Process %p is in done set", req->issuer);
 330             }
 331
 332             break;
 333           }
 334         }
 335
 336         if(MC_state_interleave_size(current_state->graph_state)){
 337           MC_restore_snapshot(current_state->system_state);
 338           xbt_fifo_unshift(mc_snapshot_stack, current_state);
 339           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));
 340           MC_UNSET_RAW_MEM;
 341           break;
 342         }
 343       }
 344
 345       MC_UNSET_RAW_MEM;
 346
 347     }
 348   }
 349   MC_UNSET_RAW_MEM;
 350   return;
 351 }
 352
 353
 354
 355 /************ DPOR 2 (invisible and independant transitions) ************/
 356
 357 xbt_dynar_t reached_pairs_prop;
 358 xbt_dynar_t visible_transitions;
 359 xbt_dynar_t enabled_processes;
 360
 361 mc_prop_ato_t new_proposition(char* id, int value){
 362   mc_prop_ato_t prop = NULL;
 363   prop = xbt_new0(s_mc_prop_ato_t, 1);
 364   prop->id = strdup(id);
 365   prop->value = value;
 366   return prop;
 367 }
 368
 369 mc_pair_prop_t new_pair_prop(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
 370   mc_pair_prop_t pair = NULL;
 371   pair = xbt_new0(s_mc_pair_prop_t, 1);
 372   pair->system_state = sn;
 373   pair->automaton_state = st;
 374   pair->graph_state = sg;
 375   pair->propositions = xbt_dynar_new(sizeof(mc_prop_ato_t), NULL);
 376   pair->fully_expanded = 0;
 377   pair->interleave = 0;
 378   mc_stats_pair->expanded_pairs++;
 379   return pair;
 380 }
 381
 382 int reached_prop(mc_pair_prop_t pair){
 383
 384   char* hash_reached = malloc(sizeof(char)*160);
 385   unsigned int c= 0;
 386
 387   MC_SET_RAW_MEM;
 388   char *hash = malloc(sizeof(char)*160);
 389   xbt_sha((char *)&pair, hash);
 390   xbt_dynar_foreach(reached_pairs_prop, c, hash_reached){
 391     if(strcmp(hash, hash_reached) == 0){
 392       MC_UNSET_RAW_MEM;
 393       return 1;
 394     }
 395   }
 396
 397   MC_UNSET_RAW_MEM;
 398   return 0;
 399 }
 400
 401 void set_pair_prop_reached(mc_pair_prop_t pair){
 402
 403   if(reached_prop(pair) == 0){
 404     MC_SET_RAW_MEM;
 405     char *hash = malloc(sizeof(char)*160) ;
 406     xbt_sha((char *)&pair, hash);
 407     xbt_dynar_push(reached_pairs_prop, &hash);
 408     MC_UNSET_RAW_MEM;
 409   }
 410
 411 }
 412
 413 int invisible(mc_pair_prop_t p, mc_pair_prop_t np){
 414   mc_prop_ato_t prop1;
 415   mc_prop_ato_t prop2;
 416   int i;
 417   for(i=0;i<xbt_dynar_length(p->propositions); i++){
 418     prop1 = xbt_dynar_get_as(p->propositions, i, mc_prop_ato_t);
 419     prop2 = xbt_dynar_get_as(np->propositions, i, mc_prop_ato_t);
 420     //XBT_DEBUG("test invisible : prop 1 = %s : %d / prop 2 = %s : %d", prop1->id, prop1->value, prop2->id, prop2->value);
 421     if(prop1->value != prop2->value)
 422           return 0;
 423   }
 424   return 1;
 425
 426 }
 427
 428 void set_fully_expanded(mc_pair_prop_t pair){
 429   pair->fully_expanded = 1;
 430 }
 431
 432 void MC_dpor2_init(xbt_automaton_t a)
 433 {
 434   mc_pair_prop_t initial_pair = NULL;
 435   mc_state_t initial_graph_state = NULL;
 436   mc_snapshot_t initial_system_state = NULL;
 437   xbt_state_t initial_automaton_state = NULL;
 438
 439
 440   MC_SET_RAW_MEM;
 441   initial_graph_state = MC_state_new();
 442   MC_UNSET_RAW_MEM;
 443
 444   /* Wait for requests (schedules processes) */
 445   MC_wait_for_requests();
 446
 447   unsigned int cursor = 0;
 448   unsigned int cursor2 = 0;
 449   xbt_state_t automaton_state = NULL;
 450   int res;
 451   xbt_transition_t transition_succ;
 452
 453   xbt_dynar_foreach(a->states, cursor, automaton_state){
 454     if(automaton_state->type == -1){
 455       xbt_dynar_foreach(automaton_state->out, cursor2, transition_succ){
 456         res = MC_automaton_evaluate_label(a, transition_succ->label);
 457         if((res == 1) || (res == 2)){
 458           initial_automaton_state = transition_succ->dst;
 459           break;
 460         }
 461       }
 462     }
 463
 464     if(xbt_fifo_size(mc_snapshot_stack) > 0)
 465       break;
 466   }
 467
 468   if(xbt_fifo_size(mc_snapshot_stack) == 0){
 469     cursor = 0;
 470     xbt_dynar_foreach(a->states, cursor, automaton_state){
 471       if(automaton_state->type == -1){
 472         initial_automaton_state = automaton_state;
 473         break;
 474       }
 475     }
 476   }
 477
 478   reached_pairs_prop = xbt_dynar_new(sizeof(char *), NULL);
 479   visible_transitions = xbt_dynar_new(sizeof(s_smx_req_t), NULL);
 480   enabled_processes = xbt_dynar_new(sizeof(smx_process_t), NULL);
 481
 482   MC_SET_RAW_MEM;
 483   initial_system_state = xbt_new0(s_mc_snapshot_t, 1);
 484   MC_take_snapshot(initial_system_state);
 485   initial_pair = new_pair_prop(initial_system_state, initial_graph_state, initial_automaton_state);
 486   cursor = 0;
 487   xbt_propositional_symbol_t ps;
 488   xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 489     int (*f)() = ps->function;
 490     int val = (*f)();
 491     mc_prop_ato_t pa = new_proposition(ps->pred, val);
 492     xbt_dynar_push(initial_pair->propositions, &pa);
 493   }
 494   xbt_fifo_unshift(mc_snapshot_stack, initial_pair);
 495   MC_UNSET_RAW_MEM;
 496
 497
 498   XBT_DEBUG("**************************************************");
 499   XBT_DEBUG("Initial pair");
 500
 501   MC_dpor2(a, 0);
 502
 503 }
 504
 505
 506 void MC_dpor2(xbt_automaton_t a, int search_cycle)
 507 {
 508   char *req_str;
 509   int value;
 510   smx_req_t req = NULL, prev_req = NULL;
 511   mc_state_t next_graph_state = NULL;
 512   mc_snapshot_t next_system_state = NULL;
 513   xbt_state_t next_automaton_state = NULL;
 514   xbt_transition_t transition_succ;
 515   unsigned int cursor;
 516   int res;
 517   mc_pair_prop_t pair = NULL, next_pair = NULL, prev_pair = NULL;
 518   smx_process_t process = NULL;
 519   xbt_fifo_item_t item = NULL;
 520   int d;
 521
 522
 523   while (xbt_fifo_size(mc_snapshot_stack) > 0) {
 524
 525     /* Get current pair */
 526     pair = (mc_pair_prop_t)
 527       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 528
 529     XBT_DEBUG("**************************************************");
 530     XBT_DEBUG("Exploration depth=%d (pair=%p) (%d interleave)",
 531               xbt_fifo_size(mc_snapshot_stack), pair, MC_state_interleave_size(pair->graph_state));
 532
 533     if(MC_state_interleave_size(pair->graph_state) == 0){
 534
 535       xbt_dynar_reset(enabled_processes);
 536
 537       MC_SET_RAW_MEM;
 538
 539       xbt_swag_foreach(process, simix_global->process_list){
 540         if(MC_process_is_enabled(process)){
 541           xbt_dynar_push(enabled_processes, &process);
 542           //XBT_DEBUG("Process : pid=%lu",process->pid);
 543         }
 544       }
 545
 546       //XBT_DEBUG("Enabled processes before pop : %lu", xbt_dynar_length(enabled_processes));
 547
 548       //XBT_DEBUG("Processes already interleaved : %d", pair->interleave);
 549
 550       if(xbt_dynar_length(enabled_processes) > 0){
 551         for(d=0;d<pair->interleave;d++){
 552           xbt_dynar_shift(enabled_processes, NULL);
 553         }
 554       }
 555
 556       //XBT_DEBUG("Enabled processes after pop : %lu", xbt_dynar_length(enabled_processes));
 557
 558       if(pair->fully_expanded == 0){
 559         if(xbt_dynar_length(enabled_processes) > 0){
 560           MC_state_interleave_process(pair->graph_state, xbt_dynar_get_as(enabled_processes, 0, smx_process_t));
 561           //XBT_DEBUG("Interleave process");
 562         }
 563       }
 564
 565       MC_UNSET_RAW_MEM;
 566
 567     }
 568
 569
 570     /* Update statistics */
 571     mc_stats_pair->visited_pairs++;
 572     //sleep(1);
 573
 574     /*cursor = 0;
 575     mc_prop_ato_t pato;
 576     xbt_dynar_foreach(pair->propositions, cursor, pato){
 577       XBT_DEBUG("%s : %d", pato->id, pato->value);
 578       }*/
 579
 580     /* Test acceptance pair and acceptance cycle*/
 581
 582     if(pair->automaton_state->type == 1){
 583       if(search_cycle == 0){
 584         set_pair_prop_reached(pair);
 585         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair->graph_state, pair->automaton_state, pair->automaton_state->id);
 586       }else{
 587         if(reached_prop(pair) == 1){
 588           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 589           XBT_INFO("|             ACCEPTANCE CYCLE            |");
 590           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 591           XBT_INFO("Counter-example that violates formula :");
 592           MC_show_snapshot_stack(mc_snapshot_stack);
 593           MC_dump_snapshot_stack(mc_snapshot_stack);
 594           MC_print_statistics_pairs(mc_stats_pair);
 595           exit(0);
 596         }
 597       }
 598     }
 599
 600     /* If there are processes to interleave and the maximum depth has not been reached
 601        then perform one step of the exploration algorithm */
 602     if (xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH &&
 603         (req = MC_state_get_request(pair->graph_state, &value))) {
 604
 605       /* Debug information */
 606       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 607         req_str = MC_request_to_string(req, value);
 608         XBT_DEBUG("Execute: %s", req_str);
 609         xbt_free(req_str);
 610       }
 611
 612       MC_state_set_executed_request(pair->graph_state, req, value);
 613       //mc_stats_pairs->executed_transitions++;
 614
 615       /* Answer the request */
 616       SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
 617
 618       /* Wait for requests (schedules processes) */
 619       MC_wait_for_requests();
 620
 621       /* Create the new expanded state */
 622       MC_SET_RAW_MEM;
 623
 624       pair->interleave++;
 625       //XBT_DEBUG("Process interleaved in pair %p : %u", pair, MC_state_interleave_size(pair->graph_state));
 626       //xbt_dynar_pop(enabled_processes, NULL);
 627
 628       next_graph_state = MC_state_new();
 629
 630       next_system_state = xbt_new0(s_mc_snapshot_t, 1);
 631       MC_take_snapshot(next_system_state);
 632       MC_UNSET_RAW_MEM;
 633
 634       cursor = 0;
 635       xbt_dynar_foreach(pair->automaton_state->out, cursor, transition_succ){
 636         res = MC_automaton_evaluate_label(a, transition_succ->label);
 637         if((res == 1) || (res == 2)){ // enabled transition in automaton
 638           next_automaton_state = transition_succ->dst;
 639           break;
 640         }
 641       }
 642
 643       if(next_automaton_state == NULL){
 644         next_automaton_state = pair->automaton_state;
 645       }
 646
 647       MC_SET_RAW_MEM;
 648
 649       next_pair = new_pair_prop(next_system_state, next_graph_state, next_automaton_state);
 650       cursor = 0;
 651       xbt_propositional_symbol_t ps;
 652       xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 653         int (*f)() = ps->function;
 654         int val = (*f)();
 655         mc_prop_ato_t pa = new_proposition(ps->pred, val);
 656         xbt_dynar_push(next_pair->propositions, &pa);
 657         //XBT_DEBUG("%s : %d", pa->id, pa->value);
 658       }
 659       xbt_fifo_unshift(mc_snapshot_stack, next_pair);
 660
 661       cursor = 0;
 662       if((invisible(pair, next_pair) == 0) && (pair->fully_expanded == 0)){
 663         set_fully_expanded(pair);
 664         if(xbt_dynar_length(enabled_processes) > 1){ // Si 1 seul process activé, déjà exécuté juste avant donc état complètement étudié
 665           xbt_dynar_foreach(enabled_processes, cursor, process){
 666             MC_state_interleave_process(pair->graph_state, process);
 667           }
 668         }
 669         XBT_DEBUG("Pair %p fully expanded (%u interleave)", pair, MC_state_interleave_size(pair->graph_state));
 670       }
 671
 672       MC_UNSET_RAW_MEM;
 673
 674
 675       /* Let's loop again */
 676
 677       /* The interleave set is empty or the maximum depth is reached, let's back-track */
 678     } else {
 679       XBT_DEBUG("There are no more processes to interleave.");
 680
 681       /* Trash the current state, no longer needed */
 682       MC_SET_RAW_MEM;
 683       xbt_fifo_shift(mc_snapshot_stack);
 684       //MC_state_delete(state);
 685       MC_UNSET_RAW_MEM;
 686
 687       /* Check for deadlocks */
 688       if(MC_deadlock_check()){
 689         MC_show_deadlock(NULL);
 690         return;
 691       }
 692
 693       MC_SET_RAW_MEM;
 694       /* Traverse the stack backwards until a state with a non empty interleave
 695          set is found, deleting all the states that have it empty in the way.
 696          For each deleted state, check if the request that has generated it
 697          (from it's predecesor state), depends on any other previous request
 698          executed before it. If it does then add it to the interleave set of the
 699          state that executed that previous request. */
 700       while ((pair = xbt_fifo_shift(mc_snapshot_stack)) != NULL) {
 701         req = MC_state_get_internal_request(pair->graph_state);
 702         xbt_fifo_foreach(mc_snapshot_stack, item, prev_pair, mc_pair_prop_t) {
 703           if(MC_request_depend(req, MC_state_get_internal_request(prev_pair->graph_state))){
 704             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 705               XBT_DEBUG("Dependent Transitions:");
 706               prev_req = MC_state_get_executed_request(prev_pair->graph_state, &value);
 707               req_str = MC_request_to_string(prev_req, value);
 708               XBT_DEBUG("%s (pair=%p)", req_str, prev_pair);
 709               xbt_free(req_str);
 710               prev_req = MC_state_get_executed_request(pair->graph_state, &value);
 711               req_str = MC_request_to_string(prev_req, value);
 712               XBT_DEBUG("%s (pair=%p)", req_str, pair);
 713               xbt_free(req_str);
 714             }
 715
 716             if(prev_pair->fully_expanded == 0){
 717               if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer)){
 718                 MC_state_interleave_process(prev_pair->graph_state, req->issuer);
 719                 XBT_DEBUG("Process %p (%lu) interleaved in pair %p", req->issuer, req->issuer->pid, prev_pair);
 720               }else{
 721                 XBT_DEBUG("Process %p (%lu) is in done set", req->issuer, req->issuer->pid);
 722               }
 723             }
 724
 725             break;
 726           }
 727         }
 728
 729
 730         if (MC_state_interleave_size(pair->graph_state) > 0) {
 731           /* We found a back-tracking point, let's loop */
 732           MC_restore_snapshot(pair->system_state);
 733           xbt_fifo_unshift(mc_snapshot_stack, pair);
 734           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));
 735           MC_UNSET_RAW_MEM;
 736           break;
 737         } else {
 738           //MC_state_delete(state);
 739         }
 740       }
 741       MC_UNSET_RAW_MEM;
 742     }
 743   }
 744   MC_UNSET_RAW_MEM;
 745   return;
 746 }
 747
 748 /************ DPOR 3 (invisible and independant transitions with coloration of pairs) ************/
 749
 750 int expanded;
 751 xbt_dynar_t reached_pairs_prop_col;
 752 xbt_dynar_t visited_pairs_prop_col;
 753
 754
 755
 756 mc_pair_prop_col_t new_pair_prop_col(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
 757
 758   mc_pair_prop_col_t pair = NULL;
 759   pair = xbt_new0(s_mc_pair_prop_col_t, 1);
 760   pair->system_state = sn;
 761   pair->automaton_state = st;
 762   pair->graph_state = sg;
 763   pair->propositions = xbt_dynar_new(sizeof(mc_prop_ato_t), NULL);
 764   pair->fully_expanded = 0;
 765   pair->interleave = 0;
 766   pair->color=ORANGE;
 767   mc_stats_pair->expanded_pairs++;
 768   //XBT_DEBUG("New pair %p : automaton=%p", pair, st);
 769   return pair;
 770 }
 771
 772 void set_expanded(mc_pair_prop_col_t pair){
 773   pair->expanded = expanded;
 774 }
 775
 776 int reached_prop_col(mc_pair_prop_col_t pair){
 777
 778   char* hash_reached = malloc(sizeof(char)*160);
 779   unsigned int c= 0;
 780
 781   MC_SET_RAW_MEM;
 782   char *hash = malloc(sizeof(char)*160);
 783   xbt_sha((char *)&pair, hash);
 784   xbt_dynar_foreach(reached_pairs_prop_col, c, hash_reached){
 785     if(strcmp(hash, hash_reached) == 0){
 786       MC_UNSET_RAW_MEM;
 787       return 1;
 788     }
 789   }
 790
 791   MC_UNSET_RAW_MEM;
 792   return 0;
 793 }
 794
 795 void set_pair_prop_col_reached(mc_pair_prop_col_t pair){
 796
 797   if(reached_prop_col(pair) == 0){
 798     MC_SET_RAW_MEM;
 799     char *hash = malloc(sizeof(char)*160) ;
 800     xbt_sha((char *)&pair, hash);
 801     xbt_dynar_push(reached_pairs_prop_col, &hash);
 802     MC_UNSET_RAW_MEM;
 803   }
 804
 805 }
 806
 807 int invisible_col(mc_pair_prop_col_t p, mc_pair_prop_col_t np){
 808   mc_prop_ato_t prop1;
 809   mc_prop_ato_t prop2;
 810   int i;
 811   for(i=0;i<xbt_dynar_length(p->propositions); i++){
 812     prop1 = xbt_dynar_get_as(p->propositions, i, mc_prop_ato_t);
 813     prop2 = xbt_dynar_get_as(np->propositions, i, mc_prop_ato_t);
 814     //XBT_DEBUG("test invisible : prop 1 = %s : %d / prop 2 = %s : %d", prop1->id, prop1->value, prop2->id, prop2->value);
 815     if(prop1->value != prop2->value)
 816           return 0;
 817   }
 818   return 1;
 819
 820 }
 821
 822 void set_fully_expanded_col(mc_pair_prop_col_t pair){
 823   pair->fully_expanded = 1;
 824   pair->color = GREEN;
 825 }
 826
 827 void set_pair_prop_col_visited(mc_pair_prop_col_t pair, int sc){
 828
 829   MC_SET_RAW_MEM;
 830   mc_visited_pair_prop_col_t p = NULL;
 831   p = xbt_new0(s_mc_visited_pair_prop_col_t, 1);
 832   p->pair = pair;
 833   p->search_cycle = sc;
 834   char *hash = malloc(sizeof(char)*160);
 835   xbt_sha((char *)&p, hash);
 836   xbt_dynar_push(visited_pairs_prop_col, &hash);
 837   MC_UNSET_RAW_MEM;
 838
 839 }
 840
 841 int visited_pair_prop_col(mc_pair_prop_col_t pair, int sc){
 842
 843   char* hash_visited = malloc(sizeof(char)*160);
 844   unsigned int c= 0;
 845
 846   MC_SET_RAW_MEM;
 847   mc_visited_pair_prop_col_t p = NULL;
 848   p = xbt_new0(s_mc_visited_pair_prop_col_t, 1);
 849   p->pair = pair;
 850   p->search_cycle = sc;
 851   char *hash = malloc(sizeof(char)*160);
 852   xbt_sha((char *)&p, hash);
 853   xbt_dynar_foreach(visited_pairs_prop_col, c, hash_visited){
 854     if(strcmp(hash, hash_visited) == 0){
 855       MC_UNSET_RAW_MEM;
 856       return 1;
 857     }
 858   }
 859
 860   MC_UNSET_RAW_MEM;
 861   return 0;
 862
 863 }
 864
 865 void MC_dpor3_init(xbt_automaton_t a)
 866 {
 867   mc_pair_prop_col_t initial_pair = NULL;
 868   mc_state_t initial_graph_state = NULL;
 869   mc_snapshot_t initial_system_state = NULL;
 870   xbt_state_t initial_automaton_state = NULL;
 871
 872
 873   MC_SET_RAW_MEM;
 874   initial_graph_state = MC_state_new();
 875   MC_UNSET_RAW_MEM;
 876
 877   /* Wait for requests (schedules processes) */
 878   MC_wait_for_requests();
 879
 880   unsigned int cursor = 0;
 881   unsigned int cursor2 = 0;
 882   xbt_state_t automaton_state = NULL;
 883   int res;
 884   xbt_transition_t transition_succ;
 885
 886   xbt_dynar_foreach(a->states, cursor, automaton_state){
 887     if(automaton_state->type == -1){
 888       xbt_dynar_foreach(automaton_state->out, cursor2, transition_succ){
 889         res = MC_automaton_evaluate_label(a, transition_succ->label);
 890         if((res == 1) || (res == 2)){
 891           initial_automaton_state = transition_succ->dst;
 892           break;
 893         }
 894       }
 895     }
 896
 897     if(initial_automaton_state != NULL)
 898       break;
 899   }
 900
 901   if(initial_automaton_state == NULL){
 902     cursor = 0;
 903     xbt_dynar_foreach(a->states, cursor, automaton_state){
 904       if(automaton_state->type == -1){
 905         initial_automaton_state = automaton_state;
 906         break;
 907       }
 908     }
 909   }
 910
 911   reached_pairs_prop_col = xbt_dynar_new(sizeof(char *), NULL);
 912   visited_pairs_prop_col = xbt_dynar_new(sizeof(char *), NULL);
 913   visible_transitions = xbt_dynar_new(sizeof(s_smx_req_t), NULL);
 914   enabled_processes = xbt_dynar_new(sizeof(smx_process_t), NULL);
 915   expanded = 0;
 916
 917   MC_SET_RAW_MEM;
 918   initial_system_state = xbt_new0(s_mc_snapshot_t, 1);
 919   MC_take_snapshot(initial_system_state);
 920   initial_pair = new_pair_prop_col(initial_system_state, initial_graph_state, initial_automaton_state);
 921   cursor = 0;
 922   xbt_propositional_symbol_t ps;
 923   xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 924     int (*f)() = ps->function;
 925     int val = (*f)();
 926     mc_prop_ato_t pa = new_proposition(ps->pred, val);
 927     xbt_dynar_push(initial_pair->propositions, &pa);
 928   }
 929   xbt_fifo_unshift(mc_snapshot_stack, initial_pair);
 930   MC_UNSET_RAW_MEM;
 931
 932
 933   XBT_DEBUG("**************************************************");
 934   XBT_DEBUG("Initial pair");
 935
 936   MC_dpor3(a, 0);
 937
 938 }
 939
 940
 941 void MC_dpor3(xbt_automaton_t a, int search_cycle)
 942 {
 943   char *req_str;
 944   int value;
 945   smx_req_t req = NULL, prev_req = NULL;
 946   mc_state_t next_graph_state = NULL;
 947   mc_snapshot_t next_system_state = NULL;
 948   xbt_state_t next_automaton_state = NULL;
 949   xbt_transition_t transition_succ;
 950   unsigned int cursor;
 951   int res;
 952   mc_pair_prop_col_t pair = NULL, next_pair = NULL, prev_pair = NULL;
 953   smx_process_t process = NULL;
 954   xbt_fifo_item_t item = NULL;
 955   int d;
 956
 957
 958   while (xbt_fifo_size(mc_snapshot_stack) > 0) {
 959
 960     /* Get current pair */
 961     pair = (mc_pair_prop_col_t)
 962       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 963
 964     XBT_DEBUG("**************************************************");
 965     XBT_DEBUG("Exploration depth=%d (pair=%p) (%d interleave)",
 966               xbt_fifo_size(mc_snapshot_stack), pair, MC_state_interleave_size(pair->graph_state));
 967
 968     if(MC_state_interleave_size(pair->graph_state) == 0){
 969
 970       xbt_dynar_reset(enabled_processes);
 971
 972       MC_SET_RAW_MEM;
 973
 974       xbt_swag_foreach(process, simix_global->process_list){
 975         if(MC_process_is_enabled(process)){
 976           xbt_dynar_push(enabled_processes, &process);
 977           //XBT_DEBUG("Process : pid=%lu",process->pid);
 978         }
 979       }
 980
 981       //XBT_DEBUG("Enabled processes before pop : %lu", xbt_dynar_length(enabled_processes));
 982
 983       //XBT_DEBUG("Processes already interleaved : %d", pair->interleave);
 984
 985       if(xbt_dynar_length(enabled_processes) > 0){
 986         for(d=0;d<pair->interleave;d++){
 987           xbt_dynar_shift(enabled_processes, NULL);
 988         }
 989       }
 990
 991       //XBT_DEBUG("Enabled processes after pop : %lu", xbt_dynar_length(enabled_processes));
 992
 993       if(pair->fully_expanded == 0){
 994         if(xbt_dynar_length(enabled_processes) > 0){
 995           MC_state_interleave_process(pair->graph_state, xbt_dynar_get_as(enabled_processes, 0, smx_process_t));
 996           //XBT_DEBUG("Interleave process");
 997         }
 998       }
 999
1000       MC_UNSET_RAW_MEM;
1001
1002     }
1003
1004
1005     /* Update statistics */
1006     mc_stats_pair->visited_pairs++;
1007     //sleep(1);
1008
1009     /* Test acceptance pair and acceptance cycle*/
1010
1011     if(pair->automaton_state->type == 1){
1012       if(search_cycle == 0){
1013         set_pair_prop_col_reached(pair);
1014         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair->graph_state, pair->automaton_state, pair->automaton_state->id);
1015       }else{
1016         if(reached_prop_col(pair) == 1){
1017           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1018           XBT_INFO("|             ACCEPTANCE CYCLE            |");
1019           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1020           XBT_INFO("Counter-example that violates formula :");
1021           MC_show_snapshot_stack(mc_snapshot_stack);
1022           MC_dump_snapshot_stack(mc_snapshot_stack);
1023           MC_print_statistics_pairs(mc_stats_pair);
1024           exit(0);
1025         }
1026       }
1027     }
1028
1029     /* If there are processes to interleave and the maximum depth has not been reached
1030        then perform one step of the exploration algorithm */
1031     if (xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH &&
1032         (req = MC_state_get_request(pair->graph_state, &value))) {
1033
1034       set_pair_prop_col_visited(pair, search_cycle);
1035
1036       /* Debug information */
1037       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
1038         req_str = MC_request_to_string(req, value);
1039         XBT_DEBUG("Execute: %s", req_str);
1040         xbt_free(req_str);
1041       }
1042
1043       MC_state_set_executed_request(pair->graph_state, req, value);
1044
1045       /* Answer the request */
1046       SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
1047
1048       /* Wait for requests (schedules processes) */
1049       MC_wait_for_requests();
1050
1051       /* Create the new expanded state */
1052       MC_SET_RAW_MEM;
1053
1054       pair->interleave++;
1055
1056       next_graph_state = MC_state_new();
1057
1058       next_system_state = xbt_new0(s_mc_snapshot_t, 1);
1059       MC_take_snapshot(next_system_state);
1060       MC_UNSET_RAW_MEM;
1061
1062       cursor = 0;
1063       xbt_dynar_foreach(pair->automaton_state->out, cursor, transition_succ){
1064         res = MC_automaton_evaluate_label(a, transition_succ->label);
1065         if((res == 1) || (res == 2)){ // enabled transition in automaton
1066           next_automaton_state = transition_succ->dst;
1067           break;
1068         }
1069       }
1070
1071       if(next_automaton_state == NULL)
1072         next_automaton_state = pair->automaton_state;
1073
1074       MC_SET_RAW_MEM;
1075
1076       next_pair = new_pair_prop_col(next_system_state, next_graph_state, next_automaton_state);
1077       cursor = 0;
1078       xbt_propositional_symbol_t ps;
1079       xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
1080         int (*f)() = ps->function;
1081         int val = (*f)();
1082         mc_prop_ato_t pa = new_proposition(ps->pred, val);
1083         xbt_dynar_push(next_pair->propositions, &pa);
1084       }
1085       xbt_fifo_unshift(mc_snapshot_stack, next_pair);
1086
1087       cursor = 0;
1088       if((invisible_col(pair, next_pair) == 0) && (pair->fully_expanded == 0)){
1089         set_fully_expanded_col(pair);
1090         if(xbt_dynar_length(enabled_processes) > 1){ // Si 1 seul process activé, déjà exécuté juste avant donc état complètement étudié
1091           xbt_dynar_foreach(enabled_processes, cursor, process){
1092             MC_state_interleave_process(pair->graph_state, process);
1093           }
1094         }
1095         XBT_DEBUG("Pair %p fully expanded (%u interleave)", pair, MC_state_interleave_size(pair->graph_state));
1096       }
1097
1098       MC_UNSET_RAW_MEM;
1099
1100
1101       /* Let's loop again */
1102
1103       /* The interleave set is empty or the maximum depth is reached, let's back-track */
1104     } else {
1105       XBT_DEBUG("There are no more processes to interleave.");
1106
1107       /* Trash the current state, no longer needed */
1108       MC_SET_RAW_MEM;
1109       xbt_fifo_shift(mc_snapshot_stack);
1110       //MC_state_delete(state);
1111       MC_UNSET_RAW_MEM;
1112
1113       /* Check for deadlocks */
1114       if(MC_deadlock_check()){
1115         MC_show_deadlock(NULL);
1116         return;
1117       }
1118
1119       MC_SET_RAW_MEM;
1120       /* Traverse the stack backwards until a state with a non empty interleave
1121          set is found, deleting all the states that have it empty in the way.
1122          For each deleted state, check if the request that has generated it
1123          (from it's predecesor state), depends on any other previous request
1124          executed before it. If it does then add it to the interleave set of the
1125          state that executed that previous request. */
1126       while ((pair = xbt_fifo_shift(mc_snapshot_stack)) != NULL) {
1127         req = MC_state_get_internal_request(pair->graph_state);
1128         xbt_fifo_foreach(mc_snapshot_stack, item, prev_pair, mc_pair_prop_col_t) {
1129           if(MC_request_depend(req, MC_state_get_internal_request(prev_pair->graph_state))){
1130             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
1131               XBT_DEBUG("Dependent Transitions:");
1132               prev_req = MC_state_get_executed_request(prev_pair->graph_state, &value);
1133               req_str = MC_request_to_string(prev_req, value);
1134               XBT_DEBUG("%s (pair=%p)", req_str, prev_pair);
1135               xbt_free(req_str);
1136               prev_req = MC_state_get_executed_request(pair->graph_state, &value);
1137               req_str = MC_request_to_string(prev_req, value);
1138               XBT_DEBUG("%s (pair=%p)", req_str, pair);
1139               xbt_free(req_str);
1140             }
1141
1142             if(prev_pair->fully_expanded == 0){
1143               if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer)){
1144                 MC_state_interleave_process(prev_pair->graph_state, req->issuer);
1145                 XBT_DEBUG("Process %p (%lu) interleaved in pair %p", req->issuer, req->issuer->pid, prev_pair);
1146               }else{
1147                 XBT_DEBUG("Process %p (%lu) is in done set", req->issuer, req->issuer->pid);
1148               }
1149             }
1150
1151             break;
1152           }
1153         }
1154
1155
1156         if (MC_state_interleave_size(pair->graph_state) > 0) {
1157           /* We found a back-tracking point, let's loop */
1158           MC_restore_snapshot(pair->system_state);
1159           xbt_fifo_unshift(mc_snapshot_stack, pair);
1160           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));
1161           MC_UNSET_RAW_MEM;
1162           break;
1163         } else {
1164           //MC_state_delete(state);
1165         }
1166       }
1167       MC_UNSET_RAW_MEM;
1168     }
1169   }
1170   MC_UNSET_RAW_MEM;
1171   return;
1172 }