Remove the stateful model-checking from the archive. It's not working anymore

[simgrid.git] / src / mc / api / State.cpp

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index d1919db..0082e67 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -40,13 +40,6 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_)
     THROW_IMPOSSIBLE;
 
   remote_app.get_actors_status(strategy_->actors_to_run_);
-
-#if SIMGRID_HAVE_STATEFUL_MC
-  /* Stateful model checking */
-  if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
-    system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
-                                                            *remote_app.get_remote_process_memory());
-#endif
 }
 
 State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
@@ -66,12 +59,6 @@ State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
 
   remote_app.get_actors_status(strategy_->actors_to_run_);
 
-#if SIMGRID_HAVE_STATEFUL_MC /* Stateful model checking */
-  if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
-    system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
-                                                            *remote_app.get_remote_process_memory());
-#endif
-
   /* Copy the sleep set and eventually removes things from it: */
   /* For each actor in the previous sleep set, keep it if it is not dependent with current transition.
    * And if we kept it and the actor is enabled in this state, mark the actor as already done, so that
@@ -183,7 +170,7 @@ std::unordered_set<aid_t> State::get_backtrack_set() const
 {
   std::unordered_set<aid_t> actors;
   for (const auto& [aid, state] : get_actors_list()) {
-    if (state.is_todo() or state.is_done()) {
+    if (state.is_todo() || state.is_done()) {
       actors.insert(aid);
     }
   }
@@ -248,12 +235,12 @@ void State::sprout_tree_from_parent_state()
                                            "deciding when to make subtrees in ODPOR is incorrect");
   xbt_assert((get_transition_in()->aid_ == min_process_node.value()->get_actor()) &&
                  (get_transition_in()->type_ == min_process_node.value()->get_action()->type_),
-             "We tried to make a subtree from a parent state who claimed to have executed `%s` "
-             "but whose wakeup tree indicates it should have executed `%s`. This indicates "
+             "We tried to make a subtree from a parent state who claimed to have executed `%s` on actor %ld"
+             "but whose wakeup tree indicates it should have executed `%s` on actor %ld. This indicates "
              "that exploration is not following ODPOR. Are you sure you're choosing actors "
              "to schedule from the wakeup tree?",
-             get_transition_in()->to_string(false).c_str(),
-             min_process_node.value()->get_action()->to_string(false).c_str());
+             get_transition_in()->to_string(false).c_str(), get_transition_in()->aid_,
+             min_process_node.value()->get_action()->to_string(false).c_str(), min_process_node.value()->get_actor());
   this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(min_process_node.value());
 }
 
@@ -291,7 +278,7 @@ void State::do_odpor_unwind()
     // works with ODPOR in the way we intend it to work. There is not a
     // good way to perform transition equality in SimGrid; instead, we
     // effectively simply check for the presence of an actor in the sleep set.
-    if (!get_actors_list().at(out_transition->aid_).has_more_to_consider())
+    if (not get_actors_list().at(out_transition->aid_).has_more_to_consider())
       add_sleep_set(std::move(out_transition));
   }
 }