return transition_;
}
-// This should be intierely done in GuidedState
aid_t State::next_transition() const
{
XBT_DEBUG("Search for an actor to run. %zu actors to consider", guide->actors_to_run_.size());
return -1;
}
+std::pair<aid_t, double> State::next_transition_guided() const
+{
+ return guide->next_transition();
+}
+
// This should be done in GuidedState, or at least interact with it
void State::execute_next(aid_t next, RemoteApp& app)
{
explicit State(RemoteApp& remote_app, const State* parent_state);
/* Returns a positive number if there is another transition to pick, or -1 if not */
aid_t next_transition() const;
+ /* Same as next_transition, but choice is now guided, and a double corresponding to the
+ internal cost of the transition is returned */
+ std::pair<aid_t, double> next_transition_guided() const;
/* Explore a new path on the remote app; the parameter 'next' must be the result of a previous call to
* next_transition() */
// Not Yet fully implemented
class BasicGuide : public GuidedState {
public:
- std::pair<aid_t, double> next_transition() const override { return std::make_pair(0, 0); }
- virtual void execute_next(aid_t aid) override { return; }
+ std::pair<aid_t, double> next_transition() const override
+ {
+
+ for (auto const& [aid, actor] : actors_to_run_) {
+ /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */
+ if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) {
+ continue;
+ }
+
+ return std::make_pair(aid, 1.0);
+ }
+ return std::make_pair(-1, 0.0);
+ }
+ void execute_next(aid_t aid, RemoteApp& app) override { return; }
};
} // namespace simgrid::mc
}
// Search for the next transition
- aid_t next = state->next_transition();
+ // next_transition returns a pair<aid_t, double> in case we want to consider multiple state
+ auto [next, _] = state->next_transition_guided();
if (next < 0) { // If there is no more transition in the current state, backtrack.
XBT_DEBUG("There remains %lu actors, but none to interleave (depth %zu).", state->get_actor_count(),
stack_.size() + 1);
-
+
if (state->get_actor_count() == 0) {
get_remote_app().finalize_app();
XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
state->get_num(), stack_.size());
-
}
-
+
this->backtrack();
continue;
}
on_state_creation_signal(next_state.get(), get_remote_app());
-
if (_sg_mc_termination)
this->check_non_termination(next_state.get());
/* We may backtrack from somewhere either because it's leaf, or because every enabled process are in done/sleep set.
* In the first case, we need to remove the last transition corresponding to the Finalize */
if (stack_.back()->get_transition()->aid_ == 0)
- stack_.pop_back();
-
+ stack_.pop_back();
+
/* 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. For each deleted state, check if the request that has generated it (from its
- * predecessor state) depends on any other previous request executed before it on another process. If there exists one,
- * find the more recent, and add its process to the interleave set. If the process is not enabled at this point,
+ * predecessor state) depends on any other previous request executed before it on another process. If there exists
+ * one, find the more recent, and add its process to the interleave set. If the process is not enabled at this point,
* then add every enabled process to the interleave */
bool found_backtracking_point = false;
while (not stack_.empty() && not found_backtracking_point) {
} else {
XBT_DEBUG("Back-tracking to state %ld at depth %zu: %lu transitions left to be explored", state->get_num(),
stack_.size() + 1, state->count_todo());
- stack_.push_back(std::move(state)); // Put it back on the stack so we can explore the next transition of the interleave
+ stack_.push_back(
+ std::move(state)); // Put it back on the stack so we can explore the next transition of the interleave
found_backtracking_point = true;
}
}
