#include "src/mc/mc_safety.h"
#include "src/mc/mc_exit.h"
#include "src/mc/Transition.hpp"
+#include "src/mc/Session.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
"Logging specific to algorithms for liveness properties verification");
void LivenessChecker::prepare(void)
{
- mc_model_checker->wait_for_requests();
initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
initial_global_state->prev_pair = 0;
state.get());
}
- mc_model_checker->handle_simcall(state->transition);
- mc_model_checker->wait_for_requests();
+ this->getSession().execute(state->transition);
}
/* Update statistics */
{
RecordTrace res;
for (std::shared_ptr<Pair> const& pair : explorationStack_)
- res.push_back(pair->graph_state->getRecordElement());
+ res.push_back(pair->graph_state->getTransition());
return res;
}