Merge branch 'master' of framagit.org:simgrid/simgrid

[simgrid.git] / src / mc / explo / LivenessChecker.cpp

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 3638fd6..3d60ef9 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,8 @@ 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());
+    if (pair->app_state_->get_transition_out() != nullptr)
+      res.push_back(pair->app_state_->get_transition_out().get());
   return res;
 }
 
@@ -285,15 +286,6 @@ void LivenessChecker::show_acceptance_cycle(std::size_t depth)
   XBT_INFO("Counter-example depth: %zu", depth);
 }
 
-std::vector<std::string> LivenessChecker::get_textual_trace() // override
-{
-  std::vector<std::string> trace;
-  for (std::shared_ptr<Pair> const& pair : exploration_stack_)
-    trace.push_back(pair->app_state_->get_transition()->to_string());
-
-  return trace;
-}
-
 std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt_automaton_state_t state,
                                                    std::shared_ptr<const std::vector<int>> propositions)
 {
@@ -384,7 +376,7 @@ void LivenessChecker::run()
       reached_pair = this->insert_acceptance_pair(current_pair.get());
       if (reached_pair == nullptr) {
         this->show_acceptance_cycle(current_pair->depth);
-        throw LivenessError();
+        throw McError(ExitStatus::LIVENESS);
       }
     }
 
@@ -402,7 +394,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) {
@@ -410,7 +402,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);