4 * \brief Create a model-checker transition and add it to the set of avaiable
5 * transitions of the current state, if not running in replay mode.
6 * \param process The process who wants to perform the transition
7 * \param comm The type of then transition (comm_send, comm_recv)
9 mc_transition_t MC_create_transition(mc_trans_type_t type, smx_process_t p, smx_rdv_t rdv, smx_comm_t comm)
11 mc_state_t current_state = NULL;
12 char *type_str = NULL;
16 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
19 /* Generate a string for the "type" */
22 type_str = bprintf("iSend");
25 type_str = bprintf("iRecv");
28 type_str = bprintf("Wait");
31 type_str = bprintf("WaitAny");
34 xbt_die("Invalid transition type");
37 trans->name = bprintf("[%s][%s] %s (%p)", p->smx_host->name, p->name, type_str, trans);
44 /* Push it onto the enabled transitions set of the current state */
45 current_state = (mc_state_t)
46 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
47 xbt_setset_set_insert(current_state->transitions, trans);
54 void MC_random_create(int min, int max)
57 mc_state_t current_state = NULL;
58 char *type_str = NULL;
61 p = SIMIX_process_self();
64 mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
66 trans->name = bprintf("[%s][%s] mc_random(%d,%d) (%p)", p->smx_host->name, p->name, min, max, trans);
70 trans->type = mc_random ;
74 trans->current_value = min;
76 /* Push it onto the enabled transitions set of the current state */
77 current_state = (mc_state_t)
78 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
79 xbt_setset_set_insert(current_state->transitions, trans);
85 * \brief Associate a communication to a transition
86 * \param trans The transition
87 * \param comm The communication
89 void MC_transition_set_comm(mc_transition_t trans, smx_comm_t comm)
97 * \brief Deletes a transition
98 * \param trans The transition to be deleted
100 void MC_transition_delete(mc_transition_t trans)
102 /* Only delete it if there are no references, otherwise decrement refcount */
103 if(--trans->refcount == 0){
104 xbt_free(trans->name);
110 * \brief Determine if two transitions are dependent
111 * \param t1 a transition
112 * \param t2 a transition
113 * \return TRUE if \a t1 and \a t2 are dependent. FALSE otherwise.
115 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
117 /* The semantics of SIMIX network operations implies that ONLY transitions
118 of the same type, in the same rendez-vous point, and from different processes
119 are dependant, except wait transitions that are always independent */
120 if(t1->process == t2->process)
123 if(t1->type == mc_isend && t2->type == mc_isend && t1->rdv == t2->rdv)
126 if(t1->type == mc_irecv && t2->type == mc_irecv && t1->rdv == t2->rdv)
129 if(t1->type == mc_wait && t2->type == mc_wait
130 && t1->comm->src_buff != NULL
131 && t1->comm->dst_buff != NULL
132 && t2->comm->src_buff != NULL
133 && t2->comm->dst_buff != NULL
134 && ( t1->comm->dst_buff == t2->comm->src_buff
135 || t1->comm->dst_buff == t2->comm->dst_buff
136 || t2->comm->dst_buff == t1->comm->src_buff))