X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2ccf9c22b2e9dee40858cb70a44763f4084e15da..7e05f459b976449ac397155eb30973ec2b425929:/src/mc/checker/LivenessChecker.cpp diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index b04c743a4b..34bdcbc588 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -10,12 +10,15 @@ #include "src/mc/mc_private.hpp" #include "src/mc/mc_request.hpp" #include "src/mc/mc_smx.hpp" +#include "src/mc/mc_api.hpp" #include #include XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification"); +using mcapi = simgrid::mc::mc_api; + /********* Static functions *********/ namespace simgrid { @@ -63,14 +66,14 @@ static bool evaluate_label(const xbt_automaton_exp_label* l, std::vector co case xbt_automaton_exp_label::AUT_ONE: return true; default: - xbt_die("Unexpected vaue for automaton"); + xbt_die("Unexpected value for automaton"); } } Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs) {} -std::shared_ptr> LivenessChecker::get_proposition_values() +std::shared_ptr> LivenessChecker::get_proposition_values() const { std::vector values; unsigned int cursor = 0; @@ -82,9 +85,8 @@ std::shared_ptr> LivenessChecker::get_proposition_values( std::shared_ptr LivenessChecker::insert_acceptance_pair(simgrid::mc::Pair* pair) { - std::shared_ptr new_pair = std::make_shared( - pair->num, pair->automaton_state, pair->atomic_propositions, - pair->graph_state); + auto new_pair = + std::make_shared(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state); auto res = boost::range::equal_range(acceptance_pairs_, new_pair.get(), DerefAndCompareByActorsCountAndUsedHeap()); @@ -145,16 +147,14 @@ void LivenessChecker::replay() smx_simcall_t req = nullptr; - if (saved_req != nullptr) { - /* because we got a copy of the executed request, we have to fetch the - real one, pointed by the request field of the issuer process */ - const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req); - req = &issuer->simcall_; + /* because we got a copy of the executed request, we have to fetch the + real one, pointed by the request field of the issuer process */ + const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req); + req = &issuer->simcall_; - /* Debug information */ - XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, - request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get()); - } + /* Debug information */ + XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, + request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get()); this->get_session().execute(state->transition_); } @@ -232,7 +232,7 @@ void LivenessChecker::log_state() // override { XBT_INFO("Expanded pairs = %lu", expanded_pairs_count_); XBT_INFO("Visited pairs = %lu", visited_pairs_count_); - XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions); + XBT_INFO("Executed transitions = %lu", mcapi::get().mc_get_executed_trans()); } void LivenessChecker::show_acceptance_cycle(std::size_t depth) @@ -243,8 +243,8 @@ void LivenessChecker::show_acceptance_cycle(std::size_t depth) XBT_INFO("Counter-example that violates formula:"); for (auto const& s : this->get_textual_trace()) XBT_INFO(" %s", s.c_str()); - mc::dumpRecordPath(); - mc::session->log_state(); + mcapi::get().dump_record_path(); + mcapi::get().log_state(); XBT_INFO("Counter-example depth: %zu", depth); } @@ -254,8 +254,8 @@ std::vector LivenessChecker::get_textual_trace() // override for (std::shared_ptr const& pair : exploration_stack_) { int req_num = pair->graph_state->transition_.argument_; smx_simcall_t req = &pair->graph_state->executed_req_; - if (req && req->call_ != SIMCALL_NONE) - trace.push_back(request_to_string(req, req_num, RequestType::executed)); + if (req->call_ != simix::Simcall::NONE) + trace.push_back(mcapi::get().request_to_string(req, req_num, RequestType::executed)); } return trace; } @@ -263,10 +263,11 @@ std::vector LivenessChecker::get_textual_trace() // override std::shared_ptr LivenessChecker::create_pair(const Pair* current_pair, xbt_automaton_state_t state, std::shared_ptr> propositions) { - expanded_pairs_count_++; - std::shared_ptr next_pair = std::make_shared(expanded_pairs_count_); + ++expanded_pairs_count_; + ++expanded_states_count_; + auto next_pair = std::make_shared(expanded_pairs_count_); next_pair->automaton_state = state; - next_pair->graph_state = std::shared_ptr(new State(++expanded_states_count_)); + next_pair->graph_state = std::make_shared(expanded_states_count_); next_pair->atomic_propositions = std::move(propositions); if (current_pair) next_pair->depth = current_pair->depth + 1; @@ -370,7 +371,7 @@ void LivenessChecker::run() } } - smx_simcall_t req = MC_state_choose_request(current_pair->graph_state.get()); + smx_simcall_t req = mcapi::get().mc_state_choose_request(current_pair->graph_state.get()); int req_num = current_pair->graph_state->transition_.argument_; if (dot_output != nullptr) { @@ -408,8 +409,8 @@ void LivenessChecker::run() // For each enabled transition in the property automaton, push a // (application_state, automaton_state) pair to the exploration stack: for (int i = xbt_dynar_length(current_pair->automaton_state->out) - 1; i >= 0; i--) { - const xbt_automaton_transition* transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as( - current_pair->automaton_state->out, i, xbt_automaton_transition_t); + const xbt_automaton_transition* transition_succ = + xbt_dynar_get_as(current_pair->automaton_state->out, i, xbt_automaton_transition_t); if (evaluate_label(transition_succ->label, *prop_values)) exploration_stack_.push_back(this->create_pair(current_pair.get(), transition_succ->dst, prop_values)); }