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,
27 initial_state->transitions);
28 xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans) {
29 if (trans->type == mc_wait
30 && (trans->wait.comm->src_proc == NULL
31 || trans->wait.comm->dst_proc == NULL)) {
32 xbt_setset_set_remove(initial_state->enabled_transitions, trans);
36 /* Fill the interleave set of the initial state with all enabled transitions */
37 xbt_setset_add(initial_state->interleave,
38 initial_state->enabled_transitions);
40 /* Update Statistics */
41 mc_stats->state_size +=
42 xbt_setset_set_size(initial_state->enabled_transitions);
48 * \brief Perform the model-checking operation using a depth-first search exploration
50 * It performs the model-checking operation by executing all possible scheduling of the communication actions
51 * \return The time spent to execute the simulation or -1 if the simulation ended
55 mc_transition_t trans = NULL;
56 mc_state_t current_state = NULL;
57 mc_state_t next_state = NULL;
58 xbt_setset_cursor_t cursor = NULL;
60 while (xbt_fifo_size(mc_stack) > 0) {
61 DEBUG0("**************************************************");
63 /* FIXME: Think about what happens if there are no transitions but there are
64 some actions on the models. (ex. all the processes do a sleep(0) in a round). */
66 /* Get current state */
67 current_state = (mc_state_t)
68 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
70 /* If there are transitions to execute and the maximun depth has not been reached
71 then perform one step of the exploration algorithm */
72 if (xbt_setset_set_size(current_state->interleave) > 0
73 && xbt_fifo_size(mc_stack) < MAX_DEPTH) {
75 DEBUG3("Exploration detph=%d (state=%p)(%d transitions)",
76 xbt_fifo_size(mc_stack), current_state,
77 xbt_setset_set_size(current_state->interleave));
79 /* Update statistics */
80 mc_stats->visited_states++;
81 mc_stats->executed_transitions++;
83 /* Choose a transition to execute from the interleave set of the current state,
84 and create the data structures for the new expanded state in the exploration
87 trans = xbt_setset_set_extract(current_state->interleave);
89 /* Define it as the executed transition of this state */
90 current_state->executed_transition = trans;
92 next_state = MC_state_new();
93 xbt_fifo_unshift(mc_stack, next_state);
96 DEBUG1("Executing transition %s", trans->name);
97 SIMIX_process_schedule(trans->process);
99 /* Do all surf's related black magic tricks to keep all working */
100 MC_execute_surf_actions();
102 /* Schedule every process that got enabled due to the executed transition */
103 MC_schedule_enabled_processes();
105 /* Calculate the enabled transitions set of the next state:
106 -add the transition sets of the current state and the next state
107 -remove the executed transition from that set
108 -remove all the transitions that are disabled (mc_wait only)
109 -use the resulting set as the enabled transitions of the next state */
111 xbt_setset_add(next_state->transitions, current_state->transitions);
112 xbt_setset_set_remove(next_state->transitions, trans);
113 xbt_setset_add(next_state->enabled_transitions,
114 next_state->transitions);
115 xbt_setset_foreach(next_state->enabled_transitions, cursor, trans) {
116 if (trans->type == mc_wait
117 && (trans->wait.comm->src_proc == NULL
118 || trans->wait.comm->dst_proc == NULL)) {
119 xbt_setset_set_remove(next_state->enabled_transitions, trans);
123 /* Fill the interleave set of the new state with all enabled transitions */
124 xbt_setset_add(next_state->interleave,
125 next_state->enabled_transitions);
128 /* Update Statistics */
129 mc_stats->state_size +=
130 xbt_setset_set_size(next_state->enabled_transitions);
132 /* Let's loop again */
134 /* The interleave set is empty or the maximum depth is reached, let's back-track */
136 DEBUG0("There are no more actions to run");
139 xbt_fifo_shift(mc_stack);
140 MC_state_delete(current_state);
142 /* Go backwards in the stack until we find a state with transitions in the interleave set */
143 while (xbt_fifo_size(mc_stack) > 0
144 && (current_state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
145 if (xbt_setset_set_size(current_state->interleave) == 0) {
146 MC_state_delete(current_state);
148 xbt_fifo_unshift(mc_stack, current_state);
149 DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
152 /* Let's loop again */
159 /* We are done, show the statistics and return */
160 MC_print_statistics(mc_stats);