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