From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Tue, 7 Feb 2023 14:04:09 +0000 (+0100)
Subject: Add implementation for state management
X-Git-Tag: v3.34~462^2~24
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/a9b5abc37884552bc82a9f3689e003ea8109779b?ds=sidebyside

Add implementation for state management
---

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 89057856ab..e11a6d597f 100644
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -28,10 +28,12 @@ void UdporChecker::run()
   Configuration C;
   EventSet prev_exC;
 
-  const auto initial_state    = get_current_state();
+  auto initial_state          = get_current_state();
   const auto initial_state_id = state_manager_.record_state(std::move(initial_state));
   const auto root_event       = std::make_unique<UnfoldingEvent>(-1, "", EventSet(), initial_state_id);
   explore(std::move(C), std::move(A), std::move(D), {EventSet()}, root_event.get(), std::move(prev_exC));
+
+  XBT_INFO("UDPOR exploration terminated -- model checking completed");
 }
 
 void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::list<EventSet> max_evt_history,
@@ -154,7 +156,7 @@ void UdporChecker::observe_unfolding_event(const UnfoldingEvent& event)
 
 StateHandle UdporChecker::record_newly_visited_state()
 {
-  const auto next_state    = this->get_current_state();
+  auto next_state          = this->get_current_state();
   const auto next_state_id = this->state_manager_.record_state(std::move(next_state));
 
   // In UDPOR, we care about all enabled transitions in a given state
@@ -164,7 +166,15 @@ StateHandle UdporChecker::record_newly_visited_state()
 
 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
 {
-  // TODO: Actually select an event here
+  if (!enC.empty()) {
+    return *(enC.begin());
+  }
+
+  for (const auto& event : A) {
+    if (enC.contains(event)) {
+      return event;
+    }
+  }
   return nullptr;
 }
 
diff --git a/src/mc/udpor_global.cpp b/src/mc/udpor_global.cpp
index ebbce0997d..71fca6cfb4 100644
--- a/src/mc/udpor_global.cpp
+++ b/src/mc/udpor_global.cpp
@@ -97,7 +97,7 @@ void Configuration::add_event(UnfoldingEvent* e)
 {
   this->events_.insert(e);
 
-  // Re-compute the maxmimal events
+  // TODO: Re-compute the maxmimal events
 }
 
 UnfoldingEvent::UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& causes,
@@ -106,31 +106,28 @@ UnfoldingEvent::UnfoldingEvent(unsigned int nb_events, std::string const& trans_
   // TODO: Implement this
 }
 
-StateManager::Handle StateManager::record_state(const std::unique_ptr<State>&& state)
+StateManager::Handle StateManager::record_state(std::unique_ptr<State> state)
 {
-  // // TODO: Throw an error perhaps if the state is nullptr?
+  if (state.get() == nullptr) {
+    throw std::invalid_argument("Expected a newly-allocated State but got NULL instead");
+  }
 
-  // // std::map<int, std::unique_ptr<int>> a;
-  // // auto test = std::make_unique<int>(10);
-  // // std::move(state);
-  // // // const auto&& ab = std::move(test);
-  // // a.insert({1, test});
+  const auto integer_handle = this->current_handle_;
+  this->state_map_.insert({integer_handle, std::move(state)});
 
-  // const auto&& state2 = std::move(state);
-
-  // const auto integer_handle = this->current_handle_;
-  // this->state_map_.insert(std::make_pair(std::move(integer_handle), state2));
-
-  // // Increment the current handle
-  // // TODO: Check for state handle overflow!
-  // this->current_handle_++;
-  return 0;
+  // TODO: Check for state handle overflow!
+  this->current_handle_++;
+  return integer_handle;
 }
 
 std::optional<std::reference_wrapper<State>> StateManager::get_state(StateManager::Handle handle)
 {
-  // TODO: Return the actual state based on the handle provided
-  return std::nullopt;
+  auto state = this->state_map_.find(handle);
+  if (state == this->state_map_.end()) {
+    return std::nullopt;
+  }
+  auto& state_ref = *state->second.get();
+  return std::optional<std::reference_wrapper<State>>{state_ref};
 }
 
 } // namespace simgrid::mc::udpor
diff --git a/src/mc/udpor_global.hpp b/src/mc/udpor_global.hpp
index 54d73758e3..2abc1e717d 100644
--- a/src/mc/udpor_global.hpp
+++ b/src/mc/udpor_global.hpp
@@ -33,8 +33,9 @@ public:
   EventSet& operator=(const EventSet&) = default;
   EventSet& operator=(EventSet&&)      = default;
   EventSet(EventSet&&)                 = default;
-  // EventSet(const Configuration&);
-  // EventSet(Configuration&&);
+
+  inline auto begin() const { return this->events_.begin(); }
+  inline auto end() const { return this->events_.end(); }
 
   void remove(UnfoldingEvent* e);
   void subtract(const EventSet& other);
@@ -155,10 +156,10 @@ private:
   using Handle = StateHandle;
 
   Handle current_handle_ = 0ul;
-  std::map<Handle, std::unique_ptr<State>> state_map_;
+  std::unordered_map<Handle, std::unique_ptr<State>> state_map_;
 
 public:
-  Handle record_state(const std::unique_ptr<State>&&);
+  Handle record_state(std::unique_ptr<State>);
   std::optional<std::reference_wrapper<State>> get_state(Handle);
 };