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: snake_case a class
[simgrid.git]
/
src
/
mc
/
checker
/
SafetyChecker.cpp
diff --git
a/src/mc/checker/SafetyChecker.cpp
b/src/mc/checker/SafetyChecker.cpp
index
9aeaff7
..
6b1c4da
100644
(file)
--- a/
src/mc/checker/SafetyChecker.cpp
+++ b/
src/mc/checker/SafetyChecker.cpp
@@
-1,4
+1,4
@@
-/* Copyright (c) 2016-201
8
. The SimGrid Team. All rights reserved. */
+/* Copyright (c) 2016-201
9
. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
@@
-17,6
+17,7
@@
#include "src/mc/Transition.hpp"
#include "src/mc/VisitedState.hpp"
#include "src/mc/checker/SafetyChecker.hpp"
#include "src/mc/Transition.hpp"
#include "src/mc/VisitedState.hpp"
#include "src/mc/checker/SafetyChecker.hpp"
+#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_record.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_record.hpp"
@@
-34,9
+35,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();
{
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)
}
void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
@@
-49,8
+48,9
@@
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("******************************************");
XBT_INFO("Counter-example execution trace:");
for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
- XBT_INFO("%s", s.c_str());
- simgrid::mc::session->logState();
+ XBT_INFO(" %s", s.c_str());
+ simgrid::mc::dumpRecordPath();
+ simgrid::mc::session->log_state();
throw simgrid::mc::TerminationError();
}
throw simgrid::mc::TerminationError();
}
@@
-182,7
+182,7
@@
void SafetyChecker::run()
}
XBT_INFO("No property violation found.");
}
XBT_INFO("No property violation found.");
- simgrid::mc::session->log
S
tate();
+ simgrid::mc::session->log
_s
tate();
}
void SafetyChecker::backtrack()
}
void SafetyChecker::backtrack()
@@
-230,7
+230,7
@@
void SafetyChecker::backtrack()
state->num);
}
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);
prev_state->addInterleavingSet(issuer);
else
XBT_DEBUG("Process %p is in done set", req->issuer);
@@
-246,7
+246,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",
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);
}
}
prev_state->num);
}
}
@@
-269,14
+269,14
@@
void SafetyChecker::backtrack()
void SafetyChecker::restoreState()
{
/* Intermediate backtracking */
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) {
+
last_state->system_state->restore(&mc_model_checker->process()
);
return;
}
/* Restore the initial state */
return;
}
/* Restore the initial state */
- simgrid::mc::session->restore
InitialS
tate();
+ simgrid::mc::session->restore
_initial_s
tate();
/* Traverse the stack from the state at position start and re-execute the transitions */
for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
/* Traverse the stack from the state at position start and re-execute the transitions */
for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
@@
-289,7
+289,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)
{
reductionMode_ = simgrid::mc::reduction_mode;
if (_sg_mc_termination)
@@
-324,9
+324,9
@@
SafetyChecker::SafetyChecker(Session& session) : Checker(session)
stack_.push_back(std::move(initial_state));
}
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);
}
}
}
}