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

diff --combined src/mc/api.cpp
index be0b7ed,ec0b7e3..aae3945
--- 1/src/mc/api.cpp
--- 2/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@@ -379,10 -379,10 +379,10 @@@ xbt::string const& Api::get_actor_host_
    return *info->hostname;
  }
  
- std::string Api::get_actor_name(smx_actor_t actor) const
+ xbt::string const& Api::get_actor_name(smx_actor_t actor) const
  {
    if (mc_model_checker == nullptr)
-     return actor->get_cname();
+     return actor->get_name();
  
    simgrid::mc::ActorInformation* info = actor_info_cast(actor);
    if (info->name.empty()) {
@@@ -400,7 -400,7 +400,7 @@@ std::string Api::get_actor_string(smx_a
    if (actor) {
      res = "(" + std::to_string(actor->get_pid()) + ")";
      if (actor->get_host())
-       res += std::string(get_actor_host_name(actor)) + " (" + get_actor_name(actor) + ")";
+       res += std::string(get_actor_host_name(actor)) + " (" + std::string(get_actor_name(actor)) + ")";
      else
        res += get_actor_name(actor);
    } else
@@@ -431,25 -431,26 +431,26 @@@ simgrid::mc::Checker* Api::initialize(c
    simgrid::mc::Checker* checker;
    switch (algo) {
      case CheckerAlgorithm::CommDeterminism:
 -      checker = simgrid::mc::createCommunicationDeterminismChecker(session);
 +      checker = simgrid::mc::create_communication_determinism_checker(session);
        break;
  
      case CheckerAlgorithm::UDPOR:
 -      checker = simgrid::mc::createUdporChecker(session);
 +      checker = simgrid::mc::create_udpor_checker(session);
        break;
  
      case CheckerAlgorithm::Safety:
 -      checker = simgrid::mc::createSafetyChecker(session);
 +      checker = simgrid::mc::create_safety_checker(session);
        break;
  
      case CheckerAlgorithm::Liveness:
 -      checker = simgrid::mc::createLivenessChecker(session);
 +      checker = simgrid::mc::create_liveness_checker(session);
        break;
  
      default:
        THROW_IMPOSSIBLE;
    }
  
+   // FIXME: session and checker are never deleted
    simgrid::mc::session_singleton = session;
    mc_model_checker->setChecker(checker);
    return checker;

diff --combined src/mc/checker/CommunicationDeterminismChecker.cpp
index 1f3bb27,ed9f983..9175947
--- 1/src/mc/checker/CommunicationDeterminismChecker.cpp
--- 2/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@@ -236,8 -236,7 +236,7 @@@ void CommunicationDeterminismChecker::c
    auto current_comm_pattern =
        std::find_if(begin(incomplete_pattern), end(incomplete_pattern),
                     [&comm_addr](const PatternCommunication* comm) { return (comm->comm_addr == comm_addr); });
-   if (current_comm_pattern == std::end(incomplete_pattern))
-     xbt_die("Corresponding communication not found!");
+   xbt_assert(current_comm_pattern != std::end(incomplete_pattern), "Corresponding communication not found!");
  
    update_comm_pattern(*current_comm_pattern, comm_addr);
    std::unique_ptr<PatternCommunication> comm_pattern(*current_comm_pattern);
@@@ -534,7 -533,7 +533,7 @@@ void CommunicationDeterminismChecker::r
    this->real_run();
  }
  
 -Checker* createCommunicationDeterminismChecker(Session* session)
 +Checker* create_communication_determinism_checker(Session* session)
  {
    return new CommunicationDeterminismChecker(session);
  }

diff --combined src/mc/checker/SafetyChecker.cpp
index 09efb3c,36423ba..4943ad2
--- 1/src/mc/checker/SafetyChecker.cpp
--- 2/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@@ -110,9 -110,11 +110,11 @@@ void SafetyChecker::run(
      // req is now the transition of the process that was selected to be executed
  
      if (req == nullptr) {
-       XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size() + 1);
+       XBT_DEBUG("There remains %zu actors, but no more processes to interleave. (depth %zu)",
+                 mc_model_checker->get_remote_process().actors().size(), stack_.size() + 1);
  
- //      mc_model_checker->finalize_app();
+       if (mc_model_checker->get_remote_process().actors().empty())
+         mc_model_checker->finalize_app();
        this->backtrack();
        continue;
      }
@@@ -185,7 -187,7 +187,7 @@@ void SafetyChecker::backtrack(
      stack_.pop_back();
      if (reductionMode_ == ReductionMode::dpor) {
        auto call = state->executed_req_.call_;
-       const kernel::actor::ActorImpl* issuer = api::get().simcall_get_issuer(&state->executed_req_);
+       kernel::actor::ActorImpl* issuer = api::get().simcall_get_issuer(&state->executed_req_);
        for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
          State* prev_state = i->get();
          if (state->executed_req_.issuer_ == prev_state->executed_req_.issuer_) {
@@@ -206,7 -208,7 +208,7 @@@
            if (not prev_state->actor_states_[issuer->get_pid()].is_done())
              prev_state->mark_todo(issuer);
            else
-             XBT_DEBUG("Actor %s %ld is in done set", issuer->get_cname(), issuer->get_pid());
+             XBT_DEBUG("Actor %s %ld is in done set", api::get().get_actor_name(issuer).c_str(), issuer->get_pid());
            break;
          } else {
            const kernel::actor::ActorImpl* previous_issuer = api::get().simcall_get_issuer(&prev_state->executed_req_);
@@@ -289,7 -291,7 +291,7 @@@ SafetyChecker::SafetyChecker(Session* s
    stack_.push_back(std::move(initial_state));
  }
  
 -Checker* createSafetyChecker(Session* session)
 +Checker* create_safety_checker(Session* session)
  {
    return new SafetyChecker(session);
  }