From 7215139acf8ac34d2b9cc0de4baba96fbbd64171 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Fri, 1 Apr 2016 11:47:55 +0200 Subject: [PATCH] [mc] Factor out Livenesschecker::newPair() --- src/mc/LivenessChecker.cpp | 78 +++++++++++++++++--------------------- src/mc/LivenessChecker.hpp | 1 + 2 files changed, 35 insertions(+), 44 deletions(-) diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index 16494c8476..c1ceaabb8c 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -157,33 +157,16 @@ void LivenessChecker::removeAcceptancePair(int pair_num) void LivenessChecker::prepare(void) { mc_model_checker->wait_for_requests(); - initial_global_state->snapshot = simgrid::mc::take_snapshot(0); initial_global_state->prev_pair = 0; + // 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) { /* Initial automaton state */ - - std::shared_ptr initial_pair = std::make_shared(); - initial_pair->automaton_state = automaton_state; - initial_pair->graph_state = std::shared_ptr(MC_state_new()); - initial_pair->atomic_propositions = this->getPropositionValues(); - initial_pair->depth = 1; - - /* Get enabled processes and insert them in the interleave set of the graph_state */ - for (auto& p : mc_model_checker->process().simix_processes()) - if (simgrid::mc::process_is_enabled(&p.copy)) - MC_state_interleave_process(initial_pair->graph_state.get(), &p.copy); - - initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state.get()); - initial_pair->search_cycle = false; - - livenessStack_.push_back(std::move(initial_pair)); - } - } + xbt_dynar_foreach(simgrid::mc::property_automaton->states, cursor, automaton_state) + if (automaton_state->type == -1) + livenessStack_.push_back(this->newPair(nullptr, automaton_state)); } @@ -430,31 +413,14 @@ int LivenessChecker::main(void) /* Get values of atomic propositions (variables used in the property formula) */ std::vector prop_values = this->getPropositionValues(); - /* Evaluate enabled/true transitions in automaton according to atomic propositions values and create new pairs */ + // 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)) { - std::shared_ptr next_pair = std::make_shared(); - next_pair->graph_state = std::shared_ptr(MC_state_new()); - next_pair->automaton_state = transition_succ->dst; - next_pair->atomic_propositions = this->getPropositionValues(); - next_pair->depth = current_pair->depth + 1; - /* Get enabled processes and insert them in the interleave set of the next graph_state */ - for (auto& p : mc_model_checker->process().simix_processes()) - if (simgrid::mc::process_is_enabled(&p.copy)) - MC_state_interleave_process(next_pair->graph_state.get(), &p.copy); - - next_pair->requests = MC_state_interleave_size(next_pair->graph_state.get()); - - /* FIXME : get search_cycle value for each acceptant state */ - if (next_pair->automaton_state->type == 1 || current_pair->search_cycle) - next_pair->search_cycle = true; - - /* Add new pair to the exploration stack */ - livenessStack_.push_back(std::move(next_pair)); - - } + if (evaluate_label(transition_succ->label, prop_values)) + livenessStack_.push_back(this->newPair( + current_pair.get(), transition_succ->dst)); cursor--; } @@ -465,6 +431,30 @@ 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 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(); + if (current_pair) + next_pair->depth = current_pair->depth + 1; + else + next_pair->depth = 1; + /* Get enabled processes and insert them in the interleave set of the next graph_state */ + for (auto& p : mc_model_checker->process().simix_processes()) + if (simgrid::mc::process_is_enabled(&p.copy)) + MC_state_interleave_process(next_pair->graph_state.get(), &p.copy); + next_pair->requests = MC_state_interleave_size(next_pair->graph_state.get()); + /* FIXME : get search_cycle value for each acceptant state */ + if (next_pair->automaton_state->type == 1 || + (current_pair && current_pair->search_cycle)) + next_pair->search_cycle = true; + else + next_pair->search_cycle = false; + return std::move(next_pair); +} + void LivenessChecker::backtrack() { /* Traverse the stack backwards until a pair with a non empty interleave diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp index 4906dba685..b595fc71fc 100644 --- a/src/mc/LivenessChecker.hpp +++ b/src/mc/LivenessChecker.hpp @@ -81,6 +81,7 @@ private: void removeAcceptancePair(int pair_num); void purgeVisitedPairs(); void backtrack(); + std::shared_ptr newPair(Pair* pair, xbt_automaton_state_t state); public: std::list> acceptancePairs_; std::list> livenessStack_; -- 2.20.1