Add int MC_random(int min, int max) function that will make the model-checker to...

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

diff --git a/include/mc/modelchecker.h b/include/mc/modelchecker.h
index 864860d..9bc3a80 100644 (file)
--- a/include/mc/modelchecker.h
+++ b/include/mc/modelchecker.h
@@ -1,3 +1,4 @@
 #include "xbt.h"
 
-XBT_PUBLIC(void) MC_assert(int);
\ No newline at end of file
+XBT_PUBLIC(void) MC_assert(int);
+XBT_PUBLIC(int) MC_random(int min, int max);
\ No newline at end of file

diff --git a/src/include/mc/datatypes.h b/src/include/mc/datatypes.h
index 7009022..430a445 100644 (file)
--- a/src/include/mc/datatypes.h
+++ b/src/include/mc/datatypes.h
@@ -20,7 +20,8 @@ typedef enum {
   mc_irecv,
   mc_test,
   mc_wait,
-  mc_waitany
+  mc_waitany,
+  mc_random
 } mc_trans_type_t;
 
 typedef struct s_mc_transition *mc_transition_t;

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 454fc4b..1958c78 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -22,6 +22,7 @@ SG_BEGIN_DECL()
 XBT_PUBLIC(void) MC_init(int);
 XBT_PUBLIC(void) MC_assert(int);
 XBT_PUBLIC(void) MC_modelcheck(int);
