-/* Copyright (c) 2011-2019. The SimGrid Team. All rights reserved. */
+/* Copyright (c) 2011-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. */
std::shared_ptr<State> graph_state)
: num(pair_num), automaton_state(automaton_state)
{
- RemoteClient* process = &(mc_model_checker->process());
+ RemoteSimulation* process = &(mc_model_checker->get_remote_simulation());
this->graph_state = std::move(graph_state);
if (this->graph_state->system_state_ == nullptr)
this->graph_state->system_state_ = std::make_shared<Snapshot>(pair_num);
this->heap_bytes_used = mmalloc_get_bytes_used_remote(process->get_heap()->heaplimit, process->get_malloc_info());
- this->actors_count = mc_model_checker->process().actors().size();
+ this->actors_count = mc_model_checker->get_remote_simulation().actors().size();
this->other_num = -1;
this->atomic_propositions = std::move(atomic_propositions);
}
-static bool evaluate_label(xbt_automaton_exp_label_t l, std::vector<int> const& values)
+static bool evaluate_label(const xbt_automaton_exp_label* l, std::vector<int> const& values)
{
switch (l->type) {
case xbt_automaton_exp_label::AUT_OR:
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->process());
+ pair->graph_state->system_state_->restore(&mc_model_checker->get_remote_simulation());
return;
}
}
/* 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);
- req = &issuer->simcall;
+ req = &issuer->simcall_;
/* Debug information */
XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
return trace;
}
-std::shared_ptr<Pair> LivenessChecker::create_pair(Pair* current_pair, xbt_automaton_state_t state,
+std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt_automaton_state_t state,
std::shared_ptr<const std::vector<int>> propositions)
{
expanded_pairs_count_++;
else
next_pair->depth = 1;
/* Get enabled actors and insert them in the interleave set of the next graph_state */
- for (auto& actor : mc_model_checker->process().actors())
+ for (auto& actor : mc_model_checker->get_remote_simulation().actors())
if (mc::actor_is_enabled(actor.copy.get_buffer()))
next_pair->graph_state->add_interleaving_set(actor.copy.get_buffer());
next_pair->requests = next_pair->graph_state->interleave_size();