#include <xbt/log.h>
#include <xbt/sysdep.h>
-#include "src/mc/Session.hpp"
#include "src/mc/Transition.hpp"
#include "src/mc/VisitedState.hpp"
#include "src/mc/checker/SafetyChecker.hpp"
#include "src/mc/mc_record.hpp"
#include "src/mc/mc_request.hpp"
#include "src/mc/mc_smx.hpp"
-#include "src/mc/mc_api.hpp"
#include "src/xbt/mmalloc/mmprivate.h"
auto checker = mcapi::get().mc_get_checker();
for (auto const& s : checker->get_textual_trace())
XBT_INFO(" %s", s.c_str());
- mcapi::get().mc_dump_record_path();
- mcapi::get().s_log_state();
+ mcapi::get().dump_record_path();
+ mcapi::get().log_state();
throw TerminationError();
}
}
XBT_INFO("No property violation found.");
- mcapi::get().s_log_state();
+ mcapi::get().log_state();
}
void SafetyChecker::backtrack()
if (req->call_ == simix::Simcall::MUTEX_LOCK || req->call_ == simix::Simcall::MUTEX_TRYLOCK)
xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none");
- const kernel::actor::ActorImpl* issuer = mcapi::get().mc_smx_simcall_get_issuer(req);
+ const kernel::actor::ActorImpl* issuer = mcapi::get().simcall_get_issuer(req);
for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
State* prev_state = i->get();
if (mcapi::get().request_depend(req, &prev_state->internal_req_)) {
XBT_DEBUG("Process %p is in done set", req->issuer_);
break;
} else if (req->issuer_ == prev_state->internal_req_.issuer_) {
- XBT_DEBUG("Simcall %s and %s with same issuer", mcapi::get().simix_simcall_name(req->call_),
- mcapi::get().simix_simcall_name(prev_state->internal_req_.call_));
+ XBT_DEBUG("Simcall %s and %s with same issuer", mcapi::get().simcall_get_name(req->call_),
+ mcapi::get().simcall_get_name(prev_state->internal_req_.call_));
break;
} else {
- const kernel::actor::ActorImpl* previous_issuer = mcapi::get().mc_smx_simcall_get_issuer(&prev_state->internal_req_);
+ const kernel::actor::ActorImpl* previous_issuer = mcapi::get().simcall_get_issuer(&prev_state->internal_req_);
XBT_DEBUG("Simcall %s, process %ld (state %d) and simcall %s, process %ld (state %d) are independent",
- mcapi::get().simix_simcall_name(req->call_), issuer->get_pid(), state->num_,
- mcapi::get().simix_simcall_name(prev_state->internal_req_.call_), previous_issuer->get_pid(), prev_state->num_);
+ mcapi::get().simcall_get_name(req->call_), issuer->get_pid(), state->num_,
+ mcapi::get().simcall_get_name(prev_state->internal_req_.call_), previous_issuer->get_pid(), prev_state->num_);
}
}
}
/* Intermediate backtracking */
const State* last_state = stack_.back().get();
if (last_state->system_state_) {
- last_state->system_state_->restore(&mcapi::get().mc_get_remote_simulation());
+ mc_api::get().restore_state(last_state->system_state_);
return;
}
/* Restore the initial state */
- mcapi::get().s_restore_initial_state();
+ mcapi::get().restore_initial_state();
/* Traverse the stack from the state at position start and re-execute the transitions */
for (std::unique_ptr<State> const& state : stack_) {
}
}
-SafetyChecker::SafetyChecker(Session& s) : Checker(s)
+SafetyChecker::SafetyChecker() : Checker()
{
reductionMode_ = reduction_mode;
if (_sg_mc_termination)
(reductionMode_ == ReductionMode::none ? "none"
: (reductionMode_ == ReductionMode::dpor ? "dpor" : "unknown")));
- mcapi::get().s_initialize();
+ mcapi::get().session_initialize();
XBT_DEBUG("Starting the safety algorithm");
stack_.push_back(std::move(initial_state));
}
-Checker* createSafetyChecker(Session& s)
+Checker* createSafetyChecker()
{
- return new SafetyChecker(s);
+ return new SafetyChecker();
}
} // namespace mc