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