if (enC.is_subset_of(D)) {
if (not C.get_events().empty()) {
-
- // g_var::nb_traces++;
+ // Report information...
}
// When `en(C)` is empty, intuitively this means that there
inline std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
private:
- /**
- * The total number of events created whilst exploring the unfolding
- */
- /* FIXME: private fields are not used
- uint32_t nb_events = 0;
- uint32_t nb_traces = 0;
- */
-
/**
* @brief The "relevant" portions of the unfolding that must be kept around to ensure that
* UDPOR properly searches the state space
std::unordered_map<Transition::Type, ExtensionFunction> incremental_extension_functions =
std::unordered_map<Transition::Type, ExtensionFunction>();
-private:
/**
* @brief Explores the unfolding of the concurrent system
* represented by the ModelChecker instance "mcmodel_checker"
std::stack<UnfoldingEvent*> event_stack;
std::vector<UnfoldingEvent*> topological_ordering;
- EventSet unknown_events = events_, temporarily_marked_events, permanently_marked_events;
+ EventSet unknown_events = events_;
+ EventSet temporarily_marked_events;
+ EventSet permanently_marked_events;
while (not unknown_events.empty()) {
EventSet discovered_events;
UnfoldingEvent e1;
UnfoldingEvent e2{&e1};
UnfoldingEvent e3{&e2};
- UnfoldingEvent e4{&e3}, e5{&e3};
+ UnfoldingEvent e4{&e3};
+ UnfoldingEvent e5{&e3};
SECTION("Creating a configuration without events")
{
UnfoldingEvent e1;
UnfoldingEvent e2{&e1};
UnfoldingEvent e3{&e2};
- UnfoldingEvent e4{&e3}, e6{&e3};
+ UnfoldingEvent e4{&e3};
UnfoldingEvent e5{&e4};
+ UnfoldingEvent e6{&e3};
SECTION("Topological ordering for subsets")
{
// / / /
// [ e12 ]
UnfoldingEvent e1;
- UnfoldingEvent e2{&e1}, e8{&e1};
+ UnfoldingEvent e2{&e1};
+ UnfoldingEvent e8{&e1};
UnfoldingEvent e3{&e2};
UnfoldingEvent e4{&e3};
- UnfoldingEvent e5{&e4}, e6{&e4};
- UnfoldingEvent e7{&e2, &e8}, e11{&e8};
- UnfoldingEvent e10{&e7}, e9{&e6, &e7};
+ UnfoldingEvent e5{&e4};
+ UnfoldingEvent e6{&e4};
+ UnfoldingEvent e7{&e2, &e8};
+ UnfoldingEvent e9{&e6, &e7};
+ UnfoldingEvent e10{&e7};
+ UnfoldingEvent e11{&e8};
UnfoldingEvent e12{&e5, &e9, &e10};
Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8, &e9, &e10, &e11, &e12};
// To test this, we ensure that for the `i`th event
// in `ordered_events`, each event in `ordered_events[0...<i]
// is contained in the history of `ordered_events[i]`.
- const auto ordered_events = C.get_topologically_sorted_events();
-
EventSet events_seen;
- for (size_t i = 0; i < ordered_events.size(); i++) {
- UnfoldingEvent* e = ordered_events[i];
+ const auto ordered_events = C.get_topologically_sorted_events();
+ std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](UnfoldingEvent* e) {
History history(e);
for (auto* e_hist : history) {
// In this demo, we want to make sure that
REQUIRE(events_seen.contains(e_hist));
}
events_seen.insert(e);
- }
+ });
}
SECTION("Test every combination of the maximal configuration (reverse graph)")
// To test this, we ensure that for the `i`th event
// in `ordered_events`, no event in `ordered_events[0...<i]
// is contained in the history of `ordered_events[i]`.
+ EventSet events_seen;
const auto ordered_events = C.get_topologically_sorted_events_of_reverse_graph();
- EventSet events_seen;
- for (size_t i = 0; i < ordered_events.size(); i++) {
- UnfoldingEvent* e = ordered_events[i];
+ std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](UnfoldingEvent* e) {
History history(e);
for (auto* e_hist : history) {
REQUIRE_FALSE(events_seen.contains(e_hist));
}
events_seen.insert(e);
- }
+ });
}
}
\ No newline at end of file
EventSet& operator=(EventSet&&) = default;
EventSet(EventSet&&) = default;
explicit EventSet(Configuration&& config);
- explicit EventSet(std::unordered_set<UnfoldingEvent*>&& raw_events) : events_(std::move(raw_events)) {}
+ explicit EventSet(std::unordered_set<UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
explicit EventSet(std::initializer_list<UnfoldingEvent*> event_list) : events_(std::move(event_list)) {}
auto begin() const { return this->events_.begin(); }
bool operator==(const EventSet& other) const { return this->events_ == other.events_; }
bool operator!=(const EventSet& other) const { return this->events_ != other.events_; }
-public:
/**
* @brief Whether or not this set of events could
* represent a configuration
TEST_CASE("simgrid::mc::udpor::EventSet: Deletions")
{
- UnfoldingEvent e1, e2, e3, e4;
+ UnfoldingEvent e1;
+ UnfoldingEvent e2;
+ UnfoldingEvent e3;
+ UnfoldingEvent e4;
EventSet event_set({&e1, &e2, &e3});
SECTION("Remove an element already present")
TEST_CASE("simgrid::mc::udpor::EventSet: Set Equality")
{
- UnfoldingEvent e1, e2, e3, e4;
+ UnfoldingEvent e1;
+ UnfoldingEvent e2;
+ UnfoldingEvent e3;
+ UnfoldingEvent e4;
EventSet A{&e1, &e2, &e3}, B{&e1, &e2, &e3}, C{&e1, &e2, &e3};
SECTION("Equality implies containment")
// in the structure and test whether those subsets are
// maximal and/or valid configurations
UnfoldingEvent e1;
- UnfoldingEvent e2{&e1}, e5{&e1};
- UnfoldingEvent e3{&e2}, e4{&e2};
+ UnfoldingEvent e2{&e1};
+ UnfoldingEvent e3{&e2};
+ UnfoldingEvent e4{&e2};
+ UnfoldingEvent e5{&e1};
UnfoldingEvent e6{&e5};
SECTION("Valid Configurations")
EventSet History::get_event_diff_with(const Configuration& config) const
{
auto wrapped_config = std::optional<std::reference_wrapper<const Configuration>>{config};
- auto first = Iterator(events_, std::move(wrapped_config));
+ auto first = Iterator(events_, wrapped_config);
const auto last = this->end();
for (; first != last; ++first)
// | \ \ / /
// e3 e4 e5 e7
UnfoldingEvent e1;
- UnfoldingEvent e2{&e1}, e6{&e1};
- UnfoldingEvent e3{&e2}, e4{&e2};
- UnfoldingEvent e5{&e2, &e6}, e7{&e6};
+ UnfoldingEvent e2{&e1};
+ UnfoldingEvent e6{&e1};
+ UnfoldingEvent e3{&e2};
+ UnfoldingEvent e4{&e2};
+ UnfoldingEvent e5{&e2, &e6};
+ UnfoldingEvent e7{&e6};
SECTION("History with no events")
{
