From afcd422c58cb381517c473c2944fde1424b6a9cc Mon Sep 17 00:00:00 2001 From: Ehsan Azimi Date: Mon, 7 Dec 2020 11:09:41 +0100 Subject: [PATCH] mc_api::set_property_automaton(), it is called in run() --- src/mc/checker/LivenessChecker.cpp | 2 +- src/mc/mc_api.cpp | 5 +++++ src/mc/mc_api.hpp | 1 + 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index 97d14fb9c9..77e28d2230 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -328,7 +328,7 @@ void LivenessChecker::run() std::shared_ptr current_pair = exploration_stack_.back(); /* Update current state in buchi automaton */ - mc::property_automaton->current_state = current_pair->automaton_state; + mcapi::get().set_property_automaton(current_pair->automaton_state); XBT_DEBUG( "********************* ( Depth = %d, search_cycle = %d, interleave size = %zu, pair_num = %d, requests = %d)", diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp index c94007f29f..42f2a6e063 100644 --- a/src/mc/mc_api.cpp +++ b/src/mc/mc_api.cpp @@ -544,5 +544,10 @@ int mc_api::compare_automaton_exp_lable(const xbt_automaton_exp_label* l, std::v return -1; } +void mc_api::set_property_automaton(xbt_automaton_state_t const& automaton_state) const +{ + mc::property_automaton->current_state = automaton_state; +} + } // namespace mc } // namespace simgrid diff --git a/src/mc/mc_api.hpp b/src/mc/mc_api.hpp index e4ecaeabcf..c8488efa77 100644 --- a/src/mc/mc_api.hpp +++ b/src/mc/mc_api.hpp @@ -114,6 +114,7 @@ public: std::vector automaton_propositional_symbol_evaluate() const; std::vector get_automaton_state() const; int compare_automaton_exp_lable(const xbt_automaton_exp_label* l, std::vector const& values) const; + void set_property_automaton(xbt_automaton_state_t const& automaton_state) const; }; } // namespace mc -- 2.20.1