A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
| inline |
side by side
mc: move some files related to ELF, DWARF or unwind reading into their own directory
[simgrid.git]
/
src
/
mc
/
checker
/
LivenessChecker.cpp
diff --git
a/src/mc/checker/LivenessChecker.cpp
b/src/mc/checker/LivenessChecker.cpp
index
a425ad6
..
cd49a87
100644
(file)
--- a/
src/mc/checker/LivenessChecker.cpp
+++ b/
src/mc/checker/LivenessChecker.cpp
@@
-100,9
+100,7
@@
int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::Visi
{
simgrid::mc::Snapshot* s1 = state1->graph_state->system_state.get();
simgrid::mc::Snapshot* s2 = state2->graph_state->system_state.get();
- int num1 = state1->num;
- int num2 = state2->num;
- return simgrid::mc::snapshot_compare(num1, s1, num2, s2);
+ return simgrid::mc::snapshot_compare(s1, s2);
}
std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::Pair* pair)
@@
-251,7
+249,7
@@
void LivenessChecker::purgeVisitedPairs()
}
}
-LivenessChecker::LivenessChecker(Session& s
ession) : Checker(session
)
+LivenessChecker::LivenessChecker(Session& s
) : Checker(s
)
{
}
@@
-275,12
+273,12
@@
void LivenessChecker::showAcceptanceCycle(std::size_t depth)
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
@@
-446,8
+444,9
@@
void LivenessChecker::run()
// 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));
@@
-459,9
+458,9
@@
void LivenessChecker::run()
simgrid::mc::session->logState();
}
-Checker* createLivenessChecker(Session& s
ession
)
+Checker* createLivenessChecker(Session& s)
{
- return new LivenessChecker(s
ession
);
+ return new LivenessChecker(s);
}
}