-/* 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. */
#include "src/mc/checker/LivenessChecker.hpp"
+#include "src/mc/Session.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
-#include "src/mc/mc_request.hpp"
#include <boost/range/algorithm.hpp>
#include <cstring>
&& evaluate_label(l->u.or_and.right_exp, values);
case xbt_automaton_exp_label::AUT_NOT:
return not evaluate_label(l->u.exp_not, values);
- case xbt_automaton_exp_label::AUT_PREDICAT:{
- auto cursor = api::get().compare_automaton_exp_label(l);
- if(cursor >= 0)
- return values[cursor] != 0;
- xbt_die("Missing predicate");
- break;
- }
+ case xbt_automaton_exp_label::AUT_PREDICAT:
+ 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));
}
}
}
- /* Restore the initial state */
- api::get().restore_initial_state();
+ get_session().restore_initial_state();
/* Traverse the stack from the initial state and re-execute the transitions */
int depth = 1;
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;
req = &issuer->simcall_;
/* Debug information */
- XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, api::get().request_to_string(req, req_num).c_str(),
+ XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
+ api::get().request_to_string(state->transition_.aid_, state->transition_.times_considered_).c_str(),
state.get());
api::get().execute(state->transition_, req);
}
}
-LivenessChecker::LivenessChecker() : Checker()
-{
-}
+LivenessChecker::LivenessChecker(Session* session) : Checker(session) {}
RecordTrace LivenessChecker::get_record_trace() // override
{
{
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(api::get().request_to_string(pair->graph_state->transition_.aid_,
+ pair->graph_state->transition_.times_considered_));
}
return trace;
}
next_pair->depth = current_pair->depth + 1;
else
next_pair->depth = 1;
- /* Get enabled actors and insert them in the interleave set of the next graph_state */
- auto actors = api::get().get_actors();
- for (auto& actor : actors)
- if (api::get().actor_is_enabled(actor.copy.get_buffer()->get_pid()))
- next_pair->graph_state->mark_todo(actor.copy.get_buffer());
+ /* 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());
+ }
+
next_pair->requests = next_pair->graph_state->count_todo();
/* FIXME : get search_cycle value for each accepting state */
if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle))
api::get().automaton_load(_sg_mc_property_file.get().c_str());
XBT_DEBUG("Starting the liveness algorithm");
- api::get().session_initialize();
+ get_session().take_initial_snapshot();
/* Initialize */
this->previous_pair_ = 0;
}
}
- smx_simcall_t req = api::get().mc_state_choose_request(current_pair->graph_state.get());
+ api::get().mc_state_choose_request(current_pair->graph_state.get());
+ aid_t aid = current_pair->graph_state->transition_.aid_;
int req_num = current_pair->graph_state->transition_.times_considered_;
if (dot_output != nullptr) {
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());
+ XBT_DEBUG("Execute: %s", api::get().request_to_string(aid, req_num).c_str());
/* Update stats */
api::get().mc_inc_executed_trans();
// (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));
}
api::get().log_state();
}
-Checker* createLivenessChecker()
+Checker* create_liveness_checker(Session* session)
{
- return new LivenessChecker();
+ return new LivenessChecker(session);
}
} // namespace mc
