#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;
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`
* `N` running actor `p` of this state's wakeup tree
*/
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