model-checker : add min and max values for MC_RANDOM simcall

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index 0993b45..5cffc94 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -19,7 +19,7 @@ extern int _sg_do_model_check; /* please don't use directly: we inline MC_is_act
 #define MC_is_active() _sg_do_model_check
 
 XBT_PUBLIC(void) MC_assert(int);
-XBT_PUBLIC(int) MC_random(void);
+XBT_PUBLIC(int) MC_random(int min, int max);
 XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, void* fct);
 XBT_PUBLIC(void *) MC_snapshot(void);
 XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2);

diff --git a/include/simgrid/simix.h b/include/simgrid/simix.h
index 5c3d41b..a13c31c 100644 (file)
--- a/include/simgrid/simix.h
+++ b/include/simgrid/simix.h
@@ -500,7 +500,7 @@ XBT_PUBLIC(xbt_dict_t) simcall_asr_get_properties(const char *name);
 /************************** MC simcalls   **********************************/
 XBT_PUBLIC(void *) simcall_mc_snapshot(void);
 XBT_PUBLIC(int) simcall_mc_compare_snapshots(void *s1, void *s2);
-XBT_PUBLIC(int) simcall_mc_random(void);
+XBT_PUBLIC(int) simcall_mc_random(int min, int max);
 
 /************************** New API simcalls **********************************/
 /* TUTORIAL: New API                                                          */

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index a7f1db8..328a69d 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -1971,16 +1971,16 @@ void MC_exit(void)
   //xbt_abort();
 }
 
-int SIMIX_pre_mc_random(smx_simcall_t simcall){
+int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
 
   return simcall->mc_value;
 }
 
 
-int MC_random(void)
+int MC_random(int min, int max)
 {
   /*FIXME: return mc_current_state->executed_transition->random.value;*/
-  return simcall_mc_random();
+  return simcall_mc_random(min, max);
 }
 
 /**

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 7c06632..5d297e2 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -79,7 +79,7 @@ void MC_show_deadlock(smx_simcall_t req);
 void MC_show_stack_safety(xbt_fifo_t stack);
 void MC_dump_stack_safety(xbt_fifo_t stack);
 void MC_init(void);
-int SIMIX_pre_mc_random(smx_simcall_t simcall);
+int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max);
 
 
 /********************************* Requests ***********************************/

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index 27e1d3f..23ca6ee 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -461,17 +461,10 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value){
     break;
 
   case SIMCALL_MC_RANDOM:
-    if(value == 0){
-      if(req->issuer->smx_host)
-        label = bprintf("[(%lu)%s] MC_RANDOM (0)", req->issuer->pid, MSG_host_get_name(req->issuer->smx_host));
-      else
-        label = bprintf("[(%lu)] MC_RANDOM (0)", req->issuer->pid);
-    }else{
-      if(req->issuer->smx_host)
-        label = bprintf("[(%lu)%s] MC_RANDOM (1)", req->issuer->pid, MSG_host_get_name(req->issuer->smx_host));
-      else
-        label = bprintf("[(%lu)] MC_RANDOM (1)", req->issuer->pid);
-    }
+    if(req->issuer->smx_host)
+      label = bprintf("[(%lu)%s] MC_RANDOM (%d)", req->issuer->pid, MSG_host_get_name(req->issuer->smx_host), value);
+    else
+      label = bprintf("[(%lu)] MC_RANDOM (%d)", req->issuer->pid, value);
     break;
 
   case SIMCALL_MC_SNAPSHOT:

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index 59cca4e..c7ff71c 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -109,12 +109,11 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int valu
 
     case SIMCALL_MC_RANDOM:
       state->internal_req = *req;
-      simcall_mc_random__set__result(&state->internal_req, value);
-      if(value == 0){
+      if(value != simcall_mc_random__get__max(req)){
         xbt_swag_foreach(process, simix_global->process_list){
           procstate = &state->proc_status[process->pid];
           if(process->pid == req->issuer->pid){
-            procstate->state = MC_MORE_INTERLEAVE;  
+            procstate->state = MC_MORE_INTERLEAVE;
             break;
           }        
         }
@@ -200,8 +199,10 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
           case SIMCALL_MC_RANDOM:
             if(procstate->state == MC_INTERLEAVE)
               *value = 0;
-            else
-              *value = 1;
+            else{
+              if(state->req_num < simcall_mc_random__get__max(&process->simcall))
+                *value = state->req_num + 1;
+            }
             procstate->state = MC_DONE;
             return &process->simcall;
             break;

diff --git a/src/simix/smx_smurf_private.h b/src/simix/smx_smurf_private.h
index 44f3524..9669242 100644 (file)
--- a/src/simix/smx_smurf_private.h
+++ b/src/simix/smx_smurf_private.h
@@ -381,7 +381,7 @@ ACTION(SIMCALL_SET_CATEGORY, set_category, WITH_ANSWER, TVOID(result), TSPEC(act
 #define SIMCALL_LIST4(ACTION, sep) \
 ACTION(SIMCALL_MC_SNAPSHOT, mc_snapshot, WITH_ANSWER, TPTR(result)) sep \
 ACTION(SIMCALL_MC_COMPARE_SNAPSHOTS, mc_compare_snapshots, WITH_ANSWER, TINT(result), TPTR(s1), TPTR(s2)) sep \
-ACTION(SIMCALL_MC_RANDOM, mc_random, WITH_ANSWER, TINT(result)) sep
+ACTION(SIMCALL_MC_RANDOM, mc_random, WITH_ANSWER, TINT(result), TINT(min), TINT(max)) sep
 #else
 #define SIMCALL_LIST4(ACTION, sep)
 #endif

diff --git a/src/simix/smx_user.c b/src/simix/smx_user.c
index a990f47..30ee757 100644 (file)
--- a/src/simix/smx_user.c
+++ b/src/simix/smx_user.c
@@ -1311,9 +1311,9 @@ int simcall_mc_compare_snapshots(void *s1, void *s2){
   return simcall_BODY_mc_compare_snapshots(s1, s2);
 }
 
-int simcall_mc_random(void)
+int simcall_mc_random(int min, int max)
 {
-  return simcall_BODY_mc_random();
+  return simcall_BODY_mc_random(min, max);
 }