Various sonar cleanups

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

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index 866a1d0..f537a48 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -38,13 +38,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)
@@ -64,12 +57,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
@@ -225,9 +212,8 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior)
     // Find an enabled transition to pick
     for (const auto& [_, actor] : get_actors_list()) {
       if (actor.is_enabled()) {
-        // For each variant of the transition, we want
-        // to insert the action into the tree. This ensures
-        // that all variants are searched
+        // For each variant of the transition that is enabled, we want to insert the action into the tree.
+        // This ensures that all variants are searched
         for (unsigned times = 0; times < actor.get_max_considered(); ++times) {
           wakeup_tree_.insert(prior, odpor::PartialExecution{actor.get_transition(times)});
         }
@@ -241,10 +227,9 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior)
 void State::sprout_tree_from_parent_state()
 {
 
-    XBT_DEBUG("Initializing Wut with parent one:");
-    XBT_DEBUG("\n%s", parent_state_->wakeup_tree_.string_of_whole_tree().c_str());
+  XBT_DEBUG("Initializing Wut with parent one:");
+  XBT_DEBUG("\n%s", parent_state_->wakeup_tree_.string_of_whole_tree().c_str());
 
-    
   xbt_assert(parent_state_ != nullptr, "Attempting to construct a wakeup tree for the root state "
                                        "(or what appears to be, rather for state without a parent defined)");
   const auto min_process_node = parent_state_->wakeup_tree_.get_min_single_process_node();
@@ -252,14 +237,18 @@ void State::sprout_tree_from_parent_state()
                                            "parent with an empty wakeup tree. This indicates either that ODPOR "
                                            "actor selection in State.cpp is incorrect, or that the code "
                                            "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` 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(), get_transition_in()->aid_,
-             min_process_node.value()->get_action()->to_string(false).c_str(), min_process_node.value()->get_actor());
+  if (not(get_transition_in()->aid_ == min_process_node.value()->get_actor() &&
+          get_transition_in()->type_ == min_process_node.value()->get_action()->type_)) {
+    XBT_ERROR("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? Trace so far:",
+              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());
+    for (auto const& elm : Exploration::get_instance()->get_textual_trace())
+      XBT_ERROR("%s", elm.c_str());
+    xbt_abort();
+  }
   this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(min_process_node.value());
 }
 
@@ -280,6 +269,11 @@ void State::remove_subtree_using_current_out_transition()
   wakeup_tree_.remove_min_single_process_subtree();
 }
 
+void State::remove_subtree_at_aid(const aid_t proc)
+{
+  wakeup_tree_.remove_subtree_at_aid(proc);
+}
+
 odpor::WakeupTree::InsertionResult State::insert_into_wakeup_tree(const odpor::PartialExecution& pe,
                                                                   const odpor::Execution& E)
 {