#ifndef SIMGRID_MC_UDPOR_CHECKER_HPP
#define SIMGRID_MC_UDPOR_CHECKER_HPP
+#include "src/mc/api/State.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/explo/udpor/Configuration.hpp"
#include "src/mc/explo/udpor/EventSet.hpp"
void run() override;
RecordTrace get_record_trace() override;
- std::vector<std::string> get_textual_trace() override;
std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
private:
Unfolding unfolding = Unfolding();
+ // The current sequence of states that the checker has
+ // visited in order to reach the current configuration
+ std::list<std::unique_ptr<State>> state_stack;
+
/**
* @brief Explores the unfolding of the concurrent system
* represented by the ModelChecker instance "mcmodel_checker"
* @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 stateSequence the sequence of states entered by the program
- * while UDPOR explored `C`. The program is in `state(C)` (using the notation of [1]),
- * which is the result of executing all actions in the stack
- *
- * TODO: We pass around the reference to the stack which is modified
- * appropriately in each recursive call. An iterative version would not
- * need to pass around the states in this manner: the `std::stack<...>`
- * could be a local variable of the function
*
* TODO: Add the optimization where we can check if e == e_prior
* to prevent repeated work when computing ex(C)
*/
- void explore(const Configuration& C, EventSet D, EventSet A, std::list<std::unique_ptr<State>>& state_stack,
- EventSet prev_exC);
+ void explore(const Configuration& C, EventSet D, EventSet A, 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
*/
- const UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
+ UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
/**
* @brief Computes the sets `ex(C)` and `en(C)` of the given configuration
* @returns the extension set `ex(C)` of `C`
*/
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_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action);
-
EventSet compute_enC(const Configuration& C, const EventSet& exC) const;
/**
*
*/
- void move_to_stateCe(State& stateC, const UnfoldingEvent& e);
+ void move_to_stateCe(State* stateC, UnfoldingEvent* e);
/**
* @brief Creates a new snapshot of the state of the application
* The UDPOR implementation in SimGrid ensures that the stack is updated appropriately,
* but the process must still be regenerated.
*/
- void restore_program_state_with_sequence(const std::list<std::unique_ptr<State>>& state_stack);
+ void restore_program_state_with_current_stack();
/**
* @brief Perform the functionality of the `Remove(e, C, D)` function in [1]
