// NOTE: `A`, `D`, and `C` are derived from the
// original UDPOR paper [1], while `prev_exC` arises
// from the incremental computation of ex(C) from [3]
- EventSet A, D;
- Configuration C;
- EventSet prev_exC;
+ Configuration C_root;
- 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), std::move(A), std::move(D), {}, root_event.get(), std::move(prev_exC));
+ // TODO: Move computing the root configuration into a method on the Unfolding
+ auto initial_state = get_current_state();
+ auto root_event = std::make_unique<UnfoldingEvent>(std::make_shared<Transition>(), EventSet());
+ auto* root_event_handle = root_event.get();
+ 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());
XBT_INFO("UDPOR exploration terminated -- model checking completed");
}
-void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::list<EventSet> max_evt_history,
- UnfoldingEvent* e_cur, EventSet prev_exC)
+void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC)
{
// Perform the incremental computation of exC
- auto [exC, enC] = compute_extension(C, max_evt_history, e_cur, prev_exC);
+ //
+ // TODO: This method will have side effects on
+ // the unfolding, but the naming of the method
+ // suggests it is doesn't have side effects. We should
+ // reconcile this in the future
+ auto [exC, enC] = compute_extension(C, 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(*e_cur);
-
UnfoldingEvent* e = select_next_unfolding_event(A, enC);
xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
"UDPOR guarantees that an event will be chosen at each point in\n"
"the search, yet no events were actually chosen\n"
"*********************************\n\n");
- e->set_state_id(next_state_id);
+
+ // Move the application into stateCe and actually make note of that state
+ move_to_stateCe(*stateC, *e);
+ auto stateCe = record_current_state();
// Ce := C + {e}
Configuration Ce = C;
Ce.add_event(e);
- max_evt_history.push_back(Ce.get_maximal_events());
A.remove(e);
exC.remove(e);
// Explore(C + {e}, D, A \ {e})
- explore(Ce, D, std::move(A), max_evt_history, e, std::move(exC));
+ explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
// D <-- D + {e}
D.insert(e);
auto J = compute_partial_alternative(D, C, K);
if (!J.empty()) {
J.subtract(C.get_events());
- max_evt_history.pop_back();
+
+ // Before searching the "right half", we need to make
+ // sure the program actually reflects the fact
+ // that we are searching again from `stateC` (the recursive
+ // search moved the program into `stateCe`)
+ restore_program_state_to(*stateC);
// Explore(C, D + {e}, J \ C)
- explore(C, D, std::move(J), std::move(max_evt_history), e_cur, std::move(prev_exC));
+ explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC));
}
// D <-- D - {e}
clean_up_explore(e, C, D);
}
-std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C,
- const std::list<EventSet>& max_evt_history,
- UnfoldingEvent* e_cur, const EventSet& prev_exC) const
+std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C, 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;
+ // C = C' + {e_cur}, i.e. C' = C - {e_cur}
+ //
+ // Then
+ //
+ // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} + U{<a, > : H }
+ UnfoldingEvent* e_cur = C.get_latest_event();
+ EventSet exC = prev_exC;
exC.remove(e_cur);
+ // ... fancy computations
+
EventSet enC;
return std::tuple<EventSet, EventSet>(exC, enC);
}
-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****** INVARIANT VIOLATION ******\n"
- "To each UDPOR event corresponds a state, but state %llu does not exist. "
- "Please report this as a bug.\n"
- "*********************************\n\n",
- state_id);
- return wrapped_state.value().get();
-}
-
-StateHandle UdporChecker::observe_unfolding_event(const UnfoldingEvent& event)
+void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
{
- auto& state = this->get_state_referenced_by(event);
- const aid_t next_actor = state.next_transition();
+ const aid_t next_actor = e.get_transition()->aid_;
// TODO: Add the trace if possible for reporting a bug
xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
"state was actually enabled. Please report this as a bug.\n"
"*********************************\n\n");
state.execute_next(next_actor);
- return this->record_current_state();
}
-StateHandle UdporChecker::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
+}
+
+std::unique_ptr<State> UdporChecker::record_current_state()
{
- auto next_state = this->get_current_state();
- const auto next_state_id = this->state_manager_.record_state(std::move(next_state));
+ auto next_state = this->get_current_state();
// In UDPOR, we care about all enabled transitions in a given state
next_state->mark_all_enabled_todo();
- return next_state_id;
+
+ return next_state;
}
UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
std::vector<std::string> UdporChecker::get_textual_trace()
{
+ // TODO: Topologically sort the events of the latest configuration
+ // and iterate through that topological sorting
std::vector<std::string> trace;
return trace;
}
#include "src/mc/explo/udpor/Configuration.hpp"
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/StateManager.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/mc_record.hpp"
*/
StateManager state_manager_;
+ /**
+ * @brief UDPOR's current "view" of the program it is exploring
+ */
+ Unfolding unfolding = Unfolding();
+
private:
/**
* @brief Explores the unfolding of the concurrent system
* @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
- *
+ * @param stateC the state of the program after having executed `C`,
+ * viz. `state(C)` using the notation of [1]
*
* 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* e_cur,
- EventSet prev_exC);
+ void explore(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
+ * that should next be explored as an extension of a configuration with
+ * enabled events `enC`
+ *
+ * @param A The set of events `A` maintained by the UDPOR algorithm to help
+ * determine how events should be selected. See the original paper [1] for more details
+ *
+ * @param enC The set `enC` of enabled events from the extension set `exC` used
+ * by the UDPOR algorithm to select new events to search. See the original
+ * paper [1] for more details
+ */
+ UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
/**
* @brief Computes the sets `ex(C)` and `en(C)` of the given configuration
*
* @param C the configuration based on which the two sets `ex(C)` and `en(C)` are
* computed
- * @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 - {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* e, const EventSet& prev_exC) const;
+ std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const EventSet& prev_exC) const;
/**
*
*/
- StateHandle observe_unfolding_event(const UnfoldingEvent& event);
+ EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const;
/**
- * @brief Resolves the state handle maintained by an event
- * into a concrete reference to a state
+ *
*/
- State& get_state_referenced_by(const UnfoldingEvent& event);
+ void move_to_stateCe(State& stateC, const UnfoldingEvent& e);
/**
* @brief Creates a new snapshot of the state of the progam undergoing
* exploration of the unfolding. You provide this handle to an event in the
* unfolding to regenerate past states
*/
- StateHandle record_current_state();
-
- /**
- * @brief Identifies the next event from the unfolding of the concurrent system
- * that should next be explored as an extension of a configuration with
- * enabled events `enC`
- *
- * @param A The set of events `A` maintained by the UDPOR algorithm to help
- * determine how events should be selected. See the original paper [1] for more details
- *
- * @param enC The set `enC` of enabled events from the extension set `exC` used
- * by the UDPOR algorithm to select new events to search. See the original
- * paper [1] for more details
- */
- UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
+ std::unique_ptr<State> record_current_state();
/**
*
*/
- EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const;
+ void restore_program_state_to(const State& stateC);
/**
*
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include "src/mc/transition/Transition.hpp"
+#include <memory>
#include <string>
namespace simgrid::mc::udpor {
class UnfoldingEvent {
public:
- 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(std::shared_ptr<Transition> transition, EventSet immediate_causes, unsigned long event_id = 0);
+
UnfoldingEvent(const UnfoldingEvent&) = default;
UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
UnfoldingEvent(UnfoldingEvent&&) = default;
bool conflicts_with(const Configuration& config) const;
bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const;
- inline StateHandle get_state_id() const { return state_id; }
- inline void set_state_id(StateHandle sid) { state_id = sid; }
+ Transition* get_transition() const { return this->associated_transition.get(); }
bool operator==(const UnfoldingEvent&) const;
private:
- int id = -1;
+ /**
+ * @brief The transition that UDPOR "attaches" to this
+ * specific event for later use while computing e.g. extension
+ * sets
+ *
+ * The transition points to that of a particular actor
+ * in the state reached by the configuration C (recall
+ * this is denoted `state(C)`) that excludes this event.
+ * In other words, this transition was the "next" event
+ * of the actor that executes it in `state(C)`.
+ */
+ std::shared_ptr<Transition> associated_transition;
/**
* @brief The "immediate" causes of this event.
* so on.
*/
EventSet immediate_causes;
- StateHandle state_id = 0ul;
+
+ unsigned long event_id = 0;
};
} // namespace simgrid::mc::udpor
