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             set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);
 391             XBT_DEBUG("Acceptance state : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 392             MC_dfs(a, 1, 0);
 393
 394           }
 395         }else{
 396           //XBT_DEBUG("Pair (graph=%p, automaton=%p) already visited !", pair_succ->graph_state, pair_succ->automaton_state );
 397           set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
 398         }
 399
 400       }
 401
 402     }else{
 403
 404       cursor = 0;
 405       xbt_dynar_foreach(elses, cursor, pair_succ){
 406
 407         //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 408
 409         if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
 410
 411           MC_SET_RAW_MEM;
 412           xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 413           MC_UNSET_RAW_MEM;
 414
 415           set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
 416           MC_dfs(a, search_cycle, 0);
 417
 418           if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){
 419
 420             set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);
 421             XBT_DEBUG("Acceptance state : graph state=%p, automaton state=%p",pair_succ->graph_state, pair_succ->automaton_state);
 422             MC_dfs(a, 1, 0);
 423
 424           }
 425         }else{
 426           //XBT_DEBUG("Pair (graph=%p, automaton=%p) already visited !", pair_succ->graph_state, pair_succ->automaton_state );
 427           /* Different graph_state */
 428           set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
 429         }
 430
 431       }
 432
 433     }
 434
 435     if(MC_state_interleave_size(current_pair->graph_state) > 0){
 436       MC_restore_snapshot(current_snapshot);
 437       MC_UNSET_RAW_MEM;
 438       //XBT_DEBUG("Snapshot restored");
 439     }
 440   }
 441
 442   if((search_cycle == 1) && (reached(current_pair->graph_state, current_pair->automaton_state) == 1)){
 443     XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 444     XBT_INFO("|             ACCEPTANCE CYCLE            |");
 445     XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 446     XBT_INFO("Counter-example that violates formula :");
 447     MC_show_snapshot_stack(mc_snapshot_stack);
 448     MC_dump_snapshot_stack(mc_snapshot_stack);
 449     exit(0);
 450   }
 451
 452   MC_SET_RAW_MEM;
 453   xbt_fifo_shift(mc_snapshot_stack);
 454   //XBT_DEBUG("State shifted in snapshot_stack, mc_snapshot_stack size=%d", xbt_fifo_size(mc_snapshot_stack));
 455   MC_UNSET_RAW_MEM;
 456
 457
 458 }
 459
 460 void MC_show_snapshot_stack(xbt_fifo_t stack){
 461   int value;
 462   mc_pairs_t pair;
 463   xbt_fifo_item_t item;
 464   smx_req_t req;
 465   char *req_str = NULL;
 466
 467   for (item = xbt_fifo_get_last_item(stack);
 468        (item ? (pair = (mc_pairs_t) (xbt_fifo_get_item_content(item)))
 469         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 470     req = MC_state_get_executed_request(pair->graph_state, &value);
 471     if(req){
 472       req_str = MC_request_to_string(req, value);
 473       XBT_INFO("%s", req_str);
 474       xbt_free(req_str);
 475     }
 476   }
 477 }
 478
 479 void MC_dump_snapshot_stack(xbt_fifo_t stack){
 480   mc_pairs_t pair;
 481
 482   MC_SET_RAW_MEM;
 483   while ((pair = (mc_pairs_t) xbt_fifo_pop(stack)) != NULL)
 484     MC_pair_delete(pair);
 485   MC_UNSET_RAW_MEM;
 486 }
 487
 488 void MC_pair_delete(mc_pairs_t pair){
 489   xbt_free(pair->graph_state->proc_status);
 490   xbt_free(pair->graph_state);
 491   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 492   xbt_free(pair);
 493 }
 494
 495
 496 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 497
 498   switch(l->type){
 499   case 0 : {
 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 1 : {
 506     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 507     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 508     return (left_res && right_res);
 509     break;
 510   }
 511   case 2 : {
 512     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
 513     return (!res);
 514     break;
 515   }
 516   case 3 : {
 517     unsigned int cursor = 0;
 518     xbt_propositional_symbol_t p = NULL;
 519     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
 520       if(strcmp(p->pred, l->u.predicat) == 0){
 521         int (*f)() = p->function;
 522         return (*f)();
 523       }
 524     }
 525     return -1;
 526     break;
 527   }
 528   case 4 : {
 529     return 2;
 530     break;
 531   }
 532   default :
 533     return -1;
 534   }
 535 }
 536
 537 /*void MC_dfs(xbt_automaton_t a, int search_cycle){
 538
 539   xbt_state_t current_state = (xbt_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(stack_automaton_dfs));
 540   xbt_transition_t transition_succ = NULL;
 541   xbt_state_t successor = NULL;
 542   unsigned int cursor = 0;
 543   xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
 544   int res;
 545
 546   //printf("++ current state : %s\n", current_state->id);
 547
 548   xbt_dynar_foreach(current_state->out, cursor, transition_succ){
 549     successor = transition_succ->dst;
 550     res = MC_automaton_evaluate_label(a, transition_succ->label);
 551     //printf("-- state : %s, transition_label : %d, res = %d\n", successor->id, transition_succ->label->type, res);
 552     if(res == 1){
 553       if(search_cycle == 1 && reached_dfs != NULL){
 554         if(strcmp(reached_dfs->id, successor->id) == 0){
 555           xbt_dynar_push(state_automaton_visited_dfs, &successor);
 556           printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 557           printf("Visited states : \n");
 558           unsigned int cursor2 = 0;
 559           xbt_state_t visited_state = NULL;
 560           xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
 561             printf("State : %s\n", visited_state->id);
 562           }
 563           exit(1);
 564         }
 565       }
 566       if(successor->visited == 0){
 567         successor->visited = 1;
 568         xbt_fifo_unshift(stack_automaton_dfs, successor);
 569         xbt_dynar_push(state_automaton_visited_dfs, &successor);
 570         MC_dfs(a, search_cycle);
 571         if(search_cycle == 0 && successor->type == 1){
 572           reached_dfs = successor;
 573           MC_dfs(a, 1);
 574         }
 575       }
 576     }else{
 577       if(res == 2){
 578         xbt_dynar_push(elses,&transition_succ);
 579       }
 580     }
 581   }
 582
 583   cursor = 0;
 584   xbt_dynar_foreach(elses, cursor, transition_succ){
 585    successor = transition_succ->dst;
 586    if(search_cycle == 1 && reached_dfs != NULL){
 587      if(strcmp(reached_dfs->id, successor->id) == 0){
 588        xbt_dynar_push(state_automaton_visited_dfs, &successor);
 589        printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 590        printf("Visited states : \n");
 591        unsigned int cursor2 = 0;
 592        xbt_state_t visited_state = NULL;
 593        xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
 594          printf("State : %s\n", visited_state->id);
 595        }
 596        exit(1);
 597      }
 598    }
 599    if(successor->visited == 0){
 600      successor->visited = 1;
 601      xbt_fifo_unshift(stack_automaton_dfs, successor);
 602      xbt_dynar_push(state_automaton_visited_dfs, &successor);
 603      MC_dfs(a, search_cycle);
 604      if(search_cycle == 0 && successor->type == 1){
 605        reached_dfs = successor;
 606        MC_dfs(a, 1);
 607      }
 608    }
 609   }
 610
 611   xbt_fifo_shift(stack_automaton_dfs);
 612   }*/