}
}
-LivenessChecker::LivenessChecker(Session& session) : Checker(session)
+LivenessChecker::LivenessChecker(Session& s) : Checker(s)
{
}
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
XBT_INFO("| ACCEPTANCE CYCLE |");
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
- XBT_INFO("Counter-example that violates formula :");
- simgrid::mc::dumpRecordPath();
+ XBT_INFO("Counter-example that violates formula:");
for (auto const& s : this->getTextualTrace())
- XBT_INFO("%s", s.c_str());
+ XBT_INFO(" %s", s.c_str());
+ simgrid::mc::dumpRecordPath();
simgrid::mc::session->logState();
- XBT_INFO("Counter-example depth : %zu", depth);
+ XBT_INFO("Counter-example depth: %zu", depth);
}
std::vector<std::string> LivenessChecker::getTextualTrace() // override
// For each enabled transition in the property automaton, push a
// (application_state, automaton_state) pair to the exploration stack:
- for (int cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1; cursor >= 0; cursor--) {
- xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
+ for (int i = xbt_dynar_length(current_pair->automaton_state->out) - 1; i >= 0; i--) {
+ xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(
+ current_pair->automaton_state->out, i, xbt_automaton_transition_t);
if (evaluate_label(transition_succ->label, *prop_values))
explorationStack_.push_back(this->newPair(
current_pair.get(), transition_succ->dst, prop_values));
simgrid::mc::session->logState();
}
-Checker* createLivenessChecker(Session& session)
+Checker* createLivenessChecker(Session& s)
{
- return new LivenessChecker(session);
+ return new LivenessChecker(s);
}
}