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 = Api::get().get_actors().size();
+ this->actors_count = mc_model_checker->get_remote_process().actors().size();
this->other_num = -1;
this->atomic_propositions = std::move(atomic_propositions);
}
++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 */
// 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));
}