src/mc/mc_transition.c

   1 #include "private.h"
   2
   3 /**
   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)
   8 */
   9 mc_transition_t MC_create_transition(mc_trans_type_t type, smx_process_t p, smx_rdv_t rdv, smx_comm_t comm)
  10 {
  11   mc_state_t current_state = NULL;
  12   char *type_str = NULL;
  13
  14   if(!mc_replay_mode){
  15     MC_SET_RAW_MEM;
  16     mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  17     trans->refcount = 1;
  18
  19     /* Generate a string for the "type" */
  20     switch(type){
  21       case mc_isend:
  22         type_str = bprintf("iSend");
  23         break;
  24       case mc_irecv:
  25         type_str = bprintf("iRecv");
  26         break;
  27       case mc_wait:
  28         type_str = bprintf("Wait");
  29         break;
  30       case mc_waitany:
  31         type_str = bprintf("WaitAny");
  32         break;
  33       default:
  34         xbt_die("Invalid transition type");
  35     }
  36
  37     trans->name = bprintf("[%s][%s] %s (%p)", p->smx_host->name, p->name, type_str, trans);
  38     xbt_free(type_str);
  39
  40     trans->type = type;
  41     trans->process = p;
  42     trans->rdv = rdv;
  43     trans->comm = comm;
  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);
  48     MC_UNSET_RAW_MEM;
  49     return trans;
  50   }
  51   return NULL;
  52 }
  53
  54 /**
  55  * \brief Associate a communication to a transition
  56  * \param trans The transition
  57  * \param comm The communication
  58  */
  59 void MC_transition_set_comm(mc_transition_t trans, smx_comm_t comm)
  60 {
  61   if(trans)
  62     trans->comm = comm;
  63   return;
  64 }
  65
  66 /**
  67  * \brief Deletes a transition
  68  * \param trans The transition to be deleted
  69  */
  70 void MC_transition_delete(mc_transition_t trans)
  71 {
  72   /* Only delete it if there are no references, otherwise decrement refcount */
  73   if(--trans->refcount == 0){
  74     xbt_free(trans->name);
  75     xbt_free(trans);
  76   }
  77 }
  78
  79 /**
  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.
  84  */
  85 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
  86 {
  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)
  91     return FALSE;
  92
  93   if(t1->type == mc_isend && t2->type == mc_isend && t1->rdv == t2->rdv)
  94     return TRUE;
  95
  96   if(t1->type == mc_irecv && t2->type == mc_irecv && t1->rdv == t2->rdv)
  97     return TRUE;
  98
  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))
 107     return TRUE;
 108
 109   return FALSE;
 110 }