X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/a40b4e049f124868e55e573d58634bd4a0992d96..f95a31a473eb41bcabca9771fb2a1659f0dfbbd3:/src/mc/api/State.hpp diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index f3fe4b2525..d951ed93e0 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -7,64 +7,158 @@ #define SIMGRID_MC_STATE_HPP #include "src/mc/api/ActorState.hpp" +#include "src/mc/api/ClockVector.hpp" #include "src/mc/api/RemoteApp.hpp" -#include "src/mc/sosp/Snapshot.hpp" +#include "src/mc/api/strategy/Strategy.hpp" +#include "src/mc/explo/odpor/WakeupTree.hpp" #include "src/mc/transition/Transition.hpp" +#if SIMGRID_HAVE_STATEFUL_MC +#include "src/mc/sosp/Snapshot.hpp" +#endif + namespace simgrid::mc { /* A node in the exploration graph (kind-of) */ class XBT_PRIVATE State : public xbt::Extendable { static long expended_states_; /* Count total amount of states, for stats */ - /** - * @brief The outgoing transition: what was the last transition that - * we took to leave this state? - * - * The owner of the transition is the `ActorState` instance which exists in this state, - * or a reference to the internal default transition `Transition()` if no transition has been - * set - */ - Transition* transition_; + /** @brief The outgoing transition is the last transition that we took to leave this state. */ + std::shared_ptr outgoing_transition_ = nullptr; - /** - * @brief An empty transition that leads to this state by default - */ - const std::unique_ptr default_transition; + /** @brief The incoming transition is what led to this state, coming from its parent */ + std::shared_ptr incoming_transition_ = nullptr; /** Sequential state ID (used for debugging) */ long num_ = 0; - /** State's exploration status by actor. Not all the actors are there, only the ones that are ready-to-run in this - * state */ - std::map actors_to_run_; - /** Snapshot of system state (if needed) */ std::shared_ptr system_state_; -public: - explicit State(const RemoteApp& remote_app); + /** Unique parent of this state. Required both for sleep set computation + and for guided model-checking */ + std::shared_ptr parent_state_ = nullptr; + + std::shared_ptr strategy_; + /* Sleep sets are composed of the actor and the corresponding transition that made it being added to the sleep + * set. With this information, it is check whether it should be removed from it or not when exploring a new + * transition */ + std::map sleep_set_; + + /** + * The wakeup tree with respect to the execution represented + * by the totality of all states before and including this one + * and with respect to this state's sleep set + */ + odpor::WakeupTree wakeup_tree_; + bool has_initialized_wakeup_tree = false; + +public: + explicit State(RemoteApp& remote_app); + explicit State(RemoteApp& remote_app, std::shared_ptr parent_state); /* Returns a positive number if there is another transition to pick, or -1 if not */ - aid_t next_transition() const; + aid_t next_transition() const; // this function should disapear as it is redundant with the next one + + /* Same as next_transition(), but choice is now guided, and an integer corresponding to the + internal cost of the transition is returned */ + std::pair next_transition_guided() const; - /* Explore a new path; the parameter must be the result of a previous call to next_transition() */ - void execute_next(aid_t next); + /** + * Same as next_transition(), but the choice is not based off the ODPOR + * wakeup tree associated with this state + */ + aid_t next_odpor_transition() const; + + /** + * @brief Explore a new path on the remote app; the parameter 'next' must be the result of a previous call to + * next_transition() + */ + std::shared_ptr execute_next(aid_t next, RemoteApp& app); long get_num() const { return num_; } std::size_t count_todo() const; - void mark_todo(aid_t actor) { actors_to_run_.at(actor).mark_todo(); } - bool is_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); } - Transition* get_transition() const; - void set_transition(Transition* t) { transition_ = t; } - std::map const& get_actors_list() const { return actors_to_run_; } + std::size_t count_todo_multiples() const; - unsigned long get_actor_count() const { return actors_to_run_.size(); } - bool is_actor_enabled(aid_t actor) { return actors_to_run_.at(actor).is_enabled(); } + /* Marking as TODO some actor in this state: + * + consider_one mark aid actor (and assert it is possible) + * + consider_best ensure one actor is marked by eventually marking the best regarding its guiding method + * + consider_all mark all enabled actor that are not done yet */ + void consider_one(aid_t aid) const { strategy_->consider_one(aid); } + void consider_best() const { strategy_->consider_best(); } + unsigned long consider_all() const { return strategy_->consider_all(); } + + bool is_actor_done(aid_t actor) const { return strategy_->actors_to_run_.at(actor).is_done(); } + std::shared_ptr get_transition_out() const { return outgoing_transition_; } + std::shared_ptr get_transition_in() const { return incoming_transition_; } + std::shared_ptr get_parent_state() const { return parent_state_; } + + std::map const& get_actors_list() const { return strategy_->actors_to_run_; } + + unsigned long get_actor_count() const { return strategy_->actors_to_run_.size(); } + bool is_actor_enabled(aid_t actor) const { return strategy_->actors_to_run_.at(actor).is_enabled(); } Snapshot* get_system_state() const { return system_state_.get(); } void set_system_state(std::shared_ptr state) { system_state_ = std::move(state); } + /** + * @brief Computes the backtrack set for this state + * according to its definition in Simgrid. + * + * The backtrack set as it appears in DPOR, SDPOR, and ODPOR + * in SimGrid consists of those actors marked as `todo` + * (i.e. those that have yet to be explored) as well as those + * marked `done` (i.e. those that have already been explored) + * since the pseudocode in none of the above algorithms explicitly + * removes elements from the backtrack set. DPOR makes use + * explicitly of the `done` set, but we again note that the + * backtrack set still contains processes added to the done set. + */ + std::unordered_set get_backtrack_set() const; + std::unordered_set get_sleeping_actors() const; + std::unordered_set get_enabled_actors() const; + std::map const& get_sleep_set() const { return sleep_set_; } + void add_sleep_set(std::shared_ptr t) + { + sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_)); + } + + /** + * @brief Inserts an arbitrary enabled actor into the wakeup tree + * associated with this state, if such an actor exists and if + * the wakeup tree is already not empty + * + * @param prior The sequence of steps leading up to this state + * with respec to which the tree associated with this state should be + * a wakeup tree (wakeup trees are defined relative to an execution) + * + * @invariant: You should not manipulate a wakeup tree with respect + * to more than one execution; doing so will almost certainly lead to + * unexpected results as wakeup trees are defined relative to a single + * execution + */ + void seed_wakeup_tree_if_needed(const odpor::Execution& prior); + + /** + * @brief Initializes the wakeup_tree_ instance by taking the subtree rooted at the + * single-process node `N` running actor `p := "actor taken by parent to form this state"` + * of the *parent's* wakeup tree + */ + void sprout_tree_from_parent_state(); + + /** + * @brief Removes the subtree rooted at the single-process node + * `N` running actor `p` of this state's wakeup tree + */ + void remove_subtree_starting_with(aid_t p); + + bool has_empty_tree() const { return this->wakeup_tree_.empty(); } + + /** + * @brief + */ + void mark_path_interesting_for_odpor(const odpor::PartialExecution&, const odpor::Execution&); + /* Returns the total amount of states created so far (for statistics) */ static long get_expanded_states() { return expended_states_; } };