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       if(nb_processes_test > current_nb_processes)
  87         end = cursor - 1;
  88       if(nb_processes_test == current_nb_processes){
  89         if(bytes_used_test < current_bytes_used)
  90           start = cursor + 1;
  91         if(bytes_used_test > current_bytes_used)
  92           end = cursor - 1;
  93         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       if(nb_processes_test > current_nb_processes)
 314         end = cursor - 1;
 315       if(nb_processes_test == current_nb_processes){
 316         if(bytes_used_test < current_bytes_used)
 317           start = cursor + 1;
 318         if(bytes_used_test > current_bytes_used)
 319           end = cursor - 1;
 320         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
 510   MC_UNSET_RAW_MEM;
 511
 512   unsigned int cursor = 0;
 513   xbt_automaton_state_t automaton_state;
 514
 515   xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
 516     if(automaton_state->type == -1){ /* Initial automaton state */
 517
 518       MC_SET_RAW_MEM;
 519
 520       initial_pair = MC_pair_new();
 521       initial_pair->automaton_state = automaton_state;
 522       initial_pair->graph_state = MC_state_new();
 523       initial_pair->atomic_propositions = get_atomic_propositions_values();
 524
 525       /* Get enabled process and insert it in the interleave set of the graph_state */
 526       xbt_swag_foreach(process, simix_global->process_list){
 527         if(MC_process_is_enabled(process)){
 528           MC_state_interleave_process(initial_pair->graph_state, process);
 529         }
 530       }
 531
 532       initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
 533       initial_pair->search_cycle = 0;
 534
 535       xbt_fifo_unshift(mc_stack_liveness, initial_pair);
 536
 537       MC_UNSET_RAW_MEM;
 538
 539       MC_ddfs();
 540
 541       if(cursor != 0){
 542         MC_restore_snapshot(initial_state_liveness->snapshot);
 543         MC_UNSET_RAW_MEM;
 544       }
 545
 546
 547     }else if(automaton_state->type == 2){ /* Acceptance automaton state */
 548
 549       MC_SET_RAW_MEM;
 550
 551       initial_pair = MC_pair_new();
 552       initial_pair->automaton_state = automaton_state;
 553       initial_pair->graph_state = MC_state_new();
 554       initial_pair->atomic_propositions = get_atomic_propositions_values();
 555
 556       /* Get enabled process and insert it in the interleave set of the graph_state */
 557       xbt_swag_foreach(process, simix_global->process_list){
 558         if(MC_process_is_enabled(process)){
 559           MC_state_interleave_process(initial_pair->graph_state, process);
 560         }
 561       }
 562
 563       initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
 564       initial_pair->search_cycle = 1;
 565
 566       xbt_fifo_unshift(mc_stack_liveness, initial_pair);
 567
 568       MC_UNSET_RAW_MEM;
 569
 570       set_acceptance_pair_reached(initial_pair);
 571
 572       MC_ddfs();
 573
 574       if(cursor != 0){
 575         MC_restore_snapshot(initial_state_liveness->snapshot);
 576         MC_UNSET_RAW_MEM;
 577       }
 578     }
 579   }
 580
 581   if(initial_state_liveness->raw_mem_set)
 582     MC_SET_RAW_MEM;
 583   else
 584     MC_UNSET_RAW_MEM;
 585
 586
 587 }
 588
 589
 590 void MC_ddfs(){
 591
 592   smx_process_t process;
 593   mc_pair_t current_pair = NULL;
 594
 595   if(xbt_fifo_size(mc_stack_liveness) == 0)
 596     return;
 597
 598   /* Get current pair */
 599   current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 600
 601   /* Update current state in buchi automaton */
 602   _mc_property_automaton->current_state = current_pair->automaton_state;
 603
 604   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), current_pair->search_cycle);
 605
 606   mc_stats->visited_pairs++;
 607
 608   int value;
 609   smx_simcall_t req = NULL;
 610   char *req_str;
 611
 612   xbt_automaton_transition_t transition_succ;
 613   unsigned int cursor = 0;
 614   int res;
 615   int reached_num, visited_num;
 616   int new_pair = 0;
 617
 618   mc_pair_t next_pair = NULL;
 619   xbt_dynar_t prop_values = NULL;
 620
 621   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 622
 623     if(current_pair->requests > 0){
 624
 625       if(current_pair->search_cycle){
 626
 627         if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 628
 629           if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
 630
 631             XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
 632
 633             MC_SET_RAW_MEM;
 634             xbt_fifo_shift(mc_stack_liveness);
 635             MC_UNSET_RAW_MEM;
 636
 637             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 638             XBT_INFO("|             ACCEPTANCE CYCLE            |");
 639             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 640             XBT_INFO("Counter-example that violates formula :");
 641             MC_show_stack_liveness(mc_stack_liveness);
 642             MC_dump_stack_liveness(mc_stack_liveness);
 643             MC_print_statistics(mc_stats);
 644             xbt_abort();
 645
 646           }
 647         }
 648       }
 649
 650       if((visited_num = is_visited_pair(current_pair)) != -1){
 651
 652         XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num);
 653
 654       }else{
 655
 656         while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 657
 658           /* Debug information */
 659
 660           if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 661             req_str = MC_request_to_string(req, value);
 662             XBT_DEBUG("Execute: %s", req_str);
 663             xbt_free(req_str);
 664           }
 665
 666           MC_state_set_executed_request(current_pair->graph_state, req, value);
 667           mc_stats->executed_transitions++;
 668
 669           /* Answer the request */
 670           SIMIX_simcall_pre(req, value);
 671
 672           /* Wait for requests (schedules processes) */
 673           MC_wait_for_requests();
 674
 675           MC_SET_RAW_MEM;
 676           prop_values = get_atomic_propositions_values();
 677           MC_UNSET_RAW_MEM;
 678
 679           /* Evaluate enabled transition according to atomic propositions values */
 680           cursor= 0;
 681           xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 682
 683             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 684
 685             if(res == 1){ // enabled transition in automaton
 686
 687               if(new_pair)
 688                MC_replay_liveness(mc_stack_liveness, 1);
 689
 690               MC_SET_RAW_MEM;
 691
 692               next_pair = MC_pair_new();
 693               next_pair->graph_state = MC_state_new();
 694               next_pair->automaton_state = transition_succ->dst;
 695               next_pair->atomic_propositions = get_atomic_propositions_values();
 696
 697               /* Get enabled process and insert it in the interleave set of the next graph_state */
 698               xbt_swag_foreach(process, simix_global->process_list){
 699                 if(MC_process_is_enabled(process)){
 700                   MC_state_interleave_process(next_pair->graph_state, process);
 701                 }
 702               }
 703
 704               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 705
 706               if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 707                 next_pair->search_cycle = 1;
 708
 709               xbt_fifo_unshift(mc_stack_liveness, next_pair);
 710
 711               if(mc_stats->expanded_pairs%1000000 == 0)
 712                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 713
 714               MC_UNSET_RAW_MEM;
 715
 716               new_pair = 1;
 717
 718               MC_ddfs();
 719
 720             }
 721
 722           }
 723
 724           /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
 725           cursor = 0;
 726           xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 727
 728             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 729
 730             if(res == 2){ // true transition in automaton
 731
 732               if(new_pair)
 733                 MC_replay_liveness(mc_stack_liveness, 1);
 734
 735               MC_SET_RAW_MEM;
 736
 737               next_pair = MC_pair_new();
 738               next_pair->graph_state = MC_state_new();
 739               next_pair->automaton_state = transition_succ->dst;
 740               next_pair->atomic_propositions = get_atomic_propositions_values();
 741
 742               /* Get enabled process and insert it in the interleave set of the next graph_state */
 743               xbt_swag_foreach(process, simix_global->process_list){
 744                 if(MC_process_is_enabled(process)){
 745                   MC_state_interleave_process(next_pair->graph_state, process);
 746                 }
 747               }
 748
 749               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 750
 751               if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 752                 next_pair->search_cycle = 1;
 753
 754               xbt_fifo_unshift(mc_stack_liveness, next_pair);
 755
 756               if(mc_stats->expanded_pairs%1000000 == 0)
 757                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 758
 759               MC_UNSET_RAW_MEM;
 760
 761               new_pair = 1;
 762
 763               MC_ddfs();
 764
 765             }
 766
 767           }
 768
 769           if(MC_state_interleave_size(current_pair->graph_state) > 0){
 770             XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 771             MC_replay_liveness(mc_stack_liveness, 0);
 772           }
 773
 774         }
 775
 776       }
 777
 778     }else{
 779
 780       mc_stats->executed_transitions++;
 781
 782       XBT_DEBUG("No request to execute in this state, search evolution in Büchi Automaton.");
 783
 784       if(current_pair->search_cycle){
 785
 786         if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 787
 788           if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
 789
 790             XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
 791
 792             MC_SET_RAW_MEM;
 793             xbt_fifo_shift(mc_stack_liveness);
 794             MC_UNSET_RAW_MEM;
 795
 796             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 797             XBT_INFO("|             ACCEPTANCE CYCLE            |");
 798             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 799             XBT_INFO("Counter-example that violates formula :");
 800             MC_show_stack_liveness(mc_stack_liveness);
 801             MC_dump_stack_liveness(mc_stack_liveness);
 802             MC_print_statistics(mc_stats);
 803             xbt_abort();
 804
 805           }
 806         }
 807       }
 808
 809       if((visited_num = is_visited_pair(current_pair)) != -1){
 810
 811         XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num);
 812
 813       }else{
 814
 815         MC_SET_RAW_MEM;
 816         prop_values = get_atomic_propositions_values();
 817         MC_UNSET_RAW_MEM;
 818
 819         /* Evaluate enabled transition according to atomic propositions values */
 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, prop_values);
 824
 825           if(res == 1){ // enabled transition in automaton
 826
 827             if(new_pair)
 828               MC_replay_liveness(mc_stack_liveness, 1);
 829
 830             MC_SET_RAW_MEM;
 831
 832             next_pair = MC_pair_new();
 833             next_pair->graph_state = MC_state_new();
 834             next_pair->automaton_state = transition_succ->dst;
 835             next_pair->atomic_propositions = get_atomic_propositions_values();
 836             next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 837
 838             if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 839               next_pair->search_cycle = 1;
 840
 841             xbt_fifo_unshift(mc_stack_liveness, next_pair);
 842
 843             if(mc_stats->expanded_pairs%1000 == 0)
 844               XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 845
 846             MC_UNSET_RAW_MEM;
 847
 848             new_pair = 1;
 849
 850             MC_ddfs();
 851
 852           }
 853
 854         }
 855
 856         /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
 857         cursor = 0;
 858         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 859
 860           res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
 861
 862           if(res == 2){ // true transition in automaton
 863
 864             if(new_pair)
 865               MC_replay_liveness(mc_stack_liveness, 1);
 866
 867             MC_SET_RAW_MEM;
 868
 869             next_pair = MC_pair_new();
 870             next_pair->graph_state = MC_state_new();
 871             next_pair->automaton_state = transition_succ->dst;
 872             next_pair->atomic_propositions = get_atomic_propositions_values();
 873             next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 874
 875             if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
 876               next_pair->search_cycle = 1;
 877
 878             xbt_fifo_unshift(mc_stack_liveness, next_pair);
 879
 880             if(mc_stats->expanded_pairs%1000 == 0)
 881               XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 882
 883             MC_UNSET_RAW_MEM;
 884
 885             new_pair = 1;
 886
 887             MC_ddfs();
 888
 889           }
 890
 891         }
 892       }
 893     }
 894
 895   }else{
 896
 897     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 898     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 899       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
 900       if(_sg_mc_max_depth == 1000)
 901         XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
 902     }
 903
 904   }
 905
 906   if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
 907     XBT_DEBUG("Pair %d (depth = %d) shifted in stack, maximum depth reached", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
 908   }else{
 909     XBT_DEBUG("Pair %d (depth = %d) shifted in stack", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
 910   }
 911
 912
 913   MC_SET_RAW_MEM;
 914   xbt_dynar_free(&prop_values);
 915   current_pair = xbt_fifo_shift(mc_stack_liveness);
 916   current_pair->stack_removed = 1;
 917   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 918     remove_acceptance_pair(current_pair);
 919   }else{
 920     if(_sg_mc_visited == 0)
 921       MC_pair_delete(current_pair);
 922     else if(current_pair->visited_removed)
 923       MC_pair_delete(current_pair);
 924   }
 925   MC_UNSET_RAW_MEM;
 926
 927 }