#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");
}
}
-Pair::Pair() : num(++mc_stats->expanded_pairs)
+Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs)
{}
Pair::~Pair() {}
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 */
- mc_stats->visited_pairs++;
+ visitedPairsCount_++;
mc_stats->executed_transitions++;
depth++;
return res;
}
+void LivenessChecker::logState() // override
+{
+ Checker::logState();
+ XBT_INFO("Expanded pairs = %lu", expandedPairsCount_);
+ XBT_INFO("Visited pairs = %lu", visitedPairsCount_);
+ 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);
}
/* Update mc_stats */
mc_stats->executed_transitions++;
if (!current_pair->exploration_started)
- mc_stats->visited_pairs++;
+ visitedPairsCount_++;
/* Answer the request */
mc_model_checker->handle_simcall(current_pair->graph_state->transition);
}
XBT_INFO("No property violation found.");
- MC_print_statistics(mc_stats);
+ simgrid::mc::session->logState();
return SIMGRID_MC_EXIT_SUCCESS;
}
std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state, std::shared_ptr<const std::vector<int>> propositions)
{
- std::shared_ptr<Pair> next_pair = std::make_shared<Pair>();
+ std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(++expandedPairsCount_);
next_pair->automaton_state = state;
next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
next_pair->atomic_propositions = std::move(propositions);