X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2ab3abe53dde0026da7545fb7a80f29caf22a39b..6df8a056a38f11dc657247acb58dd4afc553d849:/src/mc/simgrid_mc.cpp diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index 949ed65cd0..a115825b2e 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -24,12 +24,9 @@ #include "src/mc/mc_protocol.h" #include "src/mc/mc_safety.h" #include "src/mc/mc_comm_pattern.h" -#include "src/mc/LivenessChecker.hpp" #include "src/mc/mc_exit.h" #include "src/mc/Session.hpp" #include "src/mc/Checker.hpp" -#include "src/mc/CommunicationDeterminismChecker.hpp" -#include "src/mc/SafetyChecker.hpp" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc"); @@ -45,22 +42,15 @@ char** argvdup(int argc, char** argv) static std::unique_ptr createChecker(simgrid::mc::Session& session) { - using simgrid::mc::Session; - using simgrid::mc::FunctionalChecker; - - std::function code; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) return std::unique_ptr( - new simgrid::mc::CommunicationDeterminismChecker(session)); + simgrid::mc::createCommunicationDeterminismChecker(session)); else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') return std::unique_ptr( - new simgrid::mc::SafetyChecker(session)); + simgrid::mc::createSafetyChecker(session)); else return std::unique_ptr( - new simgrid::mc::LivenessChecker(session)); - - return std::unique_ptr( - new FunctionalChecker(session, std::move(code))); + simgrid::mc::createLivenessChecker(session)); } int main(int argc, char** argv) @@ -73,7 +63,6 @@ int main(int argc, char** argv) // Currently, we need this before sg_config_init: _sg_do_model_check = 1; - mc_mode = MC_MODE_SERVER; // The initialisation function can touch argv. // We make a copy of argv before modifying it in order to pass the original @@ -89,6 +78,7 @@ int main(int argc, char** argv) simgrid::mc::session = session.get(); std::unique_ptr checker = createChecker(*session); int res = checker->run(); + checker = nullptr; session->close(); return res; }