X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/0cfb40d124549f4dde6f00095847de0d04828adf..0a82e90d4cfdd7e27e1b946d22aff74a5abdda99:/src/mc/LivenessChecker.cpp diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index 584337f5b5..81b9833447 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -159,7 +159,6 @@ void LivenessChecker::removeAcceptancePair(int pair_num) void LivenessChecker::prepare(void) { - initial_global_state->snapshot = simgrid::mc::take_snapshot(0); initial_global_state->prev_pair = 0; std::shared_ptr> propos = this->getPropositionValues(); @@ -188,7 +187,7 @@ void LivenessChecker::replay() } /* Restore the initial state */ - simgrid::mc::restore_snapshot(initial_global_state->snapshot); + simgrid::mc::session->restoreInitialState(); /* Traverse the stack from the initial state and re-execute the transitions */ int depth = 1; @@ -484,14 +483,12 @@ int LivenessChecker::run() { XBT_INFO("Check the liveness property %s", _sg_mc_property_file); MC_automaton_load(_sg_mc_property_file); - mc_model_checker->wait_for_requests(); XBT_DEBUG("Starting the liveness algorithm"); - - /* Create the initial state */ simgrid::mc::initial_global_state = std::unique_ptr(new s_mc_global_t()); - + simgrid::mc::session->initialize(); this->prepare(); + int res = this->main(); simgrid::mc::initial_global_state = nullptr;