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
   9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
  10                                 "Logging specific to algorithms for liveness properties verification");
  11
  12 xbt_dynar_t reached_pairs;
  13 xbt_dynar_t reached_pairs_hash;
  14 xbt_dynar_t visited_pairs;
  15 xbt_dynar_t visited_pairs_hash;
  16 xbt_dynar_t successors;
  17
  18 xbt_dynar_t hosts_table;
  19
  20
  21 /* fast implementation of djb2 algorithm */
  22 unsigned int hash_region(char *str, int str_len){
  23
  24   int c;
  25   register unsigned int hash = 5381;
  26
  27   while (str_len--) {
  28     c = *str++;
  29     hash = ((hash << 5) + hash) + c;    /* hash * 33 + c */
  30   }
  31
  32   return hash;
  33
  34 }
  35
  36 int data_program_region_compare(void *d1, void *d2, size_t size){
  37   int distance = 0;
  38   int i;
  39
  40   for(i=0; i<size; i++){
  41     if(memcmp(((char *)d1) + i, ((char *)d2) + i, 1) != 0){
  42       fprintf(stderr,"Different byte (offset=%d) (%p - %p) in data program region\n", i, (char *)d1 + i, (char *)d2 + i);
  43       distance++;
  44     }
  45   }
  46
  47   fprintf(stderr, "Hamming distance between data program regions : %d\n", distance);
  48
  49   return distance;
  50 }
  51
  52 int data_libsimgrid_region_compare(void *d1, void *d2, size_t size){
  53   int distance = 0;
  54   int i;
  55
  56   for(i=0; i<size; i++){
  57     if(memcmp(((char *)d1) + i, ((char *)d2) + i, 1) != 0){
  58       fprintf(stderr, "Different byte (offset=%d) (%p - %p) in data libsimgrid region\n", i, (char *)d1 + i, (char *)d2 + i);
  59       distance++;
  60     }
  61   }
  62
  63   fprintf(stderr, "Hamming distance between data libsimgrid regions : %d\n", distance);
  64
  65   return distance;
  66 }
  67
  68 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
  69
  70
  71   if(s1->num_reg != s2->num_reg){
  72     XBT_INFO("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg);
  73     return 1;
  74   }
  75
  76   int i;
  77   int errors = 0;
  78
  79   for(i=0 ; i< s1->num_reg ; i++){
  80
  81     if(s1->regions[i]->type != s2->regions[i]->type){
  82       XBT_INFO("Different type of region");
  83       errors++;
  84     }
  85
  86     switch(s1->regions[i]->type){
  87     case 0:
  88       if(s1->regions[i]->size != s2->regions[i]->size){
  89         XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
  90         errors++;
  91       }
  92       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
  93         XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
  94         errors++;
  95       }
  96       if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){
  97         XBT_INFO("Different heap (mmalloc_compare)");
  98         errors++;
  99       }
 100       break;
 101     case 1 :
 102       if(s1->regions[i]->size != s2->regions[i]->size){
 103         XBT_INFO("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
 104         errors++;
 105       }
 106       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
 107         XBT_INFO("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
 108         errors++;
 109       }
 110       if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
 111         XBT_INFO("Different memcmp for data in libsimgrid");
 112         errors++;
 113       }
 114       break;
 115     case 2 :
 116       if(s1->regions[i]->size != s2->regions[i]->size){
 117         XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
 118         errors++;
 119       }
 120       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
 121         XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
 122         errors++;
 123       }
 124       if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
 125         XBT_INFO("Different memcmp for data in program");
 126         errors++;
 127       }
 128       break;
 129     default:
 130       break;
 131     }
 132   }
 133
 134   return (errors > 0);
 135
 136 }
 137
 138 int reached(xbt_state_t st){
 139
 140   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 141
 142
 143   if(xbt_dynar_is_empty(reached_pairs)){
 144
 145     return 0;
 146
 147   }else{
 148
 149     MC_SET_RAW_MEM;
 150
 151     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 152     MC_take_snapshot_liveness(sn);
 153
 154     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 155     int res;
 156     int_f_void_t f;
 157
 158     /* Get values of propositional symbols */
 159     unsigned int cursor = 0;
 160     xbt_propositional_symbol_t ps = NULL;
 161     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 162       f = (int_f_void_t)ps->function;
 163       res = (*f)();
 164       xbt_dynar_push_as(prop_ato, int, res);
 165     }
 166
 167     cursor = 0;
 168     mc_pair_reached_t pair_test = NULL;
 169
 170     //xbt_dict_t current_rdv_points = SIMIX_get_rdv_points();
 171
 172     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
 173       XBT_INFO("Pair reached #%d", pair_test->nb);
 174       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 175         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 176           //XBT_INFO("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points));
 177           //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){
 178           //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){
 179           if(snapshot_compare(pair_test->system_state, sn) == 0){
 180
 181             MC_free_snapshot(sn);
 182             xbt_dynar_reset(prop_ato);
 183             xbt_free(prop_ato);
 184             MC_UNSET_RAW_MEM;
 185
 186             if(raw_mem_set)
 187               MC_SET_RAW_MEM;
 188             else
 189               MC_UNSET_RAW_MEM;
 190
 191             return 1;
 192           }
 193           /* }
 194              }else{
 195              XBT_INFO("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) );
 196              }*/
 197         }else{
 198           XBT_INFO("Different values of propositional symbols");
 199         }
 200       }else{
 201         XBT_INFO("Different automaton state");
 202       }
 203     }
 204
 205     MC_free_snapshot(sn);
 206     xbt_dynar_reset(prop_ato);
 207     xbt_free(prop_ato);
 208     MC_UNSET_RAW_MEM;
 209
 210     if(raw_mem_set)
 211       MC_SET_RAW_MEM;
 212     else
 213       MC_UNSET_RAW_MEM;
 214
 215     return 0;
 216
 217   }
 218 }
 219
 220 int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = current_pair */
 221
 222   xbt_dict_cursor_t cursor_dict = NULL;
 223   char *key;
 224   char *data;
 225   smx_rdv_t rdv1, rdv2;
 226   xbt_fifo_item_t item1, item2;
 227   smx_action_t action1, action2;
 228   xbt_fifo_item_t item_req1, item_req2;
 229   smx_simcall_t req1, req2;
 230   int i=0;
 231   int j=0;
 232
 233   xbt_dict_foreach(d1, cursor_dict, key, data){
 234     rdv1 = (smx_rdv_t)data;
 235     rdv2 = xbt_dict_get_or_null(d2, rdv1->name);
 236     if(rdv2 == NULL){
 237       XBT_INFO("Rdv point unknown");
 238       return 1;
 239     }else{
 240       if(xbt_fifo_size(rdv1->comm_fifo) != xbt_fifo_size(rdv2->comm_fifo)){
 241         XBT_INFO("Different total of actions in mailbox \"%s\" (%d - %d)", rdv1->name, xbt_fifo_size(rdv1->comm_fifo),xbt_fifo_size(rdv2->comm_fifo) );
 242         return 1;
 243       }else{
 244
 245         XBT_INFO("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo));
 246
 247         item1 = xbt_fifo_get_first_item(rdv1->comm_fifo);
 248         item2 = xbt_fifo_get_first_item(rdv2->comm_fifo);
 249
 250         while(i<xbt_fifo_size(rdv1->comm_fifo)){
 251           action1 = (smx_action_t) xbt_fifo_get_item_content(item1);
 252           action2 = (smx_action_t) xbt_fifo_get_item_content(item2);
 253
 254           if(action1->type != action2->type){
 255             XBT_INFO("Different type of action");
 256             return 1;
 257           }
 258
 259           if(action1->state != action2->state){
 260             XBT_INFO("Different state of action");
 261             return 1;
 262           }
 263
 264           if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){
 265             XBT_INFO("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls));
 266             return 1;
 267           }else{
 268
 269             item_req1 = xbt_fifo_get_first_item(action1->simcalls);
 270             item_req2 = xbt_fifo_get_first_item(action2->simcalls);
 271
 272             while(j<xbt_fifo_size(action1->simcalls)){
 273
 274               req1 = (smx_simcall_t) xbt_fifo_get_item_content(item_req1);
 275               req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2);
 276
 277               if(req1->call != req2->call){
 278                 XBT_INFO("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call);
 279                 return 1;
 280               }
 281               if(req1->issuer->pid != req2->issuer->pid){
 282                 XBT_INFO("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid);
 283                 return 1;
 284               }
 285
 286               item_req1 = xbt_fifo_get_next_item(item_req1);
 287               item_req2 = xbt_fifo_get_next_item(item_req2);
 288               j++;
 289
 290             }
 291           }
 292
 293           switch(action1->type){
 294           case 0: /* execution */
 295           case 1: /* parallel execution */
 296             if(strcmp(action1->execution.host->name, action2->execution.host->name) != 0)
 297               return 1;
 298             break;
 299           case 2: /* comm */
 300             if(action1->comm.type != action2->comm.type)
 301               return 1;
 302             //XBT_INFO("Type of comm : %d", action1->comm.type);
 303
 304             switch(action1->comm.type){
 305             case 0: /* SEND */
 306               if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
 307                 return 1;
 308               if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
 309                 return 1;
 310               break;
 311             case 1: /* RECEIVE */
 312               if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
 313                 return 1;
 314               if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
 315                 return 1;
 316               break;
 317             case 2: /* READY */
 318               if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
 319                 return 1;
 320               if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
 321                 return 1;
 322               if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
 323                 return 1;
 324               if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
 325                 return 1;
 326               break;
 327             case 3: /* DONE */
 328               if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
 329                 return 1;
 330               if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
 331                 return 1;
 332               if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
 333                 return 1;
 334               if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
 335                 return 1;
 336               break;
 337
 338             } /* end of switch on type of comm */
 339
 340             if(action1->comm.refcount != action2->comm.refcount)
 341               return 1;
 342             if(action1->comm.detached != action2->comm.detached)
 343               return 1;
 344             if(action1->comm.rate != action2->comm.rate)
 345               return 1;
 346             if(action1->comm.task_size != action2->comm.task_size)
 347               return 1;
 348             if(action1->comm.src_buff != action2->comm.src_buff)
 349               return 1;
 350             if(action1->comm.dst_buff != action2->comm.dst_buff)
 351               return 1;
 352             if(action1->comm.src_data != action2->comm.src_data)
 353               return 1;
 354             if(action1->comm.dst_data != action2->comm.dst_data)
 355               return 1;
 356
 357             break;
 358           case 3: /* sleep */
 359             if(strcmp(action1->sleep.host->name, action2->sleep.host->name) != 0)
 360               return 1;
 361             break;
 362           case 4: /* synchro */
 363
 364             break;
 365           default:
 366             break;
 367           }
 368
 369           item1 = xbt_fifo_get_next_item(item1);
 370           item2 = xbt_fifo_get_next_item(item2);
 371           i++;
 372         }
 373       }
 374     }
 375   }
 376
 377   return 0;
 378
 379 }
 380
 381 void set_pair_reached(xbt_state_t st){
 382
 383   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 384
 385   MC_SET_RAW_MEM;
 386
 387   mc_pair_reached_t pair = NULL;
 388   pair = xbt_new0(s_mc_pair_reached_t, 1);
 389   pair->nb = xbt_dynar_length(reached_pairs) + 1;
 390   pair->automaton_state = st;
 391   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 392   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 393   //pair->rdv_points = xbt_dict_new();
 394   MC_take_snapshot_liveness(pair->system_state);
 395
 396   /* Get values of propositional symbols */
 397   unsigned int cursor = 0;
 398   xbt_propositional_symbol_t ps = NULL;
 399   int res;
 400   int_f_void_t f;
 401
 402   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 403     f = (int_f_void_t)ps->function;
 404     res = (*f)();
 405     xbt_dynar_push_as(pair->prop_ato, int, res);
 406   }
 407
 408   /*xbt_dict_t rdv_points = SIMIX_get_rdv_points();
 409
 410     xbt_dict_cursor_t cursor_dict = NULL;
 411     char *key;
 412     char *data;
 413     xbt_fifo_item_t item;
 414     smx_action_t action;
 415
 416     xbt_dict_foreach(rdv_points, cursor_dict, key, data){
 417     smx_rdv_t new_rdv = xbt_new0(s_smx_rvpoint_t, 1);
 418     new_rdv->name = strdup(((smx_rdv_t)data)->name);
 419     new_rdv->comm_fifo = xbt_fifo_new();
 420     xbt_fifo_foreach(((smx_rdv_t)data)->comm_fifo, item, action, smx_action_t) {
 421     smx_action_t a = xbt_new0(s_smx_action_t, 1);
 422     memcpy(a, action, sizeof(s_smx_action_t));
 423     xbt_fifo_push(new_rdv->comm_fifo, a);
 424     XBT_INFO("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key);
 425     if(action->type==2)
 426     XBT_INFO("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount);
 427     }
 428     //new_rdv->comm_fifo = xbt_fifo_copy(((smx_rdv_t)data)->comm_fifo);
 429     xbt_dict_set(pair->rdv_points, new_rdv->name, new_rdv, NULL);
 430     }*/
 431
 432   xbt_dynar_push(reached_pairs, &pair);
 433
 434   MC_UNSET_RAW_MEM;
 435
 436   if(raw_mem_set)
 437     MC_SET_RAW_MEM;
 438   else
 439     MC_UNSET_RAW_MEM;
 440
 441 }
 442
 443
 444 int reached_hash(xbt_state_t st){
 445
 446   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 447
 448   if(xbt_dynar_is_empty(reached_pairs_hash)){
 449
 450     return 0;
 451
 452   }else{
 453
 454     MC_SET_RAW_MEM;
 455
 456     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 457     MC_take_snapshot_liveness(sn);
 458
 459     int j;
 460     unsigned int hash_regions[sn->num_reg];
 461     for(j=0; j<sn->num_reg; j++){
 462       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
 463     }
 464
 465
 466     /* Get values of propositional symbols */
 467     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 468     unsigned int cursor = 0;
 469     xbt_propositional_symbol_t ps = NULL;
 470     int res;
 471     int_f_void_t f;
 472
 473     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 474       f = (int_f_void_t)ps->function;
 475       res = (*f)();
 476       xbt_dynar_push_as(prop_ato, int, res);
 477     }
 478
 479     mc_pair_reached_hash_t pair_test = NULL;
 480
 481     int region_diff = 0;
 482
 483     cursor = 0;
 484
 485     xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
 486
 487       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 488         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 489           for(j=0 ; j< sn->num_reg ; j++){
 490             if(hash_regions[j] != pair_test->hash_regions[j]){
 491               region_diff++;
 492             }
 493           }
 494           if(region_diff == 0){
 495             MC_free_snapshot(sn);
 496             xbt_dynar_reset(prop_ato);
 497             xbt_free(prop_ato);
 498             MC_UNSET_RAW_MEM;
 499
 500             if(raw_mem_set)
 501               MC_SET_RAW_MEM;
 502             else
 503               MC_UNSET_RAW_MEM;
 504
 505             return 1;
 506           }else{
 507             XBT_INFO("Different snapshot");
 508           }
 509         }else{
 510           XBT_INFO("Different values of propositional symbols");
 511         }
 512       }else{
 513         XBT_INFO("Different automaton state");
 514       }
 515
 516       region_diff = 0;
 517     }
 518
 519     MC_free_snapshot(sn);
 520     xbt_dynar_reset(prop_ato);
 521     xbt_free(prop_ato);
 522     MC_UNSET_RAW_MEM;
 523
 524     if(raw_mem_set)
 525       MC_SET_RAW_MEM;
 526     else
 527       MC_UNSET_RAW_MEM;
 528
 529     return 0;
 530
 531   }
 532 }
 533
 534 void set_pair_reached_hash(xbt_state_t st){
 535
 536   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 537
 538   MC_SET_RAW_MEM;
 539
 540   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 541   MC_take_snapshot_liveness(sn);
 542
 543   mc_pair_reached_hash_t pair = NULL;
 544   pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
 545   pair->automaton_state = st;
 546   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 547   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
 548
 549   int i;
 550
 551   for(i=0 ; i< sn->num_reg ; i++){
 552     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
 553   }
 554
 555   /* Get values of propositional symbols */
 556   unsigned int cursor = 0;
 557   xbt_propositional_symbol_t ps = NULL;
 558   int res;
 559   int_f_void_t f;
 560
 561   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 562     f = (int_f_void_t)ps->function;
 563     res = (*f)();
 564     xbt_dynar_push_as(pair->prop_ato, int, res);
 565   }
 566
 567   xbt_dynar_push(reached_pairs_hash, &pair);
 568
 569   MC_free_snapshot(sn);
 570
 571   MC_UNSET_RAW_MEM;
 572
 573   if(raw_mem_set)
 574     MC_SET_RAW_MEM;
 575   else
 576     MC_UNSET_RAW_MEM;
 577
 578 }
 579
 580
 581 int visited(xbt_state_t st, int sc){
 582
 583   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 584
 585   if(xbt_dynar_is_empty(visited_pairs)){
 586
 587     return 0;
 588
 589   }else{
 590
 591     MC_SET_RAW_MEM;
 592
 593     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 594     MC_take_snapshot_liveness(sn);
 595
 596     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 597
 598     /* Get values of propositional symbols */
 599     unsigned int cursor = 0;
 600     xbt_propositional_symbol_t ps = NULL;
 601     int res;
 602     int_f_void_t f;
 603
 604     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 605       f = (int_f_void_t)ps->function;
 606       res = (*f)();
 607       xbt_dynar_push_as(prop_ato, int, res);
 608     }
 609
 610     cursor = 0;
 611     mc_pair_visited_t pair_test = NULL;
 612
 613     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
 614       if(pair_test->search_cycle == sc) {
 615         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 616           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 617             if(snapshot_compare(pair_test->system_state, sn) == 0){
 618
 619               MC_free_snapshot(sn);
 620               xbt_dynar_reset(prop_ato);
 621               xbt_free(prop_ato);
 622               MC_UNSET_RAW_MEM;
 623
 624               if(raw_mem_set)
 625                 MC_SET_RAW_MEM;
 626               else
 627                 MC_UNSET_RAW_MEM;
 628
 629               return 1;
 630
 631             }else{
 632               XBT_INFO("Different snapshot");
 633             }
 634           }else{
 635             XBT_INFO("Different values of propositional symbols");
 636           }
 637         }else{
 638           XBT_INFO("Different automaton state");
 639         }
 640       }else{
 641         XBT_INFO("Different value of search_cycle");
 642       }
 643     }
 644
 645
 646     MC_free_snapshot(sn);
 647     xbt_dynar_reset(prop_ato);
 648     xbt_free(prop_ato);
 649     MC_UNSET_RAW_MEM;
 650
 651     if(raw_mem_set)
 652       MC_SET_RAW_MEM;
 653     else
 654       MC_UNSET_RAW_MEM;
 655
 656     return 0;
 657
 658   }
 659 }
 660
 661
 662 int visited_hash(xbt_state_t st, int sc){
 663
 664   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 665
 666   if(xbt_dynar_is_empty(visited_pairs_hash)){
 667
 668     return 0;
 669
 670   }else{
 671
 672     MC_SET_RAW_MEM;
 673
 674     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 675     MC_take_snapshot_liveness(sn);
 676
 677     int j;
 678     unsigned int hash_regions[sn->num_reg];
 679     for(j=0; j<sn->num_reg; j++){
 680       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
 681     }
 682
 683
 684     /* Get values of propositional symbols */
 685     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 686     unsigned int cursor = 0;
 687     xbt_propositional_symbol_t ps = NULL;
 688     int res;
 689     int_f_void_t f;
 690
 691     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 692       f = (int_f_void_t)ps->function;
 693       res = (*f)();
 694       xbt_dynar_push_as(prop_ato, int, res);
 695     }
 696
 697     mc_pair_visited_hash_t pair_test = NULL;
 698
 699     int region_diff = 0;
 700     cursor = 0;
 701
 702     xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
 703
 704       if(pair_test->search_cycle == sc) {
 705         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 706           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 707             for(j=0 ; j< sn->num_reg ; j++){
 708               if(hash_regions[j] != pair_test->hash_regions[j]){
 709                 region_diff++;
 710               }
 711             }
 712             if(region_diff == 0){
 713               MC_free_snapshot(sn);
 714               xbt_dynar_reset(prop_ato);
 715               xbt_free(prop_ato);
 716               MC_UNSET_RAW_MEM;
 717
 718               if(raw_mem_set)
 719                 MC_SET_RAW_MEM;
 720               else
 721                 MC_UNSET_RAW_MEM;
 722
 723               return 1;
 724             }else{
 725               //XBT_INFO("Different snapshot");
 726             }
 727           }else{
 728             //XBT_INFO("Different values of propositional symbols");
 729           }
 730         }else{
 731           //XBT_INFO("Different automaton state");
 732         }
 733       }else{
 734         //XBT_INFO("Different value of search_cycle");
 735       }
 736
 737       region_diff = 0;
 738     }
 739
 740     MC_free_snapshot(sn);
 741     xbt_dynar_reset(prop_ato);
 742     xbt_free(prop_ato);
 743     MC_UNSET_RAW_MEM;
 744
 745     if(raw_mem_set)
 746       MC_SET_RAW_MEM;
 747     else
 748       MC_UNSET_RAW_MEM;
 749
 750     return 0;
 751
 752   }
 753 }
 754
 755 void set_pair_visited_hash(xbt_state_t st, int sc){
 756
 757   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 758
 759   MC_SET_RAW_MEM;
 760
 761   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 762   MC_take_snapshot_liveness(sn);
 763
 764   mc_pair_visited_hash_t pair = NULL;
 765   pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
 766   pair->automaton_state = st;
 767   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 768   pair->search_cycle = sc;
 769   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
 770
 771   int i;
 772
 773   for(i=0 ; i< sn->num_reg ; i++){
 774     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
 775   }
 776
 777   /* Get values of propositional symbols */
 778   unsigned int cursor = 0;
 779   xbt_propositional_symbol_t ps = NULL;
 780   int res;
 781   int_f_void_t f;
 782
 783   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 784     f = (int_f_void_t)ps->function;
 785     res = (*f)();
 786     xbt_dynar_push_as(pair->prop_ato, int, res);
 787   }
 788
 789   xbt_dynar_push(visited_pairs_hash, &pair);
 790
 791   MC_free_snapshot(sn);
 792
 793   MC_UNSET_RAW_MEM;
 794
 795   if(raw_mem_set)
 796     MC_SET_RAW_MEM;
 797   else
 798     MC_UNSET_RAW_MEM;
 799
 800 }
 801
 802 void set_pair_visited(xbt_state_t st, int sc){
 803
 804   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 805
 806   MC_SET_RAW_MEM;
 807
 808   mc_pair_visited_t pair = NULL;
 809   pair = xbt_new0(s_mc_pair_visited_t, 1);
 810   pair->automaton_state = st;
 811   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 812   pair->search_cycle = sc;
 813   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 814   MC_take_snapshot_liveness(pair->system_state);
 815
 816
 817   /* Get values of propositional symbols */
 818   unsigned int cursor = 0;
 819   xbt_propositional_symbol_t ps = NULL;
 820   int res;
 821   int_f_void_t f;
 822
 823   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 824     f = (int_f_void_t)ps->function;
 825     res = (*f)();
 826     xbt_dynar_push_as(pair->prop_ato, int, res);
 827   }
 828
 829   xbt_dynar_push(visited_pairs, &pair);
 830
 831   MC_UNSET_RAW_MEM;
 832
 833   if(raw_mem_set)
 834     MC_SET_RAW_MEM;
 835   else
 836     MC_UNSET_RAW_MEM;
 837
 838 }
 839
 840 void MC_pair_delete(mc_pair_t pair){
 841   xbt_free(pair->graph_state->proc_status);
 842   xbt_free(pair->graph_state);
 843   xbt_free(pair);
 844 }
 845
 846
 847
 848 int MC_automaton_evaluate_label(xbt_exp_label_t l){
 849
 850   switch(l->type){
 851   case 0 : {
 852     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 853     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 854     return (left_res || right_res);
 855   }
 856   case 1 : {
 857     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 858     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 859     return (left_res && right_res);
 860   }
 861   case 2 : {
 862     int res = MC_automaton_evaluate_label(l->u.exp_not);
 863     return (!res);
 864   }
 865   case 3 : {
 866     unsigned int cursor = 0;
 867     xbt_propositional_symbol_t p = NULL;
 868     int_f_void_t f;
 869     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
 870       if(strcmp(p->pred, l->u.predicat) == 0){
 871         f = (int_f_void_t)p->function;
 872         return (*f)();
 873       }
 874     }
 875     return -1;
 876   }
 877   case 4 : {
 878     return 2;
 879   }
 880   default :
 881     return -1;
 882   }
 883 }
 884
 885
 886 /********************* Double-DFS stateless *******************/
 887
 888 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 889   xbt_free(pair->graph_state->proc_status);
 890   xbt_free(pair->graph_state);
 891   xbt_free(pair);
 892 }
 893
 894 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 895   mc_pair_stateless_t p = NULL;
 896   p = xbt_new0(s_mc_pair_stateless_t, 1);
 897   p->automaton_state = st;
 898   p->graph_state = sg;
 899   p->requests = r;
 900   mc_stats_pair->expanded_pairs++;
 901   return p;
 902 }
 903
 904 void MC_ddfs_init(void){
 905
 906   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 907
 908   XBT_INFO("**************************************************");
 909   XBT_INFO("Double-DFS init");
 910   XBT_INFO("**************************************************");
 911
 912   mc_pair_stateless_t mc_initial_pair = NULL;
 913   mc_state_t initial_graph_state = NULL;
 914   smx_process_t process;
 915
 916
 917   MC_wait_for_requests();
 918
 919   MC_SET_RAW_MEM;
 920
 921   initial_graph_state = MC_state_pair_new();
 922   xbt_swag_foreach(process, simix_global->process_list){
 923     if(MC_process_is_enabled(process)){
 924       MC_state_interleave_process(initial_graph_state, process);
 925     }
 926   }
 927
 928   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
 929   //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
 930   //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
 931   //visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
 932   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 933
 934   /* Save the initial state */
 935   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
 936   MC_take_snapshot_liveness(initial_snapshot_liveness);
 937
 938   MC_UNSET_RAW_MEM;
 939
 940   unsigned int cursor = 0;
 941   xbt_state_t state;
 942
 943   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
 944     if(state->type == -1){
 945
 946       MC_SET_RAW_MEM;
 947       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 948       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 949       MC_UNSET_RAW_MEM;
 950
 951       if(cursor != 0){
 952         MC_restore_snapshot(initial_snapshot_liveness);
 953         MC_UNSET_RAW_MEM;
 954       }
 955
 956       MC_ddfs(0);
 957
 958     }else{
 959       if(state->type == 2){
 960
 961         MC_SET_RAW_MEM;
 962         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 963         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 964         MC_UNSET_RAW_MEM;
 965
 966         set_pair_reached(state);
 967         //set_pair_reached_hash(state);
 968
 969         if(cursor != 0){
 970           MC_restore_snapshot(initial_snapshot_liveness);
 971           MC_UNSET_RAW_MEM;
 972         }
 973
 974         MC_ddfs(1);
 975
 976       }
 977     }
 978   }
 979
 980   if(raw_mem_set)
 981     MC_SET_RAW_MEM;
 982   else
 983     MC_UNSET_RAW_MEM;
 984
 985
 986 }
 987
 988
 989 void MC_ddfs(int search_cycle){
 990
 991   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 992
 993   smx_process_t process;
 994   mc_pair_stateless_t current_pair = NULL;
 995
 996   if(xbt_fifo_size(mc_stack_liveness) == 0)
 997     return;
 998
 999
1000   /* Get current pair */
1001   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
1002
1003   /* Update current state in buchi automaton */
1004   _mc_property_automaton->current_state = current_pair->automaton_state;
1005
1006
1007   XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
1008   XBT_INFO("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id, MC_state_interleave_size(current_pair->graph_state));
1009
1010   mc_stats_pair->visited_pairs++;
1011
1012   //sleep(1);
1013
1014   int value;
1015   mc_state_t next_graph_state = NULL;
1016   smx_simcall_t req = NULL;
1017   char *req_str;
1018
1019   xbt_transition_t transition_succ;
1020   unsigned int cursor = 0;
1021   int res;
1022
1023   mc_pair_stateless_t next_pair = NULL;
1024   mc_pair_stateless_t pair_succ;
1025
1026   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
1027
1028     //set_pair_visited(current_pair->automaton_state, search_cycle);
1029     //set_pair_visited_hash(current_pair->automaton_state, search_cycle);
1030
1031     //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
1032     //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
1033
1034     if(current_pair->requests > 0){
1035
1036       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
1037
1038         /* Debug information */
1039
1040         req_str = MC_request_to_string(req, value);
1041         XBT_INFO("Execute: %s", req_str);
1042         xbt_free(req_str);
1043
1044         MC_state_set_executed_request(current_pair->graph_state, req, value);
1045
1046         /* Answer the request */
1047         SIMIX_simcall_pre(req, value);
1048
1049         /* Wait for requests (schedules processes) */
1050         MC_wait_for_requests();
1051
1052
1053         MC_SET_RAW_MEM;
1054
1055         /* Create the new expanded graph_state */
1056         next_graph_state = MC_state_pair_new();
1057
1058         /* Get enabled process and insert it in the interleave set of the next graph_state */
1059         xbt_swag_foreach(process, simix_global->process_list){
1060           if(MC_process_is_enabled(process)){
1061             MC_state_interleave_process(next_graph_state, process);
1062           }
1063         }
1064
1065         xbt_dynar_reset(successors);
1066
1067         MC_UNSET_RAW_MEM;
1068
1069
1070         cursor= 0;
1071         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1072
1073           res = MC_automaton_evaluate_label(transition_succ->label);
1074
1075           if(res == 1){ // enabled transition in automaton
1076             MC_SET_RAW_MEM;
1077             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1078             xbt_dynar_push(successors, &next_pair);
1079             MC_UNSET_RAW_MEM;
1080           }
1081
1082         }
1083
1084         cursor = 0;
1085
1086         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1087
1088           res = MC_automaton_evaluate_label(transition_succ->label);
1089
1090           if(res == 2){ // true transition in automaton
1091             MC_SET_RAW_MEM;
1092             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1093             xbt_dynar_push(successors, &next_pair);
1094             MC_UNSET_RAW_MEM;
1095           }
1096
1097         }
1098
1099         cursor = 0;
1100
1101         xbt_dynar_foreach(successors, cursor, pair_succ){
1102
1103           if(search_cycle == 1){
1104
1105             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
1106
1107               if(reached(pair_succ->automaton_state)){
1108                 //if(reached_hash(pair_succ->automaton_state)){
1109
1110                 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));
1111
1112                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1113                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
1114                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1115                 XBT_INFO("Counter-example that violates formula :");
1116                 MC_show_stack_liveness(mc_stack_liveness);
1117                 MC_dump_stack_liveness(mc_stack_liveness);
1118                 MC_print_statistics_pairs(mc_stats_pair);
1119                 exit(0);
1120
1121               }else{
1122
1123                 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);
1124
1125                 set_pair_reached(pair_succ->automaton_state);
1126                 //set_pair_reached_hash(pair_succ->automaton_state);
1127
1128                 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1129                 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1130
1131                 MC_SET_RAW_MEM;
1132                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1133                 MC_UNSET_RAW_MEM;
1134
1135                 MC_ddfs(search_cycle);
1136
1137               }
1138
1139             }else{
1140
1141               //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1142                 //if(!visited(pair_succ->automaton_state, search_cycle)){
1143
1144                 MC_SET_RAW_MEM;
1145                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1146                 MC_UNSET_RAW_MEM;
1147
1148                 MC_ddfs(search_cycle);
1149
1150                 /*}else{
1151
1152                 XBT_INFO("Next pair already visited ! ");
1153
1154                 }*/
1155
1156             }
1157
1158           }else{
1159
1160             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1161
1162               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);
1163
1164               set_pair_reached(pair_succ->automaton_state);
1165               //set_pair_reached_hash(pair_succ->automaton_state);
1166
1167               search_cycle = 1;
1168
1169               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1170               //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1171
1172             }
1173
1174             //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1175               //if(!visited(pair_succ->automaton_state, search_cycle)){
1176
1177               MC_SET_RAW_MEM;
1178               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1179               MC_UNSET_RAW_MEM;
1180
1181               MC_ddfs(search_cycle);
1182
1183               /*}else{
1184
1185               XBT_INFO("Next pair already visited ! ");
1186
1187               }*/
1188
1189           }
1190
1191
1192           /* Restore system before checking others successors */
1193           if(cursor != (xbt_dynar_length(successors) - 1))
1194             MC_replay_liveness(mc_stack_liveness, 1);
1195
1196
1197         }
1198
1199         if(MC_state_interleave_size(current_pair->graph_state) > 0){
1200           XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
1201           MC_replay_liveness(mc_stack_liveness, 0);
1202         }
1203       }
1204
1205
1206     }else{  /*No request to execute, search evolution in Büchi automaton */
1207
1208       MC_SET_RAW_MEM;
1209
1210       /* Create the new expanded graph_state */
1211       next_graph_state = MC_state_pair_new();
1212
1213       xbt_dynar_reset(successors);
1214
1215       MC_UNSET_RAW_MEM;
1216
1217
1218       cursor= 0;
1219       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1220
1221         res = MC_automaton_evaluate_label(transition_succ->label);
1222
1223         if(res == 1){ // enabled transition in automaton
1224           MC_SET_RAW_MEM;
1225           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1226           xbt_dynar_push(successors, &next_pair);
1227           MC_UNSET_RAW_MEM;
1228         }
1229
1230       }
1231
1232       cursor = 0;
1233
1234       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1235
1236         res = MC_automaton_evaluate_label(transition_succ->label);
1237
1238         if(res == 2){ // true transition in automaton
1239           MC_SET_RAW_MEM;
1240           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1241           xbt_dynar_push(successors, &next_pair);
1242           MC_UNSET_RAW_MEM;
1243         }
1244
1245       }
1246
1247       cursor = 0;
1248
1249       xbt_dynar_foreach(successors, cursor, pair_succ){
1250
1251         if(search_cycle == 1){
1252
1253           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
1254
1255             if(reached(pair_succ->automaton_state)){
1256               //if(reached_hash(pair_succ->automaton_state)){
1257
1258               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
1259
1260               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1261               XBT_INFO("|             ACCEPTANCE CYCLE            |");
1262               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1263               XBT_INFO("Counter-example that violates formula :");
1264               MC_show_stack_liveness(mc_stack_liveness);
1265               MC_dump_stack_liveness(mc_stack_liveness);
1266               MC_print_statistics_pairs(mc_stats_pair);
1267               exit(0);
1268
1269             }else{
1270
1271               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);
1272
1273               set_pair_reached(pair_succ->automaton_state);
1274               //set_pair_reached_hash(pair_succ->automaton_state);
1275
1276               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1277               //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1278
1279               MC_SET_RAW_MEM;
1280               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1281               MC_UNSET_RAW_MEM;
1282
1283               MC_ddfs(search_cycle);
1284
1285             }
1286
1287           }else{
1288
1289             //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1290               //if(!visited(pair_succ->automaton_state, search_cycle)){
1291
1292               MC_SET_RAW_MEM;
1293               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1294               MC_UNSET_RAW_MEM;
1295
1296               MC_ddfs(search_cycle);
1297
1298               /*}else{
1299
1300               XBT_INFO("Next pair already visited ! ");
1301
1302               }*/
1303           }
1304
1305
1306         }else{
1307
1308           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1309
1310             set_pair_reached(pair_succ->automaton_state);
1311             //set_pair_reached_hash(pair_succ->automaton_state);
1312
1313             search_cycle = 1;
1314
1315             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1316             //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1317
1318           }
1319
1320           //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1321             //if(!visited(pair_succ->automaton_state, search_cycle)){
1322
1323             MC_SET_RAW_MEM;
1324             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1325             MC_UNSET_RAW_MEM;
1326
1327             MC_ddfs(search_cycle);
1328
1329             /*}else{
1330
1331             XBT_INFO("Next pair already visited ! ");
1332
1333             }*/
1334
1335         }
1336
1337         /* Restore system before checking others successors */
1338         if(cursor != xbt_dynar_length(successors) - 1)
1339           MC_replay_liveness(mc_stack_liveness, 1);
1340
1341
1342       }
1343
1344     }
1345
1346   }else{
1347
1348     XBT_INFO("Max depth reached");
1349
1350   }
1351
1352   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1353     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) );
1354   }else{
1355     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) );
1356   }
1357
1358
1359   MC_SET_RAW_MEM;
1360   xbt_fifo_shift(mc_stack_liveness);
1361   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1362     xbt_dynar_pop(reached_pairs, NULL);
1363     //xbt_dynar_pop(reached_pairs_hash, NULL);
1364   }
1365   MC_UNSET_RAW_MEM;
1366
1367   if(raw_mem_set)
1368     MC_SET_RAW_MEM;
1369   else
1370     MC_UNSET_RAW_MEM;
1371
1372 }
1373
1374
1375 #ifdef SIMGRID_TEST
1376
1377 XBT_TEST_SUITE("mc_liveness", "Model checking liveness properties");
1378 XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(mc_liveness);
1379
1380 XBT_TEST_UNIT("snapshots_comparison", test_compare_snapshot, "Comparison of snapshots")
1381 {
1382
1383   MC_SET_RAW_MEM;
1384
1385   /* Save first snapshot */
1386   mc_snapshot_t snapshot1 = xbt_new0(s_mc_snapshot_t, 1);
1387   MC_take_snapshot_liveness(snapshot1);
1388
1389   /* Save second snapshot */
1390   mc_snapshot_t snapshot2 = xbt_new0(s_mc_snapshot_t, 1);
1391   MC_take_snapshot_liveness(snapshot2);
1392
1393   MC_UNSET_RAW_MEM;
1394
1395   xbt_test_assert(snapshot_compare(snapshot1, snapshot2) == 0, "Different consecutive snapshot");
1396
1397
1398 }
1399
1400 XBT_TEST_UNIT("snapshots_comparison2", test2_compare_snapshot, "Comparison of snapshots with modification between")
1401 {
1402
1403   MC_SET_RAW_MEM;
1404
1405   /* Save first snapshot */
1406   mc_snapshot_t snapshot1 = xbt_new0(s_mc_snapshot_t, 1);
1407   MC_take_snapshot_liveness(snapshot1);
1408
1409   MC_UNSET_RAW_MEM;
1410
1411   void *test = snapshot1;
1412   test = (char*)test+1;
1413   char* t= strdup("toto");
1414   t=strdup("tat");
1415
1416   MC_SET_RAW_MEM;
1417
1418   /* Save second snapshot */
1419   mc_snapshot_t snapshot2 = xbt_new0(s_mc_snapshot_t, 1);
1420   MC_take_snapshot_liveness(snapshot2);
1421
1422   xbt_test_assert(snapshot_compare(snapshot1, snapshot2) != 0, "Same snapshot with new allocations");
1423
1424   MC_UNSET_RAW_MEM;
1425
1426
1427 }
1428
1429 #endif