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
clang complains about these seemingly unecessary std::move.
[simgrid.git]
/
src
/
mc
/
LivenessChecker.cpp
diff --git
a/src/mc/LivenessChecker.cpp
b/src/mc/LivenessChecker.cpp
index
81b9833
..
19e6347
100644
(file)
--- a/
src/mc/LivenessChecker.cpp
+++ b/
src/mc/LivenessChecker.cpp
@@
-6,10
+6,11
@@
#include <cstring>
#include <cstring>
-#include <algorithm>
#include <memory>
#include <list>
#include <memory>
#include <list>
+#include <boost/range/algorithm.hpp>
+
#include <unistd.h>
#include <sys/wait.h>
#include <unistd.h>
#include <sys/wait.h>
@@
-124,7
+125,7
@@
std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::
pair->num, pair->automaton_state, pair->atomic_propositions,
pair->graph_state);
pair->num, pair->automaton_state, pair->atomic_propositions,
pair->graph_state);
- auto res =
std::equal_range(acceptancePairs_.begin(), acceptancePairs_.end()
,
+ auto res =
boost::range::equal_range(acceptancePairs_
,
new_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) {
new_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) {
@@
-139,8
+140,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,7
+160,7
@@
void LivenessChecker::removeAcceptancePair(int pair_num)
void LivenessChecker::prepare(void)
{
void LivenessChecker::prepare(void)
{
-
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();
@@
-207,7
+208,7
@@
void LivenessChecker::replay()
if (saved_req != nullptr) {
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
if (saved_req != nullptr) {
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
- const smx_
process
_t issuer = MC_smx_simcall_get_issuer(saved_req);
+ const smx_
actor
_t issuer = MC_smx_simcall_get_issuer(saved_req);
req = &issuer->simcall;
/* Debug information */
req = &issuer->simcall;
/* Debug information */
@@
-245,7
+246,7
@@
int LivenessChecker::insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair
pair->num, pair->automaton_state, pair->atomic_propositions,
pair->graph_state);
pair->num, pair->automaton_state, pair->atomic_propositions,
pair->graph_state);
- auto range =
std::equal_range(visitedPairs_.begin(), visitedPairs_.end()
,
+ auto range =
boost::range::equal_range(visitedPairs_
,
visited_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
for (auto i = range.first; i != range.second; ++i) {
visited_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
for (auto i = range.first; i != range.second; ++i) {
@@
-277,8
+278,7
@@
void LivenessChecker::purgeVisitedPairs()
{
if (_sg_mc_visited != 0 && visitedPairs_.size() > (std::size_t) _sg_mc_visited) {
// Remove the oldest entry with a linear search:
{
if (_sg_mc_visited != 0 && visitedPairs_.size() > (std::size_t) _sg_mc_visited) {
// Remove the oldest entry with a linear search:
- visitedPairs_.erase(std::min_element(
- visitedPairs_.begin(), visitedPairs_.end(),
+ visitedPairs_.erase(boost::min_element(visitedPairs_,
[](std::shared_ptr<VisitedPair> const a, std::shared_ptr<VisitedPair> const& b) {
return a->num < b->num; } ));
}
[](std::shared_ptr<VisitedPair> const a, std::shared_ptr<VisitedPair> const& b) {
return a->num < b->num; } ));
}
@@
-367,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);
@@
-381,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);
@@
-445,8
+445,8
@@
std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton
next_pair->depth = 1;
/* Get enabled processes and insert them in the interleave set of the next graph_state */
for (auto& p : mc_model_checker->process().simix_processes())
next_pair->depth = 1;
/* Get enabled processes and insert them in the interleave set of the next graph_state */
for (auto& p : mc_model_checker->process().simix_processes())
- if (simgrid::mc::process_is_enabled(
&p.copy
))
- next_pair->graph_state->interleave(
&p.copy
);
+ if (simgrid::mc::process_is_enabled(
p.copy.getBuffer()
))
+ next_pair->graph_state->interleave(
p.copy.getBuffer()
);
next_pair->requests = next_pair->graph_state->interleaveSize();
/* FIXME : get search_cycle value for each acceptant state */
if (next_pair->automaton_state->type == 1 ||
next_pair->requests = next_pair->graph_state->interleaveSize();
/* FIXME : get search_cycle value for each acceptant state */
if (next_pair->automaton_state->type == 1 ||
@@
-454,7
+454,7
@@
std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton
next_pair->search_cycle = true;
else
next_pair->search_cycle = false;
next_pair->search_cycle = true;
else
next_pair->search_cycle = false;
- return
std::move(next_pair)
;
+ return
next_pair
;
}
void LivenessChecker::backtrack()
}
void LivenessChecker::backtrack()
@@
-485,12
+485,10
@@
int LivenessChecker::run()
MC_automaton_load(_sg_mc_property_file);
XBT_DEBUG("Starting the liveness algorithm");
MC_automaton_load(_sg_mc_property_file);
XBT_DEBUG("Starting the liveness algorithm");
- simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
simgrid::mc::session->initialize();
this->prepare();
int res = this->main();
simgrid::mc::session->initialize();
this->prepare();
int res = this->main();
- simgrid::mc::initial_global_state = nullptr;
return res;
}
return res;
}