/* Get an enabled actor and insert it in the interleave set of the initial state */
for (auto& actor : mc_model_checker->process().actors())
if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
- initial_state->interleave(actor.copy.getBuffer());
+ initial_state->addInterleavingSet(actor.copy.getBuffer());
stack_.push_back(std::move(initial_state));
}
/* Get enabled actors and insert them in the interleave set of the next state */
for (auto& actor : mc_model_checker->process().actors())
if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
- next_state->interleave(actor.copy.getBuffer());
+ next_state->addInterleavingSet(actor.copy.getBuffer());
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
/* Get enabled actors and insert them in the interleave set of the next graph_state */
for (auto& actor : mc_model_checker->process().actors())
if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
- next_pair->graph_state->interleave(actor.copy.getBuffer());
+ next_pair->graph_state->addInterleavingSet(actor.copy.getBuffer());
next_pair->requests = next_pair->graph_state->interleaveSize();
/* FIXME : get search_cycle value for each accepting state */
if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle))
if (visitedState_ == nullptr) {
/* Get an enabled process and insert it in the interleave set of the next state */
- for (auto& actor : mc_model_checker->process().actors())
- if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
- next_state->interleave(actor.copy.getBuffer());
+ for (auto& remoteActor : mc_model_checker->process().actors()) {
+ auto actor = remoteActor.copy.getBuffer();
+ if (simgrid::mc::actor_is_enabled(actor)) {
+ next_state->addInterleavingSet(actor);
if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
- break;
+ break; // With DPOR, we take the first enabled transition
}
+ }
if (dot_output != nullptr)
std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
}
if (not prev_state->actorStates[issuer->pid].isDone())
- prev_state->interleave(issuer);
+ prev_state->addInterleavingSet(issuer);
else
XBT_DEBUG("Process %p is in done set", req->issuer);
/* Get an enabled actor and insert it in the interleave set of the initial state */
for (auto& actor : mc_model_checker->process().actors())
if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
- initial_state->interleave(actor.copy.getBuffer());
+ initial_state->addInterleavingSet(actor.copy.getBuffer());
if (reductionMode_ != simgrid::mc::ReductionMode::none)
break;
}
State(unsigned long state_number);
std::size_t interleaveSize() const;
- void interleave(smx_actor_t actor) {
- this->actorStates[actor->pid].consider();
- }
+ void addInterleavingSet(smx_actor_t actor) { this->actorStates[actor->pid].consider(); }
Transition getTransition() const;
};