From: cristianrosa Date: Tue, 11 May 2010 15:42:33 +0000 (+0000) Subject: Add int MC_random(int min, int max) function that will make the model-checker to... X-Git-Tag: SVN~8 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/d6b585e44bd28ba41f3faae4a99b602290f16434 Add int MC_random(int min, int max) function that will make the model-checker to explore all possible return values of the functions. The possible return values are integers in the range between min and max 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 864860d875..9bc3a80f04 100644 --- 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 70090226ef..430a445938 100644 --- 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 454fc4bde1..1958c782e5 100644 --- 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 88992b91aa..eb4dd9bc1d 100644 --- 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 97e3e2a235..81a1b206d1 100644 --- 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 e397f35569..685e0dd51a 100644 --- 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 b6a3762dc4..3011c5bd20 100644 --- 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);