xbt_assert(wakeup_tree_node->get_sequence().size() == 1, "We claimed that the selected branch "
"contained only a single process, yet more "
"than one process was actually contained in it :(");
- return wakeup_tree_node->get_sequence().front()->aid_;
+ return wakeup_tree_node->get_first_actor();
}
return -1;
}
}
}
+void State::sprout_tree_from_parent_state()
+{
+ xbt_assert(parent_state_ != nullptr, "Attempting to construct a wakeup tree for the root state "
+ "(or what appears to be, rather for state without a parent defined)");
+ const auto p = parent_state_->get_transition_out()->aid_;
+ const auto branch = std::find_if(wakeup_tree_.begin(), wakeup_tree_.end(), [=](const odpor::WakeupTreeNode* node) {
+ return node->is_single_process() && node->get_first_actor() == p;
+ });
+ xbt_assert(branch != wakeup_tree_.end(),
+ "Attempted to create a subtree from the wakeup tree of the parent "
+ "state using actor `%ld`, but no such subtree could be found. "
+ "This implies that the wakeup tree management is broken, "
+ "and more specifically that subtree formation is not working "
+ "as intended; for if this state was generated by the parent "
+ "having taken an action by actor `%ld`, this implies that "
+ "ODPOR found `%ld` as a candidate branch prior",
+ p, p, p);
+ this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(*branch);
+}
+
+void State::remove_subtree_starting_with(aid_t p)
+{
+ const auto branch = std::find_if(wakeup_tree_.begin(), wakeup_tree_.end(), [=](const odpor::WakeupTreeNode* node) {
+ return node->is_single_process() && node->get_first_actor() == p;
+ });
+ xbt_assert(branch != wakeup_tree_.end(), "Attempted to remove a subtree of this state's "
+ "wakeup tree that does not exist");
+ this->wakeup_tree_.remove_subtree_rooted_at(*branch);
+}
+
} // namespace simgrid::mc
*/
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);
+
/* Returns the total amount of states created so far (for statistics) */
static long get_expanded_states() { return expended_states_; }
};
* done after next_state creation */
XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set",
state->get_transition_out()->to_string().c_str(), state->get_transition_out()->aid_);
- state->add_sleep_set(state->get_transition_out()); // Actors are marked done when they are considerd in ActorState
+ state->add_sleep_set(state->get_transition_out()); // Actors are marked done when they are considered in ActorState
+
+ if (reduction_mode_ == ReductionMode::odpor) {
+ // With ODPOR, after taking a step forward, we must:
+ // 1. remove the subtree whose root is a single-process
+ // node of actor `next` (viz. the action we took) from
+ // the wakeup tree of `state`
+ //
+ // 2. assign a copy of that subtree to the next state
+ //
+ // The latter evidently must be done BEFORE the former
+ next_state->sprout_tree_from_parent_state();
+ state->remove_subtree_starting_with(next);
+ }
/* DPOR persistent set procedure:
* for each new transition considered, check if it depends on any other previous transition executed before it
namespace simgrid::mc::odpor {
+aid_t WakeupTreeNode::get_first_actor() const
+{
+ if (seq_.empty()) {
+ throw std::invalid_argument("Attempted to extract the first actor from "
+ "a node in a wakeup tree representing the "
+ "empty execution (likely the root node)");
+ }
+ return get_sequence().front()->aid_;
+}
+
WakeupTree::WakeupTree() : WakeupTree(std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode({}))) {}
WakeupTree::WakeupTree(std::unique_ptr<WakeupTreeNode> root) : root_(root.get())
{
this->insert_node(std::move(root));
}
-WakeupTree WakeupTree::new_subtree_rooted_at(WakeupTreeNode* root)
+WakeupTree WakeupTree::make_subtree_rooted_at(WakeupTreeNode* root)
{
if (not root->is_single_process()) {
throw std::invalid_argument("Selecting subtrees is only defined for single-process nodes");
const std::list<WakeupTreeNode*>& get_ordered_children() const { return children_; }
bool is_leaf() const { return children_.empty(); }
bool is_single_process() const { return seq_.size() == static_cast<size_t>(1); }
+ aid_t get_first_actor() const;
/** Insert a node `node` as a new child of this node */
void add_child(WakeupTreeNode* node) { this->children_.push_back(node); }
class WakeupTree {
private:
- /** @brief The root node of the tree */
- WakeupTreeNode* const root_;
+ WakeupTreeNode* root_;
/**
* @brief All of the nodes that are currently are a part of the tree
auto end() const { return WakeupTreeIterator(); }
void remove_subtree_rooted_at(WakeupTreeNode* root);
- static WakeupTree new_subtree_rooted_at(WakeupTreeNode* root);
+ static WakeupTree make_subtree_rooted_at(WakeupTreeNode* root);
/**
* @brief Whether or not this tree is considered empty
