// relation. Here, then, we would be in a deadlock.
if (enC.empty()) {
get_remote_app().check_deadlock();
+ DIE_IMPOSSIBLE;
}
return;
"the search, yet no events were actually chosen\n"
"*********************************\n\n");
- // Move the application into stateCe and actually make note of that state
+ // Move the application into stateCe and make note of that state
move_to_stateCe(*stateC, *e);
auto stateCe = record_current_state();
void UdporChecker::restore_program_state_to(const State& stateC)
{
- // TODO: Perform state regeneration in the same manner as is done
- // in the DFSChecker.cpp
+ get_remote_app().restore_initial_state();
+ // TODO: We need to have the stack of past states available at this
+ // point. Since the method is recursive, we'll need to keep track of
+ // this as we progress
}
std::unique_ptr<State> UdporChecker::record_current_state()
void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
{
- // TODO: Perform clean up here
+ const EventSet C_union_D = C.get_events().make_union(D);
+ const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
+ const EventSet Q_CDU = C_union_D.make_union(es_immediate_conflicts.get_local_config());
+
+ // Move {e} \ Q_CDU from U to G
+ if (Q_CDU.contains(e)) {
+ this->unfolding.remove(e);
+ }
+
+ // foreach ê in #ⁱ_U(e)
+ for (const auto* e_hat : es_immediate_conflicts) {
+ // Move [ê] \ Q_CDU from U to G
+ const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
+ this->unfolding.remove(to_remove);
+ }
}
RecordTrace UdporChecker::get_record_trace()
return make_union(config.get_events());
}
+EventSet EventSet::get_local_config() const
+{
+ return History(*this).get_all_events();
+}
+
size_t EventSet::size() const
{
return this->events_.size();
EventSet make_union(const UnfoldingEvent*) const;
EventSet make_union(const EventSet&) const;
EventSet make_union(const Configuration&) const;
+ EventSet get_local_config() const;
size_t size() const;
bool empty() const;
namespace simgrid::mc::udpor {
+void Unfolding::remove(const EventSet& events)
+{
+ for (const auto e : events) {
+ remove(e);
+ }
+}
+
void Unfolding::remove(const UnfoldingEvent* e)
{
if (e == nullptr) {
throw std::invalid_argument("Expected a non-null pointer to an event, but received NULL");
}
this->global_events_.erase(e);
+ this->event_handles.remove(e);
}
void Unfolding::insert(std::unique_ptr<UnfoldingEvent> e)
}
// Map the handle to its owner
+ this->event_handles.insert(handle);
this->global_events_[handle] = std::move(e);
}
{
// Notice the use of `==` equality here. `e` may not be contained in the
// unfolding; but some event which is "equivalent" to it could be.
- for (const auto& [event, _] : global_events_) {
+ for (const auto event : *this) {
if (*event == *e) {
return true;
}
return false;
}
+EventSet Unfolding::get_immediate_conflicts_of(const UnfoldingEvent* e) const
+{
+ EventSet immediate_conflicts;
+
+ for (const auto event : *this) {
+ if (event->immediately_conflicts_with(e)) {
+ immediate_conflicts.insert(e);
+ }
+ }
+
+ return immediate_conflicts;
+}
+
} // namespace simgrid::mc::udpor
#ifndef SIMGRID_MC_UDPOR_UNFOLDING_HPP
#define SIMGRID_MC_UDPOR_UNFOLDING_HPP
+#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
*/
std::unordered_map<const UnfoldingEvent*, std::unique_ptr<UnfoldingEvent>> global_events_;
+ /**
+ * @brief: The collection of events in the unfolding
+ *
+ * @invariant: All of the events in this set are elements of `global_events_`
+ * and is kept updated at the same time as `global_events_`
+ */
+ EventSet event_handles;
+
public:
Unfolding() = default;
Unfolding& operator=(Unfolding&&) = default;
Unfolding(Unfolding&&) = default;
void remove(const UnfoldingEvent* e);
+ void remove(const EventSet& events);
void insert(std::unique_ptr<UnfoldingEvent> e);
bool contains_event_equivalent_to(const UnfoldingEvent* e) const;
+ auto begin() const { return this->event_handles.begin(); }
+ auto end() const { return this->event_handles.begin(); }
+ auto cbegin() const { return this->event_handles.cbegin(); }
+ auto cend() const { return this->event_handles.cend(); }
size_t size() const { return this->global_events_.size(); }
bool empty() const { return this->global_events_.empty(); }
+
+ /// @brief Computes "#ⁱ_U(e)" for the given event
+ EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const;
};
} // namespace simgrid::mc::udpor
bool UnfoldingEvent::immediately_conflicts_with(const UnfoldingEvent* other) const
{
+ // Computes "this #ⁱ other"
// They have to be in conflict at a minimum
if (not conflicts_with(other)) {
return false;
