unfolding.insert(std::move(root_event));
C_root.add_event(root_event_handle);
- explore(std::move(C_root), EventSet(), EventSet(), std::move(initial_state), EventSet());
+ explore(C_root, EventSet(), EventSet(), std::move(initial_state), EventSet());
XBT_INFO("UDPOR exploration terminated -- model checking completed");
}
-void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC)
+void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std::unique_ptr<State> stateC,
+ EventSet prev_exC)
{
// Perform the incremental computation of exC
//
// "sleep-set blocked" trace.
if (enC.is_subset_of(D)) {
- if (C.get_events().size() > 0) {
+ if (not C.get_events().empty()) {
// g_var::nb_traces++;
-
- // TODO: Log here correctly
- // XBT_DEBUG("\n Exploring executions: %d : \n", g_var::nb_traces);
- // ...
- // ...
}
// When `en(C)` is empty, intuitively this means that there
// TODO: Determine a value of K to use or don't use it at all
constexpr unsigned K = 10;
- auto J = compute_partial_alternative(D, C, K);
- if (!J.empty()) {
+ if (auto J = compute_partial_alternative(D, C, K); !J.empty()) {
J.subtract(C.get_events());
// Before searching the "right half", we need to make
* TODO: Add the optimization where we can check if e == e_prior
* to prevent repeated work when computing ex(C)
*/
- void explore(Configuration C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC);
+ void explore(const Configuration& C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC);
/**
* @brief Identifies the next event from the unfolding of the concurrent system
{
}
-Configuration::Configuration(EventSet events) : events_(events)
+Configuration::Configuration(const EventSet& events) : events_(events)
{
if (!events_.is_valid_configuration()) {
throw std::invalid_argument("The events do not form a valid configuration");
Configuration& operator=(Configuration const&) = default;
Configuration(Configuration&&) = default;
- Configuration(EventSet events);
- Configuration(std::initializer_list<UnfoldingEvent*> events);
+ explicit Configuration(const EventSet& events);
+ explicit Configuration(std::initializer_list<UnfoldingEvent*> events);
auto begin() const { return this->events_.begin(); }
auto end() const { return this->events_.end(); }
namespace simgrid::mc::udpor {
-EventSet::EventSet(Configuration&& config) : EventSet(std::move(config.get_events())) {}
+EventSet::EventSet(Configuration&& config) : EventSet(config.get_events()) {}
void EventSet::remove(UnfoldingEvent* e)
{
EventSet& operator=(EventSet&&) = default;
EventSet(EventSet&&) = default;
explicit EventSet(Configuration&& config);
- explicit EventSet(std::unordered_set<UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
+ explicit EventSet(std::unordered_set<UnfoldingEvent*>&& raw_events) : events_(std::move(raw_events)) {}
explicit EventSet(std::initializer_list<UnfoldingEvent*> event_list) : events_(std::move(event_list)) {}
auto begin() const { return this->events_.begin(); }
SECTION("List initialization")
{
- UnfoldingEvent e1, e2, e3;
EventSet event_set{&e1, &e2, &e3};
REQUIRE(event_set.size() == 3);
REQUIRE(event_set.contains(&e1));
{
REQUIRE(event_set.contains(&e1));
- // event_set = {e2, e3}
+ // Recall that event_set = {e2, e3}
event_set.remove(&e1);
// Check that
SECTION("Remove a single element more than once")
{
- // event_set = {e2, e3}
+ // Recall that event_set = {e2, e3}
event_set.remove(&e1);
REQUIRE(event_set.size() == 2);
REQUIRE_FALSE(event_set.contains(&e1));
SECTION("Remove more than one element")
{
- // event_set = {e3}
+ // Recall that event_set = {e3}
event_set.remove(&e2);
REQUIRE(event_set.size() == 1);
REQUIRE(event_set.contains(&e3));
REQUIRE_FALSE(event_set.empty());
- // event_set = {}
+ // Recall that event_set = {}
event_set.remove(&e3);
REQUIRE(event_set.size() == 0);
{
REQUIRE_FALSE(event_set.contains(&e4));
- // event_set = {e1, e2, e3}
+ // Recall that event_set = {e1, e2, e3}
event_set.remove(&e4);
REQUIRE(event_set.size() == 3);
REQUIRE(event_set.contains(&e1));
maximal_events.subtract(candidates);
candidates.subtract(current_history);
- frontier.form_union(std::move(candidates));
+ frontier.form_union(candidates);
}
return *this;
}
return first.maximal_events;
}
-bool History::contains(UnfoldingEvent* e) const
+bool History::contains(const UnfoldingEvent* e) const
{
- return std::any_of(this->begin(), this->end(), [=](UnfoldingEvent* e_hist) { return e == e_hist; });
+ return std::any_of(this->begin(), this->end(), [=](const UnfoldingEvent* e_hist) { return e == e_hist; });
}
EventSet History::get_event_diff_with(const Configuration& config) const
* @param e the event to check
* @returns whether or not `e` is contained in the collection
*/
- bool contains(UnfoldingEvent* e) const;
+ bool contains(const UnfoldingEvent* e) const;
/**
* @brief Computes all events in the history described by this instance
struct Iterator {
public:
Iterator& operator++();
- auto operator->() { return frontier.begin().operator->(); }
+ auto operator->() const { 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)); }
+ bool operator==(const Iterator& other) const { return this->frontier == other.frontier; }
+ bool operator!=(const Iterator& other) const { return not(this->operator==(other)); }
using iterator_category = std::forward_iterator_tag;
using difference_type = int; // # of steps between
class UnfoldingEvent {
public:
- UnfoldingEvent(std::initializer_list<UnfoldingEvent*> init_list);
+ explicit UnfoldingEvent(std::initializer_list<UnfoldingEvent*> init_list);
UnfoldingEvent(EventSet immediate_causes = EventSet(),
std::shared_ptr<Transition> transition = std::make_unique<Transition>());
bool operator==(const UnfoldingEvent&) const;
-private:
/**
* @brief The transition that UDPOR "attaches" to this
* specific event for later use while computing e.g. extension
