3 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc,
4 "Logging specific to MC DFS exploration");
9 mc_transition_t trans = NULL;
10 mc_state_t initial_state = NULL;
11 xbt_setset_cursor_t cursor = NULL;
14 initial_state = MC_state_new();
15 /* Add the state data structure for the initial state */
16 xbt_fifo_unshift(mc_stack, initial_state);
19 DEBUG0("**************************************************");
20 DEBUG0("Initial state");
22 /* Schedule all the processes to detect the transitions from the initial state */
23 MC_schedule_enabled_processes();
26 xbt_setset_add(initial_state->enabled_transitions, initial_state->transitions);
27 xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans){
28 if(trans->type == mc_wait
29 && (trans->wait.comm->src_proc == NULL || trans->wait.comm->dst_proc == NULL)){
30 xbt_setset_set_remove(initial_state->enabled_transitions, trans);
34 /* Fill the interleave set of the initial state with all enabled transitions */
35 xbt_setset_add(initial_state->interleave, initial_state->enabled_transitions);
37 /* Update Statistics */
38 mc_stats->state_size += xbt_setset_set_size(initial_state->enabled_transitions);
44 * \brief Perform the model-checking operation using a depth-first search exploration
46 * It performs the model-checking operation by executing all possible scheduling of the communication actions
47 * \return The time spent to execute the simulation or -1 if the simulation ended
51 mc_transition_t trans = NULL;
52 mc_state_t current_state = NULL;
53 mc_state_t next_state = NULL;
54 xbt_setset_cursor_t cursor = NULL;
56 while(xbt_fifo_size(mc_stack) > 0){
57 DEBUG0("**************************************************");
59 /* FIXME: Think about what happens if there are no transitions but there are
60 some actions on the models. (ex. all the processes do a sleep(0) in a round). */
62 /* Get current state */
63 current_state = (mc_state_t)
64 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
66 /* If there are transitions to execute and the maximun depth has not been reached
67 then perform one step of the exploration algorithm */
68 if(xbt_setset_set_size(current_state->interleave) > 0 && xbt_fifo_size(mc_stack) < MAX_DEPTH){
70 DEBUG3("Exploration detph=%d (state=%p)(%d transitions)", xbt_fifo_size(mc_stack),
71 current_state, xbt_setset_set_size(current_state->interleave));
73 /* Update statistics */
74 mc_stats->visited_states++;
75 mc_stats->executed_transitions++;
77 /* Choose a transition to execute from the interleave set of the current state,
78 and create the data structures for the new expanded state in the exploration
81 trans = xbt_setset_set_extract(current_state->interleave);
83 /* Define it as the executed transition of this state */
84 current_state->executed_transition = trans;
86 next_state = MC_state_new();
87 xbt_fifo_unshift(mc_stack, next_state);
90 DEBUG1("Executing transition %s", trans->name);
91 SIMIX_process_schedule(trans->process);
93 /* Do all surf's related black magic tricks to keep all working */
94 MC_execute_surf_actions();
96 /* Schedule every process that got enabled due to the executed transition */
97 MC_schedule_enabled_processes();
99 /* Calculate the enabled transitions set of the next state:
100 -add the transition sets of the current state and the next state
101 -remove the executed transition from that set
102 -remove all the transitions that are disabled (mc_wait only)
103 -use the resulting set as the enabled transitions of the next state */
105 xbt_setset_add(next_state->transitions, current_state->transitions);
106 xbt_setset_set_remove(next_state->transitions, trans);
107 xbt_setset_add(next_state->enabled_transitions, next_state->transitions);
108 xbt_setset_foreach(next_state->enabled_transitions, cursor, trans){
109 if(trans->type == mc_wait
110 && (trans->wait.comm->src_proc == NULL || trans->wait.comm->dst_proc == NULL)){
111 xbt_setset_set_remove(next_state->enabled_transitions, trans);
115 /* Fill the interleave set of the new state with all enabled transitions */
116 xbt_setset_add(next_state->interleave, next_state->enabled_transitions);
119 /* Update Statistics */
120 mc_stats->state_size += xbt_setset_set_size(next_state->enabled_transitions);
122 /* Let's loop again */
124 /* The interleave set is empty or the maximum depth is reached, let's back-track */
126 DEBUG0("There are no more actions to run");
129 xbt_fifo_shift(mc_stack);
130 MC_state_delete(current_state);
132 /* Go backwards in the stack until we find a state with transitions in the interleave set */
133 while(xbt_fifo_size(mc_stack) > 0 && (current_state = (mc_state_t)xbt_fifo_shift(mc_stack))){
134 if(xbt_setset_set_size(current_state->interleave) == 0){
135 MC_state_delete(current_state);
137 xbt_fifo_unshift(mc_stack, current_state);
138 DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
141 /* Let's loop again */
148 /* We are done, show the statistics and return */
149 MC_print_statistics(mc_stats);