// TODO: Move computing the root configuration into a method on the Unfolding
auto initial_state = get_current_state();
- auto root_event = std::make_unique<UnfoldingEvent>(std::make_shared<Transition>(), EventSet());
+ auto root_event = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<Transition>());
auto* root_event_handle = root_event.get();
unfolding.insert(std::move(root_event));
C_root.add_event(root_event_handle);
auto begin() const { return this->events_.begin(); }
auto end() const { return this->events_.end(); }
+
+ bool contains(UnfoldingEvent* e) const { return this->events_.contains(e); }
const EventSet& get_events() const { return this->events_; }
const EventSet& get_maximal_events() const { return this->max_events_; }
UnfoldingEvent* get_latest_event() const { return this->newest_event; }
#include "src/mc/explo/udpor/History.hpp"
#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+
+#include <stack>
namespace simgrid::mc::udpor {
-// TODO: Implement these methods
+History::Iterator& History::Iterator::operator++()
+{
+ if (not frontier.empty()) {
+ // "Pop" the event at the "front"
+ UnfoldingEvent* e = *frontier.begin();
+ frontier.remove(e);
+
+ // If we've seen this event before, skip it
+
+ // If there is a configuration and if the
+ // event is in it, skip it: the event and
+ // all of its immediate causes do not need to
+ // be searched since the configuration contains
+ // them (configuration invariant)
+ if (configuration.has_value() && configuration->get().contains(e)) {
+ return *this;
+ }
+
+ // Mark this event as seen
+ current_history.insert(e);
+
+ // Perform the expansion with all viable expansions
+ EventSet candidates = e->get_immediate_causes();
+ candidates.subtract(current_history);
+
+ frontier.form_union(std::move(candidates));
+ }
+ return *this;
+}
+
+EventSet History::get_all_events() const
+{
+ auto first = this->begin();
+ const auto last = this->end();
+
+ for (; first != last; ++first)
+ ;
+
+ return first.current_history;
+}
+
+bool History::contains(UnfoldingEvent* e) const
+{
+ return std::any_of(this->begin(), this->end(), [=](UnfoldingEvent* e_hist) { return e == e_hist; });
+}
+
+EventSet History::get_event_diff_with(const Configuration& config) const
+{
+ // auto wrapped_config = std::optional<std::reference_wrapper<Configuration>>(config);
+ // auto first = Iterator(events_, wrapped_config);
+ // const auto last = this->end();
+
+ // for (; first != last; ++first)
+ // ;
+
+ // return first.current_history;
+ // TODO: Implement this
+ return EventSet();
+}
} // namespace simgrid::mc::udpor
#ifndef SIMGRID_MC_UDPOR_HISTORY_HPP
#define SIMGRID_MC_UDPOR_HISTORY_HPP
+#include "src/mc/explo/udpor/Configuration.hpp"
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include <functional>
+#include <optional>
+
namespace simgrid::mc::udpor {
/**
*/
EventSet events_;
+ /**
+ * @brief An iterator which traverses the history of a set of events
+ */
+ struct Iterator {
+ private:
+ EventSet frontier;
+ EventSet current_history = EventSet();
+
+ std::optional<std::reference_wrapper<Configuration>> configuration;
+
+ friend History;
+
+ public:
+ Iterator(const EventSet& initial_events, std::optional<std::reference_wrapper<Configuration>> config = std::nullopt)
+ : frontier(initial_events), configuration(config)
+ {
+ }
+
+ Iterator& operator++();
+
+ auto operator->() { return frontier.begin().operator->(); }
+ auto operator*() const { return *frontier.begin(); }
+
+ // If what the iterator sees next is the same, we consider them
+ // to be the same iterator. This way, once the iterator has completed
+ // its search, it will be "equal" to an iterator searching nothing
+ bool operator==(const Iterator& other) { return this->frontier == other.frontier; }
+ bool operator!=(const Iterator& other) { return not(this->operator==(other)); }
+
+ using iterator_category = std::forward_iterator_tag;
+ using difference_type = int; // # of steps between
+ using value_type = UnfoldingEvent*;
+ using pointer = value_type*;
+ using reference = value_type&;
+ };
+
public:
History() = default;
History(const History&) = default;
explicit History(UnfoldingEvent* e) : events_({e}) {}
explicit History(EventSet event_set) : events_(std::move(event_set)) {}
+ auto begin() const { return Iterator(events_); }
+ auto end() const { return Iterator(EventSet()); }
+
/**
* @brief Whether or not the given event is contained in the history
*
namespace simgrid::mc::udpor {
-UnfoldingEvent::UnfoldingEvent(std::shared_ptr<Transition> transition, EventSet immediate_causes,
- unsigned long event_id)
- : associated_transition(std::move(transition)), immediate_causes(std::move(immediate_causes)), event_id(event_id)
+UnfoldingEvent::UnfoldingEvent(EventSet immediate_causes, std::shared_ptr<Transition> transition)
+ : associated_transition(std::move(transition)), immediate_causes(std::move(immediate_causes))
{
}
class UnfoldingEvent {
public:
- UnfoldingEvent(std::shared_ptr<Transition> transition = std::make_unique<Transition>(),
- EventSet immediate_causes = EventSet(), unsigned long event_id = 0);
+ UnfoldingEvent(EventSet immediate_causes = EventSet(),
+ std::shared_ptr<Transition> transition = std::make_unique<Transition>());
UnfoldingEvent(const UnfoldingEvent&) = default;
UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
* so on.
*/
EventSet immediate_causes;
-
- unsigned long event_id = 0;
};
} // namespace simgrid::mc::udpor
