Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Lazily compute the recipe of a state, on need only
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Thu, 27 Apr 2023 13:41:03 +0000 (15:41 +0200)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Thu, 27 Apr 2023 13:49:14 +0000 (15:49 +0200)
This will be useful when leveraging intermediate states during
backtracks. In that case, we need to compute partial recipes, up to
the advanced restaure point.

src/mc/api/State.cpp
src/mc/api/State.hpp

index a5fdc64..0366a31 100644 (file)
@@ -27,8 +27,6 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_)
   else
     THROW_IMPOSSIBLE;
 
-  recipe_ = std::list<Transition*>();
-
   remote_app.get_actors_status(strategy_->actors_to_run_);
 
 #if SIMGRID_HAVE_STATEFUL_MC
@@ -50,9 +48,6 @@ State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
     THROW_IMPOSSIBLE;
   *strategy_ = *(parent_state->strategy_);
 
-  recipe_ = std::list(parent_state_->get_recipe());
-  recipe_.push_back(incoming_transition_.get());
-
   remote_app.get_actors_status(strategy_->actors_to_run_);
 
 #if SIMGRID_HAVE_STATEFUL_MC /* Stateful model checking */
@@ -96,6 +91,16 @@ std::size_t State::count_todo_multiples() const
   return count;
 }
 
+std::deque<Transition*>& State::get_recipe()
+{
+  if (recipe_.empty()) {
+    for (auto* s = this; s != nullptr; s = s->get_parent_state().get())
+      if (s->get_transition_in() != nullptr)
+        recipe_.push_front(s->get_transition_in().get());
+  }
+  return recipe_;
+}
+
 aid_t State::next_transition() const
 {
   XBT_DEBUG("Search for an actor to run. %zu actors to consider", strategy_->actors_to_run_.size());
index 3551843..95526e9 100644 (file)
@@ -28,7 +28,7 @@ class XBT_PRIVATE State : public xbt::Extendable<State> {
   std::shared_ptr<Transition> incoming_transition_ = nullptr;
 
   /** @brief A list of transition to be replayed in order to get in this state. */
-  std::list<Transition*> recipe_;
+  std::deque<Transition*> recipe_{};
 
   /** Sequential state ID (used for debugging) */
   long num_ = 0;
@@ -77,8 +77,9 @@ public:
 
   bool is_actor_done(aid_t actor) const { return strategy_->actors_to_run_.at(actor).is_done(); }
   std::shared_ptr<Transition> get_transition_out() const { return outgoing_transition_; }
+  std::shared_ptr<Transition> get_transition_in() const { return incoming_transition_; }
   std::shared_ptr<State> get_parent_state() const { return parent_state_; }
-  std::list<Transition*> get_recipe() const { return recipe_; }
+  std::deque<Transition*>& get_recipe();
 
   std::map<aid_t, ActorState> const& get_actors_list() const { return strategy_->actors_to_run_; }