1 /* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
6 #include "udpor_global.hpp"
12 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor_global, mc, "udpor_global");
14 namespace simgrid::mc::udpor {
16 void EventSet::remove(UnfoldingEvent* e)
18 this->events_.erase(e);
21 void EventSet::subtract(const EventSet& other)
23 this->events_ = std::move(subtracting(other).events_);
26 // void EventSet::subtract(const Configuration& other);
28 EventSet EventSet::subtracting(const EventSet& other) const
30 std::set<UnfoldingEvent*> result;
31 std::set_difference(this->events_.begin(), this->events_.end(), other.events_.begin(), other.events_.end(),
32 std::inserter(result, result.end()));
33 return EventSet(std::move(result));
36 EventSet EventSet::subtracting(UnfoldingEvent* e) const
38 auto result = this->events_;
40 return EventSet(std::move(result));
42 // EventSet EventSet::subtracting(const Configuration* e) const;
44 void EventSet::insert(UnfoldingEvent* e)
46 // TODO: Potentially react if the event is already inserted
47 this->events_.insert(e);
50 void EventSet::form_union(const EventSet& other)
52 this->events_ = std::move(make_union(other).events_);
55 // void EventSet::form_union(const Configuration&);
56 EventSet EventSet::make_union(UnfoldingEvent* e) const
58 auto result = this->events_;
60 return EventSet(std::move(result));
63 EventSet EventSet::make_union(const EventSet& other) const
65 std::set<UnfoldingEvent*> result;
66 std::set_union(this->events_.begin(), this->events_.end(), other.events_.begin(), other.events_.end(),
67 std::inserter(result, result.end()));
68 return EventSet(std::move(result));
71 // EventSet EventSet::make_union(const Configuration& e) const;
73 size_t EventSet::size() const
75 return this->events_.size();
78 bool EventSet::empty() const
80 return this->events_.empty();
83 bool EventSet::contains(UnfoldingEvent* e) const
85 return this->events_.find(e) != this->events_.end();
88 bool EventSet::is_subset_of(const EventSet& other) const
90 // If there is some element not contained in `other`, then
91 // the set difference will contain that element and the
92 // result won't be empty
93 return subtracting(other).empty();
96 void Configuration::add_event(UnfoldingEvent* e)
98 this->events_.insert(e);
99 this->newest_event = e;
101 // TODO: Re-compute the maxmimal events
104 UnfoldingEvent::UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes)
105 : UnfoldingEvent(nb_events, trans_tag, immediate_causes, 0)
107 // TODO: Implement this correctly
110 UnfoldingEvent::UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes,
113 // TODO: Implement this
116 StateManager::Handle StateManager::record_state(std::unique_ptr<State> state)
118 if (state.get() == nullptr) {
119 throw std::invalid_argument("Expected a newly-allocated State but got NULL instead");
122 const auto integer_handle = this->current_handle_;
123 this->state_map_.insert({integer_handle, std::move(state)});
125 // TODO: Check for state handle overflow!
126 this->current_handle_++;
127 return integer_handle;
130 std::optional<std::reference_wrapper<State>> StateManager::get_state(StateManager::Handle handle)
132 auto state = this->state_map_.find(handle);
133 if (state == this->state_map_.end()) {
136 auto& state_ref = *state->second.get();
137 return std::optional<std::reference_wrapper<State>>{state_ref};
140 } // namespace simgrid::mc::udpor