-/* Copyright (c) 2011-2021. The SimGrid Team. All rights reserved. */
+/* Copyright (c) 2011-2022. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
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));
}
std::shared_ptr<State> state = pair->graph_state;
if (pair->exploration_started) {
- int req_num = state->transition_.times_considered_;
- const s_smx_simcall* saved_req = &state->executed_req_;
-
- smx_simcall_t req = nullptr;
-
- /* because we got a copy of the executed request, we have to fetch the
- real one, pointed by the request field of the issuer process */
- const smx_actor_t issuer = api::get().simcall_get_issuer(saved_req);
- req = &issuer->simcall_;
-
- /* Debug information */
- XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, api::get().request_to_string(req, req_num).c_str(),
- state.get());
-
- api::get().execute(state->transition_, req);
+ state->get_transition()->replay();
+ XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_cstring(), state.get());
}
/* Update statistics */
visited_pairs_count_++;
- api::get().mc_inc_executed_trans();
-
depth++;
}
XBT_DEBUG("**** End Replay ****");
{
RecordTrace res;
for (std::shared_ptr<Pair> const& pair : exploration_stack_)
- res.push_back(pair->graph_state->get_transition());
+ res.push_back(*pair->graph_state->get_transition());
return res;
}
{
XBT_INFO("Expanded pairs = %lu", expanded_pairs_count_);
XBT_INFO("Visited pairs = %lu", visited_pairs_count_);
- XBT_INFO("Executed transitions = %lu", api::get().mc_get_executed_trans());
+ XBT_INFO("Executed transitions = %lu", Transition::get_executed_transitions());
}
void LivenessChecker::show_acceptance_cycle(std::size_t depth)
{
std::vector<std::string> trace;
for (std::shared_ptr<Pair> const& pair : exploration_stack_) {
- int req_num = pair->graph_state->transition_.times_considered_;
smx_simcall_t req = &pair->graph_state->executed_req_;
if (req->call_ != simix::Simcall::NONE)
- trace.push_back(api::get().request_to_string(req, req_num));
+ 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;
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);
+ next_pair->graph_state->mark_todo(actor->get_pid());
}
next_pair->requests = next_pair->graph_state->count_todo();
}
}
- smx_simcall_t req = api::get().mc_state_choose_request(current_pair->graph_state.get());
- int req_num = current_pair->graph_state->transition_.times_considered_;
+ int next = current_pair->graph_state->next_transition();
+
+ current_pair->graph_state->execute_next(next);
+
+ aid_t aid = current_pair->graph_state->get_transition()->aid_;
+ int req_num = current_pair->graph_state->get_transition()->times_considered_;
+ XBT_DEBUG("Execute: %s", current_pair->graph_state->get_transition()->to_cstring());
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(req, req_num);
+ this->previous_request_ = api::get().request_get_dot_output(aid, req_num);
if (current_pair->search_cycle)
fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
fflush(dot_output);
}
- XBT_DEBUG("Execute: %s", api::get().request_to_string(req, req_num).c_str());
-
- /* Update stats */
- api::get().mc_inc_executed_trans();
-
if (not current_pair->exploration_started)
visited_pairs_count_++;
- /* Answer the request */
- api::get().handle_simcall(current_pair->graph_state->transition_);
-
- /* Wait for requests (schedules processes) */
- api::get().mc_wait_for_requests();
-
current_pair->requests--;
current_pair->exploration_started = true;
// (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--) {
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);
+ 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));
}
