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);
55 * \brief Associate a communication to a transition
56 * \param trans The transition
57 * \param comm The communication
59 void MC_transition_set_comm(mc_transition_t trans, smx_comm_t comm)
67 * \brief Deletes a transition
68 * \param trans The transition to be deleted
70 void MC_transition_delete(mc_transition_t trans)
72 /* Only delete it if there are no references, otherwise decrement refcount */
73 if(--trans->refcount == 0){
74 xbt_free(trans->name);
80 * \brief Determine if two transitions are dependent
81 * \param t1 a transition
82 * \param t2 a transition
83 * \return TRUE if \a t1 and \a t2 are dependent. FALSE otherwise.
85 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
87 /* The semantics of SIMIX network operations implies that ONLY transitions
88 of the same type, in the same rendez-vous point, and from different processes
89 are dependant, except wait transitions that are always independent */
90 if(t1->process == t2->process)
93 if(t1->type == mc_isend && t2->type == mc_isend && t1->rdv == t2->rdv)
96 if(t1->type == mc_irecv && t2->type == mc_irecv && t1->rdv == t2->rdv)
99 if(t1->type == mc_wait && t2->type == mc_wait
100 && t1->comm->src_buff != NULL
101 && t1->comm->dst_buff != NULL
102 && t2->comm->src_buff != NULL
103 && t2->comm->dst_buff != NULL
104 && ( t1->comm->dst_buff == t2->comm->src_buff
105 || t1->comm->dst_buff == t2->comm->dst_buff
106 || t2->comm->dst_buff == t1->comm->src_buff))