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