return boost::range::count_if(this->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); });
}
+void State::mark_all_enabled_todo()
+{
+ for (auto const& [aid, _] : this->get_actors_list()) {
+ if (this->is_actor_enabled(aid)) {
+ this->mark_todo(aid);
+ }
+ }
+}
+
Transition* State::get_transition() const
{
return transition_;
long get_num() const { return num_; }
std::size_t count_todo() const;
void mark_todo(aid_t actor) { actors_to_run_.at(actor).mark_todo(); }
+ void mark_all_enabled_todo();
bool is_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); }
Transition* get_transition() const;
void set_transition(Transition* t) { transition_ = t; }
Configuration C;
EventSet prev_exC;
- /**
- * Maintains the mapping between handles referenced by events in
- * the current state of the unfolding
- */
- StateManager state_manager_;
-
- const auto initial_state = std::make_unique<State>(get_remote_app());
+ const auto initial_state = get_current_state();
const auto initial_state_id = state_manager_.record_state(std::move(initial_state));
const auto root_event = std::make_unique<UnfoldingEvent>(-1, "", EventSet(), initial_state_id);
- explore(std::move(C), {EventSet()}, std::move(D), std::move(A), root_event.get(), std::move(prev_exC));
+ explore(std::move(C), std::move(A), std::move(D), {EventSet()}, root_event.get(), std::move(prev_exC));
}
-void UdporChecker::explore(Configuration C, std::list<EventSet> max_evt_history, EventSet D, EventSet A,
+void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::list<EventSet> max_evt_history,
UnfoldingEvent* cur_evt, EventSet prev_exC)
{
// Perform the incremental computation of exC
- auto [exC, enC] = this->extend(C, max_evt_history, *cur_evt, prev_exC);
+ auto [exC, enC] = compute_extension(C, max_evt_history, *cur_evt, prev_exC);
// If enC is a subset of D, intuitively
// there aren't any enabled transitions
// "sleep-set blocked" trace.
if (enC.is_subset_of(D)) {
- // Log traces
- if (C.events_.size() > 0) {
+ if (C.get_events().size() > 0) {
// g_var::nb_traces++;
// When `en(C)` is empty, intuitively this means that there
// are no enabled transitions that can be executed from the
- // state reached by `C` (denoted `state(C)`) (i.e. by some
+ // state reached by `C` (denoted `state(C)`), i.e. by some
// execution of the transitions in C obeying the causality
- // relation). Hence, it is at this point we should check for a deadlock
+ // relation. Here, then, we would be in a deadlock.
if (enC.empty()) {
get_remote_app().check_deadlock();
}
return;
}
- UnfoldingEvent* e = this->select_next_unfolding_event(A, enC);
- if (e == nullptr) {
- XBT_ERROR("\n\n****** CRITICAL ERROR ****** \n"
- "UDPOR guarantees that an event will be chosen here, yet no events were actually chosen...\n"
- "******************");
- DIE_IMPOSSIBLE;
- }
-
// TODO: Add verbose logging about which event is being explored
- // TODO: Execute the transition associated with the event
- // and map the new state
+ observe_unfolding_event(*cur_evt);
+ const auto next_state_id = record_newly_visited_state();
- // const auto cur_state_id = cur_evt->get_state_id();
- // auto curEv_StateId = currentEvt->get_state_id();
- // auto nextState_id = App::app_side_->execute_transition(curEv_StateId, e->get_transition_tag());
- // e->set_state_id(nextState_id);
+ UnfoldingEvent* e = select_next_unfolding_event(A, enC);
+ xbt_assert(e != nullptr, "UDPOR guarantees that an event will be chosen at each point in"
+ "the search, yet no events were actually chosen");
+ e->set_state_id(next_state_id);
- // Configuration is the same + event e
- // C1 = C + {e}
- Configuration C1 = C;
- C1.events_.insert(e);
- C1.updateMaxEvent(e);
+ // TODO: Clean up configuration code before moving into the actual
+ // implementations of everything
- max_evt_history.push_back(C1.maxEvent);
+ // Configuration is the same + event e
+ // Ce = C + {e}
+ Configuration Ce = C;
+ Ce.add_event(e);
- // A <-- A \ {e}, ex(C) <-- ex(C) \ {e}
+ max_evt_history.push_back(Ce.get_maxmimal_events());
A.remove(e);
exC.remove(e);
// Explore(C + {e}, D, A \ {e})
- this->explore(C1, max_evt_history, D, A, e, exC);
+ explore(Ce, D, std::move(A), max_evt_history, e, std::move(exC));
// D <-- D + {e}
D.insert(e);
// TODO: Determine a value of K to use or don't use it at all
constexpr unsigned K = 10;
- auto J = this->compute_partial_alternative(D, C, K);
+ auto J = compute_partial_alternative(D, C, K);
if (!J.empty()) {
- J.subtract(C.events_);
+ J.subtract(C.get_events());
max_evt_history.pop_back();
- explore(C, max_evt_history, D, J, cur_evt, prev_exC);
+
+ // Explore(C, D + {e}, J \ C)
+ explore(C, D, std::move(J), std::move(max_evt_history), cur_evt, std::move(prev_exC));
}
// D <-- D - {e}
D.remove(e);
- this->clean_up_explore(e, C, D);
+
+ // Remove(e, C, D)
+ clean_up_explore(e, C, D);
}
-std::tuple<EventSet, EventSet> UdporChecker::extend(const Configuration& C, const std::list<EventSet>& max_evt_history,
- const UnfoldingEvent& cur_event, const EventSet& prev_exC) const
+std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C,
+ const std::list<EventSet>& max_evt_history,
+ const UnfoldingEvent& cur_event,
+ const EventSet& prev_exC) const
{
// exC.remove(cur_event);
return std::tuple<EventSet, EventSet>();
}
+State& UdporChecker::get_state_referenced_by(const UnfoldingEvent& event)
+{
+ const auto state_id = event.get_state_id();
+ const auto wrapped_state = this->state_manager_.get_state(state_id);
+ xbt_assert(wrapped_state != std::nullopt,
+ "\n\n****** FATAL ERROR ******\n"
+ "To each UDPOR event corresponds a state,"
+ "but state %lu does not exist\n"
+ "******************\n\n",
+ state_id);
+ return wrapped_state.value().get();
+}
+
+void UdporChecker::observe_unfolding_event(const UnfoldingEvent& event)
+{
+ auto& state = this->get_state_referenced_by(event);
+ const aid_t next_actor = state.next_transition();
+ xbt_assert(next_actor >= 0, "\n\n****** FATAL ERROR ******\n"
+ "In reaching this execution path, UDPOR ensures that at least one\n"
+ "one transition of the state of an visited event is enabled, yet no\n"
+ "state was actually enabled");
+ state.execute_next(next_actor);
+}
+
+StateHandle UdporChecker::record_newly_visited_state()
+{
+ const auto next_state = this->get_current_state();
+ const auto next_state_id = this->state_manager_.record_state(std::move(next_state));
+
+ // In UDPOR, we care about all enabled transitions in a given state
+ next_state->mark_all_enabled_todo();
+ return next_state_id;
+}
+
UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
{
// TODO: Actually select an event here
return nullptr;
}
-EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const EventSet& C, const unsigned k) const
+EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
{
// TODO: Compute k-partial alternatives using [2]
return EventSet();
}
-void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const EventSet& C, const EventSet& D)
+void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
{
// TODO: Perform clean up here
}
RecordTrace get_record_trace() override;
std::vector<std::string> get_textual_trace() override;
+ 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
*/
EventSet G;
+ /**
+ * Maintains the mapping between handles referenced by events in
+ * the current state of the unfolding
+ */
+ StateManager state_manager_;
+
private:
/**
* @brief Explores the unfolding of the concurrent system
- * represented by the model checker instance
- * "model_checker"
+ * represented by the ModelChecker instance "mcmodel_checker"
*
- * TODO: Explain what this means here
+ * This function performs the actual search following the
+ * UDPOR algorithm according to [1].
*/
- void explore(Configuration C, std::list<EventSet> max_evt_history, EventSet D, EventSet A, UnfoldingEvent* cur_event,
+ void explore(Configuration C, EventSet D, EventSet A, std::list<EventSet> max_evt_history, UnfoldingEvent* cur_event,
EventSet prev_exC);
/**
* the configuration `C' := C - {cur_event}`
* @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively
*/
- std::tuple<EventSet, EventSet> extend(const Configuration& C, const std::list<EventSet>& max_evt_history,
- const UnfoldingEvent& cur_event, const EventSet& prev_exC) const;
+ std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const std::list<EventSet>& max_evt_history,
+ const UnfoldingEvent& cur_event, const EventSet& prev_exC) const;
+
+ /**
+ *
+ */
+ void observe_unfolding_event(const UnfoldingEvent& event);
+ State& get_state_referenced_by(const UnfoldingEvent& event);
+ StateHandle record_newly_visited_state();
/**
* @brief Identifies the next event from the unfolding of the concurrent system
*/
UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
- EventSet compute_partial_alternative(const EventSet& D, const EventSet& C, const unsigned k) const;
+ /**
+ *
+ */
+ EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const;
/**
*
*/
- void clean_up_explore(const UnfoldingEvent* e, const EventSet& C, const EventSet& D);
+ void clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D);
};
} // namespace simgrid::mc::udpor
#include "udpor_global.hpp"
#include "xbt/log.h"
+
#include <algorithm>
+#include <iterator>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor_global, mc, "udpor_global");
namespace simgrid::mc::udpor {
-// TODO: Implement methods on EventSet as appropriate
+void EventSet::remove(UnfoldingEvent* e)
+{
+ this->events_.erase(e);
+}
+
+void EventSet::subtract(const EventSet& other)
+{
+ this->events_ = std::move(subtracting(other).events_);
+}
+
+// void EventSet::subtract(const Configuration& other);
+
+EventSet EventSet::subtracting(const EventSet& other) const
+{
+ std::set<UnfoldingEvent*> result;
+ std::set_difference(this->events_.begin(), this->events_.end(), other.events_.begin(), other.events_.end(),
+ std::inserter(result, result.end()));
+ return EventSet(std::move(result));
+}
+
+EventSet EventSet::subtracting(UnfoldingEvent* e) const
+{
+ auto result = this->events_;
+ result.erase(e);
+ return EventSet(std::move(result));
+}
+// EventSet EventSet::subtracting(const Configuration* e) const;
+
+void EventSet::insert(UnfoldingEvent* e)
+{
+ // TODO: Potentially react if the event is already inserted
+ this->events_.insert(e);
+}
+
+void EventSet::form_union(const EventSet& other)
+{
+ this->events_ = std::move(make_union(other).events_);
+}
+
+// void EventSet::form_union(const Configuration&);
+EventSet EventSet::make_union(UnfoldingEvent* e) const
+{
+ auto result = this->events_;
+ result.insert(e);
+ return EventSet(std::move(result));
+}
+
+EventSet EventSet::make_union(const EventSet& other) const
+{
+ std::set<UnfoldingEvent*> result;
+ std::set_union(this->events_.begin(), this->events_.end(), other.events_.begin(), other.events_.end(),
+ std::inserter(result, result.end()));
+ return EventSet(std::move(result));
+}
+
+// EventSet EventSet::make_union(const Configuration& e) const;
+
+size_t EventSet::size() const
+{
+ return this->events_.size();
+}
+
+bool EventSet::empty() const
+{
+ return this->events_.empty();
+}
+
+bool EventSet::contains(UnfoldingEvent* e) const
+{
+ return this->events_.find(e) != this->events_.end();
+}
+
+bool EventSet::is_subset_of(const EventSet& other) const
+{
+ // If there is some element not contained in `other`, then
+ // the set difference will contain that element and the
+ // result won't be empty
+ return subtracting(other).empty();
+}
+
+void Configuration::add_event(UnfoldingEvent* e)
+{
+ this->events_.insert(e);
+
+ // Re-compute the maxmimal events
+}
+
+UnfoldingEvent::UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& causes,
+ StateHandle sid)
+{
+ // TODO: Implement this
+}
+
+StateManager::Handle StateManager::record_state(const std::unique_ptr<State>&& state)
+{
+ // // TODO: Throw an error perhaps if the state is nullptr?
+
+ // // std::map<int, std::unique_ptr<int>> a;
+ // // auto test = std::make_unique<int>(10);
+ // // std::move(state);
+ // // // const auto&& ab = std::move(test);
+ // // a.insert({1, test});
+
+ // const auto&& state2 = std::move(state);
+
+ // const auto integer_handle = this->current_handle_;
+ // this->state_map_.insert(std::make_pair(std::move(integer_handle), state2));
+
+ // // Increment the current handle
+ // // TODO: Check for state handle overflow!
+ // this->current_handle_++;
+ return 0;
+}
+
+std::optional<std::reference_wrapper<State>> StateManager::get_state(StateManager::Handle handle)
+{
+ // TODO: Return the actual state based on the handle provided
+ return std::nullopt;
+}
} // namespace simgrid::mc::udpor
#include "src/mc/api/State.hpp"
#include <iostream>
+#include <optional>
#include <queue>
#include <set>
#include <string_view>
class UnfoldingEvent;
class Configuration;
+using StateHandle = uint64_t;
class EventSet {
private:
std::set<UnfoldingEvent*> events_;
+ explicit EventSet(std::set<UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
public:
EventSet() = default;
EventSet(const EventSet&) = default;
EventSet& operator=(const EventSet&) = default;
+ EventSet& operator=(EventSet&&) = default;
EventSet(EventSet&&) = default;
- EventSet(const Configuration&);
+ // EventSet(const Configuration&);
+ // EventSet(Configuration&&);
- void remove(const UnfoldingEvent* e);
+ void remove(UnfoldingEvent* e);
void subtract(const EventSet& other);
void subtract(const Configuration& other);
+ EventSet subtracting(UnfoldingEvent* e) const;
EventSet subtracting(const EventSet& e) const;
- EventSet subtracting(const UnfoldingEvent* e) const;
EventSet subtracting(const Configuration* e) const;
void insert(UnfoldingEvent* e);
void form_union(const EventSet&);
void form_union(const Configuration&);
- EventSet make_union(const UnfoldingEvent* e) const;
+ EventSet make_union(UnfoldingEvent* e) const;
EventSet make_union(const EventSet&) const;
EventSet make_union(const Configuration& e) const;
size_t size() const;
bool empty() const;
- bool contains(const UnfoldingEvent* e) const;
+ bool contains(UnfoldingEvent* e) const;
bool is_subset_of(const EventSet& other) const;
- // TODO: What is this used for?
- UnfoldingEvent* find(const UnfoldingEvent* e) const;
+ // // TODO: What is this used for?
+ // UnfoldingEvent* find(const UnfoldingEvent* e) const;
- // TODO: What is this used for
- bool depends(const EventSet& other) const;
+ // // TODO: What is this used for
+ // bool depends(const EventSet& other) const;
- // TODO: What is this used for
- bool is_empty_intersection(EventSet evtS) const;
+ // // TODO: What is this used for
+ // bool is_empty_intersection(EventSet evtS) const;
};
struct s_evset_in_t {
Configuration& operator=(Configuration const&) = default;
Configuration(Configuration&&) = default;
- EventSet events_;
- EventSet maxEvent; // Events recently added to events_
- EventSet actorMaxEvent; // maximal events of the actors in current configuration
- UnfoldingEvent* lastEvent; // The last added event
+ // EventSet maxEvent; // Events recently added to events_
+ // EventSet actorMaxEvent; // maximal events of the actors in current configuration
+ // UnfoldingEvent* lastEvent; // The last added event
+
+ inline const EventSet& get_events() const { return this->events_; }
+ inline const EventSet& get_maxmimal_events() const { return this->max_events_; }
+
+ void add_event(UnfoldingEvent*);
- Configuration plus_config(UnfoldingEvent*) const;
+ // Configuration plus_config(UnfoldingEvent*) const;
- void createEvts(Configuration C, EventSet& result, const std::string& trans_tag, s_evset_in_t ev_sets, bool chk,
- UnfoldingEvent* immPreEvt);
+ // void createEvts(Configuration C, EventSet& result, const std::string& trans_tag, s_evset_in_t ev_sets, bool chk,
+ // UnfoldingEvent* immPreEvt);
- void updateMaxEvent(UnfoldingEvent*); // update maximal events of the configuration and actors
- UnfoldingEvent* findActorMaxEvt(int actorId); // find maximal event of a Actor whose id = actorId
+ // void updateMaxEvent(UnfoldingEvent*); // update maximal events of the configuration and actors
+ // UnfoldingEvent* findActorMaxEvt(int actorId); // find maximal event of a Actor whose id = actorId
+
+ // UnfoldingEvent* findTestedComm(const UnfoldingEvent* testEvt); // find comm tested by action testTrans
+private:
+ EventSet events_;
- UnfoldingEvent* findTestedComm(const UnfoldingEvent* testEvt); // find comm tested by action testTrans
+ /**
+ * The <-maxmimal events of the configuration. These are
+ * dynamically adjusted as events are added to the configuration
+ *
+ * @invariant: Each event that is part of this set is
+ *
+ * 1. A <-maxmimal event of the configuration, in the sense that
+ * there is no event in the configuration that is "greater" than it
+ */
+ EventSet max_events_;
+
+private:
+ void recompute_maxmimal_events(UnfoldingEvent* new_event);
};
class UnfoldingEvent {
public:
- UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& causes, int sid = -1);
+ UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& causes, StateHandle sid);
UnfoldingEvent(const UnfoldingEvent&) = default;
UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
UnfoldingEvent(UnfoldingEvent&&) = default;
EventSet get_history() const;
+ bool in_history(const UnfoldingEvent* otherEvent) const;
- bool isConflict(UnfoldingEvent* event, UnfoldingEvent* otherEvent) const;
- bool concernSameComm(const UnfoldingEvent* event, const UnfoldingEvent* otherEvent) const;
-
- // check otherEvent is in my history ?
- bool inHistory(UnfoldingEvent* otherEvent) const;
+ // bool concernSameComm(const UnfoldingEvent* event, const UnfoldingEvent* otherEvent) const;
- bool isImmediateConflict1(UnfoldingEvent* evt, UnfoldingEvent* otherEvt) const;
+ bool conflicts_with(const UnfoldingEvent* otherEvent) const;
+ bool conflicts_with(const Configuration& config) const;
+ bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const;
- bool conflictWithConfig(UnfoldingEvent* event, Configuration const& config) const;
bool operator==(const UnfoldingEvent&) const { return false; };
+
void print() const;
- inline int get_state_id() const { return state_id; }
- inline void set_state_id(int sid) { state_id = sid; }
+ inline StateHandle get_state_id() const { return state_id; }
+ inline void set_state_id(StateHandle sid) { state_id = sid; }
- inline std::string get_transition_tag() const { return transition_tag; }
- inline void set_transition_tag(std::string_view tr_tag) { transition_tag = tr_tag; }
+ // inline std::string get_transition_tag() const { return transition_tag; }
+ // inline void set_transition_tag(std::string_view tr_tag) { transition_tag = tr_tag; }
private:
EventSet causes; // used to store directed ancestors of event e
int id = -1;
- int state_id{-1};
- std::string transition_tag{""}; // The tag of the last transition that lead to creating the event
- bool transition_is_IReceive(const UnfoldingEvent* testedEvt, const UnfoldingEvent* SdRcEvt) const;
- bool transition_is_ISend(const UnfoldingEvent* testedEvt, const UnfoldingEvent* SdRcEvt) const;
- bool check_tr_concern_same_comm(bool& chk1, bool& chk2, UnfoldingEvent* evt1, UnfoldingEvent* evt2) const;
+ StateHandle state_id;
+ // std::string transition_tag{""}; // The tag of the last transition that lead to creating the event
+ // bool transition_is_IReceive(const UnfoldingEvent* testedEvt, const UnfoldingEvent* SdRcEvt) const;
+ // bool transition_is_ISend(const UnfoldingEvent* testedEvt, const UnfoldingEvent* SdRcEvt) const;
+ // bool check_tr_concern_same_comm(bool& chk1, bool& chk2, UnfoldingEvent* evt1, UnfoldingEvent* evt2) const;
};
class StateManager {
private:
- using Handle = uint64_t;
+ using Handle = StateHandle;
+
+ Handle current_handle_ = 0ul;
std::map<Handle, std::unique_ptr<State>> state_map_;
public:
Handle record_state(const std::unique_ptr<State>&&);
+ std::optional<std::reference_wrapper<State>> get_state(Handle);
};
} // namespace simgrid::mc::udpor
