Add xbt_assert() for state handle overflow

With the StateManager, the current implementation
vends out integer handles that are referred to by
each UnfoldingEvent to map it to the appropriate
State.

A better API, however, may be to have a each event
manage its own state. We should verify first that
each UnfoldingEvent object corresponds to a unique
State object, but this may be the best option

diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp
index c1e730d..2e22036 100644 (file)
--- a/src/mc/explo/udpor/Configuration.hpp
+++ b/src/mc/explo/udpor/Configuration.hpp
@@ -18,19 +18,23 @@ public:
   Configuration& operator=(Configuration const&) = default;
   Configuration(Configuration&&)                 = default;
 
-  inline auto begin() const { return this->events_.begin(); }
-  inline auto end() const { return this->events_.end(); }
-  inline const EventSet& get_events() const { return this->events_; }
-  inline const EventSet& get_maximal_events() const { return this->max_events_; }
+  auto begin() const { return this->events_.begin(); }
+  auto end() const { return this->events_.end(); }
+  const EventSet& get_events() const { return this->events_; }
+  const EventSet& get_maximal_events() const { return this->max_events_; }
+  UnfoldingEvent* get_latest_event() const { return this->newest_event; }
 
   void add_event(UnfoldingEvent*);
-  UnfoldingEvent* get_latest_event() const;
 
 private:
   /**
    * @brief The most recent event added to the configuration
    */
   UnfoldingEvent* newest_event = nullptr;
+
+  /**
+   * @brief The events which make up this configuration
+   */
   EventSet events_;
 
   /**

diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp
index 66dc8a5..8539e24 100644 (file)
--- a/src/mc/explo/udpor/EventSet.hpp
+++ b/src/mc/explo/udpor/EventSet.hpp
@@ -33,7 +33,7 @@ public:
   void subtract(const Configuration& other);
   EventSet subtracting(UnfoldingEvent* e) const;
   EventSet subtracting(const EventSet& e) const;
-  EventSet subtracting(const Configuration* e) const;
+  EventSet subtracting(const Configuration& e) const;
 
   void insert(UnfoldingEvent* e);
   void form_union(const EventSet&);

diff --git a/src/mc/explo/udpor/StateManager.cpp b/src/mc/explo/udpor/StateManager.cpp
index a2fab12..81792ce 100644 (file)
--- a/src/mc/explo/udpor/StateManager.cpp
+++ b/src/mc/explo/udpor/StateManager.cpp
@@ -4,6 +4,7 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/explo/udpor/StateManager.hpp"
+#include "xbt/asserts.h"
 
 namespace simgrid::mc::udpor {
 
@@ -16,8 +17,11 @@ StateManager::Handle StateManager::record_state(std::unique_ptr<State> state)
   const auto integer_handle = this->current_handle_;
   this->state_map_.insert({integer_handle, std::move(state)});
 
-  // TODO: Check for state handle overflow!
   this->current_handle_++;
+  xbt_assert(integer_handle <= this->current_handle_, "Too many states were vended out during exploration via UDPOR.\n"
+                                                      "It's suprising you didn't run out of memory elsewhere first...\n"
+                                                      "Please report this as a bug along with the very large program");
+
   return integer_handle;
 }
 

diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp
index 779b6fd..fd4d273 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.cpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.cpp
@@ -19,4 +19,10 @@ UnfoldingEvent::UnfoldingEvent(unsigned int nb_events, std::string const& trans_
   // TODO: Implement this
 }
 
+bool UnfoldingEvent::operator==(const UnfoldingEvent&) const
+{
+  // TODO: Implement semantic equality
+  return false;
+}
+
 } // namespace simgrid::mc::udpor

diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp
index ad4e040..5604362 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.hpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.hpp
@@ -32,11 +32,7 @@ public:
   inline StateHandle get_state_id() const { return state_id; }
   inline void set_state_id(StateHandle sid) { state_id = sid; }
 
-  bool operator==(const UnfoldingEvent&) const
-  {
-    // TODO: Implement semantic equality
-    return false;
-  };
+  bool operator==(const UnfoldingEvent&) const;
 
 private:
   int id = -1;