From fc9d6a3bc4dab9c5c44889fb35deb6cd72541fd8 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sat, 30 Jul 2022 18:11:44 +0200 Subject: [PATCH] Liveness: rename graph_state -> app_state and automaton_state -> prop_state --- src/mc/explo/LivenessChecker.cpp | 72 ++++++++++++++++---------------- src/mc/explo/LivenessChecker.hpp | 16 +++---- 2 files changed, 43 insertions(+), 45 deletions(-) diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp index cc418c5704..fb8d9f3387 100644 --- a/src/mc/explo/LivenessChecker.cpp +++ b/src/mc/explo/LivenessChecker.cpp @@ -18,14 +18,13 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms namespace simgrid::mc { -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) +VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t prop_state, + std::shared_ptr> atomic_propositions, std::shared_ptr app_state) + : num(pair_num), prop_state_(prop_state) { - this->graph_state = std::move(graph_state); - if (not this->graph_state->get_system_state()) - this->graph_state->set_system_state(std::make_shared(pair_num)); + 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 = Api::get().get_remote_heap_bytes(); this->actor_count_ = mc_model_checker->get_remote_process().actors().size(); this->other_num = -1; @@ -61,17 +60,17 @@ 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->automaton_state, pair->atomic_propositions, pair->graph_state); + std::make_shared(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_); auto [res_begin, res_end] = boost::range::equal_range(acceptance_pairs_, new_pair.get(), Api::get().compare_pair()); if (pair->search_cycle) for (auto i = res_begin; i != res_end; ++i) { std::shared_ptr const& pair_test = *i; - if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) != 0 || + if (xbt_automaton_state_compare(pair_test->prop_state_, new_pair->prop_state_) != 0 || *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) || - not Api::get().snapshot_equal(pair_test->graph_state->get_system_state(), - new_pair->graph_state->get_system_state())) + not Api::get().snapshot_equal(pair_test->app_state_->get_system_state(), + new_pair->app_state_->get_system_state())) continue; XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num); exploration_stack_.pop_back(); @@ -101,7 +100,7 @@ void LivenessChecker::replay() /* Intermediate backtracking */ if (_sg_mc_checkpoint > 0) { const Pair* pair = exploration_stack_.back().get(); - if (const auto* system_state = pair->graph_state->get_system_state()) { + if (const auto* system_state = pair->app_state_->get_system_state()) { Api::get().restore_state(system_state); return; } @@ -115,7 +114,7 @@ void LivenessChecker::replay() if (pair == exploration_stack_.back()) break; - std::shared_ptr state = pair->graph_state; + std::shared_ptr state = pair->app_state_; if (pair->exploration_started) { state->get_transition()->replay(); @@ -139,17 +138,17 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr visited_pa if (visited_pair == nullptr) visited_pair = - std::make_shared(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state); + std::make_shared(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_); auto [range_begin, range_end] = boost::range::equal_range(visited_pairs_, visited_pair.get(), Api::get().compare_pair()); for (auto i = range_begin; i != range_end; ++i) { const VisitedPair* pair_test = i->get(); - if (xbt_automaton_state_compare(pair_test->automaton_state, visited_pair->automaton_state) != 0 || + if (xbt_automaton_state_compare(pair_test->prop_state_, visited_pair->prop_state_) != 0 || *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) || - not Api::get().snapshot_equal(pair_test->graph_state->get_system_state(), - visited_pair->graph_state->get_system_state())) + not Api::get().snapshot_equal(pair_test->app_state_->get_system_state(), + visited_pair->app_state_->get_system_state())) continue; if (pair_test->other_num == -1) visited_pair->other_num = pair_test->num; @@ -185,7 +184,7 @@ RecordTrace LivenessChecker::get_record_trace() // override { RecordTrace res; for (std::shared_ptr const& pair : exploration_stack_) - res.push_back(pair->graph_state->get_transition()); + res.push_back(pair->app_state_->get_transition()); return res; } @@ -213,7 +212,7 @@ std::vector LivenessChecker::get_textual_trace() // override { std::vector trace; for (std::shared_ptr const& pair : exploration_stack_) - trace.push_back(pair->graph_state->get_transition()->to_string()); + trace.push_back(pair->app_state_->get_transition()->to_string()); return trace; } @@ -223,21 +222,21 @@ std::shared_ptr LivenessChecker::create_pair(const Pair* current_pair, xbt { ++expanded_pairs_count_; auto next_pair = std::make_shared(expanded_pairs_count_); - next_pair->automaton_state = state; - next_pair->graph_state = std::make_shared(get_session()); + next_pair->prop_state_ = state; + next_pair->app_state_ = std::make_shared(get_session()); next_pair->atomic_propositions = std::move(propositions); if (current_pair) next_pair->depth = current_pair->depth + 1; else next_pair->depth = 1; /* Add all enabled actors to the interleave set of the initial state */ - for (auto const& [aid, _] : next_pair->graph_state->get_actors_list()) - if (next_pair->graph_state->is_actor_enabled(aid)) - next_pair->graph_state->mark_todo(aid); + for (auto const& [aid, _] : next_pair->app_state_->get_actors_list()) + if (next_pair->app_state_->is_actor_enabled(aid)) + next_pair->app_state_->mark_todo(aid); - next_pair->requests = next_pair->graph_state->count_todo(); + next_pair->requests = next_pair->app_state_->count_todo(); /* FIXME : get search_cycle value for each accepting state */ - if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle)) + if (next_pair->prop_state_->type == 1 || (current_pair && current_pair->search_cycle)) next_pair->search_cycle = true; else next_pair->search_cycle = false; @@ -260,7 +259,7 @@ void LivenessChecker::backtrack() break; } else { XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth); - if (current_pair->automaton_state->type == 1) + if (current_pair->prop_state_->type == 1) this->remove_acceptance_pair(current_pair->num); } } @@ -292,11 +291,11 @@ void LivenessChecker::run() std::shared_ptr current_pair = exploration_stack_.back(); /* Update current state in buchi automaton */ - Api::get().set_property_automaton(current_pair->automaton_state); + Api::get().set_property_automaton(current_pair->prop_state_); 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->count_todo(), current_pair->num, + current_pair->depth, current_pair->search_cycle, current_pair->app_state_->count_todo(), current_pair->num, current_pair->requests); if (current_pair->requests == 0) { @@ -305,7 +304,7 @@ void LivenessChecker::run() } std::shared_ptr reached_pair; - if (current_pair->automaton_state->type == 1 && not current_pair->exploration_started) { + if (current_pair->prop_state_->type == 1 && not current_pair->exploration_started) { reached_pair = this->insert_acceptance_pair(current_pair.get()); if (reached_pair == nullptr) { this->show_acceptance_cycle(current_pair->depth); @@ -329,8 +328,8 @@ void LivenessChecker::run() } } - current_pair->graph_state->execute_next(current_pair->graph_state->next_transition()); - XBT_DEBUG("Execute: %s", current_pair->graph_state->get_transition()->to_string().c_str()); + current_pair->app_state_->execute_next(current_pair->app_state_->next_transition()); + XBT_DEBUG("Execute: %s", current_pair->app_state_->get_transition()->to_string().c_str()); if (dot_output != nullptr) { if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) { @@ -339,7 +338,7 @@ void LivenessChecker::run() this->previous_request_.clear(); } this->previous_pair_ = current_pair->num; - this->previous_request_ = current_pair->graph_state->get_transition()->dot_string(); + this->previous_request_ = current_pair->app_state_->get_transition()->dot_string(); if (current_pair->search_cycle) fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num); fflush(dot_output); @@ -356,10 +355,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 i = xbt_dynar_length(current_pair->automaton_state->out) - 1; i >= 0; i--) { - const auto* transition_succ_label = - Api::get().get_automaton_transition_label(current_pair->automaton_state->out, i); - auto* transition_succ_dst = Api::get().get_automaton_transition_dst(current_pair->automaton_state->out, i); + for (int i = xbt_dynar_length(current_pair->prop_state_->out) - 1; i >= 0; i--) { + const auto* transition_succ_label = Api::get().get_automaton_transition_label(current_pair->prop_state_->out, i); + auto* transition_succ_dst = Api::get().get_automaton_transition_dst(current_pair->prop_state_->out, i); if (evaluate_label(transition_succ_label, *prop_values)) exploration_stack_.push_back(this->create_pair(current_pair.get(), transition_succ_dst, prop_values)); } diff --git a/src/mc/explo/LivenessChecker.hpp b/src/mc/explo/LivenessChecker.hpp index a783d46b62..09e8a6041e 100644 --- a/src/mc/explo/LivenessChecker.hpp +++ b/src/mc/explo/LivenessChecker.hpp @@ -19,10 +19,10 @@ namespace simgrid::mc { class XBT_PRIVATE Pair { public: - int num = 0; - bool search_cycle = false; - std::shared_ptr graph_state = nullptr; /* System state included */ - xbt_automaton_state_t automaton_state = nullptr; + int num = 0; + bool search_cycle = false; + std::shared_ptr app_state_ = nullptr; /* State of the application (including system state) */ + xbt_automaton_state_t prop_state_ = nullptr; /* State of the property automaton */ std::shared_ptr> atomic_propositions; int requests = 0; int depth = 0; @@ -38,14 +38,14 @@ class XBT_PRIVATE VisitedPair { public: int num; int other_num = 0; /* Dot output for */ - std::shared_ptr graph_state = nullptr; /* System state included */ - xbt_automaton_state_t automaton_state; + std::shared_ptr app_state_ = nullptr; /* State of the application (including system state) */ + xbt_automaton_state_t prop_state_; /* State of the property automaton */ std::shared_ptr> atomic_propositions; std::size_t heap_bytes_used = 0; int actor_count_; - VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, - std::shared_ptr> atomic_propositions, std::shared_ptr graph_state); + VisitedPair(int pair_num, xbt_automaton_state_t prop_state, + std::shared_ptr> atomic_propositions, std::shared_ptr app_state); }; class XBT_PRIVATE LivenessChecker : public Exploration { -- 2.20.1