src/mc/mc_dfs.c

   1 #include "private.h"
   2 #include "unistd.h"
   3
   4 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc,
   5                                 "Logging specific to MC DFS algorithm");
   6
   7 xbt_dynar_t initial_pairs = NULL;
   8 int max_pair = 0;
   9 xbt_dynar_t visited_pairs;
  10 xbt_dynar_t reached_pairs;
  11
  12 mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
  13   mc_pairs_t p = NULL;
  14   p = xbt_new0(s_mc_pairs_t, 1);
  15   p->system_state = sn;
  16   p->automaton_state = st;
  17   p->graph_state = sg;
  18   p->num = max_pair;
  19   max_pair++;
  20   return p;
  21
  22 }
  23
  24 void set_pair_visited(mc_state_t gs, xbt_state_t as, int sc){
  25
  26   if(visited(gs, as, sc) == 0){
  27     //XBT_DEBUG("New visited pair : graph=%p, automaton=%p", gs, as);
  28     MC_SET_RAW_MEM;
  29     mc_visited_pairs_t p = NULL;
  30     p = xbt_new0(s_mc_visited_pairs_t, 1);
  31     p->graph_state = gs;
  32     p->automaton_state = as;
  33     p->search_cycle = sc;
  34     xbt_dynar_push(visited_pairs, &p);
  35     MC_UNSET_RAW_MEM;
  36   }
  37
  38   //XBT_DEBUG("New visited pair , length of visited pairs : %lu", xbt_dynar_length(visited_pairs));
  39 }
  40
  41 int reached(mc_state_t gs, xbt_state_t as ){
  42
  43   mc_reached_pairs_t rp = NULL;
  44   unsigned int c= 0;
  45   unsigned int i;
  46   int different_process;
  47
  48   MC_SET_RAW_MEM;
  49   xbt_dynar_foreach(reached_pairs, c, rp){
  50     if(rp->automaton_state == as){
  51       different_process=0;
  52       for(i=0; i < gs->max_pid; i++){
  53         if(gs->proc_status[i].state != rp->graph_state->proc_status[i].state){
  54           different_process++;
  55         }
  56       }
  57       if(different_process==0){
  58         MC_UNSET_RAW_MEM;
  59         return 1;
  60       }
  61     }
  62   }
  63   MC_UNSET_RAW_MEM;
  64   return 0;
  65 }
  66
  67 void set_pair_reached(mc_state_t gs, xbt_state_t as){
  68
  69   if(reached(gs, as) == 0){
  70     MC_SET_RAW_MEM;
  71     mc_reached_pairs_t p = NULL;
  72     p = xbt_new0(s_mc_reached_pairs_t, 1);
  73     p->graph_state = gs;
  74     p->automaton_state = as;
  75     xbt_dynar_push(reached_pairs, &p);
  76     //XBT_DEBUG("New reached pair : graph=%p, automaton=%p", gs, as);
  77     MC_UNSET_RAW_MEM;
  78   }
  79
  80 }
  81
  82 int visited(mc_state_t gs, xbt_state_t as, int sc){
  83   unsigned int c = 0;
  84   mc_visited_pairs_t p = NULL;
  85   unsigned int i;
  86   int different_process;
  87
  88   MC_SET_RAW_MEM;
  89   xbt_dynar_foreach(visited_pairs, c, p){
  90     if((p->automaton_state == as) && (p->search_cycle == sc)){
  91       different_process=0;
  92       for(i=0; i < gs->max_pid; i++){
  93         if(gs->proc_status[i].state != p->graph_state->proc_status[i].state){
  94           different_process++;
  95         }
  96       }
  97       if(different_process==0){
  98         MC_UNSET_RAW_MEM;
  99         return 1;
 100       }
 101     }
 102   }
 103   MC_UNSET_RAW_MEM;
 104   return 0;
 105
 106 }
 107
 108 void MC_dfs_init(xbt_automaton_t a){
 109
 110    XBT_DEBUG("**************************************************");
 111    XBT_DEBUG("DFS init");
 112    XBT_DEBUG("**************************************************");
 113
 114   mc_pairs_t mc_initial_pair;
 115   mc_state_t initial_graph_state;
 116   smx_process_t process;
 117   mc_snapshot_t init_snapshot;
 118
 119   MC_wait_for_requests();
 120
 121   MC_SET_RAW_MEM;
 122
 123   init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 124
 125   initial_graph_state = MC_state_new();
 126   xbt_swag_foreach(process, simix_global->process_list){
 127     if(MC_process_is_enabled(process)){
 128       MC_state_interleave_process(initial_graph_state, process);
 129     }
 130   }
 131
 132   visited_pairs = xbt_dynar_new(sizeof(mc_visited_pairs_t), NULL);
 133   reached_pairs = xbt_dynar_new(sizeof(mc_reached_pairs_t), NULL);
 134
 135   MC_take_snapshot(init_snapshot);
 136
 137   MC_UNSET_RAW_MEM;
 138
 139
 140   /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
 141     -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
 142
 143   unsigned int cursor = 0;
 144   unsigned int cursor2 = 0;
 145   xbt_state_t state = NULL;
 146   int res;
 147   xbt_transition_t transition_succ;
 148   xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
 149   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
 150   //  int enabled_transition = 0;
 151   mc_pairs_t pair_succ;
 152
 153   xbt_dynar_foreach(a->states, cursor, state){
 154     if(state->type == -1){
 155       xbt_dynar_foreach(state->out, cursor2, transition_succ){
 156         res = MC_automaton_evaluate_label(a, transition_succ->label);
 157
 158         if(res == 1){
 159
 160           MC_SET_RAW_MEM;
 161
 162           mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 163           xbt_dynar_push(successors, &mc_initial_pair);
 164
 165           //XBT_DEBUG("New initial successor");
 166
 167           MC_UNSET_RAW_MEM;
 168
 169         }else{
 170           if(res == 2){
 171
 172             MC_SET_RAW_MEM;
 173
 174             mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
 175             xbt_dynar_push(elses, &mc_initial_pair);
 176
 177             //XBT_DEBUG("New initial successor");
 178
 179             MC_UNSET_RAW_MEM;
 180           }
 181         }
 182       }
 183     }
 184   }
 185
 186   if(xbt_dynar_length(successors) > 0){
 187
 188     cursor = 0;
 189     xbt_dynar_foreach(successors, cursor, pair_succ){
 190       MC_SET_RAW_MEM;
 191
 192       xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 193
 194       XBT_DEBUG("**************************************************");
 195       XBT_DEBUG("Initial state=%p ", pair_succ);
 196
 197       MC_UNSET_RAW_MEM;
 198
 199       set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
 200
 201       if(cursor == 0)
 202         MC_dfs(a, 0, 0);
 203       else
 204         MC_dfs(a, 0, 1);
 205
 206     }
 207
 208   }else{
 209
 210     if(xbt_dynar_length(elses) > 0){
 211       cursor = 0;
 212       xbt_dynar_foreach(elses, cursor, pair_succ){
 213         MC_SET_RAW_MEM;
 214
 215         xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 216
 217         XBT_DEBUG("**************************************************");
 218         XBT_DEBUG("Initial state=%p ", pair_succ);
 219
 220         MC_UNSET_RAW_MEM;
 221
 222         set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
 223
 224         if(cursor == 0)
 225           MC_dfs(a, 0, 0);
 226         else
 227           MC_dfs(a, 0, 1);
 228       }
 229     }else{
 230
 231       XBT_DEBUG("No initial state !");
 232
 233       return;
 234     }
 235   }
 236
 237 }
 238
 239
 240
 241 void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
 242
 243
 244   if(xbt_fifo_size(mc_snapshot_stack) == 0)
 245     return;
 246
 247   if(restore == 1){
 248     MC_restore_snapshot(((mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
 249     MC_UNSET_RAW_MEM;
 250   }
 251
 252
 253   //XBT_DEBUG("Lpv length after restore snapshot: %lu", xbt_dynar_length(visited_pairs));
 254
 255   /* Get current state */
 256   mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 257
 258   XBT_DEBUG("**************************************************");
 259   XBT_DEBUG("State : graph=%p, automaton=%p, %u interleave, stack size=%d", current_pair->graph_state, current_pair->automaton_state, MC_state_interleave_size(current_pair->graph_state), xbt_fifo_size(mc_snapshot_stack));
 260   //XBT_DEBUG("Restore : %d", restore);
 261
 262
 263   /* Update statistics */
 264   //mc_stats->visited_states++;
 265   //set_pair_visited(current_pair->graph_state, current_pair->automaton_state, search_cycle);
 266
 267   //sleep(1);
 268
 269   smx_process_t process = NULL;
 270   int value;
 271   mc_state_t next_graph_state = NULL;
 272   smx_req_t req = NULL;
 273   char *req_str;
 274
 275   mc_pairs_t pair_succ;
 276   xbt_transition_t transition_succ;
 277   unsigned int cursor;
 278   int res;
 279   //int enabled_transition = 0;
 280
 281   xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
 282   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
 283
 284   mc_pairs_t next_pair;
 285   mc_snapshot_t next_snapshot;
 286   mc_snapshot_t current_snapshot;
 287
 288   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 289
 290     //XBT_DEBUG("Current pair : %p (%u interleave)", current_pair, MC_state_interleave_size(current_pair->graph_state)+1);
 291     //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
 292
 293     MC_SET_RAW_MEM;
 294     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 295     MC_take_snapshot(current_snapshot);
 296     MC_UNSET_RAW_MEM;
 297
 298
 299     /* Debug information */
 300     if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){
 301       req_str = MC_request_to_string(req, value);
 302       XBT_DEBUG("Execute: %s", req_str);
 303       xbt_free(req_str);
 304     }
 305
 306     MC_state_set_executed_request(current_pair->graph_state, req, value);
 307     //mc_stats->executed_transitions++;
 308
 309     /* Answer the request */
 310     SIMIX_request_pre(req, value);
 311
 312     /* Wait for requests (schedules processes) */
 313     MC_wait_for_requests();
 314
 315
 316     /* Create the new expanded graph_state */
 317     MC_SET_RAW_MEM;
 318
 319     next_graph_state = MC_state_new();
 320
 321     /* Get enabled process and insert it in the interleave set of the next graph_state */
 322     xbt_swag_foreach(process, simix_global->process_list){
 323       if(MC_process_is_enabled(process)){
 324         MC_state_interleave_process(next_graph_state, process);
 325       }
 326     }
 327
 328     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 329     MC_take_snapshot(next_snapshot);
 330
 331     MC_UNSET_RAW_MEM;
 332
 333     xbt_dynar_reset(elses);
 334     xbt_dynar_reset(successors);
 335
 336     cursor = 0;
 337     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 338
 339       res = MC_automaton_evaluate_label(a, transition_succ->label);
 340
 341       MC_SET_RAW_MEM;
 342       next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 343
 344       //XBT_DEBUG("Next pair : %p", next_pair);
 345
 346       if(res == 1){ // enabled transition in automaton
 347         xbt_dynar_push(successors, &next_pair);
 348         //XBT_DEBUG("New Successors length : %lu", xbt_dynar_length(successors));
 349       }else{
 350         if(res == 2){
 351           xbt_dynar_push(elses, &next_pair);
 352           //XBT_DEBUG("New Elses length : %lu", xbt_dynar_length(elses));
 353         }
 354       }
 355
 356       MC_UNSET_RAW_MEM;
 357     }
 358
 359
 360     if((xbt_dynar_length(successors) == 0) && (xbt_dynar_length(elses) == 0) ){
 361
 362       MC_SET_RAW_MEM;
 363       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
 364       xbt_dynar_push(successors, &next_pair);
 365       MC_UNSET_RAW_MEM;
 366
 367     }
 368
 369     //XBT_DEBUG("Successors length : %lu", xbt_dynar_length(successors));
 370     //XBT_DEBUG("Elses length : %lu", xbt_dynar_length(elses));
 371
 372     if(xbt_dynar_length(successors) >0){
 373
 374       cursor = 0;
 375       xbt_dynar_foreach(successors, cursor, pair_succ){
 376
 377         //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 378
 379         if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
 380
 381           MC_SET_RAW_MEM;
 382           xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 383           MC_UNSET_RAW_MEM;
 384
 385           set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
 386           MC_dfs(a, search_cycle, 0);
 387
 388           if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){
 389
 390             /* mc_pairs_t first_item = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); */
 391             /* if((first_item->graph_state != pair_succ->graph_state) || (first_item->automaton_state != pair_succ->automaton_state) ){ */
 392             /*   MC_SET_RAW_MEM; */
 393             /*   xbt_fifo_unshift(mc_snapshot_stack, pair_succ); */
 394             /*   MC_UNSET_RAW_MEM; */
 395             /* } */
 396
 397             set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);
 398             XBT_DEBUG("Acceptance state : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 399             MC_dfs(a, 1, 0);
 400           }
 401         }else{
 402           //XBT_DEBUG("Pair (graph=%p, automaton=%p) already visited !", pair_succ->graph_state, pair_succ->automaton_state );
 403           set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
 404         }
 405
 406       }
 407
 408     }else{
 409
 410       cursor = 0;
 411       xbt_dynar_foreach(elses, cursor, pair_succ){
 412
 413         //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 414
 415         if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
 416
 417           MC_SET_RAW_MEM;
 418           xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 419           MC_UNSET_RAW_MEM;
 420
 421           set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
 422           MC_dfs(a, search_cycle, 0);
 423
 424           if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){
 425
 426             set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);
 427             XBT_DEBUG("Acceptance state : graph state=%p, automaton state=%p",pair_succ->graph_state, pair_succ->automaton_state);
 428             MC_dfs(a, 1, 0);
 429
 430           }
 431         }else{
 432           //XBT_DEBUG("Pair (graph=%p, automaton=%p) already visited !", pair_succ->graph_state, pair_succ->automaton_state );
 433           /* Different graph_state */
 434           set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
 435         }
 436
 437       }
 438
 439     }
 440
 441     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 442       MC_restore_snapshot(current_snapshot);
 443       MC_UNSET_RAW_MEM;
 444       //XBT_DEBUG("Snapshot restored");
 445     }
 446   }
 447
 448   if((search_cycle == 1) && (reached(current_pair->graph_state, current_pair->automaton_state) == 1)){
 449     XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 450     XBT_INFO("|             ACCEPTANCE CYCLE            |");
 451     XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 452     XBT_INFO("Counter-example that violates formula :");
 453     MC_show_snapshot_stack(mc_snapshot_stack);
 454     MC_dump_snapshot_stack(mc_snapshot_stack);
 455     exit(0);
 456   }
 457
 458   MC_SET_RAW_MEM;
 459   xbt_fifo_shift(mc_snapshot_stack);
 460   //XBT_DEBUG("State shifted in snapshot_stack, mc_snapshot_stack size=%d", xbt_fifo_size(mc_snapshot_stack));
 461   MC_UNSET_RAW_MEM;
 462
 463
 464 }
 465
 466 void MC_show_snapshot_stack(xbt_fifo_t stack){
 467   int value;
 468   mc_pairs_t pair;
 469   xbt_fifo_item_t item;
 470   smx_req_t req;
 471   char *req_str = NULL;
 472
 473   for (item = xbt_fifo_get_last_item(stack);
 474        (item ? (pair = (mc_pairs_t) (xbt_fifo_get_item_content(item)))
 475         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 476     req = MC_state_get_executed_request(pair->graph_state, &value);
 477     if(req){
 478       req_str = MC_request_to_string(req, value);
 479       XBT_INFO("%s", req_str);
 480       xbt_free(req_str);
 481     }
 482   }
 483 }
 484
 485 void MC_dump_snapshot_stack(xbt_fifo_t stack){
 486
 487 }
 488
 489
 490 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 491
 492   switch(l->type){
 493   case 0 : {
 494     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 495     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 496     return (left_res || right_res);
 497     break;
 498   }
 499   case 1 : {
 500     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 501     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 502     return (left_res && right_res);
 503     break;
 504   }
 505   case 2 : {
 506     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
 507     return (!res);
 508     break;
 509   }
 510   case 3 : {
 511     unsigned int cursor = 0;
 512     xbt_propositional_symbol_t p = NULL;
 513     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
 514       if(strcmp(p->pred, l->u.predicat) == 0){
 515         int (*f)() = p->function;
 516         return (*f)();
 517       }
 518     }
 519     return -1;
 520     break;
 521   }
 522   case 4 : {
 523     return 2;
 524     break;
 525   }
 526   default :
 527     return -1;
 528   }
 529 }
 530
 531 /*void MC_dfs(xbt_automaton_t a, int search_cycle){
 532
 533   xbt_state_t current_state = (xbt_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(stack_automaton_dfs));
 534   xbt_transition_t transition_succ = NULL;
 535   xbt_state_t successor = NULL;
 536   unsigned int cursor = 0;
 537   xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
 538   int res;
 539
 540   //printf("++ current state : %s\n", current_state->id);
 541
 542   xbt_dynar_foreach(current_state->out, cursor, transition_succ){
 543     successor = transition_succ->dst;
 544     res = MC_automaton_evaluate_label(a, transition_succ->label);
 545     //printf("-- state : %s, transition_label : %d, res = %d\n", successor->id, transition_succ->label->type, res);
 546     if(res == 1){
 547       if(search_cycle == 1 && reached_dfs != NULL){
 548         if(strcmp(reached_dfs->id, successor->id) == 0){
 549           xbt_dynar_push(state_automaton_visited_dfs, &successor);
 550           printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 551           printf("Visited states : \n");
 552           unsigned int cursor2 = 0;
 553           xbt_state_t visited_state = NULL;
 554           xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
 555             printf("State : %s\n", visited_state->id);
 556           }
 557           exit(1);
 558         }
 559       }
 560       if(successor->visited == 0){
 561         successor->visited = 1;
 562         xbt_fifo_unshift(stack_automaton_dfs, successor);
 563         xbt_dynar_push(state_automaton_visited_dfs, &successor);
 564         MC_dfs(a, search_cycle);
 565         if(search_cycle == 0 && successor->type == 1){
 566           reached_dfs = successor;
 567           MC_dfs(a, 1);
 568         }
 569       }
 570     }else{
 571       if(res == 2){
 572         xbt_dynar_push(elses,&transition_succ);
 573       }
 574     }
 575   }
 576
 577   cursor = 0;
 578   xbt_dynar_foreach(elses, cursor, transition_succ){
 579    successor = transition_succ->dst;
 580    if(search_cycle == 1 && reached_dfs != NULL){
 581      if(strcmp(reached_dfs->id, successor->id) == 0){
 582        xbt_dynar_push(state_automaton_visited_dfs, &successor);
 583        printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 584        printf("Visited states : \n");
 585        unsigned int cursor2 = 0;
 586        xbt_state_t visited_state = NULL;
 587        xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
 588          printf("State : %s\n", visited_state->id);
 589        }
 590        exit(1);
 591      }
 592    }
 593    if(successor->visited == 0){
 594      successor->visited = 1;
 595      xbt_fifo_unshift(stack_automaton_dfs, successor);
 596      xbt_dynar_push(state_automaton_visited_dfs, &successor);
 597      MC_dfs(a, search_cycle);
 598      if(search_cycle == 0 && successor->type == 1){
 599        reached_dfs = successor;
 600        MC_dfs(a, 1);
 601      }
 602    }
 603   }
 604
 605   xbt_fifo_shift(stack_automaton_dfs);
 606   }*/