From e9a884e745ad230410dde4af838d5727fd33edd0 Mon Sep 17 00:00:00 2001
From: Martin Quinson <martin.quinson@ens-rennes.fr>
Date: Sun, 14 Mar 2021 02:58:15 +0100
Subject: [PATCH] cosmetics

---
 src/mc/api.cpp                                |  4 +---
 .../CommunicationDeterminismChecker.cpp       | 22 ++++++++++---------
 src/mc/checker/LivenessChecker.cpp            | 12 +++++-----
 src/mc/checker/simgrid_mc.cpp                 |  1 -
 4 files changed, 20 insertions(+), 19 deletions(-)

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index ee5858982e..b6cee6c9ba 100644
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -421,7 +421,7 @@ simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm
     xbt_assert(argv[i] != nullptr,
                "Unable to find a binary to exec on the command line. Did you only pass config flags?");
     execvp(argv[i], argv + i);
-    xbt_die("The model-checked process failed to exec(): %s", strerror(errno));
+    xbt_die("The model-checked process failed to exec(%s): %s", argv[i], strerror(errno));
   });
 
   simgrid::mc::Checker* checker;
@@ -964,12 +964,10 @@ void Api::execute(Transition& transition, smx_simcall_t simcall) const
   session->execute(transition);
 }
 
-#if SIMGRID_HAVE_MC
 void Api::automaton_load(const char* file) const
 {
   MC_automaton_load(file);
 }
-#endif
 
 std::vector<int> Api::automaton_propositional_symbol_evaluate() const
 {
diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 05eede3028..9c179abc9e 100644
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -313,11 +313,12 @@ void CommunicationDeterminismChecker::prepare()
 
   XBT_DEBUG("********* Start communication determinism verification *********");
 
-  /* Get an enabled actor and insert it in the interleave set of the initial state */
-  auto actors = api::get().get_actors();
-  for (auto& actor : actors)
-    if (api::get().actor_is_enabled(actor.copy.get_buffer()->get_pid()))
-      initial_state->mark_todo(actor.copy.get_buffer());
+  /* Add all enabled actors to the interleave set of the initial state */
+  for (auto& act : api::get().get_actors()) {
+    auto actor = act.copy.get_buffer();
+    if (api::get().actor_is_enabled(actor->get_pid()))
+      initial_state->mark_todo(actor);
+  }
 
   stack_.push_back(std::move(initial_state));
 }
@@ -467,11 +468,12 @@ void CommunicationDeterminismChecker::real_run()
         visited_state = nullptr;
 
       if (visited_state == nullptr) {
-        /* Get enabled actors and insert them in the interleave set of the next state */
-        auto actors = api::get().get_actors();
-        for (auto& actor : actors)
-          if (api::get().actor_is_enabled(actor.copy.get_buffer()->get_pid()))
-            next_state->mark_todo(actor.copy.get_buffer());
+        /* Add all enabled actors to the interleave set of the next state */
+        for (auto& act : api::get().get_actors()) {
+          auto actor = act.copy.get_buffer();
+          if (api::get().actor_is_enabled(actor->get_pid()))
+            next_state->mark_todo(actor);
+        }
 
         if (dot_output != nullptr)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", cur_state->num_, next_state->num_, req_str.c_str());
diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index de7098547b..c3730a9689 100644
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -256,11 +256,13 @@ std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt
     next_pair->depth = current_pair->depth + 1;
   else
     next_pair->depth = 1;
-  /* Get enabled actors and insert them in the interleave set of the next graph_state */
-  auto actors = api::get().get_actors();
-  for (auto& actor : actors)
-    if (api::get().actor_is_enabled(actor.copy.get_buffer()->get_pid()))
-      next_pair->graph_state->mark_todo(actor.copy.get_buffer());
+  /* Add all enabled actors to the interleave set of the initial state */
+  for (auto& act : api::get().get_actors()) {
+    auto actor = act.copy.get_buffer();
+    if (api::get().actor_is_enabled(actor->get_pid()))
+      next_pair->graph_state->mark_todo(actor);
+  }
+
   next_pair->requests = next_pair->graph_state->count_todo();
   /* FIXME : get search_cycle value for each accepting state */
   if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle))
diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/checker/simgrid_mc.cpp
index f91ef2b15b..767c0bf4d0 100644
--- a/src/mc/checker/simgrid_mc.cpp
+++ b/src/mc/checker/simgrid_mc.cpp
@@ -68,7 +68,6 @@ int main(int argc, char** argv)
   } catch (const simgrid::mc::LivenessError&) {
     res = SIMGRID_MC_EXIT_LIVENESS;
   }
-  checker = nullptr;
   api::get().s_close();
   delete[] argv_copy;
   return res;
-- 
2.20.1