#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 */
return res;
}
+void LivenessChecker::logState() // override
+{
+ Checker::logState();
+ XBT_INFO("Expanded pairs = %lu", mc_stats->expanded_pairs);
+ XBT_INFO("Visited pairs = %lu", mc_stats->visited_pairs);
+ XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
+}
+
void LivenessChecker::showAcceptanceCycle(std::size_t depth)
{
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
simgrid::mc::dumpRecordPath();
for (auto& s : this->getTextualTrace())
XBT_INFO("%s", s.c_str());
- MC_print_statistics(mc_stats);
+ simgrid::mc::session->logState();
XBT_INFO("Counter-example depth : %zd", depth);
}
}
XBT_INFO("No property violation found.");
- MC_print_statistics(mc_stats);
+ simgrid::mc::session->logState();
return SIMGRID_MC_EXIT_SUCCESS;
}