Raffine reversible race calculation for MutexWait

[simgrid.git] / src / mc / explo / UdporChecker.hpp

diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp
index d7377d1..02f2a8e 100644 (file)
--- a/src/mc/explo/UdporChecker.hpp
+++ b/src/mc/explo/UdporChecker.hpp
@@ -7,6 +7,7 @@
 #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"
@@ -38,7 +39,6 @@ public:
 
   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:
@@ -81,7 +81,7 @@ private:
    * 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
@@ -108,20 +108,12 @@ private:
    * @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