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