-/* Copyright (c) 2016-2019. The SimGrid Team. All rights reserved. */
+/* Copyright (c) 2016-2020. 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. */
this->get_session().execute(state->transition_);
/* Create the new expanded state (copy the state of MCed into our MCer data) */
- std::unique_ptr<State> next_state = std::unique_ptr<State>(new State(++expanded_states_count_));
+ ++expanded_states_count_;
+ auto next_state = std::make_unique<State>(expanded_states_count_);
if (_sg_mc_termination)
this->check_non_termination(next_state.get());
/* If this is a new state (or if we don't care about state-equality reduction) */
if (visited_state_ == nullptr) {
/* Get an enabled process and insert it in the interleave set of the next state */
- for (auto& remoteActor : mc_model_checker->process().actors()) {
+ for (auto& remoteActor : mc_model_checker->get_remote_simulation().actors()) {
auto actor = remoteActor.copy.get_buffer();
if (actor_is_enabled(actor)) {
next_state->add_interleaving_set(actor);
if (req->call_ == SIMCALL_MUTEX_LOCK || req->call_ == SIMCALL_MUTEX_TRYLOCK)
xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none");
- const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
+ const kernel::actor::ActorImpl* issuer = MC_smx_simcall_get_issuer(req);
for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
State* prev_state = i->get();
if (request_depend(req, &prev_state->internal_req_)) {
/* Intermediate backtracking */
const State* last_state = stack_.back().get();
if (last_state->system_state_) {
- last_state->system_state_->restore(&mc_model_checker->process());
+ last_state->system_state_->restore(&mc_model_checker->get_remote_simulation());
return;
}
XBT_DEBUG("Starting the safety algorithm");
- std::unique_ptr<State> initial_state = std::unique_ptr<State>(new State(++expanded_states_count_));
+ ++expanded_states_count_;
+ auto initial_state = std::make_unique<State>(expanded_states_count_);
XBT_DEBUG("**************************************************");
XBT_DEBUG("Initial state");
/* Get an enabled actor and insert it in the interleave set of the initial state */
- for (auto& actor : mc_model_checker->process().actors())
+ for (auto& actor : mc_model_checker->get_remote_simulation().actors())
if (actor_is_enabled(actor.copy.get_buffer())) {
initial_state->add_interleaving_set(actor.copy.get_buffer());
if (reductionMode_ != ReductionMode::none)