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();
+ this->actors_count = api::get().get_actors().size();
this->other_num = -1;
this->atomic_propositions = std::move(atomic_propositions);
}
std::shared_ptr<State> state = pair->graph_state;
if (pair->exploration_started) {
- state->transition_.replay();
- XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->transition_.to_string().c_str(), state.get());
+ state->get_transition()->replay();
+ XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_string().c_str(), state.get());
}
/* Update statistics */
XBT_INFO("Counter-example that violates formula:");
for (auto const& s : this->get_textual_trace())
XBT_INFO(" %s", s.c_str());
- api::get().dump_record_path();
- api::get().log_state();
+ XBT_INFO("Path = %s", get_record_trace().to_string().c_str());
+ log_state();
XBT_INFO("Counter-example depth: %zu", depth);
}
std::vector<std::string> LivenessChecker::get_textual_trace() // override
{
std::vector<std::string> trace;
- for (std::shared_ptr<Pair> const& pair : exploration_stack_) {
- smx_simcall_t req = &pair->graph_state->executed_req_;
- if (req->call_ != simix::Simcall::NONE)
- trace.push_back(pair->graph_state->transition_.to_string());
- }
+ for (std::shared_ptr<Pair> const& pair : exploration_stack_)
+ trace.push_back(pair->graph_state->get_transition()->to_string());
+
return trace;
}
std::shared_ptr<const std::vector<int>> propositions)
{
++expanded_pairs_count_;
- ++expanded_states_count_;
auto next_pair = std::make_shared<Pair>(expanded_pairs_count_);
next_pair->automaton_state = state;
- next_pair->graph_state = std::make_shared<State>(expanded_states_count_);
+ next_pair->graph_state = std::make_shared<State>();
next_pair->atomic_propositions = std::move(propositions);
if (current_pair)
next_pair->depth = current_pair->depth + 1;
}
}
- int next = current_pair->graph_state->next_transition();
-
- current_pair->graph_state->transition_.execute(current_pair->graph_state.get(), next);
-
- aid_t aid = current_pair->graph_state->transition_.aid_;
- int req_num = current_pair->graph_state->transition_.times_considered_;
- XBT_DEBUG("Execute: %s", current_pair->graph_state->transition_.to_string().c_str());
+ current_pair->graph_state->execute_next(current_pair->graph_state->next_transition());
+ XBT_DEBUG("Execute: %s", current_pair->graph_state->get_transition()->to_string().c_str());
if (dot_output != nullptr) {
if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) {
this->previous_request_.clear();
}
this->previous_pair_ = current_pair->num;
- this->previous_request_ = api::get().request_get_dot_output(aid, req_num);
+ this->previous_request_ = current_pair->graph_state->get_transition()->dot_string();
if (current_pair->search_cycle)
fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
fflush(dot_output);
// For each enabled transition in the property automaton, push a
// (application_state, automaton_state) pair to the exploration stack:
- for (int i = api::get().get_dynar_length(current_pair->automaton_state->out) - 1; i >= 0; i--) {
+ 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);
if (evaluate_label(transition_succ_label, *prop_values))
}
XBT_INFO("No property violation found.");
- api::get().log_state();
+ log_state();
}
Checker* create_liveness_checker(Session* session)