Transform random transitions into multiple // transitions one for each value in the...

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

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 364584e..c67d36d 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -15,7 +15,8 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
 void MC_dpor_init()
 {
   mc_state_t initial_state = NULL;
-  mc_transition_t trans = NULL;
+  mc_transition_t trans, trans_tmp = NULL;
+  xbt_setset_cursor_t cursor = NULL;
   
   /* Create the initial state and push it into the exploration stack */
   MC_SET_RAW_MEM;
@@ -34,8 +35,13 @@ void MC_dpor_init()
 
   /* Fill the interleave set of the initial state with an enabled process */
   trans = xbt_setset_set_choose(initial_state->enabled_transitions);  
-  if(trans)
-    xbt_setset_set_insert(initial_state->interleave, trans);
+  if(trans){
+    DEBUG1("Choosing process %s for next interleave", trans->process->name);
+    xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans_tmp){
+      if(trans_tmp->process == trans->process)
+        xbt_setset_set_insert(initial_state->interleave, trans_tmp);    
+    }
+  }
   MC_UNSET_RAW_MEM;
 
   /* Update Statistics */
@@ -70,10 +76,6 @@ void MC_dpor(void)
       DEBUG4("Exploration detph=%d (state=%p)(%d interleave) (%d enabled)", xbt_fifo_size(mc_stack),
         mc_current_state, xbt_setset_set_size(mc_current_state->interleave),
         xbt_setset_set_size(mc_current_state->enabled_transitions));
-
-      xbt_setset_foreach(mc_current_state->enabled_transitions, cursor, trans){
-        DEBUG1("\t %s", trans->name);
-      }
       
       /* Update statistics */
       mc_stats->visited_states++;
@@ -83,12 +85,10 @@ void MC_dpor(void)
          state, and create the data structures for the new expanded state in the
          exploration stack. */
       MC_SET_RAW_MEM;
-      trans = xbt_setset_set_choose(mc_current_state->interleave);
-      if(trans->type != mc_random){
-        xbt_setset_set_remove(mc_current_state->interleave, trans);
-        /* Add the transition in the done set of the current state */
-        xbt_setset_set_insert(mc_current_state->done, trans);
-      }
+      trans = xbt_setset_set_extract(mc_current_state->interleave);
+
+      /* Add the transition in the done set of the current state */
+      xbt_setset_set_insert(mc_current_state->done, trans);
       
       next_state = MC_state_new();
       xbt_fifo_unshift(mc_stack, next_state);
@@ -104,22 +104,12 @@ void MC_dpor(void)
       SIMIX_process_schedule(trans->process);
       MC_execute_surf_actions();        /* Do surf's related black magic */
       MC_schedule_enabled_processes();
-
-      if(trans->type == mc_random && trans->random.current_value < trans->random.max){
-        trans->random.current_value++;
-      }else{
-        //trans->random.current_value = trans->random.min;
-        xbt_setset_set_remove(mc_current_state->interleave, trans);
-        xbt_setset_set_insert(mc_current_state->done, trans);
-      }
       
       /* Calculate the enabled transitions set of the next state */
       MC_SET_RAW_MEM;
 
       xbt_setset_foreach(mc_current_state->transitions, cursor, trans_tmp){
-        DEBUG1("Checking transition %s", trans_tmp->name);
         if(trans_tmp->process != trans->process){
-          DEBUG2("Inherit transition %p (%lu)", trans_tmp, trans_tmp->ID);
           xbt_setset_set_insert(next_state->transitions, trans_tmp);
         }
       }
