}
void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::list<EventSet> max_evt_history,
- UnfoldingEvent* cur_evt, EventSet prev_exC)
+ UnfoldingEvent* e_cur, EventSet prev_exC)
{
// Perform the incremental computation of exC
- auto [exC, enC] = compute_extension(C, max_evt_history, cur_evt, prev_exC);
+ auto [exC, enC] = compute_extension(C, max_evt_history, e_cur, prev_exC);
// If enC is a subset of D, intuitively
// there aren't any enabled transitions
// TODO: Add verbose logging about which event is being explored
- const auto next_state_id = observe_unfolding_event(*cur_evt);
+ const auto next_state_id = observe_unfolding_event(*e_cur);
UnfoldingEvent* e = select_next_unfolding_event(A, enC);
xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
"*********************************\n\n");
e->set_state_id(next_state_id);
- // Ce = C + {e}
+ // Ce := C + {e}
Configuration Ce = C;
Ce.add_event(e);
- max_evt_history.push_back(Ce.get_maxmimal_events());
+ max_evt_history.push_back(Ce.get_maximal_events());
A.remove(e);
exC.remove(e);
max_evt_history.pop_back();
// Explore(C, D + {e}, J \ C)
- explore(C, D, std::move(J), std::move(max_evt_history), cur_evt, std::move(prev_exC));
+ explore(C, D, std::move(J), std::move(max_evt_history), e_cur, std::move(prev_exC));
}
// D <-- D - {e}
std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C,
const std::list<EventSet>& max_evt_history,
- UnfoldingEvent* cur_event,
- const EventSet& prev_exC) const
+ UnfoldingEvent* e_cur, const EventSet& prev_exC) const
{
+ // See eqs. 5.7 of section 5.2 of [3]
+ // ex(C + {e_cur}) = ex(C) / {e_cur} + U{<a, > : H }
EventSet exC = prev_exC;
-
- exC.remove(cur_event);
+ exC.remove(e_cur);
EventSet enC;
return std::tuple<EventSet, EventSet>(exC, enC);
*
* This function performs the actual search following the
* UDPOR algorithm according to [1].
+ *
+ * @param C the current configuration from which UDPOR will be used
+ * to explore expansions of the concurrent system being modeled
+ * @param D the set of events that should not be considered by UDPOR
+ * while performing its searches, in order to avoid sleep-set blocked
+ * executions. See [1] for more details
+ * @param A the set of events to "guide" UDPOR in the correct direction
+ * when it returns back to a node in the unfolding and must decide among
+ * events to select from `ex(C)`. See [1] for more details
+ * @param max_evt_history
+ *
+ * @param e the event where UDPOR currently "rests", viz. the event UDPOR
+ * is now currently considering. This event is contained in the set `C`
+ * and is the last event that was added to C
+ *
+ *
+ * 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::list<EventSet> max_evt_history, UnfoldingEvent* cur_event,
+ void explore(Configuration C, EventSet D, EventSet A, std::list<EventSet> max_evt_history, UnfoldingEvent* e_cur,
EventSet prev_exC);
/**
*
* @param C the configuration based on which the two sets `ex(C)` and `en(C)` are
* computed
- * @param cur_event the event where UDPOR currently "rests", viz. the event UDPOR
+ * @param e the event where UDPOR currently "rests", viz. the event UDPOR
* is now currently considering
* @param prev_exC the previous value of `ex(C)`, viz. that which was computed for
- * the configuration `C' := C - {cur_event}`
+ * the configuration `C' := C - {e}`
* @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively
*/
std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const std::list<EventSet>& max_evt_history,
- UnfoldingEvent* cur_event, const EventSet& prev_exC) const;
+ UnfoldingEvent* e, const EventSet& prev_exC) const;
/**
*
void Configuration::add_event(UnfoldingEvent* e)
{
this->events_.insert(e);
+ this->newest_event = e;
// TODO: Re-compute the maxmimal events
}
-UnfoldingEvent::UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& causes,
+UnfoldingEvent::UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes)
+ : UnfoldingEvent(nb_events, trans_tag, immediate_causes, 0)
+{
+ // TODO: Implement this correctly
+}
+
+UnfoldingEvent::UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes,
StateHandle sid)
{
// TODO: Implement this
bool empty() 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
- // bool depends(const EventSet& other) 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 maxEvent; // Events recently added to events_
- // EventSet actorMaxEvent; // maximal events of the actors in current configuration
- // UnfoldingEvent* lastEvent; // The last added event
-
inline auto begin() const { return this->events_.begin(); }
inline auto end() const { return this->events_.end(); }
inline const EventSet& get_events() const { return this->events_; }
- inline const EventSet& get_maxmimal_events() const { return this->max_events_; }
+ inline const EventSet& get_maximal_events() const { return this->max_events_; }
void add_event(UnfoldingEvent*);
+ UnfoldingEvent* get_latest_event() 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 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:
+ /**
+ * @brief The most recent event added to the configuration
+ */
+ UnfoldingEvent* newest_event = nullptr;
EventSet events_;
/**
*
* @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
+ * 1. a <-maxmimal event of the configuration, in the sense that
+ * there is no event in the configuration that is "greater" than it.
+ * In UDPOR terminology, each event does not "cause" another event
+ *
+ * 2. contained in the set of events `events_` which comprise
+ * the configuration
*/
EventSet max_events_;
class UnfoldingEvent {
public:
- UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& causes, StateHandle sid);
+ UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes,
+ StateHandle sid);
+ UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes);
UnfoldingEvent(const UnfoldingEvent&) = default;
UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
UnfoldingEvent(UnfoldingEvent&&) = default;
EventSet get_history() const;
bool in_history(const UnfoldingEvent* otherEvent) const;
- // bool concernSameComm(const UnfoldingEvent* event, const UnfoldingEvent* otherEvent) const;
-
bool conflicts_with(const UnfoldingEvent* otherEvent) const;
bool conflicts_with(const Configuration& config) const;
bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const;
bool operator==(const UnfoldingEvent&) const { return false; };
- void print() const;
-
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; }
-
private:
- EventSet causes; // used to store directed ancestors of event e
int id = -1;
- 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;
+
+ /**
+ * @brief The "immediate" causes of this event.
+ *
+ * An event `e` is an immediate cause of an event `e'` if
+ *
+ * 1. e < e'
+ * 2. There is no event `e''` in E such that
+ * `e < e''` and `e'' < e'`
+ *
+ * Intuitively, an immediate cause "happened right before"
+ * this event was executed. It is sufficient to store
+ * only the immediate causes of any event `e`, as any indirect
+ * causes of that event would either be an indirect cause
+ * or an immediate cause of the immediate causes of `e`, and
+ * so on.
+ */
+ EventSet immediate_causes;
+ StateHandle state_id = 0ul;
};
class StateManager {
private:
using Handle = StateHandle;
- Handle current_handle_ = 0ul;
+ Handle current_handle_ = 1ul;
std::unordered_map<Handle, std::unique_ptr<State>> state_map_;
public:
