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 void MC_random_create(int min, int max)
  55 {
  56   smx_process_t p;
  57   mc_state_t current_state = NULL;
  58   char *type_str = NULL;
  59
  60   if(!mc_replay_mode){
  61     p = SIMIX_process_self();
  62
  63     MC_SET_RAW_MEM;
  64     mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  65
  66     trans->name = bprintf("[%s][%s] mc_random(%d,%d) (%p)", p->smx_host->name, p->name, min, max, trans);
  67     xbt_free(type_str);
  68
  69     trans->refcount = 1;
  70     trans->type = mc_random ;
  71     trans->process = p;
  72     trans->min = min;
  73     trans->max = max;
  74     trans->current_value = min;
  75
  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);
  80     MC_UNSET_RAW_MEM;
  81   }
  82 }
  83
  84 /**
  85  * \brief Associate a communication to a transition
  86  * \param trans The transition
  87  * \param comm The communication
  88  */
  89 void MC_transition_set_comm(mc_transition_t trans, smx_comm_t comm)
  90 {
  91   if(trans)
  92     trans->comm = comm;
  93   return;
  94 }
  95
  96 /**
  97  * \brief Deletes a transition
  98  * \param trans The transition to be deleted
  99  */
 100 void MC_transition_delete(mc_transition_t trans)
 101 {
 102   /* Only delete it if there are no references, otherwise decrement refcount */
 103   if(--trans->refcount == 0){
 104     xbt_free(trans->name);
 105     xbt_free(trans);
 106   }
 107 }
 108
 109 /**
 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.
 114  */
 115 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
 116 {
 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)
 121     return FALSE;
 122
 123   if(t1->type == mc_isend && t2->type == mc_isend && t1->rdv == t2->rdv)
 124     return TRUE;
 125
 126   if(t1->type == mc_irecv && t2->type == mc_irecv && t1->rdv == t2->rdv)
 127     return TRUE;
 128
 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))
 137     return TRUE;
 138
 139   return FALSE;
 140 }