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   int reached_num;
 609
 610   mc_pair_t next_pair = NULL;
 611   mc_pair_t pair_succ;
 612
 613   mc_pair_t pair_to_remove;
 614
 615   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 616
 617     if(current_pair->requests > 0){
 618
 619       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 620
 621         /* Debug information */
 622
 623         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 624           req_str = MC_request_to_string(req, value);
 625           XBT_DEBUG("Execute: %s", req_str);
 626           xbt_free(req_str);
 627         }
 628
 629         MC_state_set_executed_request(current_pair->graph_state, req, value);
 630         mc_stats->executed_transitions++;
 631
 632         /* Answer the request */
 633         SIMIX_simcall_pre(req, value);
 634
 635         /* Wait for requests (schedules processes) */
 636         MC_wait_for_requests();
 637
 638         MC_SET_RAW_MEM;
 639
 640         /* Create the new expanded graph_state */
 641         next_graph_state = MC_state_new();
 642
 643         /* Get enabled process and insert it in the interleave set of the next graph_state */
 644         xbt_swag_foreach(process, simix_global->process_list){
 645           if(MC_process_is_enabled(process)){
 646             XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
 647           }
 648         }
 649
 650         xbt_swag_foreach(process, simix_global->process_list){
 651           if(MC_process_is_enabled(process)){
 652             MC_state_interleave_process(next_graph_state, process);
 653           }
 654         }
 655
 656         xbt_dynar_reset(successors);
 657
 658         MC_UNSET_RAW_MEM;
 659
 660
 661         cursor= 0;
 662         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 663
 664           res = MC_automaton_evaluate_label(transition_succ->label);
 665
 666           if(res == 1){ // enabled transition in automaton
 667             MC_SET_RAW_MEM;
 668             next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 669             xbt_dynar_push(successors, &next_pair);
 670             MC_UNSET_RAW_MEM;
 671           }
 672
 673         }
 674
 675         cursor = 0;
 676
 677         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 678
 679           res = MC_automaton_evaluate_label(transition_succ->label);
 680
 681           if(res == 2){ // true transition in automaton
 682             MC_SET_RAW_MEM;
 683             next_pair = MC_pair_new(next_graph_state, transition_succ->dst,  MC_state_interleave_size(next_graph_state));
 684             xbt_dynar_push(successors, &next_pair);
 685             MC_UNSET_RAW_MEM;
 686           }
 687
 688         }
 689
 690         cursor = 0;
 691
 692         xbt_dynar_foreach(successors, cursor, pair_succ){
 693
 694           if(search_cycle == 1){
 695
 696             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 697
 698               if((reached_num = is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state)) != -1){
 699
 700                 XBT_INFO("Next pair (depth = %d, %u interleave) already reached (equal to state %d) !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state), reached_num);
 701
 702                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 703                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 704                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 705                 XBT_INFO("Counter-example that violates formula :");
 706                 MC_show_stack_liveness(mc_stack_liveness);
 707                 MC_dump_stack_liveness(mc_stack_liveness);
 708                 MC_print_statistics(mc_stats);
 709                 xbt_abort();
 710
 711               }else{
 712
 713                 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 714
 715                   XBT_DEBUG("Next pair already visited !");
 716                   break;
 717
 718                 }else{
 719
 720                   XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 721
 722                   XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 723
 724                   MC_SET_RAW_MEM;
 725                   xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 726                   MC_UNSET_RAW_MEM;
 727
 728                   MC_ddfs(search_cycle);
 729
 730                 }
 731
 732               }
 733
 734             }else{
 735
 736               if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 737
 738                 XBT_DEBUG("Next pair already visited !");
 739                 break;
 740
 741               }else{
 742
 743                 MC_SET_RAW_MEM;
 744                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 745                 MC_UNSET_RAW_MEM;
 746
 747                 MC_ddfs(search_cycle);
 748               }
 749
 750             }
 751
 752           }else{
 753
 754             if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 755
 756               XBT_DEBUG("Next pair already visited !");
 757               break;
 758
 759             }else{
 760
 761               if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 762
 763                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 764
 765                 set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state);
 766
 767                 search_cycle = 1;
 768
 769                 XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 770
 771               }
 772
 773               MC_SET_RAW_MEM;
 774               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 775               MC_UNSET_RAW_MEM;
 776
 777               MC_ddfs(search_cycle);
 778
 779             }
 780
 781           }
 782
 783           /* Restore system before checking others successors */
 784           if(cursor != (xbt_dynar_length(successors) - 1))
 785             MC_replay_liveness(mc_stack_liveness, 1);
 786
 787         }
 788
 789         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 790           XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 791           MC_replay_liveness(mc_stack_liveness, 0);
 792         }
 793       }
 794
 795
 796     }else{
 797
 798       mc_stats->executed_transitions++;
 799
 800       XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
 801
 802       MC_SET_RAW_MEM;
 803
 804       /* Create the new expanded graph_state */
 805       next_graph_state = MC_state_new();
 806
 807       xbt_dynar_reset(successors);
 808
 809       MC_UNSET_RAW_MEM;
 810
 811
 812       cursor= 0;
 813       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 814
 815         res = MC_automaton_evaluate_label(transition_succ->label);
 816
 817         if(res == 1){ // enabled transition in automaton
 818           MC_SET_RAW_MEM;
 819           next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 820           xbt_dynar_push(successors, &next_pair);
 821           MC_UNSET_RAW_MEM;
 822         }
 823
 824       }
 825
 826       cursor = 0;
 827
 828       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 829
 830         res = MC_automaton_evaluate_label(transition_succ->label);
 831
 832         if(res == 2){ // true transition in automaton
 833           MC_SET_RAW_MEM;
 834           next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 835           xbt_dynar_push(successors, &next_pair);
 836           MC_UNSET_RAW_MEM;
 837         }
 838
 839       }
 840
 841       cursor = 0;
 842
 843       xbt_dynar_foreach(successors, cursor, pair_succ){
 844
 845         if(search_cycle == 1){
 846
 847           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 848
 849             if((reached_num = is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state)) != -1){
 850
 851               XBT_INFO("Next pair (depth = %d) already reached (equal to state %d)!", xbt_fifo_size(mc_stack_liveness) + 1, reached_num);
 852
 853               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 854               XBT_INFO("|             ACCEPTANCE CYCLE            |");
 855               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 856               XBT_INFO("Counter-example that violates formula :");
 857               MC_show_stack_liveness(mc_stack_liveness);
 858               MC_dump_stack_liveness(mc_stack_liveness);
 859               MC_print_statistics(mc_stats);
 860               xbt_abort();
 861
 862             }else{
 863
 864               if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 865
 866                 XBT_DEBUG("Next pair already visited !");
 867                 break;
 868
 869               }else{
 870
 871                 XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 872
 873                 XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 874
 875                 MC_SET_RAW_MEM;
 876                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 877                 MC_UNSET_RAW_MEM;
 878
 879                 MC_ddfs(search_cycle);
 880
 881               }
 882
 883             }
 884
 885           }else{
 886
 887             if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 888
 889               XBT_DEBUG("Next pair already visited !");
 890               break;
 891
 892             }else{
 893
 894               MC_SET_RAW_MEM;
 895               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 896               MC_UNSET_RAW_MEM;
 897
 898               MC_ddfs(search_cycle);
 899
 900             }
 901
 902           }
 903
 904
 905         }else{
 906
 907           if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 908
 909             XBT_DEBUG("Next pair already visited !");
 910             break;
 911
 912           }else{
 913
 914             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 915
 916               set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state);
 917
 918               search_cycle = 1;
 919
 920               XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 921
 922             }
 923
 924             MC_SET_RAW_MEM;
 925             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 926             MC_UNSET_RAW_MEM;
 927
 928             MC_ddfs(search_cycle);
 929
 930           }
 931
 932         }
 933
 934         /* Restore system before checking others successors */
 935         if(cursor != xbt_dynar_length(successors) - 1)
 936           MC_replay_liveness(mc_stack_liveness, 1);
 937
 938       }
 939
 940     }
 941
 942   }else{
 943
 944     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 945     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 946       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
 947       XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
 948     }
 949
 950   }
 951
 952   if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
 953     XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
 954   }else{
 955     XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
 956   }
 957
 958
 959   MC_SET_RAW_MEM;
 960   pair_to_remove = xbt_fifo_shift(mc_stack_liveness);
 961   xbt_fifo_remove(mc_stack_liveness, pair_to_remove);
 962   pair_to_remove = NULL;
 963   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 964     remove_acceptance_pair(current_pair->num);
 965   }
 966   MC_UNSET_RAW_MEM;
 967
 968 }