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