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 initial state into Session
[simgrid.git]
/
src
/
mc
/
LivenessChecker.cpp
diff --git
a/src/mc/LivenessChecker.cpp
b/src/mc/LivenessChecker.cpp
index
584337f
..
81b9833
100644
(file)
--- a/
src/mc/LivenessChecker.cpp
+++ b/
src/mc/LivenessChecker.cpp
@@
-159,7
+159,6
@@
void LivenessChecker::removeAcceptancePair(int pair_num)
void LivenessChecker::prepare(void)
{
void LivenessChecker::prepare(void)
{
- initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
initial_global_state->prev_pair = 0;
std::shared_ptr<const std::vector<int>> propos = this->getPropositionValues();
initial_global_state->prev_pair = 0;
std::shared_ptr<const std::vector<int>> propos = this->getPropositionValues();
@@
-188,7
+187,7
@@
void LivenessChecker::replay()
}
/* Restore the initial state */
}
/* Restore the initial state */
- simgrid::mc::
restore_snapshot(initial_global_state->snapshot
);
+ simgrid::mc::
session->restoreInitialState(
);
/* Traverse the stack from the initial state and re-execute the transitions */
int depth = 1;
/* Traverse the stack from the initial state and re-execute the transitions */
int depth = 1;
@@
-484,14
+483,12
@@
int LivenessChecker::run()
{
XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
MC_automaton_load(_sg_mc_property_file);
{
XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
MC_automaton_load(_sg_mc_property_file);
- mc_model_checker->wait_for_requests();
XBT_DEBUG("Starting the liveness algorithm");
XBT_DEBUG("Starting the liveness algorithm");
-
- /* Create the initial state */
simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
-
+ simgrid::mc::session->initialize();
this->prepare();
this->prepare();
+
int res = this->main();
simgrid::mc::initial_global_state = nullptr;
int res = this->main();
simgrid::mc::initial_global_state = nullptr;