model-checker : new simcall MC_RANDOM

diff --git a/include/simgrid/simix.h b/include/simgrid/simix.h
index 7dfab37..8d3ed6b 100644 (file)
--- a/include/simgrid/simix.h
+++ b/include/simgrid/simix.h
@@ -478,6 +478,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(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 f226c9c..72714a3 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -303,11 +303,16 @@ void MC_exit(void)
   xbt_abort();
 }
 
+int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
+
+  return simcall->mc_value;
+}
+
 
 int MC_random(int min, int max)
 {
   /*FIXME: return mc_current_state->executed_transition->random.value;*/
-  return 0;
+  return simcall_mc_random(min, max);
 }
 
 /**

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 865e1cb..699a467 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -74,6 +74,8 @@ 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);
 
+int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max);
+
 /********************************* Requests ***********************************/
 int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);
 char* MC_request_to_string(smx_simcall_t req, int value);

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index 1033bfc..4e12e96 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -18,6 +18,9 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) {
   if (r1->issuer == r2->issuer)
     return FALSE;
 
+  if((r1->call == SIMCALL_MC_RANDOM) || (r2->call == SIMCALL_MC_RANDOM))
+    return FALSE;
+
   if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV)
     return FALSE;
 
@@ -248,13 +251,22 @@ char *MC_request_to_string(smx_simcall_t req, int value)
     args = '\0';
     break;
 
+  case SIMCALL_MC_RANDOM:
+    type = xbt_strdup("MC_RANDOM");
+    args = '\0';
+    break;
+
   default:
     THROW_UNIMPLEMENTED;
   }
 
-  str = bprintf("[(%lu)%s] %s (%s)", req->issuer->pid ,req->issuer->name, type, args);
+  if(args != NULL){
+    str = bprintf("[(%lu)%s] %s (%s)", req->issuer->pid ,req->issuer->name, type, args);
+    xbt_free(args);
+  }else{
+    str = bprintf("[(%lu)%s] %s ", req->issuer->pid ,req->issuer->name, type);
+  }
   xbt_free(type);
-  xbt_free(args);
   xbt_free(p);
   xbt_free(bs);
   return str;
@@ -281,6 +293,7 @@ int MC_request_is_visible(smx_simcall_t req)
     || req->call == SIMCALL_COMM_WAITANY
     || req->call == SIMCALL_COMM_TEST
     || req->call == SIMCALL_COMM_TESTANY
+    || req->call == SIMCALL_MC_RANDOM
     || req->call == SIMCALL_MC_SNAPSHOT
     || req->call == SIMCALL_MC_COMPARE_SNAPSHOTS;
 }

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index 4d41ba1..d43a6bc 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -117,6 +117,11 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int valu
       simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
       break;
 
+    case SIMCALL_MC_RANDOM:
+      state->internal_req = *req;
+      simcall_mc_random__set__result(&state->internal_req, value);
+      break;
+
     default:
       state->internal_req = *req;
       break;
@@ -139,6 +144,13 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
   smx_process_t process = NULL;
   mc_procstate_t procstate = NULL;
   unsigned int start_count;
+  int min, max;
+
+  static int first = 0;
+  if(first == 0){
+    srand(987654321);
+    first = 1;
+  }
 
   xbt_swag_foreach(process, simix_global->process_list){
     procstate = &state->proc_status[process->pid];
@@ -193,6 +205,14 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
 
             break;
 
+          case SIMCALL_MC_RANDOM:
+            min = simcall_mc_random__get__min(&process->simcall);
+            max = simcall_mc_random__get__max(&process->simcall);
+            *value = (int)((rand() % ((max-min)+1)) + min);
+            procstate->state = MC_DONE;
+            return &process->simcall;
+            break;
+          
           default:
             procstate->state = MC_DONE;
             *value = 0;

diff --git a/src/simix/smx_smurf_private.h b/src/simix/smx_smurf_private.h
index db8bf14..e4224a1 100644 (file)
--- a/src/simix/smx_smurf_private.h
+++ b/src/simix/smx_smurf_private.h
@@ -367,7 +367,8 @@ ACTION(SIMCALL_SET_CATEGORY, set_category, WITH_ANSWER, TVOID(result), TSPEC(act
 #ifdef HAVE_MC
 #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_COMPARE_SNAPSHOTS, mc_compare_snapshots, WITH_ANSWER, TINT(result), TPTR(s1), TPTR(s2)) 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 6d8a67c..ae4749f 100644 (file)
--- a/src/simix/smx_user.c
+++ b/src/simix/smx_user.c
@@ -1161,6 +1161,12 @@ int simcall_mc_compare_snapshots(void *s1, void *s2){
   return simcall_BODY_mc_compare_snapshots(s1, s2);
 }
 
+int simcall_mc_random(int min, int max)
+{
+  return simcall_BODY_mc_random(min, max);
+}
+
+
 #endif /* HAVE_MC */
 
 /* ****************************************************************************************** */