+XBT_PUBLIC(int) MC_random(int,int);
 
 /******************************* Transitions **********************************/
 XBT_PUBLIC(mc_transition_t) MC_create_transition(mc_trans_type_t, smx_process_t, smx_rdv_t, smx_comm_t);

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 88992b9..eb4dd9b 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -58,7 +58,6 @@ void MC_dpor_init()
 void MC_dpor(void)
 {
   mc_transition_t trans = NULL;  
-  mc_state_t current_state = NULL;
   mc_state_t next_state = NULL;
   xbt_setset_cursor_t cursor = NULL;
   
@@ -70,17 +69,17 @@ void MC_dpor(void)
        some actions on the models. (ex. all the processes do a sleep(0) in a round). */
 
     /* Get current state */
-    current_state = (mc_state_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+    mc_current_state = (mc_state_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
    
     /* If there are transitions to execute and the maximun depth has not been reached 
        then perform one step of the exploration algorithm */
-    if(xbt_setset_set_size(current_state->interleave) > 0 && xbt_fifo_size(mc_stack) < MAX_DEPTH){
+    if(xbt_setset_set_size(mc_current_state->interleave) > 0 && xbt_fifo_size(mc_stack) < MAX_DEPTH){
 
       DEBUG4("Exploration detph=%d (state=%p)(%d interleave) (%d enabled)", xbt_fifo_size(mc_stack),
-        current_state, xbt_setset_set_size(current_state->interleave),
-        xbt_setset_set_size(current_state->enabled_transitions));
+        mc_current_state, xbt_setset_set_size(mc_current_state->interleave),
+        xbt_setset_set_size(mc_current_state->enabled_transitions));
 
-      xbt_setset_foreach(current_state->enabled_transitions, cursor, trans){
+      xbt_setset_foreach(mc_current_state->enabled_transitions, cursor, trans){
         DEBUG1("\t %s", trans->name);
       }
       
@@ -92,16 +91,19 @@ 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_extract(current_state->interleave);
+      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->refcount++;
+      }
+      
       next_state = MC_state_new();
       xbt_fifo_unshift(mc_stack, next_state);
       
-      /* Add the transition in the done set of the current state */
-      xbt_setset_set_insert(current_state->done, trans);
-      trans->refcount++;
-      
       /* Set it as the executed transition of the current state */
-      current_state->executed_transition = trans;
+      mc_current_state->executed_transition = trans;
       MC_UNSET_RAW_MEM;
 
       /* Execute the selected transition by scheduling it's associated process.
@@ -111,6 +113,14 @@ 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->current_value < trans->max ){
+        trans->current_value++;
+      }else{
+        trans->current_value = trans->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:
           -add the transition sets of the current state and the next state 
@@ -118,7 +128,7 @@ void MC_dpor(void)
           -remove all the transitions that are disabled (mc_wait only)
           -use the resulting set as the enabled transitions of the next state */
       MC_SET_RAW_MEM;
-      xbt_setset_add(next_state->transitions, current_state->transitions);
+      xbt_setset_add(next_state->transitions, mc_current_state->transitions);
       xbt_setset_set_remove(next_state->transitions, trans);
       xbt_setset_add(next_state->enabled_transitions, next_state->transitions);
       xbt_setset_foreach(next_state->enabled_transitions, cursor, trans){
@@ -152,7 +162,7 @@ void MC_dpor(void)
       /* Trash the current state, no longer needed */
       MC_SET_RAW_MEM;
       xbt_fifo_shift(mc_stack);
-      MC_state_delete(current_state);
+      MC_state_delete(mc_current_state);
       
       /* Traverse the stack backwards until a state with a non empty interleave
          set is found, deleting all the states that have it empty in the way.
@@ -160,8 +170,8 @@ void MC_dpor(void)
          (from it's predecesor state), depends on any other previous transition 
          executed before it. If it does then add it to the interleave set of the
          state that executed that previous transition. */
-      while((current_state = xbt_fifo_shift(mc_stack)) != NULL){
-        q = current_state->executed_transition;
+      while((mc_current_state = xbt_fifo_shift(mc_stack)) != NULL){
+        q = mc_current_state->executed_transition;
         xbt_fifo_foreach(mc_stack, item, state, mc_state_t){
           if(MC_transition_depend(q, state->executed_transition)){
             DEBUG3("Dependence found at state %p (%p,%p)", state, state->executed_transition, q);
@@ -176,15 +186,15 @@ void MC_dpor(void)
               break;
           }
         }
-        if(xbt_setset_set_size(current_state->interleave) > 0){
+        if(xbt_setset_set_size(mc_current_state->interleave) > 0){
           /* We found a back-tracking point, let's loop */
-          xbt_fifo_unshift(mc_stack, current_state);
+          xbt_fifo_unshift(mc_stack, mc_current_state);
           DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
           MC_replay(mc_stack);
           MC_UNSET_RAW_MEM;
           break;
         }else{
-          MC_state_delete(current_state);
+          MC_state_delete(mc_current_state);
         }        
       }
     }

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 97e3e2a..81a1b20 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -11,6 +11,7 @@ mc_snapshot_t initial_snapshot = NULL;
 xbt_fifo_t mc_stack = NULL;
 xbt_setset_t mc_setset = NULL;
 mc_stats_t mc_stats = NULL;
+mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
 
 /**
@@ -70,6 +71,16 @@ void MC_modelcheck(int method){
   }
 }
 
+int MC_random(int min, int max)
+{
+  MC_random_create(min,max);
+  SIMIX_process_yield();
+
+  if(!mc_replay_mode)
+    return mc_current_state->executed_transition->current_value;
+  else
+    return mc_current_state->executed_transition->current_value - 1;
+}
 
 /**
  * \brief Re-executes from the initial state all the transitions indicated by
@@ -79,7 +90,6 @@ void MC_modelcheck(int method){
 void MC_replay(xbt_fifo_t stack)
 {
   xbt_fifo_item_t item;
-  mc_state_t state;
   mc_transition_t trans;
 
   DEBUG0("**** Begin Replay ****");
@@ -96,8 +106,8 @@ void MC_replay(xbt_fifo_t stack)
       item != xbt_fifo_get_first_item(stack);
       item = xbt_fifo_get_prev_item(item)){
 
-    state = (mc_state_t) xbt_fifo_get_item_content(item);
-    trans = state->executed_transition;
+    mc_current_state = (mc_state_t) xbt_fifo_get_item_content(item);
+    trans = mc_current_state->executed_transition;
 
     /* Update statistics */
     mc_stats->visited_states++;

diff --git a/src/mc/mc_transition.c b/src/mc/mc_transition.c
index e397f35..685e0dd 100644 (file)
--- a/src/mc/mc_transition.c
+++ b/src/mc/mc_transition.c
@@ -51,6 +51,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->refcount = 1;    
+    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->transitions, trans);
+    MC_UNSET_RAW_MEM;
+  }
+}
+
 /** 
  * \brief Associate a communication to a transition
  * \param trans The transition

diff --git a/src/mc/private.h b/src/mc/private.h
index b6a3762..3011c5b 100644 (file)
--- a/src/mc/private.h
+++ b/src/mc/private.h
@@ -71,8 +71,14 @@ typedef struct s_mc_transition{
   smx_process_t process;
   smx_rdv_t rdv;
   smx_comm_t comm;          /* reference to the simix network communication */
+  
+  /* Used only for random transitions */
+  int min;                  /* min random value */ 
+  int max;                  /* max random value */
+  int current_value;        /* current value */
 } s_mc_transition_t;
 
+void MC_random_create(int,int);
 void MC_transition_delete(mc_transition_t);
 int MC_transition_depend(mc_transition_t, mc_transition_t);
 
@@ -87,6 +93,7 @@ typedef struct mc_state{
 
 extern xbt_fifo_t mc_stack;
 extern xbt_setset_t mc_setset;
+extern mc_state_t mc_current_state;
 
 mc_state_t MC_state_new(void);
 void MC_state_delete(mc_state_t);