#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) */
/** Sequential state ID (used for debugging) */
long num_ = 0;
- /** Snapshot of system state (if needed) */
- std::shared_ptr<Snapshot> system_state_;
-
/** Unique parent of this state. Required both for sleep set computation
and for guided model-checking */
std::shared_ptr<State> parent_state_ = nullptr;
/* 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<aid_t, Transition> sleep_set_;
+ std::map<aid_t, std::shared_ptr<Transition>> sleep_set_;
/**
* The wakeup tree with respect to the execution represented
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<Snapshot> state) { system_state_ = std::move(state); }
-
/**
* @brief Computes the backtrack set for this state
- * according to its definition in Simgrid.
+ * 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`
std::unordered_set<aid_t> get_backtrack_set() const;
std::unordered_set<aid_t> get_sleeping_actors() const;
std::unordered_set<aid_t> get_enabled_actors() const;
- std::map<aid_t, Transition> const& get_sleep_set() const { return sleep_set_; }
- void add_sleep_set(std::shared_ptr<Transition> t)
+ std::map<aid_t, std::shared_ptr<Transition>> const& get_sleep_set() const { return sleep_set_; }
+ void add_sleep_set(std::shared_ptr<Transition> t) { sleep_set_.insert_or_assign(t->aid_, std::move(t)); }
+ bool is_actor_sleeping(aid_t actor) const
{
- sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_));
+ return std::find_if(sleep_set_.begin(), sleep_set_.end(), [=](const auto& pair) { return pair.first == actor; }) !=
+ sleep_set_.end();
}
/**
* @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);
+ void remove_subtree_using_current_out_transition();
+ void remove_subtree_at_aid(aid_t proc);
bool has_empty_tree() const { return this->wakeup_tree_.empty(); }
+ std::string string_of_wut() const { return this->wakeup_tree_.string_of_whole_tree(); }
/**
* @brief
*/
- void mark_path_interesting_for_odpor(const odpor::PartialExecution&, const odpor::Execution&);
+ odpor::WakeupTree::InsertionResult insert_into_wakeup_tree(const odpor::PartialExecution&, const odpor::Execution&);
- /** */
- void do_odpor_backtrack_cleanup();
+ /** @brief Prepares the state for re-exploration following
+ * another after having followed ODPOR from this state with
+ * the current out transition
+ *
+ * After ODPOR has completed searching a maximal trace, it
+ * finds the first point in the execution with a nonempty wakeup
+ * tree. This method corresponds to lines 20 and 21 in the ODPOR
+ * pseudocode
+ */
+ void do_odpor_unwind();
/* Returns the total amount of states created so far (for statistics) */
static long get_expanded_states() { return expended_states_; }