cosmetics

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index ee58589..b6cee6c 100644 (file)
--- 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 05eede3..9c179ab 100644 (file)
--- 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 de70985..c3730a9 100644 (file)
--- 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 f91ef2b..767c0bf 100644 (file)
--- 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;