#define SIMGRID_MC_UDPOR_CHECKER_HPP
#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/EventSet.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/mc_record.hpp"
-#include "src/mc/udpor_global.hpp"
+#include <functional>
#include <optional>
namespace simgrid::mc::udpor {
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
- */
- 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
*/
EventSet G;
+ /// @brief UDPOR's current "view" of the program it is exploring
+ Unfolding unfolding = Unfolding();
+
/**
- * Maintains the mapping between handles referenced by events in
- * the current state of the unfolding
+ * @brief A collection of specialized functions which can incrementally
+ * compute the extension of a configuration based on the action taken
*/
- StateManager state_manager_;
+ using ExtensionFunction = std::function<EventSet(const Configuration&, const std::shared_ptr<Transition>)>;
+ 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"
*
* 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 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* cur_event,
- EventSet prev_exC);
+ void explore(const 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
+ */
+ const 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 cur_event the event where UDPOR currently "rests", viz. the event UDPOR
- * is now currently considering
+ * @param stateC the state of the program after having executed C (viz. `state(C)`)
* @param prev_exC the previous value of `ex(C)`, viz. that which was computed for
- * the configuration `C' := C - {cur_event}`
- * @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively
+ * the configuration `C' := C - {e}`
+ * @returns the extension set `ex(C)` of `C`
*/
- 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;
+ EventSet compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC);
+
+ /**
+ * @brief Computes a portion of the extension set of a configuration given
+ * some action `action`
+ */
+ EventSet compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action);
+
+ EventSet compute_enC(const Configuration& C, const EventSet& exC) const;
/**
*
*/
- void observe_unfolding_event(const UnfoldingEvent& event);
- State& get_state_referenced_by(const UnfoldingEvent& event);
- StateHandle record_newly_visited_state();
+ EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const;
/**
- * @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
+ */
+ void move_to_stateCe(State& stateC, const UnfoldingEvent& e);
+
+ /**
+ * @brief Creates a new snapshot of the state of the progam undergoing
+ * model checking
*
- * @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
+ * @returns the handle used to uniquely identify this state later in the
+ * exploration of the unfolding. You provide this handle to an event in the
+ * unfolding to regenerate past states
*/
- 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);
/**
*
