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   default :
 160     return -1;
 161   }
 162 }
 163
 164 /*void MC_dfs(xbt_automaton_t a, int search_cycle){
 165
 166   xbt_state_t current_state = (xbt_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(stack_automaton_dfs));
 167   xbt_transition_t transition_succ = NULL;
 168   xbt_state_t successor = NULL;
 169   unsigned int cursor = 0;
 170   xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
 171   int res;
 172
 173   //printf("++ current state : %s\n", current_state->id);
 174
 175   xbt_dynar_foreach(current_state->out, cursor, transition_succ){
 176     successor = transition_succ->dst;
 177     res = MC_automaton_evaluate_label(a, transition_succ->label);
 178     //printf("-- state : %s, transition_label : %d, res = %d\n", successor->id, transition_succ->label->type, res);
 179     if(res == 1){
 180       if(search_cycle == 1 && reached_dfs != NULL){
 181         if(strcmp(reached_dfs->id, successor->id) == 0){
 182           xbt_dynar_push(state_automaton_visited_dfs, &successor);
 183           printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 184           printf("Visited states : \n");
 185           unsigned int cursor2 = 0;
 186           xbt_state_t visited_state = NULL;
 187           xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
 188             printf("State : %s\n", visited_state->id);
 189           }
 190           exit(1);
 191         }
 192       }
 193       if(successor->visited == 0){
 194         successor->visited = 1;
 195         xbt_fifo_unshift(stack_automaton_dfs, successor);
 196         xbt_dynar_push(state_automaton_visited_dfs, &successor);
 197         MC_dfs(a, search_cycle);
 198         if(search_cycle == 0 && successor->type == 1){
 199           reached_dfs = successor;
 200           MC_dfs(a, 1);
 201         }
 202       }
 203     }else{
 204       if(res == 2){
 205         xbt_dynar_push(elses,&transition_succ);
 206       }
 207     }
 208   }
 209
 210   cursor = 0;
 211   xbt_dynar_foreach(elses, cursor, transition_succ){
 212    successor = transition_succ->dst;
 213    if(search_cycle == 1 && reached_dfs != NULL){
 214      if(strcmp(reached_dfs->id, successor->id) == 0){
 215        xbt_dynar_push(state_automaton_visited_dfs, &successor);
 216        printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 217        printf("Visited states : \n");
 218        unsigned int cursor2 = 0;
 219        xbt_state_t visited_state = NULL;
 220        xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
 221          printf("State : %s\n", visited_state->id);
 222        }
 223        exit(1);
 224      }
 225    }
 226    if(successor->visited == 0){
 227      successor->visited = 1;
 228      xbt_fifo_unshift(stack_automaton_dfs, successor);
 229      xbt_dynar_push(state_automaton_visited_dfs, &successor);
 230      MC_dfs(a, search_cycle);
 231      if(search_cycle == 0 && successor->type == 1){
 232        reached_dfs = successor;
 233        MC_dfs(a, 1);
 234      }
 235    }
 236   }
 237
 238   xbt_fifo_shift(stack_automaton_dfs);
 239   }*/
 240
 241
 242 void MC_dfs(xbt_automaton_t a, int search_cycle){
 243
 244   smx_process_t process = NULL;
 245   int value;
 246   mc_state_t next_graph_state = NULL;
 247   smx_req_t req = NULL;
 248   char *req_str;
 249
 250   xbt_transition_t transition_succ = NULL;
 251   xbt_state_t successor = NULL;
 252   unsigned int cursor = 0;
 253   xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
 254   int res;
 255   int enabled_transition = 0;
 256
 257   mc_pairs_t next_pair = NULL;
 258   mc_snapshot_t next_snapshot = NULL;
 259
 260
 261   /* Get current state */
 262   mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 263
 264   XBT_DEBUG("**************************************************");
 265   XBT_DEBUG("State=%p, %u interleave",current_pair->graph_state,MC_state_interleave_size(current_pair->graph_state));
 266
 267   /* Update statistics */
 268   mc_stats->visited_states++;
 269
 270   MC_restore_snapshot(current_pair->system_state);
 271   MC_UNSET_RAW_MEM;
 272
 273   //FIXME : vérifier condition permettant d'avoir tous les successeurs possibles dans le graph
 274
 275   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 276
 277     /* Debug information */
 278     if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){
 279       req_str = MC_request_to_string(req, value);
 280       XBT_DEBUG("Execute: %s", req_str);
 281       xbt_free(req_str);
 282     }
 283
 284     MC_state_set_executed_request(current_pair->graph_state, req, value);
 285     mc_stats->executed_transitions++;
 286
 287     /* Answer the request */
 288     SIMIX_request_pre(req, value);
 289
 290     /* Wait for requests (schedules processes) */
 291     MC_wait_for_requests();
 292
 293
 294     /* Create the new expanded graph_state */
 295     MC_SET_RAW_MEM;
 296
 297     next_graph_state = MC_state_new();
 298
 299     /* Get an enabled process and insert it in the interleave set of the next graph_state */
 300     xbt_swag_foreach(process, simix_global->process_list){
 301       if(MC_process_is_enabled(process)){
 302         MC_state_interleave_process(next_graph_state, process);
 303       }
 304     }
 305
 306     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 307     MC_take_snapshot(next_snapshot);
 308
 309     MC_UNSET_RAW_MEM;
 310
 311     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 312       successor = transition_succ->dst;
 313       res = MC_automaton_evaluate_label(a, transition_succ->label);
 314       if(res == 1){ // enabled transition
 315
 316         MC_SET_RAW_MEM;
 317         next_pair = new_pair(next_snapshot, next_graph_state, successor);
 318
 319         if((search_cycle == 1) && (pair_reached(list_pairs_reached, next_pair->num) == 1)){
 320           printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 321           // afficher chemin menant au cycle d'acceptation
 322           exit(1);
 323         }
 324         if(next_pair->visited == 0){ // FIXME : tester avec search_cycle ?
 325           xbt_fifo_unshift(mc_snapshot_stack, next_pair);
 326           set_pair_visited(next_pair);
 327           MC_dfs(a, search_cycle);
 328           if((search_cycle == 0) && (next_pair->automaton_state->type == 1)){
 329             xbt_dynar_push(list_pairs_reached, &next_pair->num);
 330             MC_dfs(a, 1);
 331           }
 332         }
 333
 334         MC_UNSET_RAW_MEM;
 335         enabled_transition = 1;
 336       }else{
 337         if(res == 2){
 338           xbt_dynar_push(elses,&transition_succ);
 339         }
 340       }
 341     }
 342
 343     if(enabled_transition == 0){
 344       cursor = 0;
 345       xbt_dynar_foreach(elses, cursor, transition_succ){
 346         successor = transition_succ->dst;
 347         MC_SET_RAW_MEM;
 348         next_pair = new_pair(next_snapshot, next_graph_state, successor);
 349
 350         if((search_cycle == 1) && (pair_reached(list_pairs_reached, next_pair->num) == 1)){
 351           printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
 352           // afficher chemin menant au cycle d'acceptation
 353           exit(1);
 354         }
 355         if(next_pair->visited == 0){ // FIXME : tester avec search_cycle ?
 356           xbt_fifo_unshift(mc_snapshot_stack, next_pair);
 357           set_pair_visited(next_pair);
 358           MC_dfs(a, search_cycle);
 359           if((search_cycle == 0) && (next_pair->automaton_state->type == 1)){
 360             xbt_dynar_push(list_pairs_reached, &next_pair->num);
 361             MC_dfs(a, 1);
 362           }
 363         }
 364
 365         MC_UNSET_RAW_MEM;
 366       }
 367     }
 368
 369   }
 370
 371   xbt_fifo_shift(mc_snapshot_stack);
 372
 373 }