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;
15 bprintf("[%s]\t iSend (%p)", trans->process->smx_host->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;
28 bprintf("[%s]\t iRecv (%p)", trans->process->smx_host->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;
41 bprintf("[%s]\t Wait (%p)", trans->process->smx_host->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;
54 bprintf("[%s]\t Test (%p)", trans->process->smx_host->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;
67 bprintf("[%s]\t WaitAny (%p)", trans->process->smx_host->name,
72 /* Creates a new Random transition */
73 mc_transition_t MC_trans_random_new(int value)
75 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
77 trans->type = mc_random;
78 trans->process = SIMIX_process_self();
79 trans->random.value = value;
81 bprintf("[%s]\t Random %d (%p)", trans->process->smx_host->name,
88 * \brief Deletes a transition
89 * \param trans The transition to be deleted
91 void MC_transition_delete(mc_transition_t trans)
93 xbt_free(trans->name);
97 /************************** Interception Functions ****************************/
98 /* These functions intercept all the actions relevant to the model-checking
99 * process, the only difference between them is the type of transition they
100 * create. The interception works by yielding the process performer of the
101 * action, and depending on the execution mode it behaves diferently.
102 * There are two running modes, a replay (back-track process) in which no
103 * transition needs to be created, or a new state expansion, which in
104 * consecuence a transition needs to be created and added to the set of
105 * transitions associated to the current state.
109 * \brief Intercept an iSend action
110 * \param rdv The rendez-vous of the iSend
112 void MC_trans_intercept_isend(smx_rdv_t rdv)
114 mc_transition_t trans = NULL;
115 mc_state_t current_state = NULL;
116 if (!mc_replay_mode) {
118 trans = MC_trans_isend_new(rdv);
119 current_state = (mc_state_t)
120 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
121 xbt_setset_set_insert(current_state->created_transitions, trans);
122 xbt_setset_set_insert(current_state->transitions, trans);
125 SIMIX_process_yield();
129 * \brief Intercept an iRecv action
130 * \param rdv The rendez-vous of the iRecv
132 void MC_trans_intercept_irecv(smx_rdv_t rdv)
134 mc_transition_t trans = NULL;
135 mc_state_t current_state = NULL;
136 if (!mc_replay_mode) {
138 trans = MC_trans_irecv_new(rdv);
139 current_state = (mc_state_t)
140 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
141 xbt_setset_set_insert(current_state->created_transitions, trans);
142 xbt_setset_set_insert(current_state->transitions, trans);
145 SIMIX_process_yield();
149 * \brief Intercept a Wait action
150 * \param comm The communication associated to the wait
152 void MC_trans_intercept_wait(smx_comm_t comm)
154 mc_transition_t trans = NULL;
155 mc_state_t current_state = NULL;
156 if (!mc_replay_mode) {
158 trans = MC_trans_wait_new(comm);
159 current_state = (mc_state_t)
160 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
161 xbt_setset_set_insert(current_state->created_transitions, trans);
162 xbt_setset_set_insert(current_state->transitions, trans);
165 SIMIX_process_yield();
169 * \brief Intercept a Test action
170 * \param comm The communication associated to the Test
172 void MC_trans_intercept_test(smx_comm_t comm)
174 mc_transition_t trans = NULL;
175 mc_state_t current_state = NULL;
176 if (!mc_replay_mode) {
178 trans = MC_trans_test_new(comm);
179 current_state = (mc_state_t)
180 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
181 xbt_setset_set_insert(current_state->created_transitions, trans);
182 xbt_setset_set_insert(current_state->transitions, trans);
185 SIMIX_process_yield();
189 * \brief Intercept a WaitAny action
190 * \param comms The communications associated to the WaitAny
192 void MC_trans_intercept_waitany(xbt_dynar_t comms)
194 unsigned int index = 0;
195 smx_comm_t comm = NULL;
196 mc_transition_t trans = NULL;
197 mc_state_t current_state = NULL;
198 if (!mc_replay_mode) {
200 current_state = (mc_state_t)
201 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
202 xbt_dynar_foreach(comms, index, comm) {
203 trans = MC_trans_wait_new(comm);
204 xbt_setset_set_insert(current_state->created_transitions, trans);
205 xbt_setset_set_insert(current_state->transitions, trans);
209 SIMIX_process_yield();
213 * \brief Intercept a Random action
214 * \param min The minimum value that can be returned by the Random action
215 * \param max The maximum value that can be returned by the Random action
217 void MC_trans_intercept_random(int min, int max)
220 mc_transition_t trans = NULL;
221 mc_state_t current_state = NULL;
222 if (!mc_replay_mode) {
224 current_state = (mc_state_t)
225 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
226 for (i = min; i <= max; i++) {
227 trans = MC_trans_random_new(i);
228 xbt_setset_set_insert(current_state->created_transitions, trans);
229 xbt_setset_set_insert(current_state->transitions, trans);
233 SIMIX_process_yield();
236 /* Compute the subset of enabled transitions of the transition set */
237 void MC_trans_compute_enabled(xbt_setset_set_t enabled,
238 xbt_setset_set_t transitions)
240 unsigned int index = 0;
241 smx_comm_t comm = NULL;
242 mc_transition_t trans = NULL;
243 xbt_setset_cursor_t cursor = NULL;
244 xbt_setset_foreach(transitions, cursor, trans) {
245 switch (trans->type) {
246 /* Wait transitions are enabled only if the communication has both a
247 sender and receiver */
249 if (trans->wait.comm->src_proc && trans->wait.comm->dst_proc) {
250 xbt_setset_set_insert(enabled, trans);
251 DEBUG1("Transition %p is enabled for next state", trans);
255 /* WaitAny transitions are enabled if any of it's communications has both
256 a sender and a receiver */
258 xbt_dynar_foreach(trans->waitany.comms, index, comm) {
259 if (comm->src_proc && comm->dst_proc) {
260 xbt_setset_set_insert(enabled, trans);
261 DEBUG1("Transition %p is enabled for next state", trans);
267 /* The rest of the transitions cannot be disabled */
269 xbt_setset_set_insert(enabled, trans);
270 DEBUG1("Transition %p is enabled for next state", trans);
277 * \brief Determine if two transitions are dependent
278 * \param t1 a transition
279 * \param t2 a transition
280 * \return TRUE if \a t1 and \a t2 are dependent. FALSE otherwise.
282 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
284 if (t1->process == t2->process)
287 if (t1->type != t2->type)
290 /* if(t1->type == mc_isend && t2->type == mc_irecv)
293 if(t1->type == mc_irecv && t2->type == mc_isend)
296 if (t1->type == mc_random || t2->type == mc_random)
299 if (t1->type == mc_isend && t2->type == mc_isend
300 && t1->isend.rdv != t2->isend.rdv)
303 if (t1->type == mc_irecv && t2->type == mc_irecv
304 && t1->irecv.rdv != t2->irecv.rdv)
307 if (t1->type == mc_wait && t2->type == mc_wait
308 && t1->wait.comm == t2->wait.comm)
311 if (t1->type == mc_wait && t2->type == mc_wait
312 && t1->wait.comm->src_buff != NULL
313 && t1->wait.comm->dst_buff != NULL
314 && t2->wait.comm->src_buff != NULL
315 && t2->wait.comm->dst_buff != NULL
316 && t1->wait.comm->dst_buff != t2->wait.comm->src_buff
317 && t1->wait.comm->dst_buff != t2->wait.comm->dst_buff
318 && t2->wait.comm->dst_buff != t1->wait.comm->src_buff)