XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification");
-using api = simgrid::mc::Api;
-
/********* Static functions *********/
-namespace simgrid {
-namespace mc {
+namespace simgrid::mc {
VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state,
std::shared_ptr<const std::vector<int>> atomic_propositions,
: num(pair_num), automaton_state(automaton_state)
{
this->graph_state = std::move(graph_state);
- if (this->graph_state->system_state_ == nullptr)
- this->graph_state->system_state_ = std::make_shared<Snapshot>(pair_num);
- this->heap_bytes_used = api::get().get_remote_heap_bytes();
- this->actors_count = api::get().get_actors().size();
+ if (not this->graph_state->get_system_state())
+ this->graph_state->set_system_state(std::make_shared<Snapshot>(pair_num));
+ this->heap_bytes_used = Api::get().get_remote_heap_bytes();
+ this->actors_count = mc_model_checker->get_remote_process().actors().size();
this->other_num = -1;
this->atomic_propositions = std::move(atomic_propositions);
}
case xbt_automaton_exp_label::AUT_NOT:
return not evaluate_label(l->u.exp_not, values);
case xbt_automaton_exp_label::AUT_PREDICAT:
- return values.at(api::get().compare_automaton_exp_label(l)) != 0;
+ return values.at(Api::get().compare_automaton_exp_label(l)) != 0;
case xbt_automaton_exp_label::AUT_ONE:
return true;
default:
std::shared_ptr<const std::vector<int>> LivenessChecker::get_proposition_values() const
{
- auto values = api::get().automaton_propositional_symbol_evaluate();
+ auto values = Api::get().automaton_propositional_symbol_evaluate();
return std::make_shared<const std::vector<int>>(std::move(values));
}
auto new_pair =
std::make_shared<VisitedPair>(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
- auto res = boost::range::equal_range(acceptance_pairs_, new_pair.get(), api::get().compare_pair());
+ 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.first; i != res.second; ++i) {
+ for (auto i = res_begin; i != res_end; ++i) {
std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
- if (api::get().automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) != 0 ||
+ if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) != 0 ||
*(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) ||
- not api::get().snapshot_equal(pair_test->graph_state->system_state_.get(),
- new_pair->graph_state->system_state_.get()))
+ not Api::get().snapshot_equal(pair_test->graph_state->get_system_state(),
+ new_pair->graph_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();
return nullptr;
}
- acceptance_pairs_.insert(res.first, new_pair);
+ acceptance_pairs_.insert(res_begin, new_pair);
return new_pair;
}
/* Intermediate backtracking */
if (_sg_mc_checkpoint > 0) {
const Pair* pair = exploration_stack_.back().get();
- if (pair->graph_state->system_state_) {
- api::get().restore_state(pair->graph_state->system_state_);
+ if (const auto* system_state = pair->graph_state->get_system_state()) {
+ Api::get().restore_state(system_state);
return;
}
}
visited_pair =
std::make_shared<VisitedPair>(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
- auto range = boost::range::equal_range(visited_pairs_, visited_pair.get(), api::get().compare_pair());
+ auto [range_begin, range_end] =
+ boost::range::equal_range(visited_pairs_, visited_pair.get(), Api::get().compare_pair());
- for (auto i = range.first; i != range.second; ++i) {
+ for (auto i = range_begin; i != range_end; ++i) {
const VisitedPair* pair_test = i->get();
- if (api::get().automaton_state_compare(pair_test->automaton_state, visited_pair->automaton_state) != 0 ||
+ if (xbt_automaton_state_compare(pair_test->automaton_state, visited_pair->automaton_state) != 0 ||
*(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) ||
- not api::get().snapshot_equal(pair_test->graph_state->system_state_.get(),
- visited_pair->graph_state->system_state_.get()))
+ not Api::get().snapshot_equal(pair_test->graph_state->get_system_state(),
+ visited_pair->graph_state->get_system_state()))
continue;
if (pair_test->other_num == -1)
visited_pair->other_num = pair_test->num;
return (*i)->other_num;
}
- visited_pairs_.insert(range.first, std::move(visited_pair));
+ visited_pairs_.insert(range_begin, std::move(visited_pair));
this->purge_visited_pairs();
return -1;
}
++expanded_pairs_count_;
auto next_pair = std::make_shared<Pair>(expanded_pairs_count_);
next_pair->automaton_state = state;
- next_pair->graph_state = std::make_shared<State>();
+ next_pair->graph_state = std::make_shared<State>(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& act : api::get().get_actors()) {
- auto actor = act.copy.get_buffer();
- if (get_session().actor_is_enabled(actor->get_pid()))
- next_pair->graph_state->mark_todo(actor->get_pid());
- }
+ 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);
next_pair->requests = next_pair->graph_state->count_todo();
/* FIXME : get search_cycle value for each accepting state */
void LivenessChecker::run()
{
XBT_INFO("Check the liveness property %s", _sg_mc_property_file.get().c_str());
- api::get().automaton_load(_sg_mc_property_file.get().c_str());
+ Api::get().automaton_load(_sg_mc_property_file.get().c_str());
XBT_DEBUG("Starting the liveness algorithm");
get_session().take_initial_snapshot();
// For each initial state of the property automaton, push a
// (application_state, automaton_state) pair to the exploration stack:
- auto automaton_stack = api::get().get_automaton_state();
+ auto automaton_stack = Api::get().get_automaton_state();
for (auto* automaton_state : automaton_stack) {
if (automaton_state->type == -1)
exploration_stack_.push_back(this->create_pair(nullptr, automaton_state, propos));
std::shared_ptr<Pair> 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->automaton_state);
XBT_DEBUG(
"********************* ( Depth = %d, search_cycle = %d, interleave size = %zu, pair_num = %d, requests = %d)",
// 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--) {
- 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);
+ 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);
if (evaluate_label(transition_succ_label, *prop_values))
exploration_stack_.push_back(this->create_pair(current_pair.get(), transition_succ_dst, prop_values));
}
return new LivenessChecker(session);
}
-} // namespace mc
-} // namespace simgrid
+} // namespace simgrid::mc