MC: give each state an incoming transition too

Using the parent's outgoing transition is not reliable anymore now
that we don't always explore the tree in order, but rather following
the exploration strategies.

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index ca0a74d..2abb88f 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -40,7 +40,7 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_)
 }
 
 State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
-    : num_(++expended_states_), parent_state_(parent_state)
+    : incoming_transition_(parent_state->get_transition_out()), num_(++expended_states_), parent_state_(parent_state)
 {
   if (_sg_mc_strategy == "none")
     strategy_ = std::make_shared<BasicStrategy>();
@@ -51,7 +51,7 @@ State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
   *strategy_ = *(parent_state->strategy_);
 
   recipe_ = std::list(parent_state_->get_recipe());
-  recipe_.push_back(parent_state_->get_transition());
+  recipe_.push_back(incoming_transition_);
 
   remote_app.get_actors_status(strategy_->actors_to_run_);
 
@@ -67,7 +67,7 @@ State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
      * And if we kept it and the actor is enabled in this state, mark the actor as already done, so that
      * it is not explored*/
     for (auto& [aid, transition] : parent_state_->get_sleep_set()) {
-      if (not parent_state_->get_transition()->depends(&transition)) {
+      if (not incoming_transition_->depends(&transition)) {
         sleep_set_.try_emplace(aid, transition);
         if (strategy_->actors_to_run_.count(aid) != 0) {
           XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
@@ -75,8 +75,8 @@ State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
           strategy_->actors_to_run_.at(aid).mark_done();
         }
       } else
-        XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with >>%s<<",
-                  transition.to_string().c_str(), parent_state_->get_transition()->to_string().c_str());
+        XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with incoming >>%s<<",
+                  transition.to_string().c_str(), incoming_transition_->to_string().c_str());
     }
   }
 }
@@ -96,11 +96,6 @@ std::size_t State::count_todo_multiples() const
   return count;
 }
 
-Transition* State::get_transition() const
-{
-  return transition_;
-}
-
 aid_t State::next_transition() const
 {
   XBT_DEBUG("Search for an actor to run. %zu actors to consider", strategy_->actors_to_run_.size());

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index 2e63961..1dc026b 100644 (file)
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -28,6 +28,13 @@ class XBT_PRIVATE State : public xbt::Extendable<State> {
    */
   Transition* transition_ = nullptr;
 
+  /**
+   * @brief The incoming transition is what led to this state, coming from its parent
+   *
+   * The owner of the transition is the `ActorState` instance of the parent.
+   */
+  Transition* incoming_transition_ = nullptr;
+
   /** @brief A list of transition to be replayed in order to get in this state. */
   std::list<Transition*> recipe_;
 
@@ -77,8 +84,8 @@ public:
   unsigned long consider_all() const { return strategy_->consider_all(); }
 
   bool is_actor_done(aid_t actor) const { return strategy_->actors_to_run_.at(actor).is_done(); }
-  Transition* get_transition() const;
-  void set_transition(Transition* t) { transition_ = t; }
+  Transition* get_transition_out() const { return transition_; }
+  void set_transition_out(Transition* t) { transition_ = t; }
   std::shared_ptr<State> get_parent_state() const { return parent_state_; }
   std::list<Transition*> get_recipe() const { return recipe_; }
 

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 3a99ca5..4e9c03b 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -71,7 +71,7 @@ RecordTrace DFSExplorer::get_record_trace() // override
   RecordTrace res;
   for (auto const& transition : stack_.back()->get_recipe())
     res.push_back(transition);
-  res.push_back(stack_.back()->get_transition());
+  res.push_back(stack_.back()->get_transition_out());
   return res;
 }
 
@@ -81,7 +81,7 @@ std::vector<std::string> DFSExplorer::get_textual_trace() // override
   for (auto const& transition : stack_.back()->get_recipe()) {
     trace.push_back(xbt::string_printf("%ld: %s", transition->aid_, transition->to_string().c_str()));
   }
-  if (const auto* trans = stack_.back()->get_transition(); trans != nullptr)
+  if (const auto* trans = stack_.back()->get_transition_out(); trans != nullptr)
     trace.push_back(xbt::string_printf("%ld: %s", trans->aid_, trans->to_string().c_str()));
   return trace;
 }
