]> AND Public Git Repository - simgrid.git/blobdiff - src/mc/explo/UdporChecker.hpp
Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Add first implementation of maximal_subsets_iterator
[simgrid.git] / src / mc / explo / UdporChecker.hpp
index 471d8a255c2bd64f6367f100ca2367e3d4ac7cc1..30407c42178afc644b3bc6046c21c0a4ca61a447 100644 (file)
@@ -42,14 +42,6 @@ public:
   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
@@ -88,7 +80,6 @@ private:
   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"
@@ -110,7 +101,7 @@ private:
    * 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