X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/5f5a10db6fc4552782638abb4817041223e17775..3f9b311ec56db95ec539001a860ae3c838c48312:/src/mc/api/State.cpp

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index 0082e67b71..f537a484b5 100644
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -25,7 +25,6 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_)
 {
   XBT_VERB("Creating a guide for the state");
 
-  
   if (_sg_mc_strategy == "none")
     strategy_ = std::make_shared<BasicStrategy>();
   else if (_sg_mc_strategy == "max_match_comm")
@@ -33,10 +32,9 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_)
   else if (_sg_mc_strategy == "min_match_comm")
     strategy_ = std::make_shared<MinMatchComm>();
   else if (_sg_mc_strategy == "uniform") {
-    xbt::random::set_mersenne_seed(_sg_mc_random_seed);  
+    xbt::random::set_mersenne_seed(_sg_mc_random_seed);
     strategy_ = std::make_shared<UniformStrategy>();
-  }
-  else
+  } else
     THROW_IMPOSSIBLE;
 
   remote_app.get_actors_status(strategy_->actors_to_run_);
@@ -51,7 +49,7 @@ State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
     strategy_ = std::make_shared<MaxMatchComm>();
   else if (_sg_mc_strategy == "min_match_comm")
     strategy_ = std::make_shared<MinMatchComm>();
-  else if (_sg_mc_strategy == "uniform") 
+  else if (_sg_mc_strategy == "uniform")
     strategy_ = std::make_shared<UniformStrategy>();
   else
     THROW_IMPOSSIBLE;
@@ -201,6 +199,9 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior)
 {
   // TODO: It would be better not to have such a flag.
   if (has_initialized_wakeup_tree) {
+    XBT_DEBUG("Reached a node with the following initialized WuT:");
+    XBT_DEBUG("\n%s", wakeup_tree_.string_of_whole_tree().c_str());
+
     return;
   }
   // TODO: Note that the next action taken by the actor may be updated
@@ -211,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)});
         }
@@ -226,6 +226,10 @@ 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_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();
@@ -233,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());
 }
 
@@ -261,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)
 {