src/mc/mc_liveness.c

   1 /* Copyright (c) 2011-2013 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 /********* Global variables *********/
  14
  15 xbt_dynar_t acceptance_pairs;
  16 xbt_dynar_t visited_pairs;
  17 xbt_dynar_t successors;
  18
  19
  20 /********* Static functions *********/
  21
  22 static mc_acceptance_pair_t acceptance_pair_new(int num, xbt_automaton_state_t as){
  23
  24   mc_acceptance_pair_t new_pair = NULL;
  25   new_pair = xbt_new0(s_mc_acceptance_pair_t, 1);
  26   new_pair->num = num;
  27   new_pair->automaton_state = as;
  28   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
  29   new_pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
  30   new_pair->nb_processes = xbt_swag_size(simix_global->process_list);
  31   new_pair->system_state = MC_take_snapshot();
  32
  33   /* Get values of propositional symbols */
  34   int res;
  35   int_f_void_t f;
  36   unsigned int cursor = 0;
  37   xbt_automaton_propositional_symbol_t ps = NULL;
  38   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
  39     f = (int_f_void_t)ps->function;
  40     res = f();
  41     xbt_dynar_push_as(new_pair->prop_ato, int, res);
  42   }
  43
  44   return new_pair;
  45
  46 }
  47
  48 static int is_reached_acceptance_pair(int num, xbt_automaton_state_t as){
  49
  50   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  51
  52   MC_SET_RAW_MEM;
  53   mc_acceptance_pair_t new_pair = acceptance_pair_new(num, as);
  54   MC_UNSET_RAW_MEM;
  55
  56   if(xbt_dynar_is_empty(acceptance_pairs)){
  57
  58     MC_SET_RAW_MEM;
  59     xbt_dynar_push(acceptance_pairs, &new_pair);
  60     MC_UNSET_RAW_MEM;
  61
  62     if(raw_mem_set)
  63       MC_SET_RAW_MEM;
  64
  65     return -1;
  66
  67   }else{
  68
  69     MC_SET_RAW_MEM;
  70
  71     size_t current_bytes_used = new_pair->heap_bytes_used;
  72     int current_nb_processes = new_pair->nb_processes;
  73
  74     unsigned int cursor = 0;
  75     int previous_cursor = 0, next_cursor = 0;
  76     int start = 0;
  77     int end = xbt_dynar_length(acceptance_pairs) - 1;
  78
  79     mc_acceptance_pair_t pair_test = NULL;
  80     size_t bytes_used_test;
  81     int nb_processes_test;
  82     int same_processes_and_bytes_not_found = 1;
  83
  84     while(start <= end && same_processes_and_bytes_not_found){
  85       cursor = (start + end) / 2;
  86       pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_acceptance_pair_t);
  87       bytes_used_test = pair_test->heap_bytes_used;
  88       nb_processes_test = pair_test->nb_processes;
  89       if(nb_processes_test < current_nb_processes)
  90         start = cursor + 1;
  91       if(nb_processes_test > current_nb_processes)
  92         end = cursor - 1;
  93       if(nb_processes_test == current_nb_processes){
  94         if(bytes_used_test < current_bytes_used)
  95           start = cursor + 1;
  96         if(bytes_used_test > current_bytes_used)
  97           end = cursor - 1;
  98         if(bytes_used_test == current_bytes_used){
  99           same_processes_and_bytes_not_found = 0;
 100           if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
 101             if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
 102               if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
 103                 if(raw_mem_set)
 104                   MC_SET_RAW_MEM;
 105                 else
 106                   MC_UNSET_RAW_MEM;
 107                 return pair_test->num;
 108               }
 109             }
 110           }
 111           /* Search another pair with same number of bytes used in std_heap */
 112           previous_cursor = cursor - 1;
 113           while(previous_cursor >= 0){
 114             pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, previous_cursor, mc_acceptance_pair_t);
 115             bytes_used_test = pair_test->system_state->heap_bytes_used;
 116             if(bytes_used_test != current_bytes_used)
 117               break;
 118             if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
 119               if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
 120                 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
 121                   if(raw_mem_set)
 122                     MC_SET_RAW_MEM;
 123                   else
 124                     MC_UNSET_RAW_MEM;
 125                   return pair_test->num;
 126                 }
 127               }
 128             }
 129             previous_cursor--;
 130           }
 131           next_cursor = cursor + 1;
 132           while(next_cursor < xbt_dynar_length(acceptance_pairs)){
 133             pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, next_cursor, mc_acceptance_pair_t);
 134             bytes_used_test = pair_test->system_state->heap_bytes_used;
 135             if(bytes_used_test != current_bytes_used)
 136               break;
 137             if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
 138               if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
 139                 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
 140                   if(raw_mem_set)
 141                     MC_SET_RAW_MEM;
 142                   else
 143                     MC_UNSET_RAW_MEM;
 144                   return pair_test->num;
 145                 }
 146               }
 147             }
 148             next_cursor++;
 149           }
 150         }
 151       }
 152     }
 153
 154     pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_acceptance_pair_t);
 155     bytes_used_test = pair_test->heap_bytes_used;
 156
 157     if(bytes_used_test < current_bytes_used)
 158       xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &new_pair);
 159     else
 160       xbt_dynar_insert_at(acceptance_pairs, cursor, &new_pair);
 161
 162     MC_UNSET_RAW_MEM;
 163
 164     if(raw_mem_set)
 165       MC_SET_RAW_MEM;
 166
 167     return -1;
 168
 169   }
 170
 171 }
 172
 173
 174 static void set_acceptance_pair_reached(int num, xbt_automaton_state_t as){
 175
 176   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 177
 178   MC_SET_RAW_MEM;
 179   mc_acceptance_pair_t new_pair = acceptance_pair_new(num, as);
 180   MC_UNSET_RAW_MEM;
 181
 182   if(xbt_dynar_is_empty(acceptance_pairs)){
 183
 184      MC_SET_RAW_MEM;
 185      xbt_dynar_push(acceptance_pairs, &new_pair);
 186      MC_UNSET_RAW_MEM;
 187
 188   }else{
 189
 190     MC_SET_RAW_MEM;
 191
 192     size_t current_bytes_used = new_pair->heap_bytes_used;
 193     int current_nb_processes = new_pair->nb_processes;
 194
 195     unsigned int cursor = 0;
 196     int start = 0;
 197     int end = xbt_dynar_length(acceptance_pairs) - 1;
 198
 199     mc_acceptance_pair_t pair_test = NULL;
 200     size_t bytes_used_test = 0;
 201     int nb_processes_test;
 202
 203     while(start <= end){
 204       cursor = (start + end) / 2;
 205       pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_acceptance_pair_t);
 206       bytes_used_test = pair_test->heap_bytes_used;
 207       nb_processes_test = pair_test->nb_processes;
 208       if(nb_processes_test < current_nb_processes)
 209         start = cursor + 1;
 210       if(nb_processes_test > current_nb_processes)
 211         end = cursor - 1;
 212       if(nb_processes_test == current_nb_processes){
 213         if(bytes_used_test < current_bytes_used)
 214           start = cursor + 1;
 215         if(bytes_used_test > current_bytes_used)
 216           end = cursor - 1;
 217         if(bytes_used_test == current_bytes_used)
 218           break;
 219       }
 220     }
 221
 222     if(bytes_used_test < current_bytes_used)
 223       xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &new_pair);
 224     else
 225       xbt_dynar_insert_at(acceptance_pairs, cursor, &new_pair);
 226
 227     MC_UNSET_RAW_MEM;
 228
 229   }
 230
 231   if(raw_mem_set)
 232     MC_SET_RAW_MEM;
 233
 234 }
 235
 236 static void remove_acceptance_pair(int num_pair){
 237
 238   unsigned int cursor = 0;
 239   mc_acceptance_pair_t current_pair;
 240
 241   xbt_dynar_foreach(acceptance_pairs, cursor, current_pair){
 242     if(current_pair->num == num_pair)
 243       break;
 244   }
 245
 246   xbt_dynar_remove_at(acceptance_pairs, cursor, NULL);
 247
 248 }
 249
 250 static mc_visited_pair_t visited_pair_new(int num, xbt_automaton_state_t as){
 251
 252   mc_visited_pair_t new_pair = NULL;
 253   new_pair = xbt_new0(s_mc_visited_pair_t, 1);
 254   new_pair->automaton_state = as;
 255   new_pair->num = num;
 256   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 257   new_pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
 258   new_pair->nb_processes = xbt_swag_size(simix_global->process_list);
 259   new_pair->system_state = MC_take_snapshot();
 260
 261   /* Get values of propositional symbols */
 262   int res;
 263   int_f_void_t f;
 264   unsigned int cursor = 0;
 265   xbt_automaton_propositional_symbol_t ps = NULL;
 266   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 267     f = (int_f_void_t)ps->function;
 268     res = f();
 269     xbt_dynar_push_as(new_pair->prop_ato, int, res);
 270   }
 271
 272   return new_pair;
 273
 274 }
 275
 276 static int is_visited_pair(int num, xbt_automaton_state_t as){
 277
 278   if(_sg_mc_visited == 0)
 279     return -1;
 280
 281   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 282
 283   MC_SET_RAW_MEM;
 284   mc_visited_pair_t new_pair = visited_pair_new(num, as);
 285   MC_UNSET_RAW_MEM;
 286
 287   if(xbt_dynar_is_empty(visited_pairs)){
 288
 289     MC_SET_RAW_MEM;
 290     xbt_dynar_push(visited_pairs, &new_pair);
 291     MC_UNSET_RAW_MEM;
 292
 293     if(raw_mem_set)
 294       MC_SET_RAW_MEM;
 295
 296     return -1;
 297
 298   }else{
 299
 300     MC_SET_RAW_MEM;
 301
 302     size_t current_bytes_used = new_pair->heap_bytes_used;
 303     int current_nb_processes = new_pair->nb_processes;
 304
 305     unsigned int cursor = 0;
 306     int previous_cursor = 0, next_cursor = 0;
 307     int start = 0;
 308     int end = xbt_dynar_length(visited_pairs) - 1;
 309
 310     mc_visited_pair_t pair_test = NULL;
 311     size_t bytes_used_test;
 312     int nb_processes_test;
 313     int same_processes_and_bytes_not_found = 1;
 314
 315     while(start <= end && same_processes_and_bytes_not_found){
 316       cursor = (start + end) / 2;
 317       pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
 318       bytes_used_test = pair_test->heap_bytes_used;
 319       nb_processes_test = pair_test->nb_processes;
 320       if(nb_processes_test < current_nb_processes)
 321         start = cursor + 1;
 322       if(nb_processes_test > current_nb_processes)
 323         end = cursor - 1;
 324       if(nb_processes_test == current_nb_processes){
 325         if(bytes_used_test < current_bytes_used)
 326           start = cursor + 1;
 327         if(bytes_used_test > current_bytes_used)
 328           end = cursor - 1;
 329         if(bytes_used_test == current_bytes_used){
 330           same_processes_and_bytes_not_found = 0;
 331           if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
 332             if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
 333               if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
 334                 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
 335                 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
 336                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
 337                 if(raw_mem_set)
 338                   MC_SET_RAW_MEM;
 339                 else
 340                   MC_UNSET_RAW_MEM;
 341                 return pair_test->num;
 342               }
 343             }
 344           }
 345           /* Search another pair with same number of bytes used in std_heap */
 346           previous_cursor = cursor - 1;
 347           while(previous_cursor >= 0){
 348             pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, previous_cursor, mc_visited_pair_t);
 349             bytes_used_test = pair_test->system_state->heap_bytes_used;
 350             if(bytes_used_test != current_bytes_used)
 351               break;
 352             if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
 353               if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
 354                 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
 355                   xbt_dynar_remove_at(visited_pairs, previous_cursor, NULL);
 356                   xbt_dynar_insert_at(visited_pairs, previous_cursor, &new_pair);
 357                   XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
 358                   if(raw_mem_set)
 359                     MC_SET_RAW_MEM;
 360                   else
 361                     MC_UNSET_RAW_MEM;
 362                   return pair_test->num;
 363                 }
 364               }
 365             }
 366             previous_cursor--;
 367           }
 368           next_cursor = cursor + 1;
 369           while(next_cursor < xbt_dynar_length(visited_pairs)){
 370             pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, next_cursor, mc_visited_pair_t);
 371             bytes_used_test = pair_test->system_state->heap_bytes_used;
 372             if(bytes_used_test != current_bytes_used)
 373               break;
 374             if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
 375               if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
 376                 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
 377                   xbt_dynar_remove_at(visited_pairs, next_cursor, NULL);
 378                   xbt_dynar_insert_at(visited_pairs, next_cursor, &new_pair);
 379                   XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
 380                   if(raw_mem_set)
 381                     MC_SET_RAW_MEM;
 382                   else
 383                     MC_UNSET_RAW_MEM;
 384                   return pair_test->num;
 385                 }
 386               }
 387             }
 388             next_cursor++;
 389           }
 390         }
 391       }
 392     }
 393
 394     pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
 395     bytes_used_test = pair_test->heap_bytes_used;
 396
 397     if(bytes_used_test < current_bytes_used)
 398       xbt_dynar_insert_at(visited_pairs, cursor + 1, &new_pair);
 399     else
 400       xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
 401
 402     if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
 403       int min = mc_stats->expanded_states;
 404       unsigned int cursor2 = 0;
 405       unsigned int index = 0;
 406       xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
 407         if(pair_test->num < min){
 408           index = cursor2;
 409           min = pair_test->num;
 410         }
 411       }
 412       xbt_dynar_remove_at(visited_pairs, index, NULL);
 413     }
 414
 415     /*cursor = 0;
 416     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
 417       fprintf(stderr, "Visited pair %d, nb_processes %d and heap_bytes_used %zu\n", pair_test->num, pair_test->nb_processes, pair_test->heap_bytes_used);
 418       }*/
 419
 420     MC_UNSET_RAW_MEM;
 421
 422     if(raw_mem_set)
 423       MC_SET_RAW_MEM;
 424
 425     return -1;
 426
 427   }
 428
 429 }
 430
 431 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l){
 432
 433   switch(l->type){
 434   case 0 : {
 435     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 436     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 437     return (left_res || right_res);
 438   }
 439   case 1 : {
 440     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 441     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 442     return (left_res && right_res);
 443   }
 444   case 2 : {
 445     int res = MC_automaton_evaluate_label(l->u.exp_not);
 446     return (!res);
 447   }
 448   case 3 : {
 449     unsigned int cursor = 0;
 450     xbt_automaton_propositional_symbol_t p = NULL;
 451     int_f_void_t f;
 452     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
 453       if(strcmp(p->pred, l->u.predicat) == 0){
 454         f = (int_f_void_t)p->function;
 455         return f();
 456       }
 457     }
 458     return -1;
 459   }
 460   case 4 : {
 461     return 2;
 462   }
 463   default :
 464     return -1;
 465   }
 466 }
 467
 468
 469 /********* Free functions *********/
 470
 471 static void visited_pair_free(mc_visited_pair_t pair){
 472   if(pair){
 473     xbt_dynar_free(&(pair->prop_ato));
 474     MC_free_snapshot(pair->system_state);
 475     xbt_free(pair);
 476   }
 477 }
 478
 479 static void visited_pair_free_voidp(void *p){
 480   visited_pair_free((mc_visited_pair_t) * (void **) p);
 481 }
 482
 483 static void acceptance_pair_free(mc_acceptance_pair_t pair){
 484   if(pair){
 485     xbt_dynar_free(&(pair->prop_ato));
 486     MC_free_snapshot(pair->system_state);
 487     xbt_free(pair);
 488   }
 489 }
 490
 491 static void acceptance_pair_free_voidp(void *p){
 492   acceptance_pair_free((mc_acceptance_pair_t) * (void **) p);
 493 }
 494
 495
 496 /********* DDFS Algorithm *********/
 497
 498
 499 void MC_ddfs_init(void){
 500
 501   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 502
 503   XBT_DEBUG("**************************************************");
 504   XBT_DEBUG("Double-DFS init");
 505   XBT_DEBUG("**************************************************");
 506
 507   mc_pair_t mc_initial_pair = NULL;
 508   mc_state_t initial_graph_state = NULL;
 509   smx_process_t process;
 510
 511
 512   MC_wait_for_requests();
 513
 514   MC_SET_RAW_MEM;
 515
 516   initial_graph_state = MC_state_new();
 517   xbt_swag_foreach(process, simix_global->process_list){
 518     if(MC_process_is_enabled(process)){
 519       MC_state_interleave_process(initial_graph_state, process);
 520     }
 521   }
 522
 523   acceptance_pairs = xbt_dynar_new(sizeof(mc_acceptance_pair_t), acceptance_pair_free_voidp);
 524   visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), visited_pair_free_voidp);
 525   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 526
 527   /* Save the initial state */
 528   initial_state_liveness->snapshot = MC_take_snapshot();
 529
 530   MC_UNSET_RAW_MEM;
 531
 532   unsigned int cursor = 0;
 533   xbt_automaton_state_t automaton_state;
 534
 535   xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
 536     if(automaton_state->type == -1){
 537
 538       MC_SET_RAW_MEM;
 539       mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));
 540       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 541       MC_UNSET_RAW_MEM;
 542
 543       if(cursor != 0){
 544         MC_restore_snapshot(initial_state_liveness->snapshot);
 545         MC_UNSET_RAW_MEM;
 546       }
 547
 548       MC_ddfs(0);
 549
 550     }else{
 551       if(automaton_state->type == 2){
 552
 553         MC_SET_RAW_MEM;
 554         mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));
 555         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 556         MC_UNSET_RAW_MEM;
 557
 558         set_acceptance_pair_reached(mc_initial_pair->num, automaton_state);
 559
 560         if(cursor != 0){
 561           MC_restore_snapshot(initial_state_liveness->snapshot);
 562           MC_UNSET_RAW_MEM;
 563         }
 564
 565         MC_ddfs(1);
 566
 567       }
 568     }
 569   }
 570
 571   if(initial_state_liveness->raw_mem_set)
 572     MC_SET_RAW_MEM;
 573   else
 574     MC_UNSET_RAW_MEM;
 575
 576
 577 }
 578
 579
 580 void MC_ddfs(int search_cycle){
 581
 582   smx_process_t process;
 583   mc_pair_t current_pair = NULL;
 584
 585   if(xbt_fifo_size(mc_stack_liveness) == 0)
 586     return;
 587
 588
 589   /* Get current pair */
 590   current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 591
 592   /* Update current state in buchi automaton */
 593   _mc_property_automaton->current_state = current_pair->automaton_state;
 594
 595
 596   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
 597
 598   mc_stats->visited_pairs++;
 599
 600   int value;
 601   mc_state_t next_graph_state = NULL;
 602   smx_simcall_t req = NULL;
 603   char *req_str;
 604
 605   xbt_automaton_transition_t transition_succ;
 606   unsigned int cursor = 0;
 607   int res;
 608
 609   mc_pair_t next_pair = NULL;
 610   mc_pair_t pair_succ;
 611
 612   mc_pair_t pair_to_remove;
 613
 614   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 615
 616     if(current_pair->requests > 0){
 617
 618       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 619
 620         /* Debug information */
 621
 622         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 623           req_str = MC_request_to_string(req, value);
 624           XBT_DEBUG("Execute: %s", req_str);
 625           xbt_free(req_str);
 626         }
 627
 628         MC_state_set_executed_request(current_pair->graph_state, req, value);
 629         mc_stats->executed_transitions++;
 630
 631         /* Answer the request */
 632         SIMIX_simcall_pre(req, value);
 633
 634         /* Wait for requests (schedules processes) */
 635         MC_wait_for_requests();
 636
 637         MC_SET_RAW_MEM;
 638
 639         /* Create the new expanded graph_state */
 640         next_graph_state = MC_state_new();
 641
 642         /* Get enabled process and insert it in the interleave set of the next graph_state */
 643         xbt_swag_foreach(process, simix_global->process_list){
 644           if(MC_process_is_enabled(process)){
 645             XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
 646           }
 647         }
 648
 649         xbt_swag_foreach(process, simix_global->process_list){
 650           if(MC_process_is_enabled(process)){
 651             MC_state_interleave_process(next_graph_state, process);
 652           }
 653         }
 654
 655         xbt_dynar_reset(successors);
 656
 657         MC_UNSET_RAW_MEM;
 658
 659
 660         cursor= 0;
 661         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 662
 663           res = MC_automaton_evaluate_label(transition_succ->label);
 664
 665           if(res == 1){ // enabled transition in automaton
 666             MC_SET_RAW_MEM;
 667             next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 668             xbt_dynar_push(successors, &next_pair);
 669             MC_UNSET_RAW_MEM;
 670           }
 671
 672         }
 673
 674         cursor = 0;
 675
 676         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 677
 678           res = MC_automaton_evaluate_label(transition_succ->label);
 679
 680           if(res == 2){ // true transition in automaton
 681             MC_SET_RAW_MEM;
 682             next_pair = MC_pair_new(next_graph_state, transition_succ->dst,  MC_state_interleave_size(next_graph_state));
 683             xbt_dynar_push(successors, &next_pair);
 684             MC_UNSET_RAW_MEM;
 685           }
 686
 687         }
 688
 689         cursor = 0;
 690
 691         xbt_dynar_foreach(successors, cursor, pair_succ){
 692
 693           if(search_cycle == 1){
 694
 695             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 696
 697               if(is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 698
 699                 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));
 700
 701                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 702                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 703                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 704                 XBT_INFO("Counter-example that violates formula :");
 705                 MC_show_stack_liveness(mc_stack_liveness);
 706                 MC_dump_stack_liveness(mc_stack_liveness);
 707                 MC_print_statistics(mc_stats);
 708                 xbt_abort();
 709
 710               }else{
 711
 712                 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 713
 714                   XBT_DEBUG("Next pair already visited !");
 715                   break;
 716
 717                 }else{
 718
 719                   XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 720
 721                   XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 722
 723                   MC_SET_RAW_MEM;
 724                   xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 725                   MC_UNSET_RAW_MEM;
 726
 727                   MC_ddfs(search_cycle);
 728
 729                 }
 730
 731               }
 732
 733             }else{
 734
 735               if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 736
 737                 XBT_DEBUG("Next pair already visited !");
 738                 break;
 739
 740               }else{
 741
 742                 MC_SET_RAW_MEM;
 743                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 744                 MC_UNSET_RAW_MEM;
 745
 746                 MC_ddfs(search_cycle);
 747               }
 748
 749             }
 750
 751           }else{
 752
 753             if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 754
 755               XBT_DEBUG("Next pair already visited !");
 756               break;
 757
 758             }else{
 759
 760               if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 761
 762                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 763
 764                 set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state);
 765
 766                 search_cycle = 1;
 767
 768                 XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 769
 770               }
 771
 772               MC_SET_RAW_MEM;
 773               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 774               MC_UNSET_RAW_MEM;
 775
 776               MC_ddfs(search_cycle);
 777
 778             }
 779
 780           }
 781
 782           /* Restore system before checking others successors */
 783           if(cursor != (xbt_dynar_length(successors) - 1))
 784             MC_replay_liveness(mc_stack_liveness, 1);
 785
 786         }
 787
 788         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 789           XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 790           MC_replay_liveness(mc_stack_liveness, 0);
 791         }
 792       }
 793
 794
 795     }else{
 796
 797       mc_stats->executed_transitions++;
 798
 799       XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
 800
 801       MC_SET_RAW_MEM;
 802
 803       /* Create the new expanded graph_state */
 804       next_graph_state = MC_state_new();
 805
 806       xbt_dynar_reset(successors);
 807
 808       MC_UNSET_RAW_MEM;
 809
 810
 811       cursor= 0;
 812       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 813
 814         res = MC_automaton_evaluate_label(transition_succ->label);
 815
 816         if(res == 1){ // enabled transition in automaton
 817           MC_SET_RAW_MEM;
 818           next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 819           xbt_dynar_push(successors, &next_pair);
 820           MC_UNSET_RAW_MEM;
 821         }
 822
 823       }
 824
 825       cursor = 0;
 826
 827       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 828
 829         res = MC_automaton_evaluate_label(transition_succ->label);
 830
 831         if(res == 2){ // true transition in automaton
 832           MC_SET_RAW_MEM;
 833           next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 834           xbt_dynar_push(successors, &next_pair);
 835           MC_UNSET_RAW_MEM;
 836         }
 837
 838       }
 839
 840       cursor = 0;
 841
 842       xbt_dynar_foreach(successors, cursor, pair_succ){
 843
 844         if(search_cycle == 1){
 845
 846           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 847
 848             if(is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 849
 850               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
 851
 852               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 853               XBT_INFO("|             ACCEPTANCE CYCLE            |");
 854               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 855               XBT_INFO("Counter-example that violates formula :");
 856               MC_show_stack_liveness(mc_stack_liveness);
 857               MC_dump_stack_liveness(mc_stack_liveness);
 858               MC_print_statistics(mc_stats);
 859               xbt_abort();
 860
 861             }else{
 862
 863               if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 864
 865                 XBT_DEBUG("Next pair already visited !");
 866                 break;
 867
 868               }else{
 869
 870                 XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 871
 872                 XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 873
 874                 MC_SET_RAW_MEM;
 875                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 876                 MC_UNSET_RAW_MEM;
 877
 878                 MC_ddfs(search_cycle);
 879
 880               }
 881
 882             }
 883
 884           }else{
 885
 886             if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 887
 888               XBT_DEBUG("Next pair already visited !");
 889               break;
 890
 891             }else{
 892
 893               MC_SET_RAW_MEM;
 894               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 895               MC_UNSET_RAW_MEM;
 896
 897               MC_ddfs(search_cycle);
 898
 899             }
 900
 901           }
 902
 903
 904         }else{
 905
 906           if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 907
 908             XBT_DEBUG("Next pair already visited !");
 909             break;
 910
 911           }else{
 912
 913             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 914
 915               set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state);
 916
 917               search_cycle = 1;
 918
 919               XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 920
 921             }
 922
 923             MC_SET_RAW_MEM;
 924             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 925             MC_UNSET_RAW_MEM;
 926
 927             MC_ddfs(search_cycle);
 928
 929           }
 930
 931         }
 932
 933         /* Restore system before checking others successors */
 934         if(cursor != xbt_dynar_length(successors) - 1)
 935           MC_replay_liveness(mc_stack_liveness, 1);
 936
 937       }
 938
 939     }
 940
 941   }else{
 942
 943     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 944     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 945       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
 946       XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
 947     }
 948
 949   }
 950
 951   if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
 952     XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
 953   }else{
 954     XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
 955   }
 956
 957
 958   MC_SET_RAW_MEM;
 959   pair_to_remove = xbt_fifo_shift(mc_stack_liveness);
 960   xbt_fifo_remove(mc_stack_liveness, pair_to_remove);
 961   pair_to_remove = NULL;
 962   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 963     remove_acceptance_pair(current_pair->num);
 964   }
 965   MC_UNSET_RAW_MEM;
 966
 967 }