From 3a70f3d43980112b067cf0f51a8327bdccaf5ef9 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Mon, 4 Apr 2016 10:30:21 +0200 Subject: [PATCH] [mc] Use shared_ptr for liveness propositions --- src/mc/LivenessChecker.cpp | 27 +++++++++++++++------------ src/mc/LivenessChecker.hpp | 10 +++++----- 2 files changed, 20 insertions(+), 17 deletions(-) diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index abf36efed1..e41d3f54fd 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -40,7 +40,8 @@ namespace mc { VisitedPair::VisitedPair( int pair_num, xbt_automaton_state_t automaton_state, - std::vector const& atomic_propositions, std::shared_ptr graph_state) + std::shared_ptr> atomic_propositions, + std::shared_ptr graph_state) { simgrid::mc::Process* process = &(mc_model_checker->process()); @@ -56,7 +57,7 @@ VisitedPair::VisitedPair( this->automaton_state = automaton_state; this->num = pair_num; this->other_num = -1; - this->atomic_propositions = atomic_propositions; + this->atomic_propositions = std::move(atomic_propositions); } VisitedPair::~VisitedPair() @@ -96,14 +97,14 @@ Pair::Pair() : num(++mc_stats->expanded_pairs) Pair::~Pair() {} -std::vector LivenessChecker::getPropositionValues() +std::shared_ptr> LivenessChecker::getPropositionValues() { std::vector values; unsigned int cursor = 0; xbt_automaton_propositional_symbol_t ps = nullptr; xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, ps) values.push_back(xbt_automaton_propositional_symbol_evaluate(ps)); - return values; + return std::make_shared>(std::move(values)); } int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2) @@ -128,7 +129,7 @@ std::shared_ptr LivenessChecker::insertAcceptancePair(simgrid::mc:: std::shared_ptr const& pair_test = *i; if (xbt_automaton_state_compare( pair_test->automaton_state, new_pair->automaton_state) != 0 - || pair_test->atomic_propositions != new_pair->atomic_propositions + || *(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) !", @@ -160,13 +161,15 @@ void LivenessChecker::prepare(void) initial_global_state->snapshot = simgrid::mc::take_snapshot(0); initial_global_state->prev_pair = 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)); + explorationStack_.push_back(this->newPair(nullptr, automaton_state, propos)); } @@ -251,7 +254,7 @@ int LivenessChecker::insertVisitedPair(std::shared_ptr visited_pair VisitedPair* pair_test = i->get(); if (xbt_automaton_state_compare( pair_test->automaton_state, visited_pair->automaton_state) != 0 - || pair_test->atomic_propositions != visited_pair->atomic_propositions + || *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) || this->compare(pair_test, visited_pair.get()) != 0) continue; if (pair_test->other_num == -1) @@ -411,16 +414,16 @@ int LivenessChecker::main(void) current_pair->exploration_started = true; /* Get values of atomic propositions (variables used in the property formula) */ - std::vector prop_values = this->getPropositionValues(); + std::shared_ptr> prop_values = this->getPropositionValues(); // 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) { 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)) + if (evaluate_label(transition_succ->label, *prop_values)) explorationStack_.push_back(this->newPair( - current_pair.get(), transition_succ->dst)); + current_pair.get(), transition_succ->dst, prop_values)); cursor--; } @@ -431,12 +434,12 @@ int LivenessChecker::main(void) return SIMGRID_MC_EXIT_SUCCESS; } -std::shared_ptr LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state) +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(); next_pair->automaton_state = state; next_pair->graph_state = std::shared_ptr(MC_state_new()); - next_pair->atomic_propositions = this->getPropositionValues(); + next_pair->atomic_propositions = std::move(propositions); if (current_pair) next_pair->depth = current_pair->depth + 1; else diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp index f12c0b3be1..18c32a0372 100644 --- a/src/mc/LivenessChecker.hpp +++ b/src/mc/LivenessChecker.hpp @@ -34,7 +34,7 @@ struct XBT_PRIVATE Pair { bool search_cycle = false; std::shared_ptr graph_state = nullptr; /* System state included */ xbt_automaton_state_t automaton_state = nullptr; - std::vector atomic_propositions; + std::shared_ptr> atomic_propositions; int requests = 0; int depth = 0; bool exploration_started = false; @@ -51,13 +51,13 @@ struct XBT_PRIVATE VisitedPair { int other_num = 0; /* Dot output for */ std::shared_ptr graph_state = nullptr; /* System state included */ xbt_automaton_state_t automaton_state = nullptr; - std::vector atomic_propositions; + std::shared_ptr> atomic_propositions; std::size_t heap_bytes_used = 0; int nb_processes = 0; VisitedPair( int pair_num, xbt_automaton_state_t automaton_state, - std::vector const& atomic_propositions, + std::shared_ptr> atomic_propositions, std::shared_ptr graph_state); ~VisitedPair(); }; @@ -73,7 +73,7 @@ private: int main(); void prepare(); int compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2); - std::vector getPropositionValues(); + std::shared_ptr> getPropositionValues(); std::shared_ptr insertAcceptancePair(simgrid::mc::Pair* pair); int insertVisitedPair(std::shared_ptr visited_pair, simgrid::mc::Pair* pair); void showAcceptanceCycle(std::size_t depth); @@ -81,7 +81,7 @@ private: void removeAcceptancePair(int pair_num); void purgeVisitedPairs(); void backtrack(); - std::shared_ptr newPair(Pair* pair, xbt_automaton_state_t state); + std::shared_ptr newPair(Pair* pair, xbt_automaton_state_t state, std::shared_ptr> propositions); public: // A stack of (application_state, automaton_state) pairs for DFS exploration: std::list> explorationStack_; -- 2.20.1