#include "src/mc/Transition.hpp"
#include "src/mc/VisitedState.hpp"
#include "src/mc/checker/SafetyChecker.hpp"
+#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_record.hpp"
{
simgrid::mc::Snapshot* s1 = state1->system_state.get();
simgrid::mc::Snapshot* s2 = state2->system_state.get();
- int num1 = state1->num;
- int num2 = state2->num;
- return snapshot_compare(num1, s1, num2, s2);
+ return snapshot_compare(s1, s2);
}
void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
XBT_INFO(" %s", s.c_str());
simgrid::mc::dumpRecordPath();
- simgrid::mc::session->logState();
+ simgrid::mc::session->log_state();
throw simgrid::mc::TerminationError();
}
}
XBT_INFO("No property violation found.");
- simgrid::mc::session->logState();
+ simgrid::mc::session->log_state();
}
void SafetyChecker::backtrack()
/* Intermediate backtracking */
simgrid::mc::State* last_state = stack_.back().get();
if (last_state->system_state) {
- simgrid::mc::restore_snapshot(last_state->system_state);
+ last_state->system_state->restore(&mc_model_checker->process());
return;
}
/* Restore the initial state */
- simgrid::mc::session->restoreInitialState();
+ simgrid::mc::session->restore_initial_state();
/* Traverse the stack from the state at position start and re-execute the transitions */
for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {