src/mc/mc_state.c

   1 #include "../simix/private.h"
   2 #include "xbt/fifo.h"
   3 #include "private.h"
   4
   5 /**
   6  * \brief Creates a state data structure used by the exploration algorithm
   7  */
   8 mc_state_t MC_state_new(void)
   9 {
  10   mc_state_t state = NULL;
  11
  12   state = xbt_new0(s_mc_state_t, 1);
  13   state->max_pid = simix_process_maxpid;
  14   state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid);
  15
  16   mc_stats->expanded_states++;
  17   return state;
  18 }
  19
  20 /**
  21  * \brief Deletes a state data structure
  22  * \param trans The state to be deleted
  23  */
  24 void MC_state_delete(mc_state_t state)
  25 {
  26   xbt_free(state->proc_status);
  27   xbt_free(state);
  28 }
  29
  30 void MC_state_interleave_process(mc_state_t state, smx_process_t process)
  31 {
  32   state->proc_status[process->pid].state = MC_INTERLEAVE;
  33   state->proc_status[process->pid].interleave_count = 0;
  34 }
  35
  36 unsigned int MC_state_interleave_size(mc_state_t state)
  37 {
  38   unsigned int i, size=0;
  39
  40   for(i=0; i < state->max_pid; i++){
  41     if(state->proc_status[i].state == MC_INTERLEAVE)
  42       size++;
  43   }
  44
  45   return size;
  46 }
  47
  48 int MC_state_process_is_done(mc_state_t state, smx_process_t process){
  49   return state->proc_status[process->pid].state == MC_DONE ? TRUE : FALSE;
  50 }
  51
  52 void MC_state_set_executed_request(mc_state_t state, smx_req_t req, int value)
  53 {
  54   /* The waitany and testany request are transformed into a wait or test request over the
  55    * corresponding communication action so it can be treated later by the dependence
  56    * function. */
  57   switch(req->call){
  58     case REQ_COMM_WAITANY:
  59       state->internal_req.call = REQ_COMM_WAIT;
  60       state->internal_req.issuer = req->issuer;
  61       state->internal_comm = *xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t);
  62       state->internal_req.comm_wait.comm = &state->internal_comm;
  63       state->internal_req.comm_wait.timeout = 0;
  64       break;
  65
  66     case REQ_COMM_TESTANY:
  67       state->internal_req.call = REQ_COMM_TEST;
  68       state->internal_req.issuer = req->issuer;
  69
  70       if(value > 0)
  71         state->internal_comm = *xbt_dynar_get_as(req->comm_testany.comms, value, smx_action_t);
  72
  73       state->internal_req.comm_wait.comm = &state->internal_comm;
  74       state->internal_req.comm_test.result = value;
  75       break;
  76
  77     case REQ_COMM_WAIT:
  78       state->internal_req = *req;
  79       state->internal_comm = *req->comm_wait.comm;
  80       state->internal_req.comm_wait.comm = &state->internal_comm;
  81       break;
  82
  83     case REQ_COMM_TEST:
  84       state->internal_req = *req;
  85       state->internal_comm = *req->comm_test.comm;
  86       state->internal_req.comm_test.comm = &state->internal_comm;
  87       break;
  88
  89     default:
  90       state->internal_req = *req;
  91       break;
  92   }
  93
  94   state->executed_req = *req;
  95   state->req_num = value;
  96 }
  97
  98 smx_req_t MC_state_get_executed_request(mc_state_t state, int *value)
  99 {
 100   *value = state->req_num;
 101   return &state->executed_req;
 102 }
 103
 104 smx_req_t MC_state_get_internal_request(mc_state_t state)
 105 {
 106   return &state->internal_req;
 107 }
 108
 109 smx_req_t MC_state_get_request(mc_state_t state, int *value)
 110 {
 111   smx_process_t process = NULL;
 112   mc_procstate_t procstate = NULL;
 113
 114
 115   xbt_swag_foreach(process, simix_global->process_list){
 116     procstate = &state->proc_status[process->pid];
 117
 118     if(procstate->state == MC_INTERLEAVE){
 119       if(SIMIX_process_is_enabled(process)){
 120         switch(process->request.call){
 121           case REQ_COMM_WAITANY:
 122             *value = -1;
 123             while(procstate->interleave_count < xbt_dynar_length(process->request.comm_waitany.comms)){
 124               if(SIMIX_request_is_enabled_by_idx(&process->request, procstate->interleave_count++)){
 125                 *value = procstate->interleave_count-1;
 126                 break;
 127               }
 128             }
 129
 130             if(procstate->interleave_count >= xbt_dynar_length(process->request.comm_waitany.comms))
 131               procstate->state = MC_DONE;
 132
 133             if(*value != -1)
 134               return &process->request;
 135
 136             break;
 137
 138           case REQ_COMM_TESTANY:
 139             *value = -1;
 140             if(MC_request_testany_fail(&process->request)){
 141               procstate->state = MC_DONE;
 142               return &process->request;
 143             }
 144
 145             while(procstate->interleave_count < xbt_dynar_length(process->request.comm_testany.comms)){
 146               if(SIMIX_request_is_enabled_by_idx(&process->request, procstate->interleave_count++)){
 147                 *value = procstate->interleave_count - 1;
 148                 break;
 149               }
 150             }
 151
 152             if(procstate->interleave_count >= xbt_dynar_length(process->request.comm_testany.comms))
 153               procstate->state = MC_DONE;
 154
 155             if(*value != -1)
 156               return &process->request;
 157
 158             break;
 159
 160           default:
 161             procstate->state = MC_DONE;
 162             *value = 0;
 163             return &process->request;
 164             break;
 165         }
 166       }
 167     }
 168   }
 169
 170   return NULL;
 171 }