Improve support for WaitAny transitions, not usable yet but closer.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/simgrid/simgrid/trunk@7784 48e7efb5-ca39-0410-a469-dd3cf9ba447f

diff --git a/src/mc/mc_transition.c b/src/mc/mc_transition.c
index 5baeb9e..d1882ab 100644 (file)
--- a/src/mc/mc_transition.c
+++ b/src/mc/mc_transition.c
@@ -80,6 +80,16 @@ mc_transition_t MC_trans_random_new(int min, int max)
   return trans;
 }
 
+/**
+ * \brief Deletes a transition
+ * \param trans The transition to be deleted
+ */
+void MC_transition_delete(mc_transition_t trans)
+{
+  xbt_free(trans->name);
+  xbt_free(trans);
+}
+
 /************************** Interception Functions ****************************/
 /* These functions intercept all the actions relevant to the model-checking
  * process, the only difference between them is the type of transition they
@@ -212,28 +222,38 @@ void MC_trans_intercept_random(int min, int max)
   SIMIX_process_yield();
 }
 
-/**
- * \brief Deletes a transition
- * \param trans The transition to be deleted
- */
-void MC_transition_delete(mc_transition_t trans)
-{
-  xbt_free(trans->name);
-  xbt_free(trans);
-}
-
 /* Compute the subset of enabled transitions of the transition set */
 void MC_trans_compute_enabled(xbt_setset_set_t enabled, xbt_setset_set_t transitions)
 {
+  unsigned int index = 0;
+  smx_comm_t comm = NULL;
   mc_transition_t trans = NULL;
   xbt_setset_cursor_t cursor = NULL;
-  /* Add all the transitions to the enabled set and then remove the disabled ones */
-  xbt_setset_add(enabled, transitions); 
   xbt_setset_foreach(transitions, cursor, trans){
-    if(trans->type == mc_wait
-       && (trans->wait.comm->src_proc == NULL || trans->wait.comm->dst_proc == NULL)){
-      xbt_setset_set_remove(enabled, trans);
-    }
+    switch(trans->type){
+      /* Wait transitions are enabled only if the communication has both a
+         sender and receiver */
+      case mc_wait:
+        if(trans->wait.comm->src_proc && trans->wait.comm->dst_proc)
+          xbt_setset_set_insert(enabled, trans);
+        break;
+
+      /* WaitAny transitions are enabled if any of it's communications has both
+         a sender and a receiver */
+      case mc_waitany:
+        xbt_dynar_foreach(trans->waitany.comms, index, comm){
+          if(comm->src_proc && comm->dst_proc){
+            xbt_setset_set_insert(enabled, trans);
+            break;
+          }
+        }
+        break;
+
+      /* The rest of the transitions cannot be disabled */
+      default:
+        xbt_setset_set_insert(enabled, trans);
+        break;
+    } 
   }
 }
 

diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c
index 0802fb7..dd7b49a 100644 (file)
--- a/src/simix/smx_network.c
+++ b/src/simix/smx_network.c
@@ -476,12 +476,7 @@ smx_comm_t SIMIX_network_isend(smx_rdv_t rdv, double task_size, double rate,
 {
   smx_comm_t comm;
 
-  /* If running in model-checking mode then intercept the communication action. 
-   * There can be two situations, this is a replay (back-track process) so no
-   * transition needs to be created, or we are expanding a new state and in 
-   * consecuence a transition needs to be created and added to the set of
-   * transitions associated to the current state.
-   */
+  /*If running in model-checking mode then intercept the communication action*/
   if (_surf_do_model_check)
     MC_trans_intercept_isend(rdv);
   
@@ -510,12 +505,7 @@ smx_comm_t SIMIX_network_irecv(smx_rdv_t rdv, void *dst_buff, size_t *dst_buff_s
 {
   smx_comm_t comm;
 
-  /* If running in model-checking mode then intercept the communication action. 
-   * There can be two situations, this is a replay (back-track process) so no
-   * transition needs to be created, or we are expanding a new state and in 
-   * consecuence a transition needs to be created and added to the set of
-   * transitions associated to the current state.
-   */
+  /*If running in model-checking mode then intercept the communication action*/
   if (_surf_do_model_check)
     MC_trans_intercept_irecv(rdv);
   
@@ -541,12 +531,7 @@ smx_comm_t SIMIX_network_irecv(smx_rdv_t rdv, void *dst_buff, size_t *dst_buff_s
 /** @brief blocks until the communication terminates or the timeout occurs */
 XBT_INLINE void SIMIX_network_wait(smx_comm_t comm, double timeout)
 {
-  /* If running in model-checking mode then intercept the communication action. 
-   * There can be two situations, this is a replay (back-track process) so no
-   * transition needs to be created, or we are expanding a new state and in 
-   * consecuence a transition needs to be created and added to the set of
-   * transitions associated to the current state.
-   */
+  /*If running in model-checking mode then intercept the communication action*/
   if (_surf_do_model_check)
     MC_trans_intercept_wait(comm);
   
@@ -557,12 +542,7 @@ XBT_INLINE void SIMIX_network_wait(smx_comm_t comm, double timeout)
 /** @Returns whether the (asynchronous) communication is done yet or not */
 XBT_INLINE int SIMIX_network_test(smx_comm_t comm)
 {
-  /* If running in model-checking mode then intercept the communication action. 
-   * There can be two situations, this is a replay (back-track process) so no
-   * transition needs to be created, or we are expanding a new state and in 
-   * consecuence a transition needs to be created and added to the set of
-   * transitions associated to the current state.
-   */
+  /*If running in model-checking mode then intercept the communication action*/
   if (_surf_do_model_check)
     MC_trans_intercept_test(comm);
 
@@ -585,12 +565,7 @@ unsigned int SIMIX_network_waitany(xbt_dynar_t comms)
   unsigned int cursor, found_comm=-1;
   smx_comm_t comm,comm_finished=NULL;
 
-  /* If running in model-checking mode then intercept the communication action. 
-   * There can be two situations, this is a replay (back-track process) so no
-   * transition needs to be created, or we are expanding a new state and in 
-   * consecuence a transition needs to be created and added to the set of
-   * transitions associated to the current state.
-   */
+  /*If running in model-checking mode then intercept the communication action*/
   if (_surf_do_model_check)
     MC_trans_intercept_waitany(comms);