X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/bdef81fa4e3566ce31b435deb98fea7b8fe70e6e..ab92608267358b56adf7a803480fa2ad9608ed1b:/src/mc/checker/LivenessChecker.cpp diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index fc2ecb1eff..3a24b367e5 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -20,21 +20,20 @@ #include #include -#include "src/mc/mc_request.h" +#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_record.h" -#include "src/mc/mc_smx.h" -#include "src/mc/Client.hpp" #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_safety.h" -#include "src/mc/mc_exit.h" -#include "src/mc/Transition.hpp" -#include "src/mc/Session.hpp" +#include "src/mc/mc_smx.h" +#include "src/mc/remote/Client.hpp" -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, - "Logging specific to algorithms for liveness properties verification"); +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification"); /********* Static functions *********/ @@ -63,12 +62,7 @@ VisitedPair::VisitedPair( this->atomic_propositions = std::move(atomic_propositions); } -VisitedPair::~VisitedPair() -{ -} - -static bool evaluate_label( - xbt_automaton_exp_label_t l, std::vector const& values) +static bool evaluate_label(xbt_automaton_exp_label_t l, std::vector const& values) { switch (l->type) { case xbt_automaton_exp_label::AUT_OR: @@ -98,8 +92,6 @@ static bool evaluate_label( Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs) {} -Pair::~Pair() {} - std::shared_ptr> LivenessChecker::getPropositionValues() { std::vector values; @@ -135,13 +127,11 @@ std::shared_ptr LivenessChecker::insertAcceptancePair(simgrid::mc:: || *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) || this->compare(pair_test.get(), new_pair.get()) != 0) continue; - XBT_INFO("Pair %d already reached (equal to pair %d) !", - new_pair->num, pair_test->num); + XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num); explorationStack_.pop_back(); if (dot_output != nullptr) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - this->previousPair_, pair_test->num, - this->previousRequest_.c_str()); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previousPair_, pair_test->num, + this->previousRequest_.c_str()); return nullptr; } @@ -158,22 +148,6 @@ void LivenessChecker::removeAcceptancePair(int pair_num) } } -void LivenessChecker::prepare(void) -{ - this->previousPair_ = 0; - - std::shared_ptr> propos = this->getPropositionValues(); - - // For each initial state of the property automaton, push a - // (application_state, automaton_state) pair to the exploration stack: - unsigned int cursor = 0; - xbt_automaton_state_t automaton_state; - xbt_dynar_foreach(simgrid::mc::property_automaton->states, cursor, automaton_state) - if (automaton_state->type == -1) - explorationStack_.push_back(this->newPair(nullptr, automaton_state, propos)); -} - - void LivenessChecker::replay() { XBT_DEBUG("**** Begin Replay ****"); @@ -238,13 +212,12 @@ void LivenessChecker::replay() */ int LivenessChecker::insertVisitedPair(std::shared_ptr visited_pair, simgrid::mc::Pair* pair) { - if (_sg_mc_visited == 0) + if (_sg_mc_max_visited_states == 0) return -1; if (visited_pair == nullptr) - visited_pair = std::make_shared( - pair->num, pair->automaton_state, pair->atomic_propositions, - pair->graph_state); + visited_pair = + std::make_shared(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state); auto range = boost::range::equal_range(visitedPairs_, visited_pair.get(), simgrid::mc::DerefAndCompareByActorsCountAndUsedHeap()); @@ -276,7 +249,7 @@ int LivenessChecker::insertVisitedPair(std::shared_ptr visited_pair void LivenessChecker::purgeVisitedPairs() { - if (_sg_mc_visited != 0 && visitedPairs_.size() > (std::size_t) _sg_mc_visited) { + if (_sg_mc_max_visited_states != 0 && visitedPairs_.size() > (std::size_t)_sg_mc_max_visited_states) { // Remove the oldest entry with a linear search: visitedPairs_.erase(boost::min_element(visitedPairs_, [](std::shared_ptr const a, std::shared_ptr const& b) { @@ -288,10 +261,6 @@ LivenessChecker::LivenessChecker(Session& session) : Checker(session) { } -LivenessChecker::~LivenessChecker() -{ -} - RecordTrace LivenessChecker::getRecordTrace() // override { RecordTrace res; @@ -334,8 +303,74 @@ std::vector LivenessChecker::getTextualTrace() // override return trace; } -int LivenessChecker::main(void) +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_); + next_pair->automaton_state = state; + next_pair->graph_state = std::shared_ptr(new simgrid::mc::State(++expandedStatesCount_)); + next_pair->atomic_propositions = std::move(propositions); + if (current_pair) + next_pair->depth = current_pair->depth + 1; + else + next_pair->depth = 1; + /* Get enabled actors and insert them in the interleave set of the next graph_state */ + for (auto& actor : mc_model_checker->process().actors()) + if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) + next_pair->graph_state->interleave(actor.copy.getBuffer()); + next_pair->requests = next_pair->graph_state->interleaveSize(); + /* FIXME : get search_cycle value for each accepting state */ + if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle)) + next_pair->search_cycle = true; + else + next_pair->search_cycle = false; + return next_pair; +} + +void LivenessChecker::backtrack() { + /* Traverse the stack backwards until a pair with a non empty interleave + set is found, deleting all the pairs that have it empty in the way. */ + while (!explorationStack_.empty()) { + std::shared_ptr current_pair = explorationStack_.back(); + explorationStack_.pop_back(); + if (current_pair->requests > 0) { + /* We found a backtracking point */ + XBT_DEBUG("Backtracking to depth %d", current_pair->depth); + explorationStack_.push_back(std::move(current_pair)); + this->replay(); + XBT_DEBUG("Backtracking done"); + break; + } else { + XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth); + if (current_pair->automaton_state->type == 1) + this->removeAcceptancePair(current_pair->num); + } + } +} + +void LivenessChecker::run() +{ + XBT_INFO("Check the liveness property %s", _sg_mc_property_file); + MC_automaton_load(_sg_mc_property_file); + + XBT_DEBUG("Starting the liveness algorithm"); + simgrid::mc::session->initialize(); + + /* Initialize */ + this->previousPair_ = 0; + + std::shared_ptr> propos = this->getPropositionValues(); + + // For each initial state of the property automaton, push a + // (application_state, automaton_state) pair to the exploration stack: + unsigned int cursor = 0; + xbt_automaton_state_t automaton_state; + xbt_dynar_foreach (simgrid::mc::property_automaton->states, cursor, automaton_state) + if (automaton_state->type == -1) + explorationStack_.push_back(this->newPair(nullptr, automaton_state, propos)); + + /* Actually run the double DFS search for counter-examples */ while (!explorationStack_.empty()){ std::shared_ptr current_pair = explorationStack_.back(); @@ -357,7 +392,7 @@ int LivenessChecker::main(void) if (current_pair->automaton_state->type == 1 && !current_pair->exploration_started && (reached_pair = this->insertAcceptancePair(current_pair.get())) == nullptr) { this->showAcceptanceCycle(current_pair->depth); - return SIMGRID_MC_EXIT_LIVENESS; + throw simgrid::mc::LivenessError(); } /* Pair already visited ? stop the exploration on the current path */ @@ -417,80 +452,17 @@ int LivenessChecker::main(void) // For each enabled transition in the property automaton, push a // (application_state, automaton_state) pair to the exploration stack: - int cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1; - while (cursor >= 0) { + 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); if (evaluate_label(transition_succ->label, *prop_values)) explorationStack_.push_back(this->newPair( current_pair.get(), transition_succ->dst, prop_values)); - cursor--; } } XBT_INFO("No property violation found."); simgrid::mc::session->logState(); - return SIMGRID_MC_EXIT_SUCCESS; -} - -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_); - next_pair->automaton_state = state; - next_pair->graph_state = std::shared_ptr(new simgrid::mc::State(++expandedStatesCount_)); - next_pair->atomic_propositions = std::move(propositions); - if (current_pair) - next_pair->depth = current_pair->depth + 1; - else - next_pair->depth = 1; - /* Get enabled actors and insert them in the interleave set of the next graph_state */ - for (auto& actor : mc_model_checker->process().actors()) - if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) - next_pair->graph_state->interleave(actor.copy.getBuffer()); - next_pair->requests = next_pair->graph_state->interleaveSize(); - /* FIXME : get search_cycle value for each accepting state */ - if (next_pair->automaton_state->type == 1 || - (current_pair && current_pair->search_cycle)) - next_pair->search_cycle = true; - else - next_pair->search_cycle = false; - return next_pair; -} - -void LivenessChecker::backtrack() -{ - /* Traverse the stack backwards until a pair with a non empty interleave - set is found, deleting all the pairs that have it empty in the way. */ - while (!explorationStack_.empty()) { - std::shared_ptr current_pair = explorationStack_.back(); - explorationStack_.pop_back(); - if (current_pair->requests > 0) { - /* We found a backtracking point */ - XBT_DEBUG("Backtracking to depth %d", current_pair->depth); - explorationStack_.push_back(std::move(current_pair)); - this->replay(); - XBT_DEBUG("Backtracking done"); - break; - } else { - XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth); - if (current_pair->automaton_state->type == 1) - this->removeAcceptancePair(current_pair->num); - } - } -} - -int LivenessChecker::run() -{ - XBT_INFO("Check the liveness property %s", _sg_mc_property_file); - MC_automaton_load(_sg_mc_property_file); - - XBT_DEBUG("Starting the liveness algorithm"); - simgrid::mc::session->initialize(); - this->prepare(); - - int res = this->main(); - - return res; } Checker* createLivenessChecker(Session& session)