src/mc/mc_liveness.c

   1 #include "private.h"
   2 #include "unistd.h"
   3
   4 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
   5                                 "Logging specific to algorithms for liveness properties verification");
   6
   7 xbt_dynar_t reached_pairs;
   8 xbt_dynar_t reached_pairs_hash;
   9 xbt_dynar_t visited_pairs;
  10 xbt_dynar_t visited_pairs_hash;
  11 xbt_dynar_t successors;
  12
  13
  14 /* fast implementation of djb2 algorithm */
  15 unsigned int hash_region(char *str, int str_len){
  16
  17   int c;
  18   register unsigned int hash = 5381;
  19
  20   while (str_len--) {
  21     c = *str++;
  22     hash = ((hash << 5) + hash) + c;    /* hash * 33 + c */
  23   }
  24
  25   return hash;
  26
  27 }
  28
  29 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
  30
  31
  32   if(s1->num_reg != s2->num_reg){
  33     //XBT_DEBUG("Different num_reg (s1 = %d, s2 = %d)", s1->num_reg, s2->num_reg);
  34     return 1;
  35   }
  36
  37   int i;
  38
  39   for(i=0 ; i< s1->num_reg ; i++){
  40
  41     if(s1->regions[i]->type != s2->regions[i]->type){
  42       //XBT_DEBUG("Different type of region");
  43       return 1;
  44     }
  45
  46     switch(s1->regions[i]->type){
  47     case 0:
  48       if(s1->regions[i]->size != s2->regions[i]->size){
  49         //XBT_DEBUG("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
  50         return 1;
  51       }
  52       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
  53         //XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
  54         return 1;
  55       }
  56       if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){
  57         //XBT_DEBUG("Different heap (mmalloc_compare)");
  58         return 1;
  59       }
  60       break;
  61     case 1 :
  62       if(s1->regions[i]->size != s2->regions[i]->size){
  63         //XBT_DEBUG("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
  64         return 1;
  65       }
  66       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
  67         //XBT_DEBUG("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
  68         return 1;
  69       }
  70       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
  71         //XBT_DEBUG("Different memcmp for data in libsimgrid");
  72         return 1;
  73       }
  74       break;
  75     case 2:
  76       if(s1->regions[i]->size != s2->regions[i]->size){
  77         //XBT_DEBUG("Different size of program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
  78         return 1;
  79       }
  80       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
  81         //XBT_DEBUG("Different start addr of program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
  82         return 1;
  83       }
  84       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
  85         //XBT_DEBUG("Different memcmp for data in program");
  86         return 1;
  87       }
  88       break;
  89     case 3:
  90       if(s1->regions[i]->size != s2->regions[i]->size){
  91         //XBT_DEBUG("Different size of stack (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
  92         return 1;
  93       }
  94       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
  95         //XBT_DEBUG("Different start addr of stack (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
  96         return 1;
  97       }
  98       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
  99         //XBT_DEBUG("Different memcmp for data in stack");
 100         return 1;
 101       }
 102       break;
 103     }
 104   }
 105
 106   return 0;
 107
 108 }
 109
 110 int reached(xbt_state_t st){
 111
 112
 113   if(xbt_dynar_is_empty(reached_pairs)){
 114
 115     return 0;
 116
 117   }else{
 118
 119     MC_SET_RAW_MEM;
 120
 121     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 122     MC_take_snapshot_liveness(sn);
 123
 124     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 125     int res;
 126     int (*f)();
 127
 128     /* Get values of propositional symbols */
 129     unsigned int cursor = 0;
 130     xbt_propositional_symbol_t ps = NULL;
 131     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 132       f = ps->function;
 133       res = (*f)();
 134       xbt_dynar_push_as(prop_ato, int, res);
 135     }
 136
 137     cursor = 0;
 138     mc_pair_reached_t pair_test = NULL;
 139
 140
 141     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
 142       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 143         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 144           if(snapshot_compare(pair_test->system_state, sn) == 0){
 145             MC_free_snapshot(sn);
 146             xbt_dynar_reset(prop_ato);
 147             xbt_free(prop_ato);
 148             MC_UNSET_RAW_MEM;
 149             return 1;
 150           }
 151         }
 152       }
 153     }
 154
 155     MC_free_snapshot(sn);
 156     xbt_dynar_reset(prop_ato);
 157     xbt_free(prop_ato);
 158     MC_UNSET_RAW_MEM;
 159     return 0;
 160
 161   }
 162 }
 163
 164 void set_pair_reached(xbt_state_t st){
 165
 166
 167   MC_SET_RAW_MEM;
 168
 169   mc_pair_reached_t pair = NULL;
 170   pair = xbt_new0(s_mc_pair_reached_t, 1);
 171   pair->automaton_state = st;
 172   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 173   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 174   MC_take_snapshot_liveness(pair->system_state);
 175
 176   /* Get values of propositional symbols */
 177   unsigned int cursor = 0;
 178   xbt_propositional_symbol_t ps = NULL;
 179   int res;
 180   int (*f)();
 181
 182   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 183     f = ps->function;
 184     res = (*f)();
 185     xbt_dynar_push_as(pair->prop_ato, int, res);
 186   }
 187
 188   xbt_dynar_push(reached_pairs, &pair);
 189
 190   MC_UNSET_RAW_MEM;
 191
 192 }
 193
 194 int reached_hash(xbt_state_t st){
 195
 196
 197   if(xbt_dynar_is_empty(reached_pairs_hash)){
 198
 199     return 0;
 200
 201   }else{
 202
 203     MC_SET_RAW_MEM;
 204
 205     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 206     MC_take_snapshot_liveness(sn);
 207
 208     int j;
 209     unsigned int hash_regions[sn->num_reg];
 210     for(j=0; j<sn->num_reg; j++){
 211       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
 212     }
 213
 214
 215     /* Get values of propositional symbols */
 216     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 217     unsigned int cursor = 0;
 218     xbt_propositional_symbol_t ps = NULL;
 219     int res;
 220     int (*f)();
 221
 222     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 223       f = ps->function;
 224       res = (*f)();
 225       xbt_dynar_push_as(prop_ato, int, res);
 226     }
 227
 228     mc_pair_reached_hash_t pair_test = NULL;
 229
 230     int region_diff = 0;
 231
 232     cursor = 0;
 233
 234     xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
 235
 236       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 237         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 238           for(j=0 ; j< sn->num_reg ; j++){
 239             if(hash_regions[j] != pair_test->hash_regions[j]){
 240               region_diff++;
 241             }
 242           }
 243           if(region_diff == 0){
 244             MC_free_snapshot(sn);
 245             xbt_dynar_reset(prop_ato);
 246             xbt_free(prop_ato);
 247             MC_UNSET_RAW_MEM;
 248             return 1;
 249           }
 250         }
 251       }
 252
 253
 254       region_diff = 0;
 255     }
 256
 257     MC_free_snapshot(sn);
 258     xbt_dynar_reset(prop_ato);
 259     xbt_free(prop_ato);
 260     MC_UNSET_RAW_MEM;
 261     return 0;
 262
 263   }
 264 }
 265
 266 void set_pair_reached_hash(xbt_state_t st){
 267
 268   MC_SET_RAW_MEM;
 269
 270   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 271   MC_take_snapshot_liveness(sn);
 272
 273   mc_pair_reached_hash_t pair = NULL;
 274   pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
 275   pair->automaton_state = st;
 276   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 277   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
 278
 279   int i;
 280
 281   for(i=0 ; i< sn->num_reg ; i++){
 282     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
 283   }
 284
 285   /* Get values of propositional symbols */
 286   unsigned int cursor = 0;
 287   xbt_propositional_symbol_t ps = NULL;
 288   int res;
 289   int (*f)();
 290
 291   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 292     f = ps->function;
 293     res = (*f)();
 294     xbt_dynar_push_as(pair->prop_ato, int, res);
 295   }
 296
 297   xbt_dynar_push(reached_pairs_hash, &pair);
 298
 299   MC_free_snapshot(sn);
 300
 301   MC_UNSET_RAW_MEM;
 302
 303 }
 304
 305
 306 int visited(xbt_state_t st, int sc){
 307
 308
 309   if(xbt_dynar_is_empty(visited_pairs)){
 310
 311     return 0;
 312
 313   }else{
 314
 315     MC_SET_RAW_MEM;
 316
 317     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 318     MC_take_snapshot_liveness(sn);
 319
 320     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 321
 322     /* Get values of propositional symbols */
 323     unsigned int cursor = 0;
 324     xbt_propositional_symbol_t ps = NULL;
 325     int res;
 326     int (*f)();
 327
 328     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 329       f = ps->function;
 330       res = (*f)();
 331       xbt_dynar_push_as(prop_ato, int, res);
 332     }
 333
 334     cursor = 0;
 335     mc_pair_visited_t pair_test = NULL;
 336
 337     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
 338       if(pair_test->search_cycle == sc) {
 339         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 340           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 341             if(snapshot_compare(pair_test->system_state, sn) == 0){
 342
 343               MC_free_snapshot(sn);
 344               xbt_dynar_reset(prop_ato);
 345               xbt_free(prop_ato);
 346               MC_UNSET_RAW_MEM;
 347
 348               return 1;
 349
 350             }
 351           }
 352         }
 353       }
 354     }
 355
 356
 357     MC_free_snapshot(sn);
 358     xbt_dynar_reset(prop_ato);
 359     xbt_free(prop_ato);
 360     MC_UNSET_RAW_MEM;
 361     return 0;
 362
 363   }
 364 }
 365
 366
 367 int visited_hash(xbt_state_t st, int sc){
 368
 369
 370   if(xbt_dynar_is_empty(visited_pairs_hash)){
 371
 372     return 0;
 373
 374   }else{
 375
 376     MC_SET_RAW_MEM;
 377
 378     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 379     MC_take_snapshot_liveness(sn);
 380
 381     int j;
 382     unsigned int hash_regions[sn->num_reg];
 383     for(j=0; j<sn->num_reg; j++){
 384       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
 385     }
 386
 387
 388     /* Get values of propositional symbols */
 389     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 390     unsigned int cursor = 0;
 391     xbt_propositional_symbol_t ps = NULL;
 392     int res;
 393     int (*f)();
 394
 395     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 396       f = ps->function;
 397       res = (*f)();
 398       xbt_dynar_push_as(prop_ato, int, res);
 399     }
 400
 401     mc_pair_visited_hash_t pair_test = NULL;
 402
 403     int region_diff = 0;
 404     cursor = 0;
 405
 406     xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
 407
 408       if(pair_test->search_cycle == sc) {
 409         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 410           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 411             for(j=0 ; j< sn->num_reg ; j++){
 412               if(hash_regions[j] != pair_test->hash_regions[j]){
 413                 region_diff++;
 414               }
 415             }
 416             if(region_diff == 0){
 417               MC_free_snapshot(sn);
 418               xbt_dynar_reset(prop_ato);
 419               xbt_free(prop_ato);
 420               MC_UNSET_RAW_MEM;
 421               return 1;
 422             }
 423           }
 424         }
 425       }
 426
 427       region_diff = 0;
 428     }
 429
 430     MC_free_snapshot(sn);
 431     xbt_dynar_reset(prop_ato);
 432     xbt_free(prop_ato);
 433     MC_UNSET_RAW_MEM;
 434     return 0;
 435
 436   }
 437 }
 438
 439 void set_pair_visited_hash(xbt_state_t st, int sc){
 440
 441   MC_SET_RAW_MEM;
 442
 443   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 444   MC_take_snapshot_liveness(sn);
 445
 446   mc_pair_visited_hash_t pair = NULL;
 447   pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
 448   pair->automaton_state = st;
 449   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 450   pair->search_cycle = sc;
 451   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
 452
 453   int i;
 454
 455   for(i=0 ; i< sn->num_reg ; i++){
 456     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
 457   }
 458
 459   /* Get values of propositional symbols */
 460   unsigned int cursor = 0;
 461   xbt_propositional_symbol_t ps = NULL;
 462   int res;
 463   int (*f)();
 464
 465   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 466     f = ps->function;
 467     res = (*f)();
 468     xbt_dynar_push_as(pair->prop_ato, int, res);
 469   }
 470
 471   xbt_dynar_push(visited_pairs_hash, &pair);
 472
 473   MC_free_snapshot(sn);
 474
 475   MC_UNSET_RAW_MEM;
 476
 477 }
 478
 479 void set_pair_visited(xbt_state_t st, int sc){
 480
 481
 482   MC_SET_RAW_MEM;
 483
 484   mc_pair_visited_t pair = NULL;
 485   pair = xbt_new0(s_mc_pair_visited_t, 1);
 486   pair->automaton_state = st;
 487   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 488   pair->search_cycle = sc;
 489   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 490   MC_take_snapshot_liveness(pair->system_state);
 491
 492
 493   /* Get values of propositional symbols */
 494   unsigned int cursor = 0;
 495   xbt_propositional_symbol_t ps = NULL;
 496   int res;
 497   int (*f)();
 498
 499   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 500     f = ps->function;
 501     res = (*f)();
 502     xbt_dynar_push_as(pair->prop_ato, int, res);
 503   }
 504
 505   xbt_dynar_push(visited_pairs, &pair);
 506
 507   MC_UNSET_RAW_MEM;
 508
 509
 510 }
 511
 512 void MC_pair_delete(mc_pair_t pair){
 513   xbt_free(pair->graph_state->proc_status);
 514   xbt_free(pair->graph_state);
 515   xbt_free(pair);
 516 }
 517
 518
 519
 520 int MC_automaton_evaluate_label(xbt_exp_label_t l){
 521
 522   switch(l->type){
 523   case 0 : {
 524     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 525     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 526     return (left_res || right_res);
 527     break;
 528   }
 529   case 1 : {
 530     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 531     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 532     return (left_res && right_res);
 533     break;
 534   }
 535   case 2 : {
 536     int res = MC_automaton_evaluate_label(l->u.exp_not);
 537     return (!res);
 538     break;
 539   }
 540   case 3 : {
 541     unsigned int cursor = 0;
 542     xbt_propositional_symbol_t p = NULL;
 543     int (*f)();
 544     xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){
 545       if(strcmp(p->pred, l->u.predicat) == 0){
 546         f = p->function;
 547         return (*f)();
 548       }
 549     }
 550     return -1;
 551     break;
 552   }
 553   case 4 : {
 554     return 2;
 555     break;
 556   }
 557   default :
 558     return -1;
 559   }
 560 }
 561
 562
 563
 564
 565
 566 /********************* Double-DFS stateless *******************/
 567
 568 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 569   xbt_free(pair->graph_state->proc_status);
 570   xbt_free(pair->graph_state);
 571   xbt_free(pair);
 572 }
 573
 574 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 575   mc_pair_stateless_t p = NULL;
 576   p = xbt_new0(s_mc_pair_stateless_t, 1);
 577   p->automaton_state = st;
 578   p->graph_state = sg;
 579   p->requests = r;
 580   mc_stats_pair->expanded_pairs++;
 581   return p;
 582 }
 583
 584 void MC_ddfs_init(){
 585
 586   XBT_DEBUG("**************************************************");
 587   XBT_DEBUG("Double-DFS init");
 588   XBT_DEBUG("**************************************************");
 589
 590   mc_pair_stateless_t mc_initial_pair = NULL;
 591   mc_state_t initial_graph_state = NULL;
 592   smx_process_t process;
 593
 594   MC_wait_for_requests();
 595
 596   MC_SET_RAW_MEM;
 597
 598   initial_graph_state = MC_state_pair_new();
 599   xbt_swag_foreach(process, simix_global->process_list){
 600     if(MC_process_is_enabled(process)){
 601       MC_state_interleave_process(initial_graph_state, process);
 602     }
 603   }
 604
 605   //reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
 606   reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
 607   //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
 608   visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
 609   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 610
 611   /* Save the initial state */
 612   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
 613   MC_take_snapshot_to_restore_liveness(initial_snapshot_liveness);
 614
 615   MC_UNSET_RAW_MEM;
 616
 617   unsigned int cursor = 0;
 618   xbt_state_t state;
 619
 620   xbt_dynar_foreach(automaton->states, cursor, state){
 621     if(state->type == -1){
 622
 623       MC_SET_RAW_MEM;
 624       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 625       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 626       MC_UNSET_RAW_MEM;
 627
 628       if(cursor != 0){
 629         MC_restore_snapshot(initial_snapshot_liveness);
 630         MC_UNSET_RAW_MEM;
 631       }
 632
 633       MC_ddfs(0);
 634
 635     }else{
 636       if(state->type == 2){
 637
 638         MC_SET_RAW_MEM;
 639         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 640         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 641         MC_UNSET_RAW_MEM;
 642
 643         //set_pair_reached(state);
 644         set_pair_reached_hash(state);
 645
 646         if(cursor != 0){
 647           MC_restore_snapshot(initial_snapshot_liveness);
 648           MC_UNSET_RAW_MEM;
 649         }
 650
 651         MC_ddfs(1);
 652
 653       }
 654     }
 655   }
 656
 657 }
 658
 659
 660 void MC_ddfs(int search_cycle){
 661
 662   smx_process_t process;
 663   mc_pair_stateless_t current_pair = NULL;
 664
 665   if(xbt_fifo_size(mc_stack_liveness) == 0)
 666     return;
 667
 668
 669   /* Get current pair */
 670   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 671
 672   /* Update current state in buchi automaton */
 673   automaton->current_state = current_pair->automaton_state;
 674
 675
 676   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
 677   XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id, MC_state_interleave_size(current_pair->graph_state));
 678
 679   mc_stats_pair->visited_pairs++;
 680
 681   //sleep(1);
 682
 683   int value;
 684   mc_state_t next_graph_state = NULL;
 685   smx_req_t req = NULL;
 686   char *req_str;
 687
 688   xbt_transition_t transition_succ;
 689   unsigned int cursor = 0;
 690   int res;
 691
 692   mc_pair_stateless_t next_pair = NULL;
 693   mc_pair_stateless_t pair_succ;
 694
 695   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
 696
 697     //set_pair_visited(current_pair->automaton_state, search_cycle);
 698     set_pair_visited_hash(current_pair->automaton_state, search_cycle);
 699
 700     //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
 701     XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
 702
 703     if(current_pair->requests > 0){
 704
 705       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 706
 707         /* Debug information */
 708         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 709           req_str = MC_request_to_string(req, value);
 710           XBT_DEBUG("Execute: %s", req_str);
 711           xbt_free(req_str);
 712         }
 713
 714         MC_state_set_executed_request(current_pair->graph_state, req, value);
 715
 716         /* Answer the request */
 717         SIMIX_request_pre(req, value);
 718
 719         /* Wait for requests (schedules processes) */
 720         MC_wait_for_requests();
 721
 722
 723         MC_SET_RAW_MEM;
 724
 725         /* Create the new expanded graph_state */
 726         next_graph_state = MC_state_pair_new();
 727
 728         /* Get enabled process and insert it in the interleave set of the next graph_state */
 729         xbt_swag_foreach(process, simix_global->process_list){
 730           if(MC_process_is_enabled(process)){
 731             MC_state_interleave_process(next_graph_state, process);
 732           }
 733         }
 734
 735         xbt_dynar_reset(successors);
 736
 737         MC_UNSET_RAW_MEM;
 738
 739
 740         cursor= 0;
 741         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 742
 743           res = MC_automaton_evaluate_label(transition_succ->label);
 744
 745           if(res == 1){ // enabled transition in automaton
 746             MC_SET_RAW_MEM;
 747             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 748             xbt_dynar_push(successors, &next_pair);
 749             MC_UNSET_RAW_MEM;
 750           }
 751
 752         }
 753
 754         cursor = 0;
 755
 756         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 757
 758           res = MC_automaton_evaluate_label(transition_succ->label);
 759
 760           if(res == 2){ // true transition in automaton
 761             MC_SET_RAW_MEM;
 762             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 763             xbt_dynar_push(successors, &next_pair);
 764             MC_UNSET_RAW_MEM;
 765           }
 766
 767         }
 768
 769         cursor = 0;
 770
 771         xbt_dynar_foreach(successors, cursor, pair_succ){
 772
 773           if(search_cycle == 1){
 774
 775             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 776
 777               //if(reached(pair_succ->automaton_state)){
 778               if(reached_hash(pair_succ->automaton_state)){
 779
 780                 XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
 781
 782                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 783                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 784                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 785                 XBT_INFO("Counter-example that violates formula :");
 786                 MC_show_stack_liveness(mc_stack_liveness);
 787                 MC_dump_stack_liveness(mc_stack_liveness);
 788                 MC_print_statistics_pairs(mc_stats_pair);
 789                 exit(0);
 790
 791               }else{
 792
 793                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 794
 795                 //set_pair_reached(pair_succ->automaton_state);
 796                 set_pair_reached_hash(pair_succ->automaton_state);
 797
 798                 //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 799                 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 800
 801                 MC_SET_RAW_MEM;
 802                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 803                 MC_UNSET_RAW_MEM;
 804
 805                 MC_ddfs(search_cycle);
 806
 807               }
 808
 809             }else{
 810
 811               if(!visited_hash(pair_succ->automaton_state, search_cycle)){
 812                 //if(!visited(pair_succ->automaton_state, search_cycle)){
 813
 814                 MC_SET_RAW_MEM;
 815                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 816                 MC_UNSET_RAW_MEM;
 817
 818                 MC_ddfs(search_cycle);
 819
 820               }else{
 821
 822                 XBT_DEBUG("Next pair already visited ! ");
 823
 824               }
 825
 826             }
 827
 828           }else{
 829
 830             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 831
 832               XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 833
 834               //set_pair_reached(pair_succ->automaton_state);
 835               set_pair_reached_hash(pair_succ->automaton_state);
 836
 837               search_cycle = 1;
 838
 839               //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 840               XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 841
 842             }
 843
 844             if(!visited_hash(pair_succ->automaton_state, search_cycle)){
 845               //if(!visited(pair_succ->automaton_state, search_cycle)){
 846
 847               MC_SET_RAW_MEM;
 848               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 849               MC_UNSET_RAW_MEM;
 850
 851               MC_ddfs(search_cycle);
 852
 853             }else{
 854
 855               XBT_DEBUG("Next pair already visited ! ");
 856
 857             }
 858
 859           }
 860
 861
 862           /* Restore system before checking others successors */
 863           if(cursor != (xbt_dynar_length(successors) - 1))
 864             MC_replay_liveness(mc_stack_liveness, 1);
 865
 866
 867         }
 868
 869         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 870           XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness));
 871           MC_replay_liveness(mc_stack_liveness, 0);
 872         }
 873       }
 874
 875
 876     }else{  /*No request to execute, search evolution in Büchi automaton */
 877
 878       MC_SET_RAW_MEM;
 879
 880       /* Create the new expanded graph_state */
 881       next_graph_state = MC_state_pair_new();
 882
 883       xbt_dynar_reset(successors);
 884
 885       MC_UNSET_RAW_MEM;
 886
 887
 888       cursor= 0;
 889       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 890
 891         res = MC_automaton_evaluate_label(transition_succ->label);
 892
 893         if(res == 1){ // enabled transition in automaton
 894           MC_SET_RAW_MEM;
 895           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 896           xbt_dynar_push(successors, &next_pair);
 897           MC_UNSET_RAW_MEM;
 898         }
 899
 900       }
 901
 902       cursor = 0;
 903
 904       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 905
 906         res = MC_automaton_evaluate_label(transition_succ->label);
 907
 908         if(res == 2){ // true transition in automaton
 909           MC_SET_RAW_MEM;
 910           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 911           xbt_dynar_push(successors, &next_pair);
 912           MC_UNSET_RAW_MEM;
 913         }
 914
 915       }
 916
 917       cursor = 0;
 918
 919       xbt_dynar_foreach(successors, cursor, pair_succ){
 920
 921         if(search_cycle == 1){
 922
 923           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 924
 925             //if(reached(pair_succ->automaton_state)){
 926             if(reached_hash(pair_succ->automaton_state)){
 927
 928               XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
 929
 930               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 931               XBT_INFO("|             ACCEPTANCE CYCLE            |");
 932               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 933               XBT_INFO("Counter-example that violates formula :");
 934               MC_show_stack_liveness(mc_stack_liveness);
 935               MC_dump_stack_liveness(mc_stack_liveness);
 936               MC_print_statistics_pairs(mc_stats_pair);
 937               exit(0);
 938
 939             }else{
 940
 941               XBT_DEBUG("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 942
 943               //set_pair_reached(pair_succ->automaton_state);
 944               set_pair_reached_hash(pair_succ->automaton_state);
 945
 946               //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 947               XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 948
 949               MC_SET_RAW_MEM;
 950               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 951               MC_UNSET_RAW_MEM;
 952
 953               MC_ddfs(search_cycle);
 954
 955             }
 956
 957           }else{
 958
 959             if(!visited_hash(pair_succ->automaton_state, search_cycle)){
 960               //if(!visited(pair_succ->automaton_state, search_cycle)){
 961
 962               MC_SET_RAW_MEM;
 963               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 964               MC_UNSET_RAW_MEM;
 965
 966               MC_ddfs(search_cycle);
 967
 968             }else{
 969
 970               XBT_DEBUG("Next pair already visited ! ");
 971
 972             }
 973           }
 974
 975
 976         }else{
 977
 978           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 979
 980             //set_pair_reached(pair_succ->automaton_state);
 981             set_pair_reached_hash(pair_succ->automaton_state);
 982
 983             search_cycle = 1;
 984
 985             //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 986             XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 987
 988           }
 989
 990           //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
 991           if(!visited(pair_succ->automaton_state, search_cycle)){
 992
 993             MC_SET_RAW_MEM;
 994             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 995             MC_UNSET_RAW_MEM;
 996
 997             MC_ddfs(search_cycle);
 998
 999           }else{
1000
1001             XBT_DEBUG("Next pair already visited ! ");
1002
1003           }
1004
1005         }
1006
1007         /* Restore system before checking others successors */
1008         if(cursor != xbt_dynar_length(successors) - 1)
1009           MC_replay_liveness(mc_stack_liveness, 1);
1010
1011
1012       }
1013
1014     }
1015
1016   }else{
1017
1018     XBT_DEBUG("Max depth reached");
1019
1020   }
1021
1022   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1023     XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1024   }else{
1025     XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1026   }
1027
1028
1029   MC_SET_RAW_MEM;
1030   xbt_fifo_shift(mc_stack_liveness);
1031   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1032     //xbt_dynar_pop(reached_pairs, NULL);
1033     xbt_dynar_pop(reached_pairs_hash, NULL);
1034   }
1035   MC_UNSET_RAW_MEM;
1036
1037
1038
1039 }