void MC_dpor_init()
{
mc_state_t initial_state = NULL;
- mc_transition_t trans = NULL;
+ mc_transition_t trans, trans_tmp = NULL;
+ xbt_setset_cursor_t cursor = NULL;
/* Create the initial state and push it into the exploration stack */
MC_SET_RAW_MEM;
/* Fill the interleave set of the initial state with an enabled process */
trans = xbt_setset_set_choose(initial_state->enabled_transitions);
- if(trans)
- xbt_setset_set_insert(initial_state->interleave, trans);
+ if(trans){
+ DEBUG1("Choosing process %s for next interleave", trans->process->name);
+ xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans_tmp){
+ if(trans_tmp->process == trans->process)
+ xbt_setset_set_insert(initial_state->interleave, trans_tmp);
+ }
+ }
MC_UNSET_RAW_MEM;
/* Update Statistics */
DEBUG4("Exploration detph=%d (state=%p)(%d interleave) (%d enabled)", xbt_fifo_size(mc_stack),
mc_current_state, xbt_setset_set_size(mc_current_state->interleave),
xbt_setset_set_size(mc_current_state->enabled_transitions));
-
- xbt_setset_foreach(mc_current_state->enabled_transitions, cursor, trans){
- DEBUG1("\t %s", trans->name);
- }
/* Update statistics */
mc_stats->visited_states++;
state, and create the data structures for the new expanded state in the
exploration stack. */
MC_SET_RAW_MEM;
- 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 = xbt_setset_set_extract(mc_current_state->interleave);
+
+ /* Add the transition in the done set of the current state */
+ xbt_setset_set_insert(mc_current_state->done, trans);
next_state = MC_state_new();
xbt_fifo_unshift(mc_stack, next_state);
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->random.current_value < trans->random.max){
- trans->random.current_value++;
- }else{
- //trans->random.current_value = trans->random.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 */
MC_SET_RAW_MEM;
xbt_setset_foreach(mc_current_state->transitions, cursor, trans_tmp){
- DEBUG1("Checking transition %s", trans_tmp->name);
if(trans_tmp->process != trans->process){
- DEBUG2("Inherit transition %p (%lu)", trans_tmp, trans_tmp->ID);
xbt_setset_set_insert(next_state->transitions, trans_tmp);
}
}
/* Choose one transition to interleave from the enabled transition set */
trans = xbt_setset_set_choose(next_state->enabled_transitions);
if(trans){
- DEBUG1("Choosing transition %p", trans);
+ DEBUG1("Choosing process %s for next interleave", trans->process->name);
xbt_setset_foreach(next_state->enabled_transitions, cursor, trans_tmp){
if(trans_tmp->process == trans->process)
xbt_setset_set_insert(next_state->interleave, trans_tmp);
}
/* Creates a new Random transition */
-mc_transition_t MC_trans_random_new(int min, int max)
+mc_transition_t MC_trans_random_new(int value)
{
mc_transition_t trans = xbt_new0(s_mc_transition_t, 1);
trans->type = mc_random;
trans->process = SIMIX_process_self();
- trans->random.min = min;
- trans->random.max = max;
- trans->random.current_value = min;
- trans->name = bprintf("[%s][%s] Random (%p)", trans->process->smx_host->name,
- trans->process->name, trans);
+ trans->random.value = value;
+ trans->name = bprintf("[%s][%s] Random %d (%p)", trans->process->smx_host->name,
+ trans->process->name, value, trans);
+
return trans;
}
*/
void MC_trans_intercept_random(int min, int max)
{
+ int i;
mc_transition_t trans=NULL;
mc_state_t current_state = NULL;
if(!mc_replay_mode){
MC_SET_RAW_MEM;
- trans = MC_trans_random_new(min, max);
- current_state = (mc_state_t)
- xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
- xbt_setset_set_insert(current_state->created_transitions, trans);
- xbt_setset_set_insert(current_state->transitions, trans);
+ current_state = (mc_state_t)
+ xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+ for(i=min; i <= max; i++){
+ trans = MC_trans_random_new(i);
+ xbt_setset_set_insert(current_state->created_transitions, trans);
+ xbt_setset_set_insert(current_state->transitions, trans);
+ }
MC_UNSET_RAW_MEM;
}
SIMIX_process_yield();
if(t1->type != t2->type)
return FALSE;
+
+ if(t1->type == mc_random || t2->type == mc_random)
+ return FALSE;
if(t1->type == mc_isend && t2->type == mc_isend && t1->isend.rdv != t2->isend.rdv)
return FALSE;