#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/mc_record.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
- */
- /* FIXME: private fields are not used
- 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();
+
+ using ExtensionFunction = std::function<EventSet(const Configuration&, const Transition&)>;
+
/**
- * @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();
+ 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
*
* @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
*/
- std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const EventSet& prev_exC) const;
+ std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const State& stateC,
+ const EventSet& prev_exC) const;
+
+ EventSet compute_extension_by_enumeration(const Configuration& C, const Transition& action) const;
/**
*