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] Use Session::execute() in LivenessChecker as well
[simgrid.git]
/
src
/
mc
/
LivenessChecker.cpp
diff --git
a/src/mc/LivenessChecker.cpp
b/src/mc/LivenessChecker.cpp
index
2837d43
..
537dd9b
100644
(file)
--- a/
src/mc/LivenessChecker.cpp
+++ b/
src/mc/LivenessChecker.cpp
@@
-29,6
+29,8
@@
#include "src/mc/mc_replay.h"
#include "src/mc/mc_safety.h"
#include "src/mc/mc_exit.h"
#include "src/mc/mc_replay.h"
#include "src/mc/mc_safety.h"
#include "src/mc/mc_exit.h"
+#include "src/mc/Transition.hpp"
+#include "src/mc/Session.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
"Logging specific to algorithms for liveness properties verification");
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
"Logging specific to algorithms for liveness properties verification");
@@
-157,7
+159,6
@@
void LivenessChecker::removeAcceptancePair(int pair_num)
void LivenessChecker::prepare(void)
{
void LivenessChecker::prepare(void)
{
- mc_model_checker->wait_for_requests();
initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
initial_global_state->prev_pair = 0;
initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
initial_global_state->prev_pair = 0;
@@
-199,8
+200,8
@@
void LivenessChecker::replay()
if (pair->exploration_started) {
if (pair->exploration_started) {
- int
value
;
- smx_simcall_t saved_req =
MC_state_get_executed_request(state.get(), &value)
;
+ int
req_num = state->transition.argument
;
+ smx_simcall_t saved_req =
&state->executed_req
;
smx_simcall_t req = nullptr;
smx_simcall_t req = nullptr;
@@
-214,12
+215,11
@@
void LivenessChecker::replay()
XBT_DEBUG("Replay (depth = %d) : %s (%p)",
depth,
simgrid::mc::request_to_string(
XBT_DEBUG("Replay (depth = %d) : %s (%p)",
depth,
simgrid::mc::request_to_string(
- req,
value
, simgrid::mc::RequestType::simix).c_str(),
+ req,
req_num
, simgrid::mc::RequestType::simix).c_str(),
state.get());
}
state.get());
}
- simgrid::mc::handle_simcall(req, value);
- mc_model_checker->wait_for_requests();
+ this->getSession().execute(state->transition);
}
/* Update statistics */
}
/* Update statistics */
@@
-297,7
+297,7
@@
RecordTrace LivenessChecker::getRecordTrace() // override
{
RecordTrace res;
for (std::shared_ptr<Pair> const& pair : explorationStack_)
{
RecordTrace res;
for (std::shared_ptr<Pair> const& pair : explorationStack_)
- res.push_back(pair->graph_state->get
RecordElement
());
+ res.push_back(pair->graph_state->get
Transition
());
return res;
}
return res;
}
@@
-318,11
+318,11
@@
std::vector<std::string> LivenessChecker::getTextualTrace() // override
{
std::vector<std::string> trace;
for (std::shared_ptr<Pair> const& pair : explorationStack_) {
{
std::vector<std::string> trace;
for (std::shared_ptr<Pair> const& pair : explorationStack_) {
- int
value
;
- smx_simcall_t req =
MC_state_get_executed_request(pair->graph_state.get(), &value)
;
+ int
req_num = pair->graph_state->transition.argument
;
+ smx_simcall_t req =
&pair->graph_state->executed_req
;
if (req && req->call != SIMCALL_NONE)
trace.push_back(simgrid::mc::request_to_string(
if (req && req->call != SIMCALL_NONE)
trace.push_back(simgrid::mc::request_to_string(
- req,
value
, simgrid::mc::RequestType::executed));
+ req,
req_num
, simgrid::mc::RequestType::executed));
}
return trace;
}
}
return trace;
}
@@
-370,8
+370,8
@@
int LivenessChecker::main(void)
continue;
}
continue;
}
-
int value
;
-
smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get(), &value)
;
+
smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get())
;
+
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 (dot_output != nullptr) {
if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
@@
-381,7
+381,7
@@
int LivenessChecker::main(void)
initial_global_state->prev_req.clear();
}
initial_global_state->prev_pair = current_pair->num;
initial_global_state->prev_req.clear();
}
initial_global_state->prev_pair = current_pair->num;
- initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req,
value
);
+ initial_global_state->prev_req = 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);
@@
-389,7
+389,7
@@
int LivenessChecker::main(void)
XBT_DEBUG("Execute: %s",
simgrid::mc::request_to_string(
XBT_DEBUG("Execute: %s",
simgrid::mc::request_to_string(
- req,
value
, simgrid::mc::RequestType::simix).c_str());
+ req,
req_num
, simgrid::mc::RequestType::simix).c_str());
/* Update mc_stats */
mc_stats->executed_transitions++;
/* Update mc_stats */
mc_stats->executed_transitions++;
@@
-397,7
+397,7
@@
int LivenessChecker::main(void)
mc_stats->visited_pairs++;
/* Answer the request */
mc_stats->visited_pairs++;
/* Answer the request */
-
simgrid::mc::handle_simcall(req, value
);
+
mc_model_checker->handle_simcall(current_pair->graph_state->transition
);
/* Wait for requests (schedules processes) */
mc_model_checker->wait_for_requests();
/* Wait for requests (schedules processes) */
mc_model_checker->wait_for_requests();