@@ -176,12 +176,12 @@ void DFSExplorer::run()
 
     /* Actually answer the request: let's execute the selected request (MCed does one step) */
     state->execute_next(next, get_remote_app());
-    on_transition_execute_signal(state->get_transition(), get_remote_app());
+    on_transition_execute_signal(state->get_transition_out(), get_remote_app());
 
     // If there are processes to interleave and the maximum depth has not been
     // reached then perform one step of the exploration algorithm.
-    XBT_VERB("Execute %ld: %.60s (stack depth: %zu, state: %ld, %zu interleaves)", state->get_transition()->aid_,
-             state->get_transition()->to_string().c_str(), stack_.size(), state->get_num(), state->count_todo());
+    XBT_VERB("Execute %ld: %.60s (stack depth: %zu, state: %ld, %zu interleaves)", state->get_transition_out()->aid_,
+             state->get_transition_out()->to_string().c_str(), stack_.size(), state->get_num(), state->count_todo());
 
     /* Create the new expanded state (copy the state of MCed into our MCer data) */
     auto next_state = std::make_shared<State>(get_remote_app(), state);
@@ -192,27 +192,27 @@ void DFSExplorer::run()
      * <!> Since the parent sleep set is used to compute the child sleep set, this need to be
      * done after next_state creation */
     XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set",
-              state->get_transition()->to_string().c_str(), state->get_transition()->aid_);
-    state->add_sleep_set(state->get_transition()); // Actors are marked done when they are considerd in ActorState
+              state->get_transition_out()->to_string().c_str(), state->get_transition_out()->aid_);
+    state->add_sleep_set(state->get_transition_out()); // Actors are marked done when they are considerd in ActorState
 
     /* DPOR persistent set procedure:
      * for each new transition considered, check if it depends on any other previous transition executed before it
      * on another process. If there exists one, find the more recent, and add its process to the interleave set.
      * If the process is not enabled at this  point, then add every enabled process to the interleave */
     if (reduction_mode_ == ReductionMode::dpor) {
-      aid_t issuer_id   = state->get_transition()->aid_;
+      aid_t issuer_id   = state->get_transition_out()->aid_;
       stack_t tmp_stack = stack_;
       while (not tmp_stack.empty()) {
         if (const State* prev_state = tmp_stack.back().get();
-            state->get_transition()->aid_ == prev_state->get_transition()->aid_) {
-          XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(),
-                    prev_state->get_transition()->to_string().c_str(), issuer_id);
+            state->get_transition_out()->aid_ == prev_state->get_transition_out()->aid_) {
+          XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition_out()->to_string().c_str(),
+                    prev_state->get_transition_out()->to_string().c_str(), issuer_id);
           tmp_stack.pop_back();
           continue;
-        } else if (prev_state->get_transition()->depends(state->get_transition())) {
+        } else if (prev_state->get_transition_out()->depends(state->get_transition_out())) {
           XBT_VERB("Dependent Transitions:");
-          XBT_VERB("  %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
-          XBT_VERB("  %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
+          XBT_VERB("  %s (state=%ld)", prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
+          XBT_VERB("  %s (state=%ld)", state->get_transition_out()->to_string().c_str(), state->get_num());
 
           if (prev_state->is_actor_enabled(issuer_id)) {
             if (not prev_state->is_actor_done(issuer_id)) {
@@ -231,8 +231,8 @@ void DFSExplorer::run()
           break;
         } else {
           XBT_VERB("INDEPENDENT Transitions:");
-          XBT_VERB("  %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
-          XBT_VERB("  %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
+          XBT_VERB("  %s (state=%ld)", prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
+          XBT_VERB("  %s (state=%ld)", state->get_transition_out()->to_string().c_str(), state->get_num());
         }
         tmp_stack.pop_back();
       }
@@ -264,12 +264,12 @@ void DFSExplorer::run()
       }
 
       dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), stack_.back()->get_num(),
-                 state->get_transition()->dot_string().c_str());
+                 state->get_transition_out()->dot_string().c_str());
 #if SIMGRID_HAVE_STATEFUL_MC
     } else {
       dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(),
                  visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_,
-                 state->get_transition()->dot_string().c_str());
+                 state->get_transition_out()->dot_string().c_str());
 #endif
     }
   }

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 1cd4388..46f11b1 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -120,8 +120,8 @@ void LivenessChecker::replay()
     std::shared_ptr<State> state = pair->app_state_;
 
     if (pair->exploration_started) {
-      state->get_transition()->replay(get_remote_app());
-      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_string().c_str(), state.get());
+      state->get_transition_out()->replay(get_remote_app());
+      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition_out()->to_string().c_str(), state.get());
     }
 
     /* Update statistics */
