// when reconstructing the Exploration for SDPOR.
for (auto iter = stack_.begin(); iter != stack_.end() - 1 and iter != stack_.end(); ++iter) {
const auto& state = *(iter);
- execution_seq_.push_transition(state->get_transition_out().get());
+ execution_seq_.push_transition(state->get_transition_out());
}
}
XBT_DEBUG("Additionally replaced corresponding SDPOR execution stack");
* The intuition is that some subsequence of `v` may enable `p`, so
* we want to be sure that search "in that direction"
*/
- execution_seq_.push_transition(executed_transition.get());
-
+ const aid_t p = executed_transition->aid_;
+ execution_seq_.push_transition(std::move(executed_transition));
xbt_assert(execution_seq_.get_latest_event_handle().has_value(),
"No events are contained in the SDPOR/OPDPOR execution "
"even though one was just added");
- const aid_t p = executed_transition->aid_;
- const auto next_E_p = execution_seq_.get_latest_event_handle().value();
+ const auto next_E_p = execution_seq_.get_latest_event_handle().value();
for (const auto racing_event_handle : execution_seq_.get_racing_events_of(next_E_p)) {
// To determine if the race is reversible, we have to ensure
// that actor `p` running `next_E_p` (viz. the event such that
} else if (reduction_mode_ == ReductionMode::odpor) {
// In the case of ODPOR, we simply observe the transition that was executed
// until we've reached a maximal trace
- execution_seq_.push_transition(executed_transition.get());
+ execution_seq_.push_transition(std::move(executed_transition));
}
// Before leaving that state, if the transition we just took can be taken multiple times, we
namespace simgrid::mc::odpor {
-void Execution::push_transition(const Transition* t)
+void Execution::push_transition(std::shared_ptr<Transition> t)
{
if (t == nullptr) {
throw std::invalid_argument("Unexpectedly received `nullptr`");
}
ClockVector max_clock_vector;
for (const Event& e : this->contents_) {
- if (e.get_transition()->depends(t)) {
+ if (e.get_transition()->depends(t.get())) {
max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector());
}
}
max_clock_vector[t->aid_] = this->size();
- contents_.push_back(Event({t, max_clock_vector}));
+ contents_.push_back(Event({std::move(t), max_clock_vector}));
}
std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
std::vector<EventHandle> w_handles;
for (const auto& w_i : w) {
// Take one step in the direction of `w`
- E_w.push_transition(w_i.get());
+ E_w.push_transition(w_i);
// If that step happened to be executed by `p`,
// great: we know that `p` is contained in `w`.
return false;
}
-bool Execution::is_independent_with_execution(const PartialExecution& w, const Transition* next_E_p) const
+bool Execution::is_independent_with_execution(const PartialExecution& w, std::shared_ptr<Transition> next_E_p) const
{
// INVARIANT: Here, we assume that for any process `p_i` of `w`,
// the events of this execution followed by the execution of all
// `v := notdep(e, E)` for some execution `E` and event `e` of
// that execution.
auto E_p_w = *this;
- E_p_w.push_transition(next_E_p);
+ E_p_w.push_transition(std::move(next_E_p));
const auto p_handle = E_p_w.get_latest_event_handle().value();
// As we add events to `w`, verify that none
// of them "happen-after" the event associated with
// the step `next_E_p` (viz. p_handle)
for (const auto& w_i : w) {
- E_p_w.push_transition(w_i.get());
+ E_p_w.push_transition(w_i);
const auto w_i_handle = E_p_w.get_latest_event_handle().value();
if (E_p_w.happens_before(p_handle, w_i_handle)) {
return false;
auto E_v = *this;
auto w_now = w;
- for (const auto& next_p_E : v) {
- const aid_t p = next_p_E->aid_;
+ for (const auto& next_E_p : v) {
+ const aid_t p = next_E_p->aid_;
// Is `p in `I_[E](w)`?
if (E_v.is_initial_after_execution(w_now, p)) {
w_now.erase(action_by_p_in_w);
}
// Is `E ⊢ p ◇ w`?
- else if (E_v.is_independent_with_execution(w, next_p_E.get())) {
+ else if (E_v.is_independent_with_execution(w, next_E_p)) {
// INVARIANT: Note that it is impossible for `p` to be
// excluded from the set `I_[E](w)` BUT ALSO be contained in
// `w` itself if `E ⊢ p ◇ w`. We assert this is the case here
}
// Move one step forward in the direction of `v` and repeat
- E_v.push_transition(next_p_E.get());
+ E_v.push_transition(next_p_E);
}
// Construct, finally, v.w' by adding `v` to the front of
* actor `j`
*/
class Event {
- std::pair<const Transition*, ClockVector> contents_;
+ std::pair<std::shared_ptr<Transition>, ClockVector> contents_;
public:
Event() = default;
Event(Event&&) = default;
Event(const Event&) = default;
Event& operator=(const Event&) = default;
- explicit Event(std::pair<const Transition*, ClockVector> pair) : contents_(std::move(pair)) {}
+ explicit Event(std::pair<std::shared_ptr<Transition>, ClockVector> pair) : contents_(std::move(pair)) {}
- const Transition* get_transition() const { return std::get<0>(contents_); }
+ std::shared_ptr<Transition> get_transition() const { return std::get<0>(contents_); }
const ClockVector& get_clock_vector() const { return std::get<1>(contents_); }
};
std::unordered_set<aid_t> enabled_actors) const;
bool is_initial_after_execution(const PartialExecution& w, aid_t p) const;
- bool is_independent_with_execution(const PartialExecution& w, const Transition* next_E_p) const;
+ bool is_independent_with_execution(const PartialExecution& w, std::shared_ptr<Transition> next_E_p) const;
/**
* @brief Determines the event associated with
* notation of [1]) `E.proc(t)` where `proc(t)` is the
* actor which executed transition `t`.
*/
- void push_transition(const Transition*);
+ void push_transition(std::shared_ptr<Transition>);
};
} // namespace simgrid::mc::odpor
