src/mc/mc_liveness.c

   1 /* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "mc_private.h"
   7 #include <unistd.h>
   8 #include <sys/wait.h>
   9
  10 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
  11                                 "Logging specific to algorithms for liveness properties verification");
  12
  13 xbt_dynar_t reached_pairs;
  14 xbt_dynar_t successors;
  15
  16 int create_dump(int pair)
  17 {
  18    // Try to enable core dumps
  19   struct rlimit core_limit;
  20   core_limit.rlim_cur = RLIM_INFINITY;
  21   core_limit.rlim_max = RLIM_INFINITY;
  22
  23   if(setrlimit(RLIMIT_CORE, &core_limit) < 0)
  24     fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno));
  25
  26   int status;
  27   switch(fork()){
  28   case 0:
  29     // We are the child process -- run the actual program
  30     xbt_abort();
  31     break;
  32
  33   case -1:
  34     // An error occurred, shouldn't happen
  35     perror("fork");
  36     return -1;
  37
  38   default:
  39     // We are the parent process -- wait for the child process to exit
  40     if(wait(&status) < 0)
  41       perror("wait");
  42     if(WIFSIGNALED(status) && WCOREDUMP(status)){
  43       char *core_name = malloc(20);
  44       sprintf(core_name,"core_%d", pair);
  45       rename("core", core_name);
  46       free(core_name);
  47     }
  48   }
  49
  50   return 0;
  51 }
  52
  53 void MC_print_comparison_times_statistics(mc_comparison_times_t ct){
  54
  55   XBT_DEBUG("Comparisons done : %d", ct->nb_comparisons);
  56
  57   double total, min, max;
  58   unsigned int cursor;
  59
  60   if(xbt_dynar_length(ct->chunks_used_comparison_times) > 0){
  61     cursor = 0;
  62     total = 0.0;
  63     max = 0.0;
  64     min = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
  65     while(cursor < xbt_dynar_length(ct->chunks_used_comparison_times) - 1){
  66       total += xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
  67       if(xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double) > max)
  68         max = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
  69       if(xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double) < min)
  70         min = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
  71       cursor++;
  72     }
  73     XBT_DEBUG("Chunks used comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->chunks_used_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->chunks_used_comparison_times), max, min);
  74   }
  75
  76   if(xbt_dynar_length(ct->stacks_sizes_comparison_times) > 0){
  77     cursor = 0;
  78     total = 0.0;
  79     max = 0.0;
  80     min = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
  81     while(cursor < xbt_dynar_length(ct->stacks_sizes_comparison_times) - 1){
  82       total += xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
  83       if(xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double) > max)
  84         max = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
  85       if(xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double) < min)
  86         min = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
  87       cursor++;
  88     }
  89     XBT_DEBUG("Stacks sizes comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->stacks_sizes_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->stacks_sizes_comparison_times), max, min);
  90   }
  91
  92   if(xbt_dynar_length(ct->program_data_segment_comparison_times) > 0){
  93     cursor = 0;
  94     total = 0.0;
  95     max = 0.0;
  96     min = xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double);
  97     while(cursor < xbt_dynar_length(ct->program_data_segment_comparison_times) - 1){
  98       total += xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double);
  99       if(xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double) > max)
 100         max = xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double);
 101       if(xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double) < min)
 102         min = xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double);
 103       cursor++;
 104     }
 105     XBT_DEBUG("Program data/bss segments comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->program_data_segment_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->program_data_segment_comparison_times), max, min);
 106   }
 107
 108   if(xbt_dynar_length(ct->libsimgrid_data_segment_comparison_times) > 0){
 109     cursor = 0;
 110     total = 0.0;
 111     max = 0.0;
 112     min = xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double);
 113     while(cursor < xbt_dynar_length(ct->libsimgrid_data_segment_comparison_times) - 1){
 114       total += xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double);
 115       if(xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double) > max)
 116         max = xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double);
 117       if(xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double) < min)
 118         min = xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double);
 119       cursor++;
 120     }
 121     XBT_DEBUG("Libsimgrid data/bss segments comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->libsimgrid_data_segment_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->libsimgrid_data_segment_comparison_times), max, min);
 122   }
 123
 124   if(xbt_dynar_length(ct->heap_comparison_times) > 0){
 125     cursor = 0;
 126     total = 0.0;
 127     max = 0.0;
 128     min = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
 129     while(cursor < xbt_dynar_length(ct->heap_comparison_times) - 1){
 130       total += xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
 131       if(xbt_dynar_get_as(ct->heap_comparison_times, cursor, double) > max)
 132         max = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
 133       if(xbt_dynar_get_as(ct->heap_comparison_times, cursor, double) < min)
 134         min = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
 135       cursor++;
 136     }
 137     XBT_DEBUG("Heap comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->heap_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->heap_comparison_times), max, min);
 138   }
 139
 140   if(xbt_dynar_length(ct->stacks_comparison_times) > 0){
 141     cursor = 0;
 142     total = 0.0;
 143     max = 0.0;
 144     min = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
 145     while(cursor < xbt_dynar_length(ct->stacks_comparison_times) - 1){
 146       total += xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
 147       if(xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double) > max)
 148         max = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
 149       if(xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double) < min)
 150         min = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
 151       cursor++;
 152     }
 153     XBT_DEBUG("Stacks comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->stacks_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->stacks_comparison_times), max, min);
 154   }
 155
 156   if(xbt_dynar_length(ct->snapshot_comparison_times) > 0){
 157     cursor = 0;
 158     total = 0.0;
 159     max = 0.0;
 160     min = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
 161     while(cursor < xbt_dynar_length(ct->snapshot_comparison_times) - 1){
 162       total += xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
 163       if(xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double) > max)
 164         max = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
 165       if(xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double) < min)
 166         min = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
 167       cursor++;
 168     }
 169     XBT_DEBUG("Snapshot comparison (Whole funnel) -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->snapshot_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->snapshot_comparison_times), max, min);
 170   }
 171
 172 }
 173
 174 mc_comparison_times_t new_comparison_times(){
 175   mc_comparison_times_t ct = NULL;
 176   ct = xbt_new0(s_mc_comparison_times_t, 1);
 177   ct->nb_comparisons = 0;
 178   ct->snapshot_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 179   ct->chunks_used_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 180   ct->stacks_sizes_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 181   ct->program_data_segment_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 182   ct->libsimgrid_data_segment_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 183   ct->heap_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 184   ct->stacks_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 185   return ct;
 186 }
 187
 188 int reached(xbt_state_t st){
 189
 190   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 191
 192   MC_SET_RAW_MEM;
 193
 194   mc_pair_reached_t new_pair = NULL;
 195   new_pair = xbt_new0(s_mc_pair_reached_t, 1);
 196   new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
 197   new_pair->automaton_state = st;
 198   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 199   new_pair->comparison_times = new_comparison_times();
 200   new_pair->system_state = MC_take_snapshot_liveness();
 201
 202   /* Get values of propositional symbols */
 203   int res;
 204   int_f_void_t f;
 205   unsigned int cursor = 0;
 206   xbt_propositional_symbol_t ps = NULL;
 207   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 208     f = (int_f_void_t)ps->function;
 209     res = (*f)();
 210     xbt_dynar_push_as(new_pair->prop_ato, int, res);
 211   }
 212
 213   MC_UNSET_RAW_MEM;
 214
 215   if(xbt_dynar_is_empty(reached_pairs)/* || !compare*/){
 216
 217     MC_SET_RAW_MEM;
 218     /* New pair reached */
 219     xbt_dynar_push(reached_pairs, &new_pair);
 220     MC_UNSET_RAW_MEM;
 221
 222     if(raw_mem_set)
 223       MC_SET_RAW_MEM;
 224
 225     return 0;
 226
 227   }else{
 228
 229     MC_SET_RAW_MEM;
 230
 231     cursor = 0;
 232     mc_pair_reached_t pair_test = NULL;
 233
 234     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
 235       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
 236         XBT_DEBUG("****** Pair reached #%d ******", pair_test->nb);
 237       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 238         if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
 239           if(snapshot_compare(new_pair->system_state, pair_test->system_state, new_pair->comparison_times, pair_test->comparison_times) == 0){
 240
 241             if(raw_mem_set)
 242               MC_SET_RAW_MEM;
 243             else
 244               MC_UNSET_RAW_MEM;
 245
 246             return 1;
 247           }
 248         }else{
 249           XBT_INFO("Different values of propositional symbols");
 250         }
 251       }else{
 252         XBT_INFO("Different automaton state");
 253       }
 254       if(pair_test->comparison_times != NULL && XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 255         XBT_DEBUG("*** Comparison times statistics ***");
 256         MC_print_comparison_times_statistics(pair_test->comparison_times);
 257       }
 258     }
 259
 260     /* New pair reached */
 261     xbt_dynar_push(reached_pairs, &new_pair);
 262
 263     MC_UNSET_RAW_MEM;
 264
 265     if(raw_mem_set)
 266       MC_SET_RAW_MEM;
 267
 268     compare = 0;
 269
 270     return 0;
 271
 272   }
 273 }
 274
 275
 276 void set_pair_reached(xbt_state_t st){
 277
 278   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 279
 280   MC_SET_RAW_MEM;
 281
 282   mc_pair_reached_t pair = NULL;
 283   pair = xbt_new0(s_mc_pair_reached_t, 1);
 284   pair->nb = xbt_dynar_length(reached_pairs) + 1;
 285   pair->automaton_state = st;
 286   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 287   pair->comparison_times = new_comparison_times();
 288   pair->system_state = MC_take_snapshot_liveness();
 289
 290   /* Get values of propositional symbols */
 291   unsigned int cursor = 0;
 292   xbt_propositional_symbol_t ps = NULL;
 293   int res;
 294   int_f_void_t f;
 295
 296   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 297     f = (int_f_void_t)ps->function;
 298     res = (*f)();
 299     xbt_dynar_push_as(pair->prop_ato, int, res);
 300   }
 301
 302   xbt_dynar_push(reached_pairs, &pair);
 303
 304   MC_UNSET_RAW_MEM;
 305
 306   if(raw_mem_set)
 307     MC_SET_RAW_MEM;
 308
 309 }
 310
 311 void MC_pair_delete(mc_pair_t pair){
 312   xbt_free(pair->graph_state->proc_status);
 313   xbt_free(pair->graph_state);
 314   xbt_free(pair);
 315 }
 316
 317
 318
 319 int MC_automaton_evaluate_label(xbt_exp_label_t l){
 320
 321   switch(l->type){
 322   case 0 : {
 323     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 324     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 325     return (left_res || right_res);
 326   }
 327   case 1 : {
 328     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 329     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 330     return (left_res && right_res);
 331   }
 332   case 2 : {
 333     int res = MC_automaton_evaluate_label(l->u.exp_not);
 334     return (!res);
 335   }
 336   case 3 : {
 337     unsigned int cursor = 0;
 338     xbt_propositional_symbol_t p = NULL;
 339     int_f_void_t f;
 340     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
 341       if(strcmp(p->pred, l->u.predicat) == 0){
 342         f = (int_f_void_t)p->function;
 343         return (*f)();
 344       }
 345     }
 346     return -1;
 347   }
 348   case 4 : {
 349     return 2;
 350   }
 351   default :
 352     return -1;
 353   }
 354 }
 355
 356
 357 /********************* Double-DFS stateless *******************/
 358
 359 void pair_stateless_free(mc_pair_stateless_t pair){
 360   xbt_free(pair->graph_state->system_state);
 361   xbt_free(pair->graph_state->proc_status);
 362   xbt_free(pair->graph_state);
 363   xbt_free(pair);
 364 }
 365
 366 void pair_stateless_free_voidp(void *p){
 367   pair_stateless_free((mc_pair_stateless_t) * (void **) p);
 368 }
 369
 370 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 371   mc_pair_stateless_t p = NULL;
 372   p = xbt_new0(s_mc_pair_stateless_t, 1);
 373   p->automaton_state = st;
 374   p->graph_state = sg;
 375   p->requests = r;
 376   mc_stats_pair->expanded_pairs++;
 377   return p;
 378 }
 379
 380 void pair_reached_free(mc_pair_reached_t pair){
 381   if(pair){
 382     pair->automaton_state = NULL;
 383     xbt_dynar_free(&(pair->prop_ato));
 384     MC_free_snapshot(pair->system_state);
 385     xbt_free(pair);
 386   }
 387 }
 388
 389 void pair_reached_free_voidp(void *p){
 390   pair_reached_free((mc_pair_reached_t) * (void **) p);
 391 }
 392
 393 void MC_ddfs_init(void){
 394
 395   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 396
 397   XBT_INFO("**************************************************");
 398   XBT_INFO("Double-DFS init");
 399   XBT_INFO("**************************************************");
 400
 401   mc_pair_stateless_t mc_initial_pair = NULL;
 402   mc_state_t initial_graph_state = NULL;
 403   smx_process_t process;
 404
 405
 406   MC_wait_for_requests();
 407
 408   MC_SET_RAW_MEM;
 409
 410   initial_graph_state = MC_state_pair_new();
 411   xbt_swag_foreach(process, simix_global->process_list){
 412     if(MC_process_is_enabled(process)){
 413       MC_state_interleave_process(initial_graph_state, process);
 414     }
 415   }
 416
 417   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), pair_reached_free_voidp);
 418   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 419
 420   /* Save the initial state */
 421   initial_state_liveness->initial_snapshot = MC_take_snapshot_liveness();
 422
 423   MC_UNSET_RAW_MEM;
 424
 425   unsigned int cursor = 0;
 426   xbt_state_t state;
 427
 428   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
 429     if(state->type == -1){
 430
 431       MC_SET_RAW_MEM;
 432       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 433       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 434       MC_UNSET_RAW_MEM;
 435
 436       if(cursor != 0){
 437         MC_restore_snapshot(initial_state_liveness->initial_snapshot);
 438         MC_UNSET_RAW_MEM;
 439       }
 440
 441       MC_ddfs(0);
 442
 443     }else{
 444       if(state->type == 2){
 445
 446         MC_SET_RAW_MEM;
 447         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 448         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 449         MC_UNSET_RAW_MEM;
 450
 451         set_pair_reached(state);
 452
 453         if(cursor != 0){
 454           MC_restore_snapshot(initial_state_liveness->initial_snapshot);
 455           MC_UNSET_RAW_MEM;
 456         }
 457
 458         MC_ddfs(1);
 459
 460       }
 461     }
 462   }
 463
 464   if(raw_mem_set)
 465     MC_SET_RAW_MEM;
 466   else
 467     MC_UNSET_RAW_MEM;
 468
 469
 470 }
 471
 472
 473 void MC_ddfs(int search_cycle){
 474
 475   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 476
 477   smx_process_t process;
 478   mc_pair_stateless_t current_pair = NULL;
 479
 480   if(xbt_fifo_size(mc_stack_liveness) == 0)
 481     return;
 482
 483
 484   /* Get current pair */
 485   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 486
 487   /* Update current state in buchi automaton */
 488   _mc_property_automaton->current_state = current_pair->automaton_state;
 489
 490
 491   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
 492
 493   mc_stats_pair->visited_pairs++;
 494
 495   //sleep(1);
 496
 497   int value;
 498   mc_state_t next_graph_state = NULL;
 499   smx_simcall_t req = NULL;
 500   char *req_str;
 501
 502   xbt_transition_t transition_succ;
 503   unsigned int cursor = 0;
 504   int res;
 505
 506   mc_pair_stateless_t next_pair = NULL;
 507   mc_pair_stateless_t pair_succ;
 508
 509   mc_pair_stateless_t remove_pair;
 510   mc_pair_reached_t remove_pair_reached;
 511
 512   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
 513
 514     if(current_pair->requests > 0){
 515
 516       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 517
 518         /* Debug information */
 519
 520         req_str = MC_request_to_string(req, value);
 521         XBT_DEBUG("Execute: %s", req_str);
 522         xbt_free(req_str);
 523
 524         MC_state_set_executed_request(current_pair->graph_state, req, value);
 525
 526         /* Answer the request */
 527         SIMIX_simcall_pre(req, value);
 528
 529         /* Wait for requests (schedules processes) */
 530         MC_wait_for_requests();
 531
 532         MC_SET_RAW_MEM;
 533
 534         /* Create the new expanded graph_state */
 535         next_graph_state = MC_state_pair_new();
 536
 537         /* Get enabled process and insert it in the interleave set of the next graph_state */
 538
 539         xbt_swag_foreach(process, simix_global->process_list){
 540           if(MC_process_is_enabled(process)){
 541             XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
 542           }
 543         }
 544
 545         xbt_swag_foreach(process, simix_global->process_list){
 546           if(MC_process_is_enabled(process)){
 547             MC_state_interleave_process(next_graph_state, process);
 548           }
 549         }
 550
 551         xbt_dynar_reset(successors);
 552
 553         MC_UNSET_RAW_MEM;
 554
 555
 556         cursor= 0;
 557         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 558
 559           res = MC_automaton_evaluate_label(transition_succ->label);
 560
 561           if(res == 1){ // enabled transition in automaton
 562             MC_SET_RAW_MEM;
 563             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 564             xbt_dynar_push(successors, &next_pair);
 565             MC_UNSET_RAW_MEM;
 566           }
 567
 568         }
 569
 570         cursor = 0;
 571
 572         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 573
 574           res = MC_automaton_evaluate_label(transition_succ->label);
 575
 576           if(res == 2){ // true transition in automaton
 577             MC_SET_RAW_MEM;
 578             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 579             xbt_dynar_push(successors, &next_pair);
 580             MC_UNSET_RAW_MEM;
 581           }
 582
 583         }
 584
 585         cursor = 0;
 586
 587         xbt_dynar_foreach(successors, cursor, pair_succ){
 588
 589           if(search_cycle == 1){
 590
 591             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 592
 593               if(reached(pair_succ->automaton_state)){
 594
 595                 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));
 596
 597                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 598                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 599                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 600                 XBT_INFO("Counter-example that violates formula :");
 601                 MC_show_stack_liveness(mc_stack_liveness);
 602                 MC_dump_stack_liveness(mc_stack_liveness);
 603                 MC_print_statistics_pairs(mc_stats_pair);
 604                 xbt_abort();
 605
 606               }else{
 607
 608                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 609
 610                 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 611
 612                 MC_SET_RAW_MEM;
 613                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 614                 MC_UNSET_RAW_MEM;
 615
 616                 MC_ddfs(search_cycle);
 617
 618               }
 619
 620             }else{
 621
 622               MC_SET_RAW_MEM;
 623               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 624               MC_UNSET_RAW_MEM;
 625
 626               MC_ddfs(search_cycle);
 627
 628             }
 629
 630           }else{
 631
 632             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 633
 634               XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 635
 636               set_pair_reached(pair_succ->automaton_state);
 637
 638               search_cycle = 1;
 639
 640               XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 641
 642             }
 643
 644             MC_SET_RAW_MEM;
 645             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 646             MC_UNSET_RAW_MEM;
 647
 648             MC_ddfs(search_cycle);
 649
 650           }
 651
 652
 653           /* Restore system before checking others successors */
 654           if(cursor != (xbt_dynar_length(successors) - 1))
 655             MC_replay_liveness(mc_stack_liveness, 1);
 656
 657
 658         }
 659
 660         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 661           XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 662           MC_replay_liveness(mc_stack_liveness, 0);
 663         }
 664       }
 665
 666
 667     }else{
 668
 669       XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
 670
 671       MC_SET_RAW_MEM;
 672
 673       /* Create the new expanded graph_state */
 674       next_graph_state = MC_state_pair_new();
 675
 676       xbt_dynar_reset(successors);
 677
 678       MC_UNSET_RAW_MEM;
 679
 680
 681       cursor= 0;
 682       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 683
 684         res = MC_automaton_evaluate_label(transition_succ->label);
 685
 686         if(res == 1){ // enabled transition in automaton
 687           MC_SET_RAW_MEM;
 688           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 689           xbt_dynar_push(successors, &next_pair);
 690           MC_UNSET_RAW_MEM;
 691         }
 692
 693       }
 694
 695       cursor = 0;
 696
 697       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 698
 699         res = MC_automaton_evaluate_label(transition_succ->label);
 700
 701         if(res == 2){ // true transition in automaton
 702           MC_SET_RAW_MEM;
 703           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 704           xbt_dynar_push(successors, &next_pair);
 705           MC_UNSET_RAW_MEM;
 706         }
 707
 708       }
 709
 710       cursor = 0;
 711
 712       xbt_dynar_foreach(successors, cursor, pair_succ){
 713
 714         if(search_cycle == 1){
 715
 716           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 717
 718             if(reached(pair_succ->automaton_state)){
 719
 720               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
 721
 722               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 723               XBT_INFO("|             ACCEPTANCE CYCLE            |");
 724               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 725               XBT_INFO("Counter-example that violates formula :");
 726               MC_show_stack_liveness(mc_stack_liveness);
 727               MC_dump_stack_liveness(mc_stack_liveness);
 728               MC_print_statistics_pairs(mc_stats_pair);
 729               exit(0);
 730
 731             }else{
 732
 733               XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 734
 735               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 736
 737               MC_SET_RAW_MEM;
 738               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 739               MC_UNSET_RAW_MEM;
 740
 741               MC_ddfs(search_cycle);
 742
 743             }
 744
 745           }else{
 746
 747             MC_SET_RAW_MEM;
 748             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 749             MC_UNSET_RAW_MEM;
 750
 751             MC_ddfs(search_cycle);
 752
 753           }
 754
 755
 756         }else{
 757
 758           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 759
 760             set_pair_reached(pair_succ->automaton_state);
 761
 762             search_cycle = 1;
 763
 764             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 765
 766           }
 767
 768           MC_SET_RAW_MEM;
 769           xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 770           MC_UNSET_RAW_MEM;
 771
 772           MC_ddfs(search_cycle);
 773
 774         }
 775
 776         /* Restore system before checking others successors */
 777         if(cursor != xbt_dynar_length(successors) - 1)
 778           MC_replay_liveness(mc_stack_liveness, 1);
 779
 780       }
 781
 782     }
 783
 784   }else{
 785
 786     XBT_DEBUG("Max depth reached");
 787
 788   }
 789
 790   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
 791     XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
 792   }else{
 793     XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
 794   }
 795
 796
 797   MC_SET_RAW_MEM;
 798   remove_pair = xbt_fifo_shift(mc_stack_liveness);
 799   xbt_fifo_remove(mc_stack_liveness, remove_pair);
 800   remove_pair = NULL;
 801   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 802     remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t);
 803     pair_reached_free(remove_pair_reached);
 804     remove_pair_reached = NULL;
 805   }
 806   MC_UNSET_RAW_MEM;
 807
 808   if(raw_mem_set)
 809     MC_SET_RAW_MEM;
 810
 811 }