namespace simgrid::mc::odpor {
+void Execution::push_transition(const 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)) {
+ max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector());
+ }
+ }
+ // The entry in the vector for `t->aid_` is the size
+ // of the new stack, which will have a size one greater
+ // than that before we insert the new events
+ max_clock_vector[t->aid_] = this->size() + 1;
+ contents_.push_back(Event({t, max_clock_vector}));
+}
+
+void Execution::pop_latest()
+{
+ contents_.pop_back();
+}
+
std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
{
std::unordered_set<Execution::EventHandle> racing_events;
return racing_events;
}
+Execution Execution::get_prefix_up_to(Execution::EventHandle handle) const
+{
+ return Execution(std::vector<Event>{contents_.begin(), contents_.begin() + handle});
+}
+
+std::optional<aid_t> Execution::get_first_ssdpor_initial_from(EventHandle e,
+ std::unordered_set<aid_t> disqualified_actors) const
+{
+ // If this execution is empty, there are no initials
+ // relative to the last transition added to the execution
+ // since such a transition does not exist
+ if (empty()) {
+ return std::nullopt;
+ }
+
+ // First, grab `E' := pre(e, E)` and determine what actor `p` is
+ // TODO: Instead of copying around these big structs, it
+ // would behoove us to incorporate some way to reference
+ // portions of an execution. For simplicity and for a
+ // "proof of concept" version, we opt to simply copy
+ // the contents instead of making a view into the execution
+ const auto next_E_p = get_latest_event_handle().value();
+ Execution E_prime_v = get_prefix_up_to(e);
+ std::vector<sdpor::Execution::EventHandle> v;
+
+ for (auto e_prime = e; e_prime <= next_E_p; ++e_prime) {
+ // Any event `e*` which occurs after `e` but which does not
+ // happen after `e` is a member of `v`. In addition to marking
+ // the event in `v`, we also "simulate" running the action `v`
+ // from E'
+ if (not happens_before(e, e_prime) or e_prime == next_E_p) {
+ v.push_back(e_prime);
+ E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
+ } else {
+ continue;
+ }
+ const EventHandle e_prime_in_E_prime = E_prime_v.get_latest_event_handle().value();
+ const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime);
+ if (disqualified_actors.count(q) > 0) {
+ continue;
+ }
+ const bool is_initial = std::none_of(
+ v.begin(), v.end(), [&](const auto& e_star) { return E_prime_v.happens_before(e_star, e_prime_in_E_prime); });
+ if (is_initial) {
+ return q;
+ } else {
+ disqualified_actors.insert(q);
+ }
+ }
+ return std::nullopt;
+}
+
+std::unordered_set<aid_t> Execution::get_ssdpor_initials_from(EventHandle e,
+ std::unordered_set<aid_t> disqualified) const
+{
+ return std::unordered_set<aid_t>();
+}
+
bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const
{
// 1. "happens-before" is a subset of "occurs before"
return e1_handle <= e2.get_clock_vector().get(proc_e1).value_or(0);
}
-Execution Execution::get_prefix_up_to(Execution::EventHandle handle)
-{
- if (handle == static_cast<Execution::EventHandle>(0)) {
- return Execution();
- }
- return Execution(std::vector<Event>{contents_.begin(), contents_.begin() + (handle - 1)});
-}
-
-void Execution::push_transition(const 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)) {
- max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector());
- }
- }
- // The entry in the vector for `t->aid_` is the size
- // of the new stack, which will have a size one greater
- // than that before we insert the new events
- max_clock_vector[t->aid_] = this->size() + 1;
- contents_.push_back(Event({t, max_clock_vector}));
-}
-
-void Execution::pop_latest()
-{
- contents_.pop_back();
-}
-
} // namespace simgrid::mc::odpor
\ No newline at end of file
