Add logging for transitions

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

diff --git a/src/mc/mc_transition.c b/src/mc/mc_transition.c
index 5baeb9e..3d46e0f 100644 (file)
--- a/src/mc/mc_transition.c
+++ b/src/mc/mc_transition.c
@@ -1,5 +1,8 @@
 #include "private.h"
 
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans, mc,
+                               "Logging specific to MC transitions");
+
 /* Creates a new iSend transition */
 mc_transition_t MC_trans_isend_new(smx_rdv_t rdv)
 {
@@ -80,6 +83,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 +225,42 @@ 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);
+          DEBUG1("Transition %p is enabled for next state", 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);
+            DEBUG1("Transition %p is enabled for next state", trans);
+            break;
+          }
+        }
+        break;
+
+      /* The rest of the transitions cannot be disabled */
+      default:
+        xbt_setset_set_insert(enabled, trans);
+        DEBUG1("Transition %p is enabled for next state", trans);
+        break;
+    } 
   }
 }