1 #include "../simix/private.h"
6 * \brief Creates a state data structure used by the exploration algorithm
8 mc_state_t MC_state_new(void)
10 mc_state_t state = NULL;
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);
16 mc_stats->expanded_states++;
21 * \brief Deletes a state data structure
22 * \param trans The state to be deleted
24 void MC_state_delete(mc_state_t state)
26 xbt_free(state->proc_status);
30 void MC_state_interleave_process(mc_state_t state, smx_process_t process)
32 state->proc_status[process->pid].state = MC_INTERLEAVE;
33 state->proc_status[process->pid].interleave_count = 0;
36 unsigned int MC_state_interleave_size(mc_state_t state)
38 unsigned int i, size=0;
40 for(i=0; i < state->max_pid; i++){
41 if(state->proc_status[i].state == MC_INTERLEAVE)
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;
52 void MC_state_set_executed_request(mc_state_t state, smx_req_t req, int value)
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
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;
66 case REQ_COMM_TESTANY:
67 state->internal_req.call = REQ_COMM_TEST;
68 state->internal_req.issuer = req->issuer;
71 state->internal_comm = *xbt_dynar_get_as(req->comm_testany.comms, value, smx_action_t);
73 state->internal_req.comm_wait.comm = &state->internal_comm;
74 state->internal_req.comm_test.result = value;
78 state->internal_req = *req;
79 state->internal_comm = *req->comm_wait.comm;
80 state->internal_req.comm_wait.comm = &state->internal_comm;
84 state->internal_req = *req;
85 state->internal_comm = *req->comm_test.comm;
86 state->internal_req.comm_test.comm = &state->internal_comm;
90 state->internal_req = *req;
94 state->executed_req = *req;
95 state->req_num = value;
98 smx_req_t MC_state_get_executed_request(mc_state_t state, int *value)
100 *value = state->req_num;
101 return &state->executed_req;
104 smx_req_t MC_state_get_internal_request(mc_state_t state)
106 return &state->internal_req;
109 smx_req_t MC_state_get_request(mc_state_t state, int *value)
111 smx_process_t process = NULL;
112 mc_procstate_t procstate = NULL;
115 xbt_swag_foreach(process, simix_global->process_list){
116 procstate = &state->proc_status[process->pid];
118 if(procstate->state == MC_INTERLEAVE){
119 if(SIMIX_process_is_enabled(process)){
120 switch(process->request.call){
121 case REQ_COMM_WAITANY:
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;
130 if(procstate->interleave_count >= xbt_dynar_length(process->request.comm_waitany.comms))
131 procstate->state = MC_DONE;
134 return &process->request;
138 case REQ_COMM_TESTANY:
140 if(MC_request_testany_fail(&process->request)){
141 procstate->state = MC_DONE;
142 return &process->request;
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;
152 if(procstate->interleave_count >= xbt_dynar_length(process->request.comm_testany.comms))
153 procstate->state = MC_DONE;
156 return &process->request;
161 procstate->state = MC_DONE;
163 return &process->request;