VisitedState::VisitedState(unsigned long state_number) : num(state_number)
{
this->heap_bytes_used = Api::get().get_remote_heap_bytes();
- this->actors_count = Api::get().get_actors().size();
+ this->actors_count = mc_model_checker->get_remote_process().actors().size();
this->system_state = std::make_shared<simgrid::mc::Snapshot>(state_number);
}
return explo;
}
-std::vector<simgrid::mc::ActorInformation>& Api::get_actors() const
-{
- return mc_model_checker->get_remote_process().actors();
-}
-
unsigned long Api::get_maxpid() const
{
return mc_model_checker->get_remote_process().get_maxpid();
simgrid::mc::ExplorationAlgorithm algo);
// ACTOR APIs
- std::vector<simgrid::mc::ActorInformation>& get_actors() const;
unsigned long get_maxpid() const;
// REMOTE APIs
/* 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 */
- auto actors = Api::get().get_actors();
+ auto actors = mc_model_checker->get_remote_process().actors();
for (auto& remoteActor : actors) {
auto actor = remoteActor.copy.get_buffer();
if (get_session().actor_is_enabled(actor->get_pid())) {
XBT_DEBUG("**************************************************");
/* Get an enabled actor and insert it in the interleave set of the initial state */
- auto actors = Api::get().get_actors();
+ auto actors = mc_model_checker->get_remote_process().actors();
XBT_DEBUG("Initial state. %zu actors to consider", actors.size());
for (auto& actor : actors) {
aid_t aid = actor.copy.get_buffer()->get_pid();
if (not this->graph_state->get_system_state())
this->graph_state->set_system_state(std::make_shared<Snapshot>(pair_num));
this->heap_bytes_used = Api::get().get_remote_heap_bytes();
- this->actors_count = Api::get().get_actors().size();
+ this->actors_count = mc_model_checker->get_remote_process().actors().size();
this->other_num = -1;
this->atomic_propositions = std::move(atomic_propositions);
}
else
next_pair->depth = 1;
/* Add all enabled actors to the interleave set of the initial state */
- for (auto& act : Api::get().get_actors()) {
+ for (auto& act : mc_model_checker->get_remote_process().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());