+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans, mc,
+ "Logging specific to MC transitions");
+
+/* Creates a new iSend transition */
+mc_transition_t MC_trans_isend_new(smx_rdv_t rdv)
+{
+ mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+
+ trans->type = mc_isend;
+ trans->process = SIMIX_process_self();
+ trans->isend.rdv = rdv;
+ trans->name = bprintf("[%s][%s] iSend (%p)", trans->process->smx_host->name,
+ trans->process->name, trans);
+ return trans;
+}
+
+/* Creates a new iRecv transition */
+mc_transition_t MC_trans_irecv_new(smx_rdv_t rdv)
+{
+ mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+
+ trans->type = mc_irecv;
+ trans->process = SIMIX_process_self();
+ trans->irecv.rdv = rdv;
+ trans->name = bprintf("[%s][%s] iRecv (%p)", trans->process->smx_host->name,
+ trans->process->name, trans);
+ return trans;
+}
+
+/* Creates a new Wait transition */
+mc_transition_t MC_trans_wait_new(smx_comm_t comm)
+{
+ mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+
+ trans->type = mc_wait;
+ trans->process = SIMIX_process_self();
+ trans->wait.comm = comm;
+ trans->name = bprintf("[%s][%s] Wait (%p)", trans->process->smx_host->name,
+ trans->process->name, trans);
+ return trans;
+}
+
+/* Creates a new test transition */
+mc_transition_t MC_trans_test_new(smx_comm_t comm)
+{
+ mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+
+ trans->type = mc_test;
+ trans->process = SIMIX_process_self();
+ trans->test.comm = comm;
+ trans->name = bprintf("[%s][%s] Test (%p)", trans->process->smx_host->name,
+ trans->process->name, trans);
+ return trans;
+}
+
+/* Creates a new WaitAny transition */
+mc_transition_t MC_trans_waitany_new(xbt_dynar_t comms)
+{
+ mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+
+ trans->type = mc_waitany;
+ trans->process = SIMIX_process_self();
+ trans->waitany.comms = comms;
+ trans->name = bprintf("[%s][%s] WaitAny (%p)", trans->process->smx_host->name,
+ trans->process->name, trans);
+ return trans;
+}
+
+/* Creates a new Random transition */
+mc_transition_t MC_trans_random_new(int min, int max)
+{
+ mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+
+ trans->type = mc_random;
+ trans->process = SIMIX_process_self();
+ trans->random.min = min;
+ trans->random.max = max;
+ trans->random.current_value = min;
+ trans->name = bprintf("[%s][%s] Random (%p)", trans->process->smx_host->name,
+ trans->process->name, trans);
+ return trans;
+}
+
+/**
+ * \brief Deletes a transition
+ * \param trans The transition to be deleted
+ */
+void MC_transition_delete(mc_transition_t trans)
+{
+ xbt_free(trans->name);
+ xbt_free(trans);
+}
+
+/************************** Interception Functions ****************************/
+/* These functions intercept all the actions relevant to the model-checking
+ * process, the only difference between them is the type of transition they
+ * create. The interception works by yielding the process performer of the
+ * action, and depending on the execution mode it behaves diferently.
+ * There are two running modes, a replay (back-track process) in which no
+ * transition needs to be created, or a new state expansion, which in
+ * consecuence a transition needs to be created and added to the set of
+ * transitions associated to the current state.
+ */
+