1 /* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
6 #include "simgrid/sg_config.hpp"
7 #include "src/internal_config.h"
8 #include "src/mc/explo/Exploration.hpp"
9 #include "src/mc/mc_config.hpp"
10 #include "src/mc/mc_exit.hpp"
13 #include "smpi/smpi.h"
16 #include <boost/tokenizer.hpp>
21 static simgrid::config::Flag<std::string> _sg_mc_setenv{
22 "model-check/setenv", "Extra environment variables to pass to the child process (ex: 'AZE=aze;QWE=qwe').", "",
23 [](std::string_view value) {
24 xbt_assert(value.empty() || value.find('=', 0) != std::string_view::npos,
25 "The 'model-check/setenv' parameter must be like 'AZE=aze', but it does not contain an equal sign.");
28 int main(int argc, char** argv)
30 xbt_assert(argc >= 2, "Missing arguments");
32 // Currently, we need this before sg_config_init:
33 _sg_do_model_check = 1;
35 // The initialization function can touch argv.
36 // We make a copy of argv before modifying it in order to pass the original value to the model-checked application:
37 std::vector<char*> argv_copy{argv, argv + argc + 1};
39 xbt_log_init(&argc, argv);
41 smpi_init_options(); // only performed once
43 sg_config_init(&argc, argv);
45 simgrid::mc::ExplorationAlgorithm algo;
46 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
47 algo = simgrid::mc::ExplorationAlgorithm::CommDeterminism;
48 else if (_sg_mc_unfolding_checker)
49 algo = simgrid::mc::ExplorationAlgorithm::UDPOR;
50 else if (_sg_mc_property_file.get().empty())
51 algo = simgrid::mc::ExplorationAlgorithm::Safety;
53 algo = simgrid::mc::ExplorationAlgorithm::Liveness;
55 std::unordered_map<std::string, std::string> environment;
56 /** Setup the tokenizer that parses the string **/
57 using Tokenizer = boost::tokenizer<boost::char_separator<char>>;
58 boost::char_separator<char> semicol_sep(";");
59 boost::char_separator<char> equal_sep("=");
60 Tokenizer token_vars(_sg_mc_setenv.get(), semicol_sep); /* Iterate over all FOO=foo parts */
61 for (const auto& token : token_vars) {
62 std::vector<std::string> kv;
63 Tokenizer token_kv(token, equal_sep);
64 for (const auto& t : token_kv) /* Iterate over 'FOO' and then 'foo' in that 'FOO=foo' */
66 xbt_assert(kv.size() == 2, "Parse error on 'model-check/setenv' value %s. Does it contain an equal sign?",
68 environment[kv[0]] = kv[1];
71 int res = SIMGRID_MC_EXIT_SUCCESS;
72 std::unique_ptr<simgrid::mc::Exploration> checker{
73 simgrid::mc::Api::get().initialize(argv_copy.data(), environment, algo)};
76 } catch (const simgrid::mc::DeadlockError&) {
77 res = SIMGRID_MC_EXIT_DEADLOCK;
78 } catch (const simgrid::mc::TerminationError&) {
79 res = SIMGRID_MC_EXIT_NON_TERMINATION;
80 } catch (const simgrid::mc::LivenessError&) {
81 res = SIMGRID_MC_EXIT_LIVENESS;
83 simgrid::mc::Api::get().s_close();
84 checker.release(); // FIXME: this line should not exist, but it segfaults in liveness