X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/944476b942061ce790c641503707cb01443628c0..4bcfd40036f842e976d329cd0cee7349b8e0f4d6:/src/mc/checker/LivenessChecker.cpp diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index df9cd0301b..cd49a87e4d 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -1,5 +1,4 @@ -/* Copyright (c) 2011-2017. The SimGrid Team. - * All rights reserved. */ +/* Copyright (c) 2011-2019. The SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ @@ -16,20 +15,19 @@ #include #include -#include #include #include #include "src/mc/Session.hpp" #include "src/mc/Transition.hpp" #include "src/mc/checker/LivenessChecker.hpp" -#include "src/mc/mc_exit.h" -#include "src/mc/mc_private.h" -#include "src/mc/mc_private.h" -#include "src/mc/mc_record.h" -#include "src/mc/mc_replay.h" -#include "src/mc/mc_request.h" -#include "src/mc/mc_smx.h" +#include "src/mc/mc_exit.hpp" +#include "src/mc/mc_private.hpp" +#include "src/mc/mc_private.hpp" +#include "src/mc/mc_record.hpp" +#include "src/mc/mc_replay.hpp" +#include "src/mc/mc_request.hpp" +#include "src/mc/mc_smx.hpp" #include "src/mc/remote/Client.hpp" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification"); @@ -76,6 +74,7 @@ static bool evaluate_label(xbt_automaton_exp_label_t l, std::vector const& return values[cursor] != 0; } xbt_die("Missing predicate"); + break; } case xbt_automaton_exp_label::AUT_ONE: return true; @@ -101,9 +100,7 @@ int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::Visi { simgrid::mc::Snapshot* s1 = state1->graph_state->system_state.get(); simgrid::mc::Snapshot* s2 = state2->graph_state->system_state.get(); - int num1 = state1->num; - int num2 = state2->num; - return simgrid::mc::snapshot_compare(num1, s1, num2, s2); + return simgrid::mc::snapshot_compare(s1, s2); } std::shared_ptr LivenessChecker::insertAcceptancePair(simgrid::mc::Pair* pair) @@ -203,7 +200,7 @@ void LivenessChecker::replay() } /** - * \brief Checks whether a given pair has already been visited by the algorithm. + * @brief Checks whether a given pair has already been visited by the algorithm. */ int LivenessChecker::insertVisitedPair(std::shared_ptr visited_pair, simgrid::mc::Pair* pair) { @@ -252,7 +249,7 @@ void LivenessChecker::purgeVisitedPairs() } } -LivenessChecker::LivenessChecker(Session& session) : Checker(session) +LivenessChecker::LivenessChecker(Session& s) : Checker(s) { } @@ -266,7 +263,6 @@ RecordTrace LivenessChecker::getRecordTrace() // override void LivenessChecker::logState() // override { - Checker::logState(); XBT_INFO("Expanded pairs = %lu", expandedPairsCount_); XBT_INFO("Visited pairs = %lu", visitedPairsCount_); XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions); @@ -277,12 +273,12 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth) XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("Counter-example that violates formula :"); - simgrid::mc::dumpRecordPath(); + XBT_INFO("Counter-example that violates formula:"); for (auto const& s : this->getTextualTrace()) - XBT_INFO("%s", s.c_str()); + XBT_INFO(" %s", s.c_str()); + simgrid::mc::dumpRecordPath(); simgrid::mc::session->logState(); - XBT_INFO("Counter-example depth : %zu", depth); + XBT_INFO("Counter-example depth: %zu", depth); } std::vector LivenessChecker::getTextualTrace() // override @@ -301,7 +297,8 @@ std::vector LivenessChecker::getTextualTrace() // override std::shared_ptr LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state, std::shared_ptr> propositions) { - std::shared_ptr next_pair = std::make_shared(++expandedPairsCount_); + expandedPairsCount_++; + std::shared_ptr next_pair = std::make_shared(expandedPairsCount_); next_pair->automaton_state = state; next_pair->graph_state = std::shared_ptr(new simgrid::mc::State(++expandedStatesCount_)); next_pair->atomic_propositions = std::move(propositions); @@ -346,8 +343,8 @@ void LivenessChecker::backtrack() void LivenessChecker::run() { - XBT_INFO("Check the liveness property %s", _sg_mc_property_file); - MC_automaton_load(_sg_mc_property_file); + XBT_INFO("Check the liveness property %s", _sg_mc_property_file.get().c_str()); + MC_automaton_load(_sg_mc_property_file.get().c_str()); XBT_DEBUG("Starting the liveness algorithm"); simgrid::mc::session->initialize(); @@ -392,9 +389,8 @@ void LivenessChecker::run() } /* Pair already visited ? stop the exploration on the current path */ - int visited_num = -1; if (not current_pair->exploration_started) { - visited_num = this->insertVisitedPair(reached_pair, current_pair.get()); + int visited_num = this->insertVisitedPair(reached_pair, current_pair.get()); if (visited_num != -1) { if (dot_output != nullptr) { fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previousPair_, visited_num, @@ -448,8 +444,9 @@ void LivenessChecker::run() // For each enabled transition in the property automaton, push a // (application_state, automaton_state) pair to the exploration stack: - for (int cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1; cursor >= 0; cursor--) { - xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t); + for (int i = xbt_dynar_length(current_pair->automaton_state->out) - 1; i >= 0; i--) { + xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as( + current_pair->automaton_state->out, i, xbt_automaton_transition_t); if (evaluate_label(transition_succ->label, *prop_values)) explorationStack_.push_back(this->newPair( current_pair.get(), transition_succ->dst, prop_values)); @@ -461,9 +458,9 @@ void LivenessChecker::run() simgrid::mc::session->logState(); } -Checker* createLivenessChecker(Session& session) +Checker* createLivenessChecker(Session& s) { - return new LivenessChecker(session); + return new LivenessChecker(s); } }