src/mc/mc_dfs.c

   1 #include "private.h"
   2
   3 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc,
   4                                 "Logging specific to MC DFS algorithm");
   5
   6
   7 extern xbt_fifo_t mc_snapshot_stack;
   8 mc_pairs_t mc_reached = NULL;
   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
  14 mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
  15   mc_pairs_t p = NULL;
  16   p = xbt_new0(s_mc_pairs_t, 1);
  17   p->system_state = sn;
  18   p->automaton_state = st;
  19   p->graph_state = sg;
  20   p->visited = 0;
  21   p->num = max_pair;
  22   max_pair++;
  23   return p;
  24
  25 }
  26
  27 void set_pair_visited(mc_pairs_t p){
  28   p->visited = 1;
  29 }
  30
  31 int pair_reached(xbt_dynar_t p, int num_pair){
  32   int n;
  33   unsigned int cursor = 0;
  34   xbt_dynar_foreach(p, cursor, n){
  35     if(n == num_pair)
  36       return 1;
  37   }
  38   return 0;
  39 }
  40
  41 void MC_dfs_init(xbt_automaton_t a){
  42
  43   mc_pairs_t mc_initial_pair = NULL;
  44   mc_state_t initial_graph_state = NULL;
  45   smx_process_t process;
  46
  47   MC_wait_for_requests();
  48
  49   MC_SET_RAW_MEM;
  50
  51   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
  52   MC_take_snapshot(initial_snapshot);
  53   initial_graph_state = MC_state_new();
  54   xbt_swag_foreach(process, simix_global->process_list){
  55     if(MC_process_is_enabled(process)){
  56       MC_state_interleave_process(initial_graph_state, process);
  57     }
  58   }
  59
  60   list_pairs_reached = xbt_dynar_new(sizeof(int), NULL);
  61
  62   MC_UNSET_RAW_MEM;
  63
  64
  65   //regarder dans l'automate toutes les transitions activables grâce à l'état initial du système -> donnera les états initiaux de la propriété consistants avec l'état initial du système
  66
  67   unsigned int cursor = 0;
  68   xbt_state_t state = NULL;
  69   unsigned int cursor2 = 0;
  70   int res;
  71   xbt_transition_t transition_succ = NULL;
  72   xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
  73   int enabled_transition = 0;
  74
  75   xbt_dynar_foreach(a->states, cursor, state){
  76     if(state->type == -1){
  77       xbt_dynar_foreach(state->out, cursor2, transition_succ){
  78
  79         res = MC_automaton_evaluate_label(a, transition_succ->label);
  80
  81         if(res == 1){
  82
  83           MC_SET_RAW_MEM;
  84
  85           mc_initial_pair = new_pair(initial_snapshot, initial_graph_state, transition_succ->dst);
  86           xbt_fifo_unshift(mc_snapshot_stack, mc_initial_pair);
  87           set_pair_visited(mc_initial_pair);
  88
  89           MC_UNSET_RAW_MEM;
  90
  91           enabled_transition = 1;
  92
  93           XBT_DEBUG(" ++++++++++++++++++ new initial pair +++++++++++++++++++");
  94
  95           MC_dfs(a, 0);
  96         }else{
  97           if(res == 2){
  98             xbt_dynar_push(elses,&transition_succ);
  99           }
 100         }
 101       }
 102     }
 103   }
 104
 105   if(enabled_transition == 0){
 106     cursor2 = 0;
 107     xbt_dynar_foreach(elses, cursor, transition_succ){
 108
 109       MC_SET_RAW_MEM;
 110
 111       mc_initial_pair = new_pair(initial_snapshot, initial_graph_state, transition_succ->dst);
 112       xbt_fifo_unshift(mc_snapshot_stack, mc_initial_pair);
 113       set_pair_visited(mc_initial_pair);
 114
 115       MC_UNSET_RAW_MEM;
 116
 117       MC_dfs(a, 0);
 118     }
 119   }
 120
 121 }
 122
 123 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 124
 125   switch(l->type){
 126   case 0 : {
 127     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 128     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 129     return (left_res || right_res);
 130     break;
 131   }
 132   case 1 : {
 133     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 134     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 135     return (left_res && right_res);
 136     break;
 137   }
 138   case 2 : {
 139     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
 140     return (!res);
 141     break;
 142   }
 143   case 3 : {
 144     unsigned int cursor = 0;
 145     xbt_propositional_symbol_t p = NULL;
 146     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
 147       if(strcmp(p->pred, l->u.predicat) == 0){
 148         int (*f)() = p->function;
 149         return (*f)();
 150       }
 151     }
 152     return -1;
 153     break;
 154   }
 155   case 4 : {
 156     return 2;
 157     break;
 158   }
 159   }
 160 }
 161
 162 /*void MC_dfs(xbt_automaton_t a, int search_cycle){
 163
 164   xbt_state_t current_state = (xbt_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(stack_automaton_dfs));
 165   xbt_transition_t transition_succ = NULL;
 166   xbt_state_t successor = NULL;
 167   unsigned int cursor = 0;
 168   xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
 169   int res;
 170
 171   //printf("++ current state : %s\n", current_state->id);
 172
 173   xbt_dynar_foreach(current_state->out, cursor, transition_succ){
 174     successor = transition_succ->dst;
 175     res = MC_automaton_evaluate_label(a, transition_succ->label);
 176     //printf("-- state : %s, transition_label : %d, res = %d\n", successor->id, transition_succ->label->type, res);
 177     if(res == 1){
 178       if(search_cycle == 1 && reached_dfs != NULL){
 179         if(strcmp(reached_dfs->id, successor->id) == 0){
 180           xbt_dynar_push(state_automaton_visited_dfs, &successor);
 181           printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 182           printf("Visited states : \n");
 183           unsigned int cursor2 = 0;
 184           xbt_state_t visited_state = NULL;
 185           xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
 186             printf("State : %s\n", visited_state->id);
 187           }
 188           exit(1);
 189         }
 190       }
 191       if(successor->visited == 0){
 192         successor->visited = 1;
 193         xbt_fifo_unshift(stack_automaton_dfs, successor);
 194         xbt_dynar_push(state_automaton_visited_dfs, &successor);
 195         MC_dfs(a, search_cycle);
 196         if(search_cycle == 0 && successor->type == 1){
 197           reached_dfs = successor;
 198           MC_dfs(a, 1);
 199         }
 200       }
 201     }else{
 202       if(res == 2){
 203         xbt_dynar_push(elses,&transition_succ);
 204       }
 205     }
 206   }
 207
 208   cursor = 0;
 209   xbt_dynar_foreach(elses, cursor, transition_succ){
 210    successor = transition_succ->dst;
 211    if(search_cycle == 1 && reached_dfs != NULL){
 212      if(strcmp(reached_dfs->id, successor->id) == 0){
 213        xbt_dynar_push(state_automaton_visited_dfs, &successor);
 214        printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 215        printf("Visited states : \n");
 216        unsigned int cursor2 = 0;
 217        xbt_state_t visited_state = NULL;
 218        xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
 219          printf("State : %s\n", visited_state->id);
 220        }
 221        exit(1);
 222      }
 223    }
 224    if(successor->visited == 0){
 225      successor->visited = 1;
 226      xbt_fifo_unshift(stack_automaton_dfs, successor);
 227      xbt_dynar_push(state_automaton_visited_dfs, &successor);
 228      MC_dfs(a, search_cycle);
 229      if(search_cycle == 0 && successor->type == 1){
 230        reached_dfs = successor;
 231        MC_dfs(a, 1);
 232      }
 233    }
 234   }
 235
 236   xbt_fifo_shift(stack_automaton_dfs);
 237   }*/
 238
 239
 240 void MC_dfs(xbt_automaton_t a, int search_cycle){
 241
 242   smx_process_t process = NULL;
 243   int value;
 244   mc_state_t state = NULL;
 245   mc_state_t next_graph_state = NULL;
 246   smx_req_t req = NULL;
 247   char *req_str;
 248
 249   xbt_transition_t transition_succ = NULL;
 250   xbt_state_t successor = NULL;
 251   unsigned int cursor = 0;
 252   xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
 253   int res;
 254   int enabled_transition = 0;
 255
 256   mc_pairs_t next_pair = NULL;
 257   mc_snapshot_t next_snapshot = NULL;
 258
 259
 260   /* Get current state */
 261   mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 262
 263   XBT_DEBUG("**************************************************");
 264   XBT_DEBUG("State=%p, %u interleave",current_pair->graph_state,MC_state_interleave_size(current_pair->graph_state));
 265
 266   /* Update statistics */
 267   mc_stats->visited_states++;
 268
 269   MC_restore_snapshot(current_pair->system_state);
 270   MC_UNSET_RAW_MEM;
 271
 272   //FIXME : vérifier condition permettant d'avoir tous les successeurs possibles dans le graph
 273
 274   while(req = MC_state_get_request(current_pair->graph_state, &value)){
 275
 276     /* Debug information */
 277     if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){
 278       req_str = MC_request_to_string(req, value);
 279       XBT_DEBUG("Execute: %s", req_str);
 280       xbt_free(req_str);
 281     }
 282
 283     MC_state_set_executed_request(current_pair->graph_state, req, value);
 284     mc_stats->executed_transitions++;
 285
 286     /* Answer the request */
 287     SIMIX_request_pre(req, value);
 288
 289     /* Wait for requests (schedules processes) */
 290     MC_wait_for_requests();
 291
 292
 293     /* Create the new expanded graph_state */
 294     MC_SET_RAW_MEM;
 295
 296     next_graph_state = MC_state_new();
 297
 298     /* Get an enabled process and insert it in the interleave set of the next graph_state */
 299     xbt_swag_foreach(process, simix_global->process_list){
 300       if(MC_process_is_enabled(process)){
 301         MC_state_interleave_process(next_graph_state, process);
 302       }
 303     }
 304
 305     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 306     MC_take_snapshot(next_snapshot);
 307
 308     MC_UNSET_RAW_MEM;
 309
 310     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 311       successor = transition_succ->dst;
 312       res = MC_automaton_evaluate_label(a, transition_succ->label);
 313       if(res == 1){ // enabled transition
 314
 315         MC_SET_RAW_MEM;
 316         next_pair = new_pair(next_snapshot, next_graph_state, successor);
 317
 318         if((search_cycle == 1) && (pair_reached(list_pairs_reached, next_pair->num) == 1)){
 319           printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 320           // afficher chemin menant au cycle d'acceptation
 321           exit(1);
 322         }
 323         if(next_pair->visited == 0){ // FIXME : tester avec search_cycle ?
 324           xbt_fifo_unshift(mc_snapshot_stack, next_pair);
 325           set_pair_visited(next_pair);
 326           MC_dfs(a, search_cycle);
 327           if((search_cycle == 0) && (next_pair->automaton_state->type == 1)){
 328             xbt_dynar_push(list_pairs_reached, &next_pair->num);
 329             MC_dfs(a, 1);
 330           }
 331         }
 332
 333         MC_UNSET_RAW_MEM;
 334         enabled_transition = 1;
 335       }else{
 336         if(res == 2){
 337           xbt_dynar_push(elses,&transition_succ);
 338         }
 339       }
 340     }
 341
 342     if(enabled_transition == 0){
 343       cursor = 0;
 344       xbt_dynar_foreach(elses, cursor, transition_succ){
 345         successor = transition_succ->dst;
 346         MC_SET_RAW_MEM;
 347         next_pair = new_pair(next_snapshot, next_graph_state, successor);
 348
 349         if((search_cycle == 1) && (pair_reached(list_pairs_reached, next_pair->num) == 1)){
 350           printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 351           // afficher chemin menant au cycle d'acceptation
 352           exit(1);
 353         }
 354         if(next_pair->visited == 0){ // FIXME : tester avec search_cycle ?
 355           xbt_fifo_unshift(mc_snapshot_stack, next_pair);
 356           set_pair_visited(next_pair);
 357           MC_dfs(a, search_cycle);
 358           if((search_cycle == 0) && (next_pair->automaton_state->type == 1)){
 359             xbt_dynar_push(list_pairs_reached, &next_pair->num);
 360             MC_dfs(a, 1);
 361           }
 362         }
 363
 364         MC_UNSET_RAW_MEM;
 365       }
 366     }
 367
 368   }
 369
 370   xbt_fifo_shift(mc_snapshot_stack);
 371
 372 }