X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/093ee3ab84a46a3a5a6673aeb1f4980a3cc50647..d098dd9e12ee321b061421f535b2b56ce7691673:/src/mc/simgrid_mc.cpp?ds=inline diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index 4dcc0bab00..a923cdbcea 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -29,13 +29,13 @@ #include "simgrid/sg_config.h" #include "src/xbt_modinter.h" -#include "mc_base.h" -#include "mc_private.h" -#include "mc_protocol.h" -#include "src/mc/Server.hpp" -#include "mc_safety.h" -#include "mc_comm_pattern.h" -#include "mc_liveness.h" +#include "src/mc/mc_base.h" +#include "src/mc/mc_private.h" +#include "src/mc/mc_protocol.h" +#include "src/mc/mc_safety.h" +#include "src/mc/mc_comm_pattern.h" +#include "src/mc/mc_liveness.h" +#include "src/mc/mc_exit.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc"); @@ -88,25 +88,26 @@ static int do_child(int socket, char** argv) static int do_parent(int socket, pid_t child) { XBT_DEBUG("Inside the parent process"); - if (simgrid::mc::server) + if (mc_model_checker) xbt_die("MC server already present"); try { mc_mode = MC_MODE_SERVER; - simgrid::mc::server = new simgrid::mc::Server(child, socket); - simgrid::mc::server->start(); + mc_model_checker = new simgrid::mc::ModelChecker(child, socket); + mc_model_checker->start(); + int res = 0; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) - MC_modelcheck_comm_determinism(); + res = MC_modelcheck_comm_determinism(); else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') - MC_modelcheck_safety(); + res = MC_modelcheck_safety(); else - MC_modelcheck_liveness(); - simgrid::mc::server->shutdown(); - simgrid::mc::server->exit(); + res = MC_modelcheck_liveness(); + mc_model_checker->shutdown(); + return res; } catch(std::exception& e) { XBT_ERROR("Exception: %s", e.what()); + return SIMGRID_MC_EXIT_ERROR; } - exit(SIMGRID_MC_EXIT_ERROR); } static char** argvdup(int argc, char** argv)