X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/7f626fa7e7d9a7d28fdc994ae197f82f0a0c6e52..239cd16f4e95031d3a106e487c1485726069f1d7:/src/mc/explo/LivenessChecker.cpp diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp index 26fb2a8de3..370a146d0b 100644 --- a/src/mc/explo/LivenessChecker.cpp +++ b/src/mc/explo/LivenessChecker.cpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2011-2022. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2011-2023. 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. */ @@ -19,13 +19,15 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms namespace simgrid::mc { VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t prop_state, - std::shared_ptr> atomic_propositions, std::shared_ptr app_state) + std::shared_ptr> atomic_propositions, std::shared_ptr app_state, + RemoteApp& remote_app) : num(pair_num), prop_state_(prop_state) { + auto& memory = mc_model_checker->get_remote_process_memory(); this->app_state_ = std::move(app_state); if (not this->app_state_->get_system_state()) - this->app_state_->set_system_state(std::make_shared(pair_num)); - this->heap_bytes_used = mc_model_checker->get_remote_process().get_remote_heap_bytes(); + this->app_state_->set_system_state(std::make_shared(pair_num, remote_app.get_page_store(), memory)); + this->heap_bytes_used = memory.get_remote_heap_bytes(); this->actor_count_ = app_state_->get_actor_count(); this->other_num = -1; this->atomic_propositions = std::move(atomic_propositions); @@ -59,8 +61,8 @@ std::shared_ptr> LivenessChecker::get_proposition_values( std::shared_ptr LivenessChecker::insert_acceptance_pair(simgrid::mc::Pair* pair) { - auto new_pair = - std::make_shared(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_); + auto new_pair = std::make_shared(pair->num, pair->prop_state_, pair->atomic_propositions, + pair->app_state_, get_remote_app()); auto [res_begin, res_end] = boost::range::equal_range(acceptance_pairs_, new_pair.get(), [](auto const& a, auto const& b) { @@ -76,8 +78,7 @@ std::shared_ptr LivenessChecker::insert_acceptance_pair(simgrid::mc continue; XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num); exploration_stack_.pop_back(); - mc_model_checker->dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num, - this->previous_request_.c_str()); + dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num, this->previous_request_.c_str()); return nullptr; } @@ -102,7 +103,7 @@ void LivenessChecker::replay() if (_sg_mc_checkpoint > 0) { const Pair* pair = exploration_stack_.back().get(); if (const auto* system_state = pair->app_state_->get_system_state()) { - system_state->restore(&get_remote_app().get_remote_process()); + system_state->restore(get_remote_app().get_remote_process_memory()); return; } } @@ -138,8 +139,8 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr visited_pa return -1; if (visited_pair == nullptr) - visited_pair = - std::make_shared(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_); + visited_pair = std::make_shared(pair->num, pair->prop_state_, pair->atomic_propositions, + pair->app_state_, get_remote_app()); auto [range_begin, range_end] = boost::range::equal_range(visited_pairs_, visited_pair.get(), [](auto const& a, auto const& b) { @@ -180,13 +181,12 @@ void LivenessChecker::purge_visited_pairs() LivenessChecker::LivenessChecker(const std::vector& args) : Exploration(args) {} LivenessChecker::~LivenessChecker() { - if (property_automaton_ != nullptr) - xbt_automaton_free(property_automaton_); + xbt_automaton_free(property_automaton_); } xbt_automaton_t LivenessChecker::property_automaton_ = nullptr; -void LivenessChecker::automaton_load(const char* file) +void LivenessChecker::automaton_load(const char* file) const { if (property_automaton_ == nullptr) property_automaton_ = xbt_automaton_new(); @@ -242,7 +242,8 @@ xbt_automaton_state_t LivenessChecker::get_automaton_transition_dst(xbt_dynar_t const xbt_automaton_transition* transition = xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t); return transition->dst; } -void LivenessChecker::automaton_register_symbol(RemoteProcess& remote_process, const char* name, RemotePtr address) +void LivenessChecker::automaton_register_symbol(RemoteProcessMemory const& remote_process, const char* name, + RemotePtr address) { if (property_automaton_ == nullptr) property_automaton_ = xbt_automaton_new(); @@ -275,7 +276,9 @@ 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()); - XBT_INFO("Path = %s", get_record_trace().to_string().c_str()); + XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with " + "--cfg=model-check/replay:'%s'", + get_record_trace().to_string().c_str()); log_state(); XBT_INFO("Counter-example depth: %zu", depth); } @@ -387,9 +390,7 @@ void LivenessChecker::run() if (not current_pair->exploration_started) { int visited_num = this->insert_visited_pair(reached_pair, current_pair.get()); if (visited_num != -1) { - mc_model_checker->dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, visited_num, - this->previous_request_.c_str()); - mc_model_checker->dot_output_flush(); + dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, visited_num, this->previous_request_.c_str()); XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num); current_pair->requests = 0; @@ -398,20 +399,18 @@ void LivenessChecker::run() } } - current_pair->app_state_->execute_next(current_pair->app_state_->next_transition()); + current_pair->app_state_->execute_next(current_pair->app_state_->next_transition(), get_remote_app()); XBT_DEBUG("Execute: %s", current_pair->app_state_->get_transition()->to_string().c_str()); /* Update the dot output */ if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) { - mc_model_checker->dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, current_pair->num, - this->previous_request_.c_str()); + dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, current_pair->num, this->previous_request_.c_str()); this->previous_request_.clear(); } this->previous_pair_ = current_pair->num; this->previous_request_ = current_pair->app_state_->get_transition()->dot_string(); if (current_pair->search_cycle) - mc_model_checker->dot_output("%d [shape=doublecircle];\n", current_pair->num); - mc_model_checker->dot_output_flush(); + dot_output("%d [shape=doublecircle];\n", current_pair->num); if (not current_pair->exploration_started) visited_pairs_count_++;