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
079f3fe
..
6b1c4da
100644
(file)
--- a/
src/mc/checker/SafetyChecker.cpp
+++ b/
src/mc/checker/SafetyChecker.cpp
@@
-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()
@@
-271,12
+271,12
@@
void SafetyChecker::restoreState()
/* Intermediate backtracking */
simgrid::mc::State* last_state = stack_.back().get();
if (last_state->system_state) {
/* Intermediate backtracking */
simgrid::mc::State* last_state = stack_.back().get();
if (last_state->system_state) {
-
simgrid::mc::restore_snapshot(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_) {