@@ -129,7 +119,7 @@ void MC_dpor(void)
       /* Choose one transition to interleave from the enabled transition set */      
       trans = xbt_setset_set_choose(next_state->enabled_transitions);
       if(trans){
-        DEBUG1("Choosing transition %p", trans);
+        DEBUG1("Choosing process %s for next interleave", trans->process->name);
         xbt_setset_foreach(next_state->enabled_transitions, cursor, trans_tmp){
           if(trans_tmp->process == trans->process)
             xbt_setset_set_insert(next_state->interleave, trans_tmp);    

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index d5b0aa1..4618a70 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -103,13 +103,8 @@ void MC_exit(int method)
 
 int MC_random(int min, int max)
 {
-  MC_trans_random_new(min,max);
-  SIMIX_process_yield();
-
-  if(!mc_replay_mode)
-    return mc_current_state->executed_transition->random.current_value;
-  else
-    return mc_current_state->executed_transition->random.current_value - 1;
+  MC_trans_intercept_random(min, max);
+  return mc_current_state->executed_transition->random.value;
 }
 
 /**

diff --git a/src/mc/mc_transition.c b/src/mc/mc_transition.c
index 3d46e0f..99cf291 100644 (file)
--- a/src/mc/mc_transition.c
+++ b/src/mc/mc_transition.c
@@ -69,17 +69,16 @@ mc_transition_t MC_trans_waitany_new(xbt_dynar_t comms)
 }
 
 /* Creates a new Random transition */
-mc_transition_t MC_trans_random_new(int min, int max)
+mc_transition_t MC_trans_random_new(int value)
 {
   mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
 
   trans->type = mc_random;
   trans->process = SIMIX_process_self();
-  trans->random.min = min;
-  trans->random.max = max;
-  trans->random.current_value = min;
-  trans->name = bprintf("[%s][%s] Random (%p)", trans->process->smx_host->name, 
-                        trans->process->name, trans);
+  trans->random.value = value;
+  trans->name = bprintf("[%s][%s] Random %d (%p)", trans->process->smx_host->name, 
+                        trans->process->name, value, trans);
+
   return trans;
 }
 
@@ -211,15 +210,18 @@ void MC_trans_intercept_waitany(xbt_dynar_t comms)
  */
 void MC_trans_intercept_random(int min, int max)
 {
+  int i;
   mc_transition_t trans=NULL;
   mc_state_t current_state = NULL;
   if(!mc_replay_mode){
     MC_SET_RAW_MEM;
-    trans = MC_trans_random_new(min, max);
-    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);
+    current_state = (mc_state_t)
+        xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+    for(i=min; i <= max; i++){    
+      trans = MC_trans_random_new(i);
+      xbt_setset_set_insert(current_state->created_transitions, trans);
+      xbt_setset_set_insert(current_state->transitions, trans);
+    }
     MC_UNSET_RAW_MEM;
   }
   SIMIX_process_yield();
@@ -277,6 +279,9 @@ int MC_transition_depend(mc_transition_t t1, mc_transition_t t2)
 
   if(t1->type != t2->type)
     return FALSE;
+
+  if(t1->type == mc_random || t2->type == mc_random)
+    return FALSE;
   
   if(t1->type == mc_isend && t2->type == mc_isend && t1->isend.rdv != t2->isend.rdv)
     return FALSE;

diff --git a/src/mc/private.h b/src/mc/private.h
index 8b3ac7b..6b4e47d 100644 (file)
--- a/src/mc/private.h
+++ b/src/mc/private.h
@@ -104,9 +104,7 @@ typedef struct s_mc_transition{
     } waitany;
 
     struct {
-      int min;
-      int max;
-      int current_value;
+      int value;
     } random;
   };
 } s_mc_transition_t;
@@ -116,7 +114,7 @@ mc_transition_t MC_trans_irecv_new(smx_rdv_t);
 mc_transition_t MC_trans_wait_new(smx_comm_t);
 mc_transition_t MC_trans_test_new(smx_comm_t);
 mc_transition_t MC_trans_waitany_new(xbt_dynar_t);
-mc_transition_t MC_trans_random_new(int, int);
+mc_transition_t MC_trans_random_new(int);
 void MC_transition_delete(mc_transition_t);
 int MC_transition_depend(mc_transition_t, mc_transition_t);
 void MC_trans_compute_enabled(xbt_setset_set_t, xbt_setset_set_t);