#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/mc_record.hpp"
+#include <functional>
#include <optional>
namespace simgrid::mc::udpor {
* current implementation of `tiny_simgrid`:
*
* 1. "Unfolding-based Partial Order Reduction" by Rodriguez et al.
- * 2. Quasi-Optimal Partial Order Reduction by Nguyen et al.
+ * 2. "Quasi-Optimal Partial Order Reduction" by Nguyen et al.
* 3. The Anh Pham's Thesis "Exploration efficace de l'espace ..."
*/
class XBT_PRIVATE UdporChecker : public Exploration {
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
- *
- * The set `U` is a global variable which is maintained by UDPOR
- * to keep track of "just enough" information about the unfolding
- * to compute *alternatives* (see the paper for more details).
- *
- * @invariant: When a new event is created by UDPOR, it is inserted into
- * this set. All new events that are created by UDPOR have causes that
- * also exist in U and are valid for the duration of the search.
- *
- * If an event is discarded instead of moved from set `U` to set `G`,
- * the event and its contents will be discarded.
- */
- EventSet U;
-
- /**
- * @brief The "irrelevant" portions of the unfolding that do not need to be kept
- * around to ensure that UDPOR functions correctly
- *
- * The set `G` is another global variable maintained by the UDPOR algorithm which
- * is used to keep track of all events which used to be important to UDPOR
- */
- EventSet G;
+ Unfolding unfolding = Unfolding();
/**
- * @brief UDPOR's current "view" of the program it is exploring
+ * @brief A collection of specialized functions which can incrementally
+ * compute the extension of a configuration based on the action taken
*/
- Unfolding unfolding = Unfolding();
+ 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"
* 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::unique_ptr<State> stateC, 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
* 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);
+ 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
* SimGrid is apart, which allow for `ex(C)` to be computed much more efficiently.
* Intuitively, the idea is to take advantage of the fact that you can avoid a lot
* of repeated computation by exploiting the aforementioned properties (in [3]) in
- * what is effectively a dynamic programming optimization. See [3] for more details
+ * what is akin to a dynamic programming optimization. See [3] for more details
*
* @param C the configuration based on which the two sets `ex(C)` and `en(C)` are
* computed
+ * @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 - {e}`
- * @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively
+ * @returns the extension set `ex(C)` of `C`
*/
- std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, 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` by directly enumerating all maximal subsets of C
+ * (i.e. without specializations based on the action)
*/
- EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const;
+ EventSet compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action);
+
+ EventSet compute_enC(const Configuration& C, const EventSet& exC) const;
/**
*
