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
  18     /* Generate a string for the "type" */
  19     switch(type){
  20       case mc_isend:
  21         type_str = bprintf("iSend");
  22         break;
  23       case mc_irecv:
  24         type_str = bprintf("iRecv");
  25         break;
  26       case mc_wait:
  27         type_str = bprintf("Wait");
  28         break;
  29       case mc_waitany:
  30         type_str = bprintf("WaitAny");
  31         break;
  32       default:
  33         xbt_die("Invalid transition type");
  34     }
  35
  36     trans->name = bprintf("[%s][%s] %s (%p)", p->smx_host->name, p->name, type_str, trans);
  37     xbt_free(type_str);
  38
  39     trans->type = type;
  40     trans->process = p;
  41     trans->rdv = rdv;
  42     trans->comm = comm;
  43     /* Push it onto the enabled transitions set of the current state */
  44
  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->created_transitions, trans);
  48     xbt_setset_set_insert(current_state->transitions, trans);
  49     MC_UNSET_RAW_MEM;
  50     return trans;
  51   }
  52   return NULL;
  53 }
  54
  55 void MC_random_create(int min, int max)
  56 {
  57   smx_process_t p;
  58   mc_state_t current_state = NULL;
  59   char *type_str = NULL;
  60
  61   if(!mc_replay_mode){
  62     p = SIMIX_process_self();
  63
  64     MC_SET_RAW_MEM;
  65     mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  66
  67     trans->name = bprintf("[%s][%s] mc_random(%d,%d) (%p)", p->smx_host->name, p->name, min, max, trans);
  68     xbt_free(type_str);
  69
  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->created_transitions, trans);
  80     xbt_setset_set_insert(current_state->transitions, trans);
  81     MC_UNSET_RAW_MEM;
  82   }
  83 }
  84
  85 /**
  86  * \brief Associate a communication to a transition
  87  * \param trans The transition
  88  * \param comm The communication
  89  */
  90 void MC_transition_set_comm(mc_transition_t trans, smx_comm_t comm)
  91 {
  92   if(trans)
  93     trans->comm = comm;
  94   return;
  95 }
  96
  97 /**
  98  * \brief Deletes a transition
  99  * \param trans The transition to be deleted
 100  */
 101 void MC_transition_delete(mc_transition_t trans)
 102 {
 103   xbt_free(trans->name);
 104   xbt_free(trans);
 105 }
 106
 107 /**
 108  * \brief Determine if two transitions are dependent
 109  * \param t1 a transition
 110  * \param t2 a transition
 111  * \return TRUE if \a t1 and \a t2 are dependent. FALSE otherwise.
 112  */
 113 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
 114 {
 115   /* The semantics of SIMIX network operations implies that ONLY transitions
 116      of the same type, in the same rendez-vous point, and from different processes
 117      are dependant, except wait transitions that are always independent */
 118   if(t1->process == t2->process)
 119     return FALSE;
 120
 121   if(t1->type == mc_isend && t2->type == mc_isend && t1->rdv == t2->rdv)
 122     return TRUE;
 123
 124   if(t1->type == mc_irecv && t2->type == mc_irecv && t1->rdv == t2->rdv)
 125     return TRUE;
 126
 127   if(t1->type == mc_wait && t2->type == mc_wait
 128      && t1->comm->src_buff != NULL
 129      && t1->comm->dst_buff != NULL
 130      && t2->comm->src_buff != NULL
 131      && t2->comm->dst_buff != NULL
 132      && (   t1->comm->dst_buff == t2->comm->src_buff
 133          || t1->comm->dst_buff == t2->comm->dst_buff
 134          || t2->comm->dst_buff == t1->comm->src_buff))
 135     return TRUE;
 136
 137   return FALSE;
 138 }