namespace simgrid {
namespace mc {
-static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
-{
- simgrid::mc::Snapshot* s1 = state1->system_state.get();
- simgrid::mc::Snapshot* s2 = state2->system_state.get();
- return snapshot_compare(s1, s2);
-}
-
void SafetyChecker::check_non_termination(simgrid::mc::State* current_state)
{
for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
- if (snapshot_compare(state->get(), current_state) == 0) {
+ if (snapshot_equal((*state)->system_state.get(), current_state->system_state.get())) {
XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num, current_state->num);
XBT_INFO("******************************************");
XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
simgrid::mc::State* state = stack_.back().get();
XBT_DEBUG("**************************************************");
- XBT_DEBUG("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num,
- state->interleaveSize());
+ XBT_VERB("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num,
+ state->interleaveSize());
mc_model_checker->visited_states++;
/* Get an enabled process and insert it in the interleave set of the next state */
for (auto& remoteActor : mc_model_checker->process().actors()) {
- auto actor = remoteActor.copy.getBuffer();
+ auto actor = remoteActor.copy.get_buffer();
if (simgrid::mc::actor_is_enabled(actor)) {
next_state->addInterleavingSet(actor);
if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
/* 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->addInterleavingSet(actor.copy.getBuffer());
+ if (simgrid::mc::actor_is_enabled(actor.copy.get_buffer())) {
+ initial_state->addInterleavingSet(actor.copy.get_buffer());
if (reductionMode_ != simgrid::mc::ReductionMode::none)
break;
}