3 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans, mc,
4 "Logging specific to MC transitions");
6 /* Creates a new iSend transition */
7 mc_transition_t MC_trans_isend_new(smx_rdv_t rdv)
9 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
11 trans->type = mc_isend;
12 trans->process = SIMIX_process_self();
13 trans->isend.rdv = rdv;
14 trans->name = bprintf("[%s][%s] iSend (%p)", trans->process->smx_host->name,
15 trans->process->name, trans);
19 /* Creates a new iRecv transition */
20 mc_transition_t MC_trans_irecv_new(smx_rdv_t rdv)
22 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
24 trans->type = mc_irecv;
25 trans->process = SIMIX_process_self();
26 trans->irecv.rdv = rdv;
27 trans->name = bprintf("[%s][%s] iRecv (%p)", trans->process->smx_host->name,
28 trans->process->name, trans);
32 /* Creates a new Wait transition */
33 mc_transition_t MC_trans_wait_new(smx_comm_t comm)
35 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
37 trans->type = mc_wait;
38 trans->process = SIMIX_process_self();
39 trans->wait.comm = comm;
40 trans->name = bprintf("[%s][%s] Wait (%p)", trans->process->smx_host->name,
41 trans->process->name, trans);
45 /* Creates a new test transition */
46 mc_transition_t MC_trans_test_new(smx_comm_t comm)
48 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
50 trans->type = mc_test;
51 trans->process = SIMIX_process_self();
52 trans->test.comm = comm;
53 trans->name = bprintf("[%s][%s] Test (%p)", trans->process->smx_host->name,
54 trans->process->name, trans);
58 /* Creates a new WaitAny transition */
59 mc_transition_t MC_trans_waitany_new(xbt_dynar_t comms)
61 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
63 trans->type = mc_waitany;
64 trans->process = SIMIX_process_self();
65 trans->waitany.comms = comms;
66 trans->name = bprintf("[%s][%s] WaitAny (%p)", trans->process->smx_host->name,
67 trans->process->name, trans);
71 /* Creates a new Random transition */
72 mc_transition_t MC_trans_random_new(int value)
74 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
76 trans->type = mc_random;
77 trans->process = SIMIX_process_self();
78 trans->random.value = value;
79 trans->name = bprintf("[%s][%s] Random %d (%p)", trans->process->smx_host->name,
80 trans->process->name, value, trans);
86 * \brief Deletes a transition
87 * \param trans The transition to be deleted
89 void MC_transition_delete(mc_transition_t trans)
91 xbt_free(trans->name);
95 /************************** Interception Functions ****************************/
96 /* These functions intercept all the actions relevant to the model-checking
97 * process, the only difference between them is the type of transition they
98 * create. The interception works by yielding the process performer of the
99 * action, and depending on the execution mode it behaves diferently.
100 * There are two running modes, a replay (back-track process) in which no
101 * transition needs to be created, or a new state expansion, which in
102 * consecuence a transition needs to be created and added to the set of
103 * transitions associated to the current state.
107 * \brief Intercept an iSend action
108 * \param rdv The rendez-vous of the iSend
110 void MC_trans_intercept_isend(smx_rdv_t rdv)
112 mc_transition_t trans=NULL;
113 mc_state_t current_state = NULL;
116 trans = MC_trans_isend_new(rdv);
117 current_state = (mc_state_t)
118 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
119 xbt_setset_set_insert(current_state->created_transitions, trans);
120 xbt_setset_set_insert(current_state->transitions, trans);
123 SIMIX_process_yield();
127 * \brief Intercept an iRecv action
128 * \param rdv The rendez-vous of the iRecv
130 void MC_trans_intercept_irecv(smx_rdv_t rdv)
132 mc_transition_t trans=NULL;
133 mc_state_t current_state = NULL;
136 trans = MC_trans_irecv_new(rdv);
137 current_state = (mc_state_t)
138 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
139 xbt_setset_set_insert(current_state->created_transitions, trans);
140 xbt_setset_set_insert(current_state->transitions, trans);
143 SIMIX_process_yield();
147 * \brief Intercept a Wait action
148 * \param comm The communication associated to the wait
150 void MC_trans_intercept_wait(smx_comm_t comm)
152 mc_transition_t trans=NULL;
153 mc_state_t current_state = NULL;
156 trans = MC_trans_wait_new(comm);
157 current_state = (mc_state_t)
158 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
159 xbt_setset_set_insert(current_state->created_transitions, trans);
160 xbt_setset_set_insert(current_state->transitions, trans);
163 SIMIX_process_yield();
167 * \brief Intercept a Test action
168 * \param comm The communication associated to the Test
170 void MC_trans_intercept_test(smx_comm_t comm)
172 mc_transition_t trans=NULL;
173 mc_state_t current_state = NULL;
176 trans = MC_trans_test_new(comm);
177 current_state = (mc_state_t)
178 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
179 xbt_setset_set_insert(current_state->created_transitions, trans);
180 xbt_setset_set_insert(current_state->transitions, trans);
183 SIMIX_process_yield();
187 * \brief Intercept a WaitAny action
188 * \param comms The communications associated to the WaitAny
190 void MC_trans_intercept_waitany(xbt_dynar_t comms)
193 mc_transition_t trans = NULL;
194 mc_state_t current_state = NULL;
195 smx_comm_t comm = NULL;
199 current_state = (mc_state_t)
200 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
201 xbt_dynar_foreach(comms, cursor, comm){
202 trans = MC_trans_wait_new(comm);
203 xbt_setset_set_insert(current_state->created_transitions, trans);
204 xbt_setset_set_insert(current_state->transitions, trans);
208 SIMIX_process_yield();
212 * \brief Intercept a Random action
213 * \param min The minimum value that can be returned by the Random action
214 * \param max The maximum value that can be returned by the Random action
216 void MC_trans_intercept_random(int min, int max)
219 mc_transition_t trans=NULL;
220 mc_state_t current_state = NULL;
223 current_state = (mc_state_t)
224 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
225 for(i=min; i <= max; i++){
226 trans = MC_trans_random_new(i);
227 xbt_setset_set_insert(current_state->created_transitions, trans);
228 xbt_setset_set_insert(current_state->transitions, trans);
232 SIMIX_process_yield();
235 /* Compute the subset of enabled transitions of the transition set */
236 void MC_trans_compute_enabled(xbt_setset_set_t enabled, xbt_setset_set_t transitions)
238 unsigned int index = 0;
239 smx_comm_t comm = NULL;
240 mc_transition_t trans = NULL;
241 xbt_setset_cursor_t cursor = NULL;
242 xbt_setset_foreach(transitions, cursor, trans){
244 /* Wait transitions are enabled only if the communication has both a
245 sender and receiver */
247 if(trans->wait.comm->src_proc && trans->wait.comm->dst_proc){
248 xbt_setset_set_insert(enabled, trans);
249 DEBUG1("Transition %p is enabled for next state", trans);
253 /* WaitAny transitions are enabled if any of it's communications has both
254 a sender and a receiver */
256 xbt_dynar_foreach(trans->waitany.comms, index, comm){
257 if(comm->src_proc && comm->dst_proc){
258 xbt_setset_set_insert(enabled, trans);
259 DEBUG1("Transition %p is enabled for next state", trans);
265 /* The rest of the transitions cannot be disabled */
267 xbt_setset_set_insert(enabled, trans);
268 DEBUG1("Transition %p is enabled for next state", trans);
275 * \brief Determine if two transitions are dependent
276 * \param t1 a transition
277 * \param t2 a transition
278 * \return TRUE if \a t1 and \a t2 are dependent. FALSE otherwise.
280 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
282 if(t1->process == t2->process)
285 if(t1->type != t2->type)
288 if(t1->type == mc_random || t2->type == mc_random)
291 if(t1->type == mc_isend && t2->type == mc_isend && t1->isend.rdv != t2->isend.rdv)
294 if(t1->type == mc_irecv && t2->type == mc_irecv && t1->irecv.rdv != t2->irecv.rdv)
297 if(t1->type == mc_wait && t2->type == mc_wait && t1->wait.comm == t2->wait.comm)
300 if(t1->type == mc_wait && t2->type == mc_wait
301 && t1->wait.comm->src_buff != NULL
302 && t1->wait.comm->dst_buff != NULL
303 && t2->wait.comm->src_buff != NULL
304 && t2->wait.comm->dst_buff != NULL
305 && t1->wait.comm->dst_buff != t2->wait.comm->src_buff
306 && t1->wait.comm->dst_buff != t2->wait.comm->dst_buff
307 && t2->wait.comm->dst_buff != t1->wait.comm->src_buff)