src/mc/mc_liveness.c

   1 /* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "mc_private.h"
   7 #include <unistd.h>
   8 #include <sys/wait.h>
   9
  10 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
  11                                 "Logging specific to algorithms for liveness properties verification");
  12
  13 xbt_dynar_t reached_pairs;
  14 xbt_dynar_t reached_pairs_hash;
  15 xbt_dynar_t visited_pairs;
  16 xbt_dynar_t visited_pairs_hash;
  17 xbt_dynar_t successors;
  18
  19 xbt_dynar_t hosts_table;
  20
  21
  22 /* fast implementation of djb2 algorithm */
  23 unsigned int hash_region(char *str, int str_len){
  24
  25   int c;
  26   register unsigned int hash = 5381;
  27
  28   while (str_len--) {
  29     c = *str++;
  30     hash = ((hash << 5) + hash) + c;    /* hash * 33 + c */
  31   }
  32
  33   return hash;
  34
  35 }
  36
  37 int create_dump(int pair)
  38 {
  39    // Try to enable core dumps
  40   struct rlimit core_limit;
  41   core_limit.rlim_cur = RLIM_INFINITY;
  42   core_limit.rlim_max = RLIM_INFINITY;
  43
  44   if(setrlimit(RLIMIT_CORE, &core_limit) < 0)
  45     fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno));
  46
  47   int status;
  48   switch(fork()){
  49   case 0:
  50     // We are the child process -- run the actual program
  51     abort();
  52     break;
  53
  54   case -1:
  55     // An error occurred, shouldn't happen
  56     perror("fork");
  57     return -1;
  58
  59   default:
  60     // We are the parent process -- wait for the child process to exit
  61     if(wait(&status) < 0)
  62       perror("wait");
  63     if(WIFSIGNALED(status) && WCOREDUMP(status)){
  64       char *core_name = malloc(20);
  65       sprintf(core_name,"core_%d", pair);
  66       rename("core", core_name);
  67       free(core_name);
  68     }
  69   }
  70
  71   return 0;
  72 }
  73
  74 int reached(xbt_state_t st){
  75
  76   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  77
  78   MC_SET_RAW_MEM;
  79
  80   mc_pair_reached_t new_pair = NULL;
  81   new_pair = xbt_new0(s_mc_pair_reached_t, 1);
  82   new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
  83   new_pair->automaton_state = st;
  84   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
  85   new_pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
  86   MC_take_snapshot_liveness(new_pair->system_state);
  87
  88   /* Get values of propositional symbols */
  89   int res;
  90   int_f_void_t f;
  91   unsigned int cursor = 0;
  92   xbt_propositional_symbol_t ps = NULL;
  93   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
  94     f = (int_f_void_t)ps->function;
  95     res = (*f)();
  96     xbt_dynar_push_as(new_pair->prop_ato, int, res);
  97   }
  98
  99   MC_UNSET_RAW_MEM;
 100
 101   if(xbt_dynar_is_empty(reached_pairs) || !compare){
 102
 103     MC_SET_RAW_MEM;
 104     /* New pair reached */
 105     xbt_dynar_push(reached_pairs, &new_pair);
 106     MC_UNSET_RAW_MEM;
 107
 108
 109     return 0;
 110
 111   }else{
 112
 113     MC_SET_RAW_MEM;
 114
 115     cursor = 0;
 116     mc_pair_reached_t pair_test = NULL;
 117
 118     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
 119       XBT_INFO("Pair reached #%d", pair_test->nb);
 120       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 121         if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
 122           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
 123
 124             if(raw_mem_set)
 125               MC_SET_RAW_MEM;
 126             else
 127               MC_UNSET_RAW_MEM;
 128
 129             return 1;
 130           }
 131         }else{
 132           XBT_INFO("Different values of propositional symbols");
 133         }
 134       }else{
 135         XBT_INFO("Different automaton state");
 136       }
 137     }
 138
 139     //create_dump(xbt_dynar_length(reached_pairs));
 140
 141     /* New pair reached */
 142     xbt_dynar_push(reached_pairs, &new_pair);
 143
 144     MC_UNSET_RAW_MEM;
 145
 146     if(raw_mem_set)
 147       MC_SET_RAW_MEM;
 148     else
 149       MC_UNSET_RAW_MEM;
 150
 151     compare = 0;
 152
 153     return 0;
 154
 155   }
 156 }
 157
 158
 159 void set_pair_reached(xbt_state_t st){
 160
 161   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 162
 163   MC_SET_RAW_MEM;
 164
 165   mc_pair_reached_t pair = NULL;
 166   pair = xbt_new0(s_mc_pair_reached_t, 1);
 167   pair->nb = xbt_dynar_length(reached_pairs) + 1;
 168   pair->automaton_state = st;
 169   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 170   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 171   MC_take_snapshot_liveness(pair->system_state);
 172
 173   /* Get values of propositional symbols */
 174   unsigned int cursor = 0;
 175   xbt_propositional_symbol_t ps = NULL;
 176   int res;
 177   int_f_void_t f;
 178
 179   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 180     f = (int_f_void_t)ps->function;
 181     res = (*f)();
 182     xbt_dynar_push_as(pair->prop_ato, int, res);
 183   }
 184
 185   xbt_dynar_push(reached_pairs, &pair);
 186
 187   MC_UNSET_RAW_MEM;
 188
 189   if(raw_mem_set)
 190     MC_SET_RAW_MEM;
 191   else
 192     MC_UNSET_RAW_MEM;
 193
 194 }
 195
 196
 197 int reached_hash(xbt_state_t st){
 198
 199   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 200
 201   if(xbt_dynar_is_empty(reached_pairs_hash)){
 202
 203     return 0;
 204
 205   }else{
 206
 207     MC_SET_RAW_MEM;
 208
 209     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 210     MC_take_snapshot_liveness(sn);
 211
 212     int j;
 213     unsigned int hash_regions[sn->num_reg];
 214     for(j=0; j<sn->num_reg; j++){
 215       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
 216     }
 217
 218
 219     /* Get values of propositional symbols */
 220     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 221     unsigned int cursor = 0;
 222     xbt_propositional_symbol_t ps = NULL;
 223     int res;
 224     int_f_void_t f;
 225
 226     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 227       f = (int_f_void_t)ps->function;
 228       res = (*f)();
 229       xbt_dynar_push_as(prop_ato, int, res);
 230     }
 231
 232     mc_pair_reached_hash_t pair_test = NULL;
 233
 234     int region_diff = 0;
 235
 236     cursor = 0;
 237
 238     xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
 239
 240       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 241         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 242           for(j=0 ; j< sn->num_reg ; j++){
 243             if(hash_regions[j] != pair_test->hash_regions[j]){
 244               region_diff++;
 245             }
 246           }
 247           if(region_diff == 0){
 248             MC_free_snapshot(sn);
 249             xbt_dynar_reset(prop_ato);
 250             xbt_free(prop_ato);
 251             MC_UNSET_RAW_MEM;
 252
 253             if(raw_mem_set)
 254               MC_SET_RAW_MEM;
 255             else
 256               MC_UNSET_RAW_MEM;
 257
 258             return 1;
 259           }else{
 260             XBT_INFO("Different snapshot");
 261           }
 262         }else{
 263           XBT_INFO("Different values of propositional symbols");
 264         }
 265       }else{
 266         XBT_INFO("Different automaton state");
 267       }
 268
 269       region_diff = 0;
 270     }
 271
 272     MC_free_snapshot(sn);
 273     xbt_dynar_reset(prop_ato);
 274     xbt_free(prop_ato);
 275     MC_UNSET_RAW_MEM;
 276
 277     if(raw_mem_set)
 278       MC_SET_RAW_MEM;
 279     else
 280       MC_UNSET_RAW_MEM;
 281
 282     return 0;
 283
 284   }
 285 }
 286
 287 void set_pair_reached_hash(xbt_state_t st){
 288
 289   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 290
 291   MC_SET_RAW_MEM;
 292
 293   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 294   MC_take_snapshot_liveness(sn);
 295
 296   mc_pair_reached_hash_t pair = NULL;
 297   pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
 298   pair->automaton_state = st;
 299   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 300   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
 301
 302   int i;
 303
 304   for(i=0 ; i< sn->num_reg ; i++){
 305     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
 306   }
 307
 308   /* Get values of propositional symbols */
 309   unsigned int cursor = 0;
 310   xbt_propositional_symbol_t ps = NULL;
 311   int res;
 312   int_f_void_t f;
 313
 314   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 315     f = (int_f_void_t)ps->function;
 316     res = (*f)();
 317     xbt_dynar_push_as(pair->prop_ato, int, res);
 318   }
 319
 320   xbt_dynar_push(reached_pairs_hash, &pair);
 321
 322   MC_free_snapshot(sn);
 323
 324   MC_UNSET_RAW_MEM;
 325
 326   if(raw_mem_set)
 327     MC_SET_RAW_MEM;
 328   else
 329     MC_UNSET_RAW_MEM;
 330
 331 }
 332
 333
 334 int visited(xbt_state_t st, int sc){
 335
 336   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 337
 338   if(xbt_dynar_is_empty(visited_pairs)){
 339
 340     return 0;
 341
 342   }else{
 343
 344     MC_SET_RAW_MEM;
 345
 346     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 347     MC_take_snapshot_liveness(sn);
 348
 349     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 350
 351     /* Get values of propositional symbols */
 352     unsigned int cursor = 0;
 353     xbt_propositional_symbol_t ps = NULL;
 354     int res;
 355     int_f_void_t f;
 356
 357     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 358       f = (int_f_void_t)ps->function;
 359       res = (*f)();
 360       xbt_dynar_push_as(prop_ato, int, res);
 361     }
 362
 363     cursor = 0;
 364     mc_pair_visited_t pair_test = NULL;
 365
 366     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
 367       if(pair_test->search_cycle == sc) {
 368         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 369           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 370             if(snapshot_compare(pair_test->system_state, sn) == 0){
 371
 372               MC_free_snapshot(sn);
 373               xbt_dynar_reset(prop_ato);
 374               xbt_free(prop_ato);
 375               MC_UNSET_RAW_MEM;
 376
 377               if(raw_mem_set)
 378                 MC_SET_RAW_MEM;
 379               else
 380                 MC_UNSET_RAW_MEM;
 381
 382               return 1;
 383
 384             }else{
 385               XBT_INFO("Different snapshot");
 386             }
 387           }else{
 388             XBT_INFO("Different values of propositional symbols");
 389           }
 390         }else{
 391           XBT_INFO("Different automaton state");
 392         }
 393       }else{
 394         XBT_INFO("Different value of search_cycle");
 395       }
 396     }
 397
 398
 399     MC_free_snapshot(sn);
 400     xbt_dynar_reset(prop_ato);
 401     xbt_free(prop_ato);
 402     MC_UNSET_RAW_MEM;
 403
 404     if(raw_mem_set)
 405       MC_SET_RAW_MEM;
 406     else
 407       MC_UNSET_RAW_MEM;
 408
 409     return 0;
 410
 411   }
 412 }
 413
 414
 415 int visited_hash(xbt_state_t st, int sc){
 416
 417   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 418
 419   if(xbt_dynar_is_empty(visited_pairs_hash)){
 420
 421     return 0;
 422
 423   }else{
 424
 425     MC_SET_RAW_MEM;
 426
 427     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 428     MC_take_snapshot_liveness(sn);
 429
 430     int j;
 431     unsigned int hash_regions[sn->num_reg];
 432     for(j=0; j<sn->num_reg; j++){
 433       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
 434     }
 435
 436
 437     /* Get values of propositional symbols */
 438     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 439     unsigned int cursor = 0;
 440     xbt_propositional_symbol_t ps = NULL;
 441     int res;
 442     int_f_void_t f;
 443
 444     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 445       f = (int_f_void_t)ps->function;
 446       res = (*f)();
 447       xbt_dynar_push_as(prop_ato, int, res);
 448     }
 449
 450     mc_pair_visited_hash_t pair_test = NULL;
 451
 452     int region_diff = 0;
 453     cursor = 0;
 454
 455     xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
 456
 457       if(pair_test->search_cycle == sc) {
 458         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 459           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 460             for(j=0 ; j< sn->num_reg ; j++){
 461               if(hash_regions[j] != pair_test->hash_regions[j]){
 462                 region_diff++;
 463               }
 464             }
 465             if(region_diff == 0){
 466               MC_free_snapshot(sn);
 467               xbt_dynar_reset(prop_ato);
 468               xbt_free(prop_ato);
 469               MC_UNSET_RAW_MEM;
 470
 471               if(raw_mem_set)
 472                 MC_SET_RAW_MEM;
 473               else
 474                 MC_UNSET_RAW_MEM;
 475
 476               return 1;
 477             }else{
 478               //XBT_INFO("Different snapshot");
 479             }
 480           }else{
 481             //XBT_INFO("Different values of propositional symbols");
 482           }
 483         }else{
 484           //XBT_INFO("Different automaton state");
 485         }
 486       }else{
 487         //XBT_INFO("Different value of search_cycle");
 488       }
 489
 490       region_diff = 0;
 491     }
 492
 493     MC_free_snapshot(sn);
 494     xbt_dynar_reset(prop_ato);
 495     xbt_free(prop_ato);
 496     MC_UNSET_RAW_MEM;
 497
 498     if(raw_mem_set)
 499       MC_SET_RAW_MEM;
 500     else
 501       MC_UNSET_RAW_MEM;
 502
 503     return 0;
 504
 505   }
 506 }
 507
 508 void set_pair_visited_hash(xbt_state_t st, int sc){
 509
 510   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 511
 512   MC_SET_RAW_MEM;
 513
 514   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 515   MC_take_snapshot_liveness(sn);
 516
 517   mc_pair_visited_hash_t pair = NULL;
 518   pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
 519   pair->automaton_state = st;
 520   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 521   pair->search_cycle = sc;
 522   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
 523
 524   int i;
 525
 526   for(i=0 ; i< sn->num_reg ; i++){
 527     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
 528   }
 529
 530   /* Get values of propositional symbols */
 531   unsigned int cursor = 0;
 532   xbt_propositional_symbol_t ps = NULL;
 533   int res;
 534   int_f_void_t f;
 535
 536   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 537     f = (int_f_void_t)ps->function;
 538     res = (*f)();
 539     xbt_dynar_push_as(pair->prop_ato, int, res);
 540   }
 541
 542   xbt_dynar_push(visited_pairs_hash, &pair);
 543
 544   MC_free_snapshot(sn);
 545
 546   MC_UNSET_RAW_MEM;
 547
 548   if(raw_mem_set)
 549     MC_SET_RAW_MEM;
 550   else
 551     MC_UNSET_RAW_MEM;
 552
 553 }
 554
 555 void set_pair_visited(xbt_state_t st, int sc){
 556
 557   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 558
 559   MC_SET_RAW_MEM;
 560
 561   mc_pair_visited_t pair = NULL;
 562   pair = xbt_new0(s_mc_pair_visited_t, 1);
 563   pair->automaton_state = st;
 564   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 565   pair->search_cycle = sc;
 566   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 567   MC_take_snapshot_liveness(pair->system_state);
 568
 569
 570   /* Get values of propositional symbols */
 571   unsigned int cursor = 0;
 572   xbt_propositional_symbol_t ps = NULL;
 573   int res;
 574   int_f_void_t f;
 575
 576   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 577     f = (int_f_void_t)ps->function;
 578     res = (*f)();
 579     xbt_dynar_push_as(pair->prop_ato, int, res);
 580   }
 581
 582   xbt_dynar_push(visited_pairs, &pair);
 583
 584   MC_UNSET_RAW_MEM;
 585
 586   if(raw_mem_set)
 587     MC_SET_RAW_MEM;
 588   else
 589     MC_UNSET_RAW_MEM;
 590
 591 }
 592
 593 void MC_pair_delete(mc_pair_t pair){
 594   xbt_free(pair->graph_state->proc_status);
 595   xbt_free(pair->graph_state);
 596   xbt_free(pair);
 597 }
 598
 599
 600
 601 int MC_automaton_evaluate_label(xbt_exp_label_t l){
 602
 603   switch(l->type){
 604   case 0 : {
 605     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 606     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 607     return (left_res || right_res);
 608   }
 609   case 1 : {
 610     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 611     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 612     return (left_res && right_res);
 613   }
 614   case 2 : {
 615     int res = MC_automaton_evaluate_label(l->u.exp_not);
 616     return (!res);
 617   }
 618   case 3 : {
 619     unsigned int cursor = 0;
 620     xbt_propositional_symbol_t p = NULL;
 621     int_f_void_t f;
 622     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
 623       if(strcmp(p->pred, l->u.predicat) == 0){
 624         f = (int_f_void_t)p->function;
 625         return (*f)();
 626       }
 627     }
 628     return -1;
 629   }
 630   case 4 : {
 631     return 2;
 632   }
 633   default :
 634     return -1;
 635   }
 636 }
 637
 638
 639 /********************* Double-DFS stateless *******************/
 640
 641 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 642   xbt_free(pair->graph_state->proc_status);
 643   xbt_free(pair->graph_state);
 644   xbt_free(pair);
 645 }
 646
 647 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 648   mc_pair_stateless_t p = NULL;
 649   p = xbt_new0(s_mc_pair_stateless_t, 1);
 650   p->automaton_state = st;
 651   p->graph_state = sg;
 652   p->requests = r;
 653   mc_stats_pair->expanded_pairs++;
 654   return p;
 655 }
 656
 657 void MC_ddfs_init(void){
 658
 659   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 660
 661   XBT_INFO("**************************************************");
 662   XBT_INFO("Double-DFS init");
 663   XBT_INFO("**************************************************");
 664
 665   mc_pair_stateless_t mc_initial_pair = NULL;
 666   mc_state_t initial_graph_state = NULL;
 667   smx_process_t process;
 668
 669
 670   MC_wait_for_requests();
 671
 672   MC_SET_RAW_MEM;
 673
 674   initial_graph_state = MC_state_pair_new();
 675   xbt_swag_foreach(process, simix_global->process_list){
 676     if(MC_process_is_enabled(process)){
 677       MC_state_interleave_process(initial_graph_state, process);
 678     }
 679   }
 680
 681   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
 682   //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
 683   //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
 684   //visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
 685   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 686
 687   /* Save the initial state */
 688   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
 689   MC_take_snapshot_liveness(initial_snapshot_liveness);
 690
 691   MC_UNSET_RAW_MEM;
 692
 693   unsigned int cursor = 0;
 694   xbt_state_t state;
 695
 696   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
 697     if(state->type == -1){
 698
 699       MC_SET_RAW_MEM;
 700       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 701       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 702       MC_UNSET_RAW_MEM;
 703
 704       if(cursor != 0){
 705         MC_restore_snapshot(initial_snapshot_liveness);
 706         MC_UNSET_RAW_MEM;
 707       }
 708
 709       MC_ddfs(0);
 710
 711     }else{
 712       if(state->type == 2){
 713
 714         MC_SET_RAW_MEM;
 715         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 716         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 717         MC_UNSET_RAW_MEM;
 718
 719         set_pair_reached(state);
 720         //set_pair_reached_hash(state);
 721
 722         if(cursor != 0){
 723           MC_restore_snapshot(initial_snapshot_liveness);
 724           MC_UNSET_RAW_MEM;
 725         }
 726
 727         MC_ddfs(1);
 728
 729       }
 730     }
 731   }
 732
 733   if(raw_mem_set)
 734     MC_SET_RAW_MEM;
 735   else
 736     MC_UNSET_RAW_MEM;
 737
 738
 739 }
 740
 741
 742 void MC_ddfs(int search_cycle){
 743
 744   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 745
 746   smx_process_t process;
 747   mc_pair_stateless_t current_pair = NULL;
 748
 749   if(xbt_fifo_size(mc_stack_liveness) == 0)
 750     return;
 751
 752
 753   /* Get current pair */
 754   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 755
 756   /* Update current state in buchi automaton */
 757   _mc_property_automaton->current_state = current_pair->automaton_state;
 758
 759
 760   XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
 761
 762   mc_stats_pair->visited_pairs++;
 763
 764   //sleep(1);
 765
 766   int value;
 767   mc_state_t next_graph_state = NULL;
 768   smx_simcall_t req = NULL;
 769   char *req_str;
 770
 771   xbt_transition_t transition_succ;
 772   unsigned int cursor = 0;
 773   int res;
 774
 775   mc_pair_stateless_t next_pair = NULL;
 776   mc_pair_stateless_t pair_succ;
 777
 778   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
 779
 780     //set_pair_visited(current_pair->automaton_state, search_cycle);
 781     //set_pair_visited_hash(current_pair->automaton_state, search_cycle);
 782
 783     //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
 784     //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
 785
 786     if(current_pair->requests > 0){
 787
 788       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 789
 790         /* Debug information */
 791
 792         req_str = MC_request_to_string(req, value);
 793         XBT_INFO("Execute: %s", req_str);
 794         xbt_free(req_str);
 795
 796         MC_state_set_executed_request(current_pair->graph_state, req, value);
 797
 798         /* Answer the request */
 799         SIMIX_simcall_pre(req, value);
 800
 801         /* Wait for requests (schedules processes) */
 802         MC_wait_for_requests();
 803
 804
 805         MC_SET_RAW_MEM;
 806
 807         /* Create the new expanded graph_state */
 808         next_graph_state = MC_state_pair_new();
 809
 810         /* Get enabled process and insert it in the interleave set of the next graph_state */
 811         xbt_swag_foreach(process, simix_global->process_list){
 812           if(MC_process_is_enabled(process)){
 813             MC_state_interleave_process(next_graph_state, process);
 814           }
 815         }
 816
 817         xbt_dynar_reset(successors);
 818
 819         MC_UNSET_RAW_MEM;
 820
 821
 822         cursor= 0;
 823         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 824
 825           res = MC_automaton_evaluate_label(transition_succ->label);
 826
 827           if(res == 1){ // enabled transition in automaton
 828             MC_SET_RAW_MEM;
 829             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 830             xbt_dynar_push(successors, &next_pair);
 831             MC_UNSET_RAW_MEM;
 832           }
 833
 834         }
 835
 836         cursor = 0;
 837
 838         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 839
 840           res = MC_automaton_evaluate_label(transition_succ->label);
 841
 842           if(res == 2){ // true transition in automaton
 843             MC_SET_RAW_MEM;
 844             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 845             xbt_dynar_push(successors, &next_pair);
 846             MC_UNSET_RAW_MEM;
 847           }
 848
 849         }
 850
 851         cursor = 0;
 852
 853         xbt_dynar_foreach(successors, cursor, pair_succ){
 854
 855           if(search_cycle == 1){
 856
 857             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 858
 859               if(reached(pair_succ->automaton_state)){
 860                 //if(reached_hash(pair_succ->automaton_state)){
 861
 862                 XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
 863
 864                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 865                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 866                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 867                 XBT_INFO("Counter-example that violates formula :");
 868                 MC_show_stack_liveness(mc_stack_liveness);
 869                 MC_dump_stack_liveness(mc_stack_liveness);
 870                 MC_print_statistics_pairs(mc_stats_pair);
 871                 exit(0);
 872
 873               }else{
 874
 875                 XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 876
 877                 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 878                 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 879
 880                 MC_SET_RAW_MEM;
 881                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 882                 MC_UNSET_RAW_MEM;
 883
 884                 MC_ddfs(search_cycle);
 885
 886               }
 887
 888             }else{
 889
 890               //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
 891                 //if(!visited(pair_succ->automaton_state, search_cycle)){
 892
 893                 MC_SET_RAW_MEM;
 894                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 895                 MC_UNSET_RAW_MEM;
 896
 897                 MC_ddfs(search_cycle);
 898
 899                 /*}else{
 900
 901                 XBT_INFO("Next pair already visited ! ");
 902
 903                 }*/
 904
 905             }
 906
 907           }else{
 908
 909             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 910
 911               XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 912
 913               set_pair_reached(pair_succ->automaton_state);
 914               //set_pair_reached_hash(pair_succ->automaton_state);
 915
 916               search_cycle = 1;
 917
 918               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 919               //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 920
 921             }
 922
 923             //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
 924               //if(!visited(pair_succ->automaton_state, search_cycle)){
 925
 926               MC_SET_RAW_MEM;
 927               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 928               MC_UNSET_RAW_MEM;
 929
 930               MC_ddfs(search_cycle);
 931
 932               /*}else{
 933
 934               XBT_INFO("Next pair already visited ! ");
 935
 936               }*/
 937
 938           }
 939
 940
 941           /* Restore system before checking others successors */
 942           if(cursor != (xbt_dynar_length(successors) - 1))
 943             MC_replay_liveness(mc_stack_liveness, 1);
 944
 945
 946         }
 947
 948         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 949           XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 950           MC_replay_liveness(mc_stack_liveness, 0);
 951         }
 952       }
 953
 954
 955     }else{  /*No request to execute, search evolution in Büchi automaton */
 956
 957       MC_SET_RAW_MEM;
 958
 959       /* Create the new expanded graph_state */
 960       next_graph_state = MC_state_pair_new();
 961
 962       xbt_dynar_reset(successors);
 963
 964       MC_UNSET_RAW_MEM;
 965
 966
 967       cursor= 0;
 968       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 969
 970         res = MC_automaton_evaluate_label(transition_succ->label);
 971
 972         if(res == 1){ // enabled transition in automaton
 973           MC_SET_RAW_MEM;
 974           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 975           xbt_dynar_push(successors, &next_pair);
 976           MC_UNSET_RAW_MEM;
 977         }
 978
 979       }
 980
 981       cursor = 0;
 982
 983       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 984
 985         res = MC_automaton_evaluate_label(transition_succ->label);
 986
 987         if(res == 2){ // true transition in automaton
 988           MC_SET_RAW_MEM;
 989           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 990           xbt_dynar_push(successors, &next_pair);
 991           MC_UNSET_RAW_MEM;
 992         }
 993
 994       }
 995
 996       cursor = 0;
 997
 998       xbt_dynar_foreach(successors, cursor, pair_succ){
 999
1000         if(search_cycle == 1){
1001
1002           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
1003
1004             if(reached(pair_succ->automaton_state)){
1005               //if(reached_hash(pair_succ->automaton_state)){
1006
1007               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
1008
1009               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1010               XBT_INFO("|             ACCEPTANCE CYCLE            |");
1011               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1012               XBT_INFO("Counter-example that violates formula :");
1013               MC_show_stack_liveness(mc_stack_liveness);
1014               MC_dump_stack_liveness(mc_stack_liveness);
1015               MC_print_statistics_pairs(mc_stats_pair);
1016               exit(0);
1017
1018             }else{
1019
1020               XBT_INFO("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1021
1022               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1023               //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1024
1025               MC_SET_RAW_MEM;
1026               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1027               MC_UNSET_RAW_MEM;
1028
1029               MC_ddfs(search_cycle);
1030
1031             }
1032
1033           }else{
1034
1035             //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1036               //if(!visited(pair_succ->automaton_state, search_cycle)){
1037
1038               MC_SET_RAW_MEM;
1039               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1040               MC_UNSET_RAW_MEM;
1041
1042               MC_ddfs(search_cycle);
1043
1044               /*}else{
1045
1046               XBT_INFO("Next pair already visited ! ");
1047
1048               }*/
1049           }
1050
1051
1052         }else{
1053
1054           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1055
1056             set_pair_reached(pair_succ->automaton_state);
1057             //set_pair_reached_hash(pair_succ->automaton_state);
1058
1059             search_cycle = 1;
1060
1061             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1062             //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1063
1064           }
1065
1066           //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1067             //if(!visited(pair_succ->automaton_state, search_cycle)){
1068
1069             MC_SET_RAW_MEM;
1070             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1071             MC_UNSET_RAW_MEM;
1072
1073             MC_ddfs(search_cycle);
1074
1075             /*}else{
1076
1077             XBT_INFO("Next pair already visited ! ");
1078
1079             }*/
1080
1081         }
1082
1083         /* Restore system before checking others successors */
1084         if(cursor != xbt_dynar_length(successors) - 1)
1085           MC_replay_liveness(mc_stack_liveness, 1);
1086
1087
1088       }
1089
1090     }
1091
1092   }else{
1093
1094     XBT_INFO("Max depth reached");
1095
1096   }
1097
1098   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1099     XBT_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1100   }else{
1101     XBT_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1102   }
1103
1104
1105   MC_SET_RAW_MEM;
1106   xbt_fifo_shift(mc_stack_liveness);
1107   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1108     xbt_dynar_pop(reached_pairs, NULL);
1109     //xbt_dynar_pop(reached_pairs_hash, NULL);
1110   }
1111   MC_UNSET_RAW_MEM;
1112
1113   if(raw_mem_set)
1114     MC_SET_RAW_MEM;
1115   else
1116     MC_UNSET_RAW_MEM;
1117
1118 }