Improve independence detection of transitions (more reduction of state space)

[simgrid.git] / src / mc / mc_transition.c

diff --git a/src/mc/mc_transition.c b/src/mc/mc_transition.c
index 4e5c95d..6b9d7f8 100644 (file)
--- a/src/mc/mc_transition.c
+++ b/src/mc/mc_transition.c
@@ -14,7 +14,6 @@ mc_transition_t MC_create_transition(mc_trans_type_t type, smx_process_t p, smx_
   if(!mc_replay_mode){
     MC_SET_RAW_MEM;
     mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
-    trans->refcount = 1;
 
     /* Generate a string for the "type" */
     switch(type){
@@ -42,8 +41,10 @@ mc_transition_t MC_create_transition(mc_trans_type_t type, smx_process_t p, smx_
     trans->rdv = rdv;
     trans->comm = comm;
     /* Push it onto the enabled transitions set of the current state */
-    current_state = (mc_state_t) 
+
+   current_state = (mc_state_t) 
       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+    xbt_setset_set_insert(current_state->created_transitions, trans);
     xbt_setset_set_insert(current_state->transitions, trans);
     MC_UNSET_RAW_MEM;
     return trans;
@@ -51,6 +52,36 @@ mc_transition_t MC_create_transition(mc_trans_type_t type, smx_process_t p, smx_
   return NULL;
 }
 
+void MC_random_create(int min, int max)
+{
+  smx_process_t p;
+  mc_state_t current_state = NULL;
+  char *type_str = NULL;
+  
+  if(!mc_replay_mode){
+    p = SIMIX_process_self();
+    
+    MC_SET_RAW_MEM;
+    mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
+    
+    trans->name = bprintf("[%s][%s] mc_random(%d,%d) (%p)", p->smx_host->name, p->name, min, max, trans);
+    xbt_free(type_str);
+
+    trans->type = mc_random ;
+    trans->process = p;
+    trans->min = min;
+    trans->max = max;
+    trans->current_value = min;
+    
+    /* Push it onto the enabled transitions set of the current state */
+    current_state = (mc_state_t) 
+      xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+    xbt_setset_set_insert(current_state->created_transitions, trans);
+    xbt_setset_set_insert(current_state->transitions, trans);
+    MC_UNSET_RAW_MEM;
+  }
+}
+
 /** 
  * \brief Associate a communication to a transition
  * \param trans The transition
@@ -69,11 +100,8 @@ void MC_transition_set_comm(mc_transition_t trans, smx_comm_t comm)
  */
 void MC_transition_delete(mc_transition_t trans)
 {
-  /* Only delete it if there are no references, otherwise decrement refcount */  
-  if(--trans->refcount == 0){
-    xbt_free(trans->name);
-    xbt_free(trans);
-  }
+  xbt_free(trans->name);
+  xbt_free(trans);
 }
 
 /**
@@ -84,21 +112,30 @@ void MC_transition_delete(mc_transition_t trans)
  */
 int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
 {
-  /* The semantics of SIMIX network operations implies that ONLY transitions 
-     of the same type, in the same rendez-vous point, and from different processes
-     are dependant, except wait transitions that are always independent */
-  if(   t1->type == mc_wait 
-     || t2->type == mc_wait
-     || t1->process == t2->process
-     || t1->type != t2->type
-     || t1->rdv != t2->rdv)
+  if(t1->process == t2->process) 
     return FALSE;
-  else
-    return TRUE;
-}
-
-
-
 
+  if(t1->type != t2->type)
+    return FALSE;
+  
+  if(t1->type == mc_isend && t2->type == mc_isend && t1->rdv != t2->rdv)
+    return FALSE;
 
+  if(t1->type == mc_irecv && t2->type == mc_irecv && t1->rdv != t2->rdv)
+    return FALSE;
 
+  if(t1->type == mc_wait && t2->type == mc_wait && t1->comm == t2->comm)
+    return FALSE;
+  
+  if(t1->type == mc_wait && t2->type == mc_wait 
+     && t1->comm->src_buff != NULL
+     && t1->comm->dst_buff != NULL
+     && t2->comm->src_buff != NULL
+     && t2->comm->dst_buff != NULL
+     && t1->comm->dst_buff != t2->comm->src_buff
+     && t1->comm->dst_buff != t2->comm->dst_buff
+     && t2->comm->dst_buff != t1->comm->src_buff)
+    return FALSE;
+  
+  return TRUE;
+}
\ No newline at end of file