@@ -258,7 +258,7 @@ RecordTrace LivenessChecker::get_record_trace() // override
 {
   RecordTrace res;
   for (std::shared_ptr<Pair> const& pair : exploration_stack_)
-    res.push_back(pair->app_state_->get_transition());
+    res.push_back(pair->app_state_->get_transition_out());
   return res;
 }
 
@@ -289,8 +289,8 @@ std::vector<std::string> LivenessChecker::get_textual_trace() // override
 {
   std::vector<std::string> trace;
   for (std::shared_ptr<Pair> const& pair : exploration_stack_)
-    if (pair->app_state_->get_transition() != nullptr)
-      trace.push_back(pair->app_state_->get_transition()->to_string());
+    if (pair->app_state_->get_transition_out() != nullptr)
+      trace.push_back(pair->app_state_->get_transition_out()->to_string());
 
   return trace;
 }
@@ -403,7 +403,7 @@ void LivenessChecker::run()
     }
 
     current_pair->app_state_->execute_next(current_pair->app_state_->next_transition(), get_remote_app());
-    XBT_DEBUG("Execute: %s", current_pair->app_state_->get_transition()->to_string().c_str());
+    XBT_DEBUG("Execute: %s", current_pair->app_state_->get_transition_out()->to_string().c_str());
 
     /* Update the dot output */
     if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) {
@@ -411,7 +411,7 @@ void LivenessChecker::run()
       this->previous_request_.clear();
     }
     this->previous_pair_    = current_pair->num;
-    this->previous_request_ = current_pair->app_state_->get_transition()->dot_string();
+    this->previous_request_ = current_pair->app_state_->get_transition_out()->dot_string();
     if (current_pair->search_cycle)
       dot_output("%d [shape=doublecircle];\n", current_pair->num);
 

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index b297183..743d999 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -214,7 +214,7 @@ void UdporChecker::restore_program_state_with_current_stack()
   for (const std::unique_ptr<State>& state : state_stack) {
     if (state == state_stack.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
       break;
-    state->get_transition()->replay(get_remote_app());
+    state->get_transition_out()->replay(get_remote_app());
   }
 }
 
@@ -321,7 +321,7 @@ RecordTrace UdporChecker::get_record_trace()
 {
   RecordTrace res;
   for (auto const& state : state_stack)
-    res.push_back(state->get_transition());
+    res.push_back(state->get_transition_out());
   return res;
 }
 
@@ -329,7 +329,7 @@ std::vector<std::string> UdporChecker::get_textual_trace()
 {
   std::vector<std::string> trace;
   for (auto const& state : state_stack) {
-    const auto* t = state->get_transition();
+    const auto* t = state->get_transition_out();
     trace.push_back(xbt::string_printf("%ld: %s", t->aid_, t->to_string().c_str()));
   }
   return trace;

diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp
index 7e71fe1..2b28f18 100644 (file)
--- a/src/mc/remote/CheckerSide.cpp
+++ b/src/mc/remote/CheckerSide.cpp
@@ -184,7 +184,7 @@ CheckerSide::CheckerSide(const std::vector<char*>& args, bool need_memory_info)
   int sockets[2];
   xbt_assert(socketpair(AF_UNIX,
 #ifdef __APPLE__
-                        SOCK_STREAM, /* Mac OSX does not have AF_UNIX + SOCK_SEQPACKET, even if that's faster*/
+                        SOCK_STREAM, /* Mac OSX does not have AF_UNIX + SOCK_SEQPACKET, even if that's faster */
 #else
                         SOCK_SEQPACKET,
 #endif