From ec3bf45915829f16601f4a221afff11f7bf0a138 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Sat, 10 Aug 2013 12:27:52 +0200 Subject: [PATCH] model-checker : add min and max values for MC_RANDOM simcall --- include/simgrid/modelchecker.h | 2 +- include/simgrid/simix.h | 2 +- src/mc/mc_global.c | 6 +++--- src/mc/mc_private.h | 2 +- src/mc/mc_request.c | 15 ++++----------- src/mc/mc_state.c | 11 ++++++----- src/simix/smx_smurf_private.h | 2 +- src/simix/smx_user.c | 4 ++-- 8 files changed, 19 insertions(+), 25 deletions(-) diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h index 0993b4566c..5cffc94440 100644 --- 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 5c3d41b1a0..a13c31cb61 100644 --- 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 a7f1db87e7..328a69dd8b 100644 --- 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 7c06632aaa..5d297e23ad 100644 --- 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 27e1d3f342..23ca6ee6a7 100644 --- 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 59cca4e6cc..c7ff71ce1b 100644 --- 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 44f3524a13..9669242dba 100644 --- 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 a990f4799d..30ee757f9f 100644 --- 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); } -- 2.20.1