Add methods between EventSet and Configuration

The distinction between a Configuration and an
EventSet is a subtle one. Indeed, a configuration
in UDPOR is merely a set. There may be the opportunity
perhaps even to replace the Configuration class
with a typedef, although this may not be possible or
improve readability.

diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp
index f026200..76469f9 100644 (file)
--- a/src/mc/explo/UdporChecker.hpp
+++ b/src/mc/explo/UdporChecker.hpp
@@ -9,17 +9,51 @@
 
 #include "src/mc/explo/Exploration.hpp"
 #include "src/mc/mc_record.hpp"
+#include "src/mc/udpor_global.hpp"
 
 namespace simgrid::mc {
 
 class XBT_PRIVATE UdporChecker : public Exploration {
 public:
   explicit UdporChecker(const std::vector<char*>& args);
+
   void run() override;
   RecordTrace get_record_trace() override;
   std::vector<std::string> get_textual_trace() override;
-};
 
+private:
+  /**
+   * The total number of events created whilst exploring the unfolding
+   */
+  uint32_t nb_events = 0;
+  uint32_t nb_traces = 0;
+
+  /**
+   * 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
+   */
+  EventSet U;
+  EventSet G;
+
+private:
+  /**
+   * @brief Explores the unfolding of the concurrent system
+   * represented by the model checker instance
+   * "model_checker"
+   *
+   * TODO: Explain what this means here
+   */
+  void explore(Configuration C, std::list<EventSet> maxEvtHistory, EventSet D, EventSet A, UnfoldingEvent* currentEvt,
+               EventSet prev_exC);
+};
 } // namespace simgrid::mc
 
 #endif

diff --git a/src/mc/udpor_global.hpp b/src/mc/udpor_global.hpp
index 154c9ba..050c8ff 100644 (file)
--- a/src/mc/udpor_global.hpp
+++ b/src/mc/udpor_global.hpp
@@ -6,6 +6,8 @@
 #ifndef SIMGRID_MC_UDPOR_GLOBAL_HPP
 #define SIMGRID_MC_UDPOR_GLOBAL_HPP
 
+#include "src/mc/api/State.hpp"
+
 #include <iostream>
 #include <queue>
 #include <set>
@@ -25,20 +27,27 @@ private:
 public:
   EventSet()                           = default;
   EventSet(const EventSet&)            = default;
-  EventSet& operator=(EventSet const&) = default;
+  EventSet& operator=(const EventSet&) = default;
   EventSet(EventSet&&)                 = default;
+  EventSet(const Configuration&);
 
   void remove(UnfoldingEvent* e);
   void subtract(const EventSet& other);
-  EventSet subtracting(const EventSet& e);
-  EventSet subtracting(const UnfoldingEvent* e);
+  void subtract(const Configuration& other);
+  EventSet subtracting(const EventSet& e) const;
+  EventSet subtracting(const UnfoldingEvent* e) const;
+  EventSet subtracting(const Configuration* e) const;
 
   void insert(UnfoldingEvent* e);
   void form_union(const EventSet&);
-  EventSet make_union(const EventSet&) const;
+  void form_union(const Configuration&);
   EventSet make_union(const UnfoldingEvent* e) const;
+  EventSet make_union(const EventSet&) const;
+  EventSet make_union(const Configuration& e) const;
 
+  bool empty() const;
   bool contains(const UnfoldingEvent* e) const;
+  bool is_subset_of(const EventSet& other) const;
 
   // TODO: What is this used for?
   UnfoldingEvent* find(const UnfoldingEvent* e) const;
@@ -86,7 +95,7 @@ public:
   UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
   UnfoldingEvent(UnfoldingEvent&&)                 = default;
 
-  EventSet getHistory() const;
+  EventSet get_history() const;
 
   bool isConflict(UnfoldingEvent* event, UnfoldingEvent* otherEvent) const;
   bool concernSameComm(const UnfoldingEvent* event, const UnfoldingEvent* otherEvent) const;
@@ -115,5 +124,15 @@ private:
   bool transition_is_ISend(const UnfoldingEvent* testedEvt, const UnfoldingEvent* SdRcEvt) const;
   bool check_tr_concern_same_comm(bool& chk1, bool& chk2, UnfoldingEvent* evt1, UnfoldingEvent* evt2) const;
 };
+
+class StateManager {
+private:
+  using Handle = uint64_t;
+  std::map<Handle, std::unique_ptr<State>> state_map_;
+
+public:
+  Handle record_state(std::unique_ptr<State>&&);
+};
+
 } // namespace simgrid::mc
 #endif