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