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 mc_global stuff into LivenessChecker
[simgrid.git]
/
src
/
mc
/
LivenessChecker.cpp
diff --git
a/src/mc/LivenessChecker.cpp
b/src/mc/LivenessChecker.cpp
index
e5613cd
..
8dae669
100644
(file)
--- a/
src/mc/LivenessChecker.cpp
+++ b/
src/mc/LivenessChecker.cpp
@@
-139,8
+139,8
@@
std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::
explorationStack_.pop_back();
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
explorationStack_.pop_back();
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
-
initial_global_state->prev_pair
, pair_test->num,
-
initial_global_state->prev_req
.c_str());
+
this->previousPair_
, pair_test->num,
+
this->previousRequest_
.c_str());
return nullptr;
}
return nullptr;
}
@@
-159,8
+159,7
@@
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;
+ this->previousPair_ = 0;
std::shared_ptr<const std::vector<int>> propos = this->getPropositionValues();
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;
@@
-224,7
+223,7
@@
void LivenessChecker::replay()
/* Update statistics */
visitedPairsCount_++;
/* Update statistics */
visitedPairsCount_++;
- mc_
stats
->executed_transitions++;
+ mc_
model_checker
->executed_transitions++;
depth++;
depth++;
@@
-306,7
+305,7
@@
void LivenessChecker::logState() // override
Checker::logState();
XBT_INFO("Expanded pairs = %lu", expandedPairsCount_);
XBT_INFO("Visited pairs = %lu", visitedPairsCount_);
Checker::logState();
XBT_INFO("Expanded pairs = %lu", expandedPairsCount_);
XBT_INFO("Visited pairs = %lu", visitedPairsCount_);
- XBT_INFO("Executed transitions = %lu", mc_
stats
->executed_transitions);
+ XBT_INFO("Executed transitions = %lu", mc_
model_checker
->executed_transitions);
}
void LivenessChecker::showAcceptanceCycle(std::size_t depth)
}
void LivenessChecker::showAcceptanceCycle(std::size_t depth)
@@
-368,8
+367,8
@@
int LivenessChecker::main(void)
reached_pair, current_pair.get())) != -1) {
if (dot_output != nullptr){
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
reached_pair, current_pair.get())) != -1) {
if (dot_output != nullptr){
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
-
initial_global_state->prev_pair
, visited_num,
-
initial_global_state->prev_req
.c_str());
+
this->previousPair_
, visited_num,
+
this->previousRequest_
.c_str());
fflush(dot_output);
}
XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
fflush(dot_output);
}
XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
@@
-382,14
+381,14
@@
int LivenessChecker::main(void)
int req_num = current_pair->graph_state->transition.argument;
if (dot_output != nullptr) {
int req_num = current_pair->graph_state->transition.argument;
if (dot_output != nullptr) {
- if (
initial_global_state->prev_pair != 0 && initial_global_state->prev_pair
!= current_pair->num) {
+ if (
this->previousPair_ != 0 && this->previousPair_
!= current_pair->num) {
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
-
initial_global_state->prev_pair
, current_pair->num,
-
initial_global_state->prev_req
.c_str());
-
initial_global_state->prev_req
.clear();
+
this->previousPair_
, current_pair->num,
+
this->previousRequest_
.c_str());
+
this->previousRequest_
.clear();
}
}
-
initial_global_state->prev_pair
= current_pair->num;
-
initial_global_state->prev_req
= simgrid::mc::request_get_dot_output(req, req_num);
+
this->previousPair_
= current_pair->num;
+
this->previousRequest_
= simgrid::mc::request_get_dot_output(req, req_num);
if (current_pair->search_cycle)
fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
fflush(dot_output);
if (current_pair->search_cycle)
fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
fflush(dot_output);
@@
-399,8
+398,8
@@
int LivenessChecker::main(void)
simgrid::mc::request_to_string(
req, req_num, simgrid::mc::RequestType::simix).c_str());
simgrid::mc::request_to_string(
req, req_num, simgrid::mc::RequestType::simix).c_str());
- /* Update
mc_
stats */
- mc_
stats
->executed_transitions++;
+ /* Update stats */
+ mc_
model_checker
->executed_transitions++;
if (!current_pair->exploration_started)
visitedPairsCount_++;
if (!current_pair->exploration_started)
visitedPairsCount_++;
@@
-438,7
+437,7
@@
std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton
{
std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(++expandedPairsCount_);
next_pair->automaton_state = state;
{
std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(++expandedPairsCount_);
next_pair->automaton_state = state;
- next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
+ next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new(
++expandedStatesCount_
));
next_pair->atomic_propositions = std::move(propositions);
if (current_pair)
next_pair->depth = current_pair->depth + 1;
next_pair->atomic_propositions = std::move(propositions);
if (current_pair)
next_pair->depth = current_pair->depth + 1;
@@
-484,16
+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::session->initialize();
this->prepare();
this->prepare();
+
int res = this->main();
int res = this->main();
- simgrid::mc::initial_global_state = nullptr;
return res;
}
return res;
}