* 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 "src/mc/mc_smx.hpp"
-#include "src/mc/mc_api.hpp"
#include <boost/range/algorithm.hpp>
#include <cstring>
if (this->graph_state->system_state_ == nullptr)
this->graph_state->system_state_ = std::make_shared<Snapshot>(pair_num);
this->heap_bytes_used = mcapi::get().get_remote_heap_bytes();
- this->actors_count = mc_model_checker->get_remote_simulation().actors().size();
-
+ this->actors_count = mcapi::get().get_actors_size();
this->other_num = -1;
this->atomic_propositions = std::move(atomic_propositions);
}
if(_sg_mc_checkpoint > 0) {
const Pair* pair = exploration_stack_.back().get();
if (pair->graph_state->system_state_) {
- pair->graph_state->system_state_->restore(&mc_model_checker->get_remote_simulation());
+ mcapi::get().restore_state(pair->graph_state->system_state_);
return;
}
}
/* Restore the initial state */
- mc::session->restore_initial_state();
+ mcapi::get().restore_initial_state();
/* Traverse the stack from the initial state and re-execute the transitions */
int depth = 1;
/* 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 = MC_smx_simcall_get_issuer(saved_req);
+ const smx_actor_t issuer = mcapi::get().simcall_get_issuer(saved_req);
req = &issuer->simcall_;
/* Debug information */
XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
mcapi::get().request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
- this->get_session().execute(state->transition_);
+ mcapi::get().execute(state->transition_);
}
/* Update statistics */
visited_pairs_count_++;
- mc_model_checker->executed_transitions++;
+ mcapi::get().mc_inc_executed_trans();
depth++;
}
}
}
-LivenessChecker::LivenessChecker(Session& s) : Checker(s)
+LivenessChecker::LivenessChecker() : Checker()
{
}
mcapi::get().log_state();
}
-Checker* createLivenessChecker(Session& s)
+Checker* createLivenessChecker()
{
- return new LivenessChecker(s);
+ return new LivenessChecker();
}
} // namespace mc