X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/f12d544431f7dd3889e91793f35fec12e3ff2fa7..100576aab36daab0f4674d9a6c1044925bc8853c:/src/mc/checker/LivenessChecker.cpp diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index 487762aef3..3ff91d3e51 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2011-2015. The SimGrid Team. +/* Copyright (c) 2011-2017. The SimGrid Team. * All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it @@ -20,53 +20,44 @@ #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_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_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.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_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"); +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification"); /********* Static functions *********/ namespace simgrid { namespace mc { -VisitedPair::VisitedPair( - int pair_num, xbt_automaton_state_t automaton_state, - std::shared_ptr> atomic_propositions, - std::shared_ptr graph_state) +VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, + std::shared_ptr> atomic_propositions, + std::shared_ptr graph_state) + : num(pair_num), automaton_state(automaton_state) { - simgrid::mc::Process* process = &(mc_model_checker->process()); + simgrid::mc::RemoteClient* process = &(mc_model_checker->process()); this->graph_state = std::move(graph_state); if(this->graph_state->system_state == nullptr) this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num); - this->heap_bytes_used = mmalloc_get_bytes_used_remote( - process->get_heap()->heaplimit, - process->get_malloc_info()); + this->heap_bytes_used = mmalloc_get_bytes_used_remote(process->get_heap()->heaplimit, process->get_malloc_info()); this->actors_count = mc_model_checker->process().actors().size(); - this->automaton_state = automaton_state; - this->num = pair_num; this->other_num = -1; this->atomic_propositions = std::move(atomic_propositions); } -VisitedPair::~VisitedPair() = default; - -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: @@ -76,7 +67,7 @@ static bool evaluate_label( return evaluate_label(l->u.or_and.left_exp, values) && evaluate_label(l->u.or_and.right_exp, values); case xbt_automaton_exp_label::AUT_NOT: - return !evaluate_label(l->u.exp_not, values); + return not evaluate_label(l->u.exp_not, values); case xbt_automaton_exp_label::AUT_PREDICAT:{ unsigned int cursor = 0; xbt_automaton_propositional_symbol_t p = nullptr; @@ -85,6 +76,7 @@ static bool evaluate_label( return values[cursor] != 0; } xbt_die("Missing predicate"); + break; } case xbt_automaton_exp_label::AUT_ONE: return true; @@ -96,8 +88,6 @@ static bool evaluate_label( Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs) {} -Pair::~Pair() {} - std::shared_ptr> LivenessChecker::getPropositionValues() { std::vector values; @@ -133,13 +123,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; } @@ -220,13 +208,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()); @@ -258,7 +245,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) { @@ -270,10 +257,6 @@ LivenessChecker::LivenessChecker(Session& session) : Checker(session) { } -LivenessChecker::~LivenessChecker() -{ -} - RecordTrace LivenessChecker::getRecordTrace() // override { RecordTrace res; @@ -284,7 +267,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); @@ -297,10 +279,10 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth) XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("Counter-example that violates formula :"); simgrid::mc::dumpRecordPath(); - for (auto& s : this->getTextualTrace()) + for (auto const& s : this->getTextualTrace()) XBT_INFO("%s", s.c_str()); simgrid::mc::session->logState(); - XBT_INFO("Counter-example depth : %zd", depth); + XBT_INFO("Counter-example depth : %zu", depth); } std::vector LivenessChecker::getTextualTrace() // override @@ -319,7 +301,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); @@ -330,7 +313,7 @@ std::shared_ptr LivenessChecker::newPair(Pair* current_pair, xbt_automaton /* 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->graph_state->addInterleavingSet(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)) @@ -344,7 +327,7 @@ 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()) { + while (not explorationStack_.empty()) { std::shared_ptr current_pair = explorationStack_.back(); explorationStack_.pop_back(); if (current_pair->requests > 0) { @@ -384,17 +367,16 @@ void LivenessChecker::run() explorationStack_.push_back(this->newPair(nullptr, automaton_state, propos)); /* Actually run the double DFS search for counter-examples */ - while (!explorationStack_.empty()){ + while (not explorationStack_.empty()) { std::shared_ptr current_pair = explorationStack_.back(); /* Update current state in buchi automaton */ simgrid::mc::property_automaton->current_state = current_pair->automaton_state; - XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size = %zd, pair_num = %d, requests = %d)", - current_pair->depth, current_pair->search_cycle, - current_pair->graph_state->interleaveSize(), - current_pair->num, - current_pair->requests); + XBT_DEBUG( + "********************* ( Depth = %d, search_cycle = %d, interleave size = %zu, pair_num = %d, requests = %d)", + current_pair->depth, current_pair->search_cycle, current_pair->graph_state->interleaveSize(), current_pair->num, + current_pair->requests); if (current_pair->requests == 0) { this->backtrack(); @@ -402,27 +384,28 @@ void LivenessChecker::run() } std::shared_ptr reached_pair; - if (current_pair->automaton_state->type == 1 && !current_pair->exploration_started - && (reached_pair = this->insertAcceptancePair(current_pair.get())) == nullptr) { - this->showAcceptanceCycle(current_pair->depth); - throw simgrid::mc::LivenessError(); + if (current_pair->automaton_state->type == 1 && not current_pair->exploration_started) { + reached_pair = this->insertAcceptancePair(current_pair.get()); + if (reached_pair == nullptr) { + this->showAcceptanceCycle(current_pair->depth); + throw simgrid::mc::LivenessError(); + } } /* Pair already visited ? stop the exploration on the current path */ - int visited_num = -1; - if ((!current_pair->exploration_started) - && (visited_num = this->insertVisitedPair( - reached_pair, current_pair.get())) != -1) { - if (dot_output != nullptr){ - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - this->previousPair_, visited_num, - this->previousRequest_.c_str()); - fflush(dot_output); + if (not current_pair->exploration_started) { + 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, + this->previousRequest_.c_str()); + fflush(dot_output); + } + XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num); + current_pair->requests = 0; + this->backtrack(); + continue; } - XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num); - current_pair->requests = 0; - this->backtrack(); - continue; } smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get()); @@ -448,7 +431,7 @@ void LivenessChecker::run() /* Update stats */ mc_model_checker->executed_transitions++; - if (!current_pair->exploration_started) + if (not current_pair->exploration_started) visitedPairsCount_++; /* Answer the request */ @@ -465,13 +448,11 @@ void LivenessChecker::run() // 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--; } }