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]\t iSend (%p)", trans->process->smx_host->name, trans);
18 /* Creates a new iRecv transition */
19 mc_transition_t MC_trans_irecv_new(smx_rdv_t rdv)
21 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
23 trans->type = mc_irecv;
24 trans->process = SIMIX_process_self();
25 trans->irecv.rdv = rdv;
26 trans->name = bprintf("[%s]\t iRecv (%p)", trans->process->smx_host->name, trans);
30 /* Creates a new Wait transition */
31 mc_transition_t MC_trans_wait_new(smx_comm_t comm)
33 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
35 trans->type = mc_wait;
36 trans->process = SIMIX_process_self();
37 trans->wait.comm = comm;
38 trans->name = bprintf("[%s]\t Wait (%p)", trans->process->smx_host->name, trans);
42 /* Creates a new test transition */
43 mc_transition_t MC_trans_test_new(smx_comm_t comm)
45 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
47 trans->type = mc_test;
48 trans->process = SIMIX_process_self();
49 trans->test.comm = comm;
50 trans->name = bprintf("[%s]\t Test (%p)", trans->process->smx_host->name, trans);
54 /* Creates a new WaitAny transition */
55 mc_transition_t MC_trans_waitany_new(xbt_dynar_t comms)
57 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
59 trans->type = mc_waitany;
60 trans->process = SIMIX_process_self();
61 trans->waitany.comms = comms;
62 trans->name = bprintf("[%s]\t WaitAny (%p)", trans->process->smx_host->name, trans);
66 /* Creates a new Random transition */
67 mc_transition_t MC_trans_random_new(int value)
69 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
71 trans->type = mc_random;
72 trans->process = SIMIX_process_self();
73 trans->random.value = value;
74 trans->name = bprintf("[%s]\t Random %d (%p)", trans->process->smx_host->name, value, trans);
80 * \brief Deletes a transition
81 * \param trans The transition to be deleted
83 void MC_transition_delete(mc_transition_t trans)
85 xbt_free(trans->name);
89 /************************** Interception Functions ****************************/
90 /* These functions intercept all the actions relevant to the model-checking
91 * process, the only difference between them is the type of transition they
92 * create. The interception works by yielding the process performer of the
93 * action, and depending on the execution mode it behaves diferently.
94 * There are two running modes, a replay (back-track process) in which no
95 * transition needs to be created, or a new state expansion, which in
96 * consecuence a transition needs to be created and added to the set of
97 * transitions associated to the current state.
101 * \brief Intercept an iSend action
102 * \param rdv The rendez-vous of the iSend
104 void MC_trans_intercept_isend(smx_rdv_t rdv)
106 mc_transition_t trans=NULL;
107 mc_state_t current_state = NULL;
110 trans = MC_trans_isend_new(rdv);
111 current_state = (mc_state_t)
112 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
113 xbt_setset_set_insert(current_state->created_transitions, trans);
114 xbt_setset_set_insert(current_state->transitions, trans);
117 SIMIX_process_yield();
121 * \brief Intercept an iRecv action
122 * \param rdv The rendez-vous of the iRecv
124 void MC_trans_intercept_irecv(smx_rdv_t rdv)
126 mc_transition_t trans=NULL;
127 mc_state_t current_state = NULL;
130 trans = MC_trans_irecv_new(rdv);
131 current_state = (mc_state_t)
132 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
133 xbt_setset_set_insert(current_state->created_transitions, trans);
134 xbt_setset_set_insert(current_state->transitions, trans);
137 SIMIX_process_yield();
141 * \brief Intercept a Wait action
142 * \param comm The communication associated to the wait
144 void MC_trans_intercept_wait(smx_comm_t comm)
146 mc_transition_t trans=NULL;
147 mc_state_t current_state = NULL;
150 trans = MC_trans_wait_new(comm);
151 current_state = (mc_state_t)
152 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
153 xbt_setset_set_insert(current_state->created_transitions, trans);
154 xbt_setset_set_insert(current_state->transitions, trans);
157 SIMIX_process_yield();
161 * \brief Intercept a Test action
162 * \param comm The communication associated to the Test
164 void MC_trans_intercept_test(smx_comm_t comm)
166 mc_transition_t trans=NULL;
167 mc_state_t current_state = NULL;
170 trans = MC_trans_test_new(comm);
171 current_state = (mc_state_t)
172 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
173 xbt_setset_set_insert(current_state->created_transitions, trans);
174 xbt_setset_set_insert(current_state->transitions, trans);
177 SIMIX_process_yield();
181 * \brief Intercept a WaitAny action
182 * \param comms The communications associated to the WaitAny
184 void MC_trans_intercept_waitany(xbt_dynar_t comms)
186 unsigned int index = 0;
187 smx_comm_t comm = NULL;
188 mc_transition_t trans = NULL;
189 mc_state_t current_state = NULL;
192 current_state = (mc_state_t)
193 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
194 xbt_dynar_foreach(comms, index, comm){
195 trans = MC_trans_wait_new(comm);
196 xbt_setset_set_insert(current_state->created_transitions, trans);
197 xbt_setset_set_insert(current_state->transitions, trans);
201 SIMIX_process_yield();
205 * \brief Intercept a Random action
206 * \param min The minimum value that can be returned by the Random action
207 * \param max The maximum value that can be returned by the Random action
209 void MC_trans_intercept_random(int min, int max)
212 mc_transition_t trans=NULL;
213 mc_state_t current_state = NULL;
216 current_state = (mc_state_t)
217 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
218 for(i=min; i <= max; i++){
219 trans = MC_trans_random_new(i);
220 xbt_setset_set_insert(current_state->created_transitions, trans);
221 xbt_setset_set_insert(current_state->transitions, trans);
225 SIMIX_process_yield();
228 /* Compute the subset of enabled transitions of the transition set */
229 void MC_trans_compute_enabled(xbt_setset_set_t enabled, xbt_setset_set_t transitions)
231 unsigned int index = 0;
232 smx_comm_t comm = NULL;
233 mc_transition_t trans = NULL;
234 xbt_setset_cursor_t cursor = NULL;
235 xbt_setset_foreach(transitions, cursor, trans){
237 /* Wait transitions are enabled only if the communication has both a
238 sender and receiver */
240 if(trans->wait.comm->src_proc && trans->wait.comm->dst_proc){
241 xbt_setset_set_insert(enabled, trans);
242 DEBUG1("Transition %p is enabled for next state", trans);
246 /* WaitAny transitions are enabled if any of it's communications has both
247 a sender and a receiver */
249 xbt_dynar_foreach(trans->waitany.comms, index, comm){
250 if(comm->src_proc && comm->dst_proc){
251 xbt_setset_set_insert(enabled, trans);
252 DEBUG1("Transition %p is enabled for next state", trans);
258 /* The rest of the transitions cannot be disabled */
260 xbt_setset_set_insert(enabled, trans);
261 DEBUG1("Transition %p is enabled for next state", trans);
268 * \brief Determine if two transitions are dependent
269 * \param t1 a transition
270 * \param t2 a transition
271 * \return TRUE if \a t1 and \a t2 are dependent. FALSE otherwise.
273 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
275 if(t1->process == t2->process)
278 if(t1->type != t2->type)
281 /* if(t1->type == mc_isend && t2->type == mc_irecv)
284 if(t1->type == mc_irecv && t2->type == mc_isend)
287 if(t1->type == mc_random || t2->type == mc_random)
290 if(t1->type == mc_isend && t2->type == mc_isend && t1->isend.rdv != t2->isend.rdv)
293 if(t1->type == mc_irecv && t2->type == mc_irecv && t1->irecv.rdv != t2->irecv.rdv)
296 if(t1->type == mc_wait && t2->type == mc_wait && t1->wait.comm == t2->wait.comm)
299 if(t1->type == mc_wait && t2->type == mc_wait
300 && t1->wait.comm->src_buff != NULL
301 && t1->wait.comm->dst_buff != NULL
302 && t2->wait.comm->src_buff != NULL
303 && t2->wait.comm->dst_buff != NULL
304 && t1->wait.comm->dst_buff != t2->wait.comm->src_buff
305 && t1->wait.comm->dst_buff != t2->wait.comm->dst_buff
306 && t2->wait.comm->dst_buff != t1->wait.comm->src_buff)