src/mc/mc_transition.c

   1 #include "private.h"
   2
   3 /* Creates a new iSend transition */
   4 mc_transition_t MC_trans_isend_new(smx_rdv_t rdv)
   5 {
   6   mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
   7
   8   trans->type = mc_isend;
   9   trans->process = SIMIX_process_self();
  10   trans->isend.rdv = rdv;
  11   trans->name = bprintf("[%s][%s] iSend (%p)", trans->process->smx_host->name,
  12                         trans->process->name, trans);
  13   return trans;
  14 }
  15
  16 /* Creates a new iRecv transition */
  17 mc_transition_t MC_trans_irecv_new(smx_rdv_t rdv)
  18 {
  19   mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  20
  21   trans->type = mc_irecv;
  22   trans->process = SIMIX_process_self();
  23   trans->irecv.rdv = rdv;
  24   trans->name = bprintf("[%s][%s] iRecv (%p)", trans->process->smx_host->name,
  25                         trans->process->name, trans);
  26   return trans;
  27 }
  28
  29 /* Creates a new Wait transition */
  30 mc_transition_t MC_trans_wait_new(smx_comm_t comm)
  31 {
  32   mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  33
  34   trans->type = mc_wait;
  35   trans->process = SIMIX_process_self();
  36   trans->wait.comm = comm;
  37   trans->name = bprintf("[%s][%s] Wait (%p)", trans->process->smx_host->name,
  38                         trans->process->name, trans);
  39   return trans;
  40 }
  41
  42 /* Creates a new test transition */
  43 mc_transition_t MC_trans_test_new(smx_comm_t comm)
  44 {
  45   mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  46
  47   trans->type = mc_test;
  48   trans->process = SIMIX_process_self();
  49   trans->test.comm = comm;
  50   trans->name = bprintf("[%s][%s] Test (%p)", trans->process->smx_host->name,
  51                         trans->process->name, trans);
  52   return trans;
  53 }
  54
  55 /* Creates a new WaitAny transition */
  56 mc_transition_t MC_trans_waitany_new(xbt_dynar_t comms)
  57 {
  58   mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  59
  60   trans->type = mc_waitany;
  61   trans->process = SIMIX_process_self();
  62   trans->waitany.comms = comms;
  63   trans->name = bprintf("[%s][%s] WaitAny (%p)", trans->process->smx_host->name,
  64                         trans->process->name, trans);
  65   return trans;
  66 }
  67
  68 /* Creates a new Random transition */
  69 mc_transition_t MC_trans_random_new(int min, int max)
  70 {
  71   mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
  72
  73   trans->type = mc_random;
  74   trans->process = SIMIX_process_self();
  75   trans->random.min = min;
  76   trans->random.max = max;
  77   trans->random.current_value = min;
  78   trans->name = bprintf("[%s][%s] Random (%p)", trans->process->smx_host->name,
  79                         trans->process->name, trans);
  80   return trans;
  81 }
  82
  83 /************************** Interception Functions ****************************/
  84 /* These functions intercept all the actions relevant to the model-checking
  85  * process, the only difference between them is the type of transition they
  86  * create. The interception works by yielding the process performer of the
  87  * action, and depending on the execution mode it behaves diferently.
  88  * There are two running modes, a replay (back-track process) in which no
  89  * transition needs to be created, or a new state expansion, which in
  90  * consecuence a transition needs to be created and added to the set of
  91  * transitions associated to the current state.
  92  */
  93
  94 /**
  95  * \brief Intercept an iSend action
  96  * \param rdv The rendez-vous of the iSend
  97  */
  98 void MC_trans_intercept_isend(smx_rdv_t rdv)
  99 {
 100   mc_transition_t trans=NULL;
 101   mc_state_t current_state = NULL;
 102   if(!mc_replay_mode){
 103     MC_SET_RAW_MEM;
 104     trans = MC_trans_isend_new(rdv);
 105     current_state = (mc_state_t)
 106       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 107     xbt_setset_set_insert(current_state->created_transitions, trans);
 108     xbt_setset_set_insert(current_state->transitions, trans);
 109     MC_UNSET_RAW_MEM;
 110   }
 111   SIMIX_process_yield();
 112 }
 113
 114 /**
 115  * \brief Intercept an iRecv action
 116  * \param rdv The rendez-vous of the iRecv
 117  */
 118 void MC_trans_intercept_irecv(smx_rdv_t rdv)
 119 {
 120   mc_transition_t trans=NULL;
 121   mc_state_t current_state = NULL;
 122   if(!mc_replay_mode){
 123     MC_SET_RAW_MEM;
 124     trans = MC_trans_irecv_new(rdv);
 125     current_state = (mc_state_t)
 126       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 127     xbt_setset_set_insert(current_state->created_transitions, trans);
 128     xbt_setset_set_insert(current_state->transitions, trans);
 129     MC_UNSET_RAW_MEM;
 130   }
 131   SIMIX_process_yield();
 132 }
 133
 134 /**
 135  * \brief Intercept a Wait action
 136  * \param comm The communication associated to the wait
 137  */
 138 void MC_trans_intercept_wait(smx_comm_t comm)
 139 {
 140   mc_transition_t trans=NULL;
 141   mc_state_t current_state = NULL;
 142   if(!mc_replay_mode){
 143     MC_SET_RAW_MEM;
 144     trans = MC_trans_wait_new(comm);
 145     current_state = (mc_state_t)
 146       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 147     xbt_setset_set_insert(current_state->created_transitions, trans);
 148     xbt_setset_set_insert(current_state->transitions, trans);
 149     MC_UNSET_RAW_MEM;
 150   }
 151   SIMIX_process_yield();
 152 }
 153
 154 /**
 155  * \brief Intercept a Test action
 156  * \param comm The communication associated to the Test
 157  */
 158 void MC_trans_intercept_test(smx_comm_t comm)
 159 {
 160   mc_transition_t trans=NULL;
 161   mc_state_t current_state = NULL;
 162   if(!mc_replay_mode){
 163     MC_SET_RAW_MEM;
 164     trans = MC_trans_test_new(comm);
 165     current_state = (mc_state_t)
 166       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 167     xbt_setset_set_insert(current_state->created_transitions, trans);
 168     xbt_setset_set_insert(current_state->transitions, trans);
 169     MC_UNSET_RAW_MEM;
 170   }
 171   SIMIX_process_yield();
 172 }
 173
 174 /**
 175  * \brief Intercept a WaitAny action
 176  * \param comms The communications associated to the WaitAny
 177  */
 178 void MC_trans_intercept_waitany(xbt_dynar_t comms)
 179 {
 180   mc_transition_t trans=NULL;
 181   mc_state_t current_state = NULL;
 182   if(!mc_replay_mode){
 183     MC_SET_RAW_MEM;
 184     trans = MC_trans_waitany_new(comms);
 185     current_state = (mc_state_t)
 186       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 187     xbt_setset_set_insert(current_state->created_transitions, trans);
 188     xbt_setset_set_insert(current_state->transitions, trans);
 189     MC_UNSET_RAW_MEM;
 190   }
 191   SIMIX_process_yield();
 192 }
 193
 194 /**
 195  * \brief Intercept a Random action
 196  * \param min The minimum value that can be returned by the Random action
 197  * \param max The maximum value that can be returned by the Random action
 198  */
 199 void MC_trans_intercept_random(int min, int max)
 200 {
 201   mc_transition_t trans=NULL;
 202   mc_state_t current_state = NULL;
 203   if(!mc_replay_mode){
 204     MC_SET_RAW_MEM;
 205     trans = MC_trans_random_new(min, max);
 206     current_state = (mc_state_t)
 207       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 208     xbt_setset_set_insert(current_state->created_transitions, trans);
 209     xbt_setset_set_insert(current_state->transitions, trans);
 210     MC_UNSET_RAW_MEM;
 211   }
 212   SIMIX_process_yield();
 213 }
 214
 215 /**
 216  * \brief Deletes a transition
 217  * \param trans The transition to be deleted
 218  */
 219 void MC_transition_delete(mc_transition_t trans)
 220 {
 221   xbt_free(trans->name);
 222   xbt_free(trans);
 223 }
 224
 225 /* Compute the subset of enabled transitions of the transition set */
 226 void MC_trans_compute_enabled(xbt_setset_set_t enabled, xbt_setset_set_t transitions)
 227 {
 228   mc_transition_t trans = NULL;
 229   xbt_setset_cursor_t cursor = NULL;
 230   /* Add all the transitions to the enabled set and then remove the disabled ones */
 231   xbt_setset_add(enabled, transitions);
 232   xbt_setset_foreach(transitions, cursor, trans){
 233     if(trans->type == mc_wait
 234        && (trans->wait.comm->src_proc == NULL || trans->wait.comm->dst_proc == NULL)){
 235       xbt_setset_set_remove(enabled, trans);
 236     }
 237   }
 238 }
 239
 240 /**
 241  * \brief Determine if two transitions are dependent
 242  * \param t1 a transition
 243  * \param t2 a transition
 244  * \return TRUE if \a t1 and \a t2 are dependent. FALSE otherwise.
 245  */
 246 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
 247 {
 248   if(t1->process == t2->process)
 249     return FALSE;
 250
 251   if(t1->type != t2->type)
 252     return FALSE;
 253
 254   if(t1->type == mc_isend && t2->type == mc_isend && t1->isend.rdv != t2->isend.rdv)
 255     return FALSE;
 256
 257   if(t1->type == mc_irecv && t2->type == mc_irecv && t1->irecv.rdv != t2->irecv.rdv)
 258     return FALSE;
 259
 260   if(t1->type == mc_wait && t2->type == mc_wait && t1->wait.comm == t2->wait.comm)
 261     return FALSE;
 262
 263   if(t1->type == mc_wait && t2->type == mc_wait
 264      && t1->wait.comm->src_buff != NULL
 265      && t1->wait.comm->dst_buff != NULL
 266      && t2->wait.comm->src_buff != NULL
 267      && t2->wait.comm->dst_buff != NULL
 268      && t1->wait.comm->dst_buff != t2->wait.comm->src_buff
 269      && t1->wait.comm->dst_buff != t2->wait.comm->dst_buff
 270      && t2->wait.comm->dst_buff != t1->wait.comm->src_buff)
 271     return FALSE;
 272
 273   return TRUE;
 274 }