src/mc/mc_state.c

   1 #include "../simix/private.h"
   2 #include "xbt/fifo.h"
   3 #include "private.h"
   4
   5 static void MC_state_add_transition(mc_state_t state, mc_transition_t trans);
   6
   7 /**
   8  * \brief Creates a state data structure used by the exploration algorithm
   9  */
  10 mc_state_t MC_state_new(void)
  11 {
  12   mc_state_t state = NULL;
  13
  14   state = xbt_new0(s_mc_state_t, 1);
  15   state->max_pid = simix_process_maxpid;
  16   state->interleave = xbt_new0(char, state->max_pid);
  17
  18   mc_stats->expanded_states++;
  19   return state;
  20 }
  21
  22 /**
  23  * \brief Deletes a state data structure
  24  * \param trans The state to be deleted
  25  */
  26 void MC_state_delete(mc_state_t state)
  27 {
  28   xbt_free(state->interleave);
  29   xbt_free(state);
  30 }
  31
  32 void MC_state_add_to_interleave(mc_state_t state, smx_process_t process)
  33 {
  34   state->interleave[process->pid] = 1;
  35 }
  36
  37 unsigned int MC_state_interleave_size(mc_state_t state)
  38 {
  39   unsigned int i, size=0;
  40
  41   for(i=0; i < state->max_pid; i++){
  42     if(state->interleave[i] != 0 && state->interleave[i] != -1)
  43       size++;
  44   }
  45
  46   return size;
  47 }
  48
  49 int MC_state_process_is_done(mc_state_t state, smx_process_t process){
  50   return state->interleave[process->pid] == -1 ? TRUE : FALSE;
  51 }
  52
  53 void MC_state_set_executed_request(mc_state_t state, smx_req_t req)
  54 {
  55   state->executed = *req;
  56 }
  57
  58 smx_req_t MC_state_get_executed_request(mc_state_t state)
  59 {
  60   return &state->executed;
  61 }
  62
  63 smx_req_t MC_state_get_request(mc_state_t state, char *value)
  64 {
  65   unsigned int i;
  66   smx_process_t process = NULL;
  67
  68   for(i=0; i < state->max_pid; i++){
  69     if(state->interleave[i] > 0){
  70       *value = state->interleave[i]--;
  71
  72       /* If 0 was reached means that the process is done, so we
  73        * set it's value to -1 (the "done" value) */
  74       if(state->interleave[i] == 0)
  75         state->interleave[i]--;
  76
  77       /* FIXME: SIMIX should implement a process table indexed by pid */
  78       /* So we should use that instead of traversing the swag */
  79       xbt_swag_foreach(process, simix_global->process_list){
  80         if(process->pid == i)
  81           break;
  82       }
  83
  84       if(SIMIX_process_is_enabled(process))
  85         return &process->request;
  86     }
  87   }
  88
  89   return NULL;
  90 }