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
Merge branch 'master' of https://framagit.org/simgrid/simgrid
[simgrid.git]
/
src
/
mc
/
checker
/
SafetyChecker.cpp
diff --git
a/src/mc/checker/SafetyChecker.cpp
b/src/mc/checker/SafetyChecker.cpp
index
51c0a97
..
faca5d2
100644
(file)
--- a/
src/mc/checker/SafetyChecker.cpp
+++ b/
src/mc/checker/SafetyChecker.cpp
@@
-34,9
+34,7
@@
static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* stat
{
simgrid::mc::Snapshot* s1 = state1->system_state.get();
simgrid::mc::Snapshot* s2 = state2->system_state.get();
- int num1 = state1->num;
- int num2 = state2->num;
- return snapshot_compare(num1, s1, num2, s2);
+ return snapshot_compare(s1, s2);
}
void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
@@
-49,7
+47,8
@@
void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
XBT_INFO("******************************************");
XBT_INFO("Counter-example execution trace:");
for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
- XBT_INFO("%s", s.c_str());
+ XBT_INFO(" %s", s.c_str());
+ simgrid::mc::dumpRecordPath();
simgrid::mc::session->logState();
throw simgrid::mc::TerminationError();
@@
-230,7
+229,7
@@
void SafetyChecker::backtrack()
state->num);
}
- if (not prev_state->actorStates[issuer->
pid_
].isDone())
+ if (not prev_state->actorStates[issuer->
get_pid()
].isDone())
prev_state->addInterleavingSet(issuer);
else
XBT_DEBUG("Process %p is in done set", req->issuer);
@@
-246,7
+245,7
@@
void SafetyChecker::backtrack()
const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
XBT_DEBUG("Simcall %d, process %ld (state %d) and simcall %d, process %ld (state %d) are independent",
- req->call, issuer->
pid_, state->num, prev_state->internal_req.call, previous_issuer->pid_
,
+ req->call, issuer->
get_pid(), state->num, prev_state->internal_req.call, previous_issuer->get_pid()
,
prev_state->num);
}
}
@@
-269,9
+268,9
@@
void SafetyChecker::backtrack()
void SafetyChecker::restoreState()
{
/* Intermediate backtracking */
- simgrid::mc::State* state = stack_.back().get();
- if (state->system_state) {
- simgrid::mc::restore_snapshot(state->system_state);
+ simgrid::mc::State*
last_
state = stack_.back().get();
+ if (
last_
state->system_state) {
+ simgrid::mc::restore_snapshot(
last_
state->system_state);
return;
}
@@
-289,7
+288,7
@@
void SafetyChecker::restoreState()
}
}
-SafetyChecker::SafetyChecker(Session& s
ession) : Checker(session
)
+SafetyChecker::SafetyChecker(Session& s
) : Checker(s
)
{
reductionMode_ = simgrid::mc::reduction_mode;
if (_sg_mc_termination)
@@
-324,9
+323,9
@@
SafetyChecker::SafetyChecker(Session& session) : Checker(session)
stack_.push_back(std::move(initial_state));
}
-Checker* createSafetyChecker(Session& s
ession
)
+Checker* createSafetyChecker(Session& s)
{
- return new SafetyChecker(s
ession
);
+ return new SafetyChecker(s);
}
}