Simplify the MC initialization code

diff --git a/src/mc/explo/simgrid_mc.cpp b/src/mc/explo/simgrid_mc.cpp
index 6f55f3d..ceeae70 100644 (file)
--- a/src/mc/explo/simgrid_mc.cpp
+++ b/src/mc/explo/simgrid_mc.cpp
@@ -27,6 +27,34 @@ static simgrid::config::Flag<std::string> _sg_mc_setenv{
                  "The 'model-check/setenv' parameter must be like 'AZE=aze', but it does not contain an equal sign.");
     }};
 
+static void mc_exec_user_code(std::vector<char*> const& argv)
+{
+  int i = 1;
+  while (argv[i] != nullptr && argv[i][0] == '-')
+    i++;
+
+  /* Setup the tokenizer that parses the cfg:model-check/setenv parameter */
+  using Tokenizer = boost::tokenizer<boost::char_separator<char>>;
+  boost::char_separator<char> semicol_sep(";");
+  boost::char_separator<char> equal_sep("=");
+  Tokenizer token_vars(_sg_mc_setenv.get(), semicol_sep); /* Iterate over all FOO=foo parts */
+  for (const auto& token : token_vars) {
+    std::vector<std::string> kv;
+    Tokenizer token_kv(token, equal_sep);
+    for (const auto& t : token_kv) /* Iterate over 'FOO' and then 'foo' in that 'FOO=foo' */
+      kv.push_back(t);
+    xbt_assert(kv.size() == 2, "Parse error on 'model-check/setenv' value %s. Does it contain an equal sign?",
+               token.c_str());
+    XBT_INFO("setenv '%s'='%s'", kv[0].c_str(), kv[1].c_str());
+    setenv(kv[0].c_str(), kv[1].c_str(), 1);
+  }
+  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.data() + i);
+  xbt_die("The model-checked process failed to exec(%s): %s", argv[i], strerror(errno));
+}
+
 int main(int argc, char** argv)
 {
   xbt_assert(argc >= 2, "Missing arguments");
@@ -40,71 +68,22 @@ int main(int argc, char** argv)
 
   xbt_log_init(&argc, argv);
 #if HAVE_SMPI
-  smpi_init_options(); // only performed once
+  smpi_init_options(); // that's OK to call it twice, and we need it ASAP
 #endif
   sg_config_init(&argc, argv);
 
-  simgrid::mc::ExplorationAlgorithm algo;
+  auto remote_app = std::make_unique<simgrid::mc::RemoteApp>([argv_copy] { mc_exec_user_code(argv_copy); });
+
+  simgrid::mc::Exploration* explo;
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
-    algo = simgrid::mc::ExplorationAlgorithm::CommDeterminism;
+    explo = simgrid::mc::create_communication_determinism_checker(*remote_app.get());
   else if (_sg_mc_unfolding_checker)
-    algo = simgrid::mc::ExplorationAlgorithm::UDPOR;
+    explo = simgrid::mc::create_udpor_checker(*remote_app.get());
   else if (_sg_mc_property_file.get().empty())
-    algo = simgrid::mc::ExplorationAlgorithm::Safety;
+    explo = simgrid::mc::create_dfs_exploration(*remote_app.get());
   else
-    algo = simgrid::mc::ExplorationAlgorithm::Liveness;
+    explo = simgrid::mc::create_liveness_checker(*remote_app.get());
 
-  std::unordered_map<std::string, std::string> environment;
-  /** Setup the tokenizer that parses the string **/
-  using Tokenizer = boost::tokenizer<boost::char_separator<char>>;
-  boost::char_separator<char> semicol_sep(";");
-  boost::char_separator<char> equal_sep("=");
-  Tokenizer token_vars(_sg_mc_setenv.get(), semicol_sep); /* Iterate over all FOO=foo parts */
-  for (const auto& token : token_vars) {
-    std::vector<std::string> kv;
-    Tokenizer token_kv(token, equal_sep);
-    for (const auto& t : token_kv) /* Iterate over 'FOO' and then 'foo' in that 'FOO=foo' */
-      kv.push_back(t);
-    xbt_assert(kv.size() == 2, "Parse error on 'model-check/setenv' value %s. Does it contain an equal sign?",
-               token.c_str());
-    environment[kv[0]] = kv[1];
-  }
-  auto remote_app = std::make_unique<simgrid::mc::RemoteApp>([argv_copy, &environment] {
-    int i = 1;
-    while (argv_copy[i] != nullptr && argv_copy[i][0] == '-')
-      i++;
-
-    for (auto const& [key, val] : environment) {
-      XBT_INFO("setenv '%s'='%s'", key.c_str(), val.c_str());
-      setenv(key.c_str(), val.c_str(), 1);
-    }
-    xbt_assert(argv_copy[i] != nullptr,
-               "Unable to find a binary to exec on the command line. Did you only pass config flags?");
-    execvp(argv_copy[i], argv_copy.data() + i);
-    xbt_die("The model-checked process failed to exec(%s): %s", argv_copy[i], strerror(errno));
-  });
-
-  simgrid::mc::Exploration* explo;
-  switch (algo) {
-    case simgrid::mc::ExplorationAlgorithm::CommDeterminism:
-      explo = simgrid::mc::create_communication_determinism_checker(*remote_app.get());
-      break;
-
-    case simgrid::mc::ExplorationAlgorithm::UDPOR:
-      explo = simgrid::mc::create_udpor_checker(*remote_app.get());
-      break;
-
-    case simgrid::mc::ExplorationAlgorithm::Safety:
-      explo = simgrid::mc::create_dfs_exploration(*remote_app.get());
-      break;
-
-    case simgrid::mc::ExplorationAlgorithm::Liveness:
-      explo = simgrid::mc::create_liveness_checker(*remote_app.get());
-      break;
-
-    default:
-      THROW_IMPOSSIBLE;
-  }
   mc_model_checker->set_exploration(explo);
   std::unique_ptr<simgrid::mc::Exploration> checker{explo};