/**
* @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`
*/
void remove_subtree_using_current_out_transition();
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_; }