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