This gets rid of initial_global_state in LivenessChecker.
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());
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();
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);
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);
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;
unsigned long visitedPairsCount_ = 0;
unsigned long expandedPairsCount_ = 0;
unsigned long expandedStatesCount_ = 0;
unsigned long visitedPairsCount_ = 0;
unsigned long expandedPairsCount_ = 0;
unsigned long expandedStatesCount_ = 0;
+ int previousPair_ = 0;
+ std::string previousRequest_;
} s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
typedef struct s_mc_global_t {
} s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
typedef struct s_mc_global_t {
- int prev_pair = 0;
- std::string prev_req;
int initial_communications_pattern_done = 0;
int recv_deterministic = 0;
int send_deterministic = 0;
int initial_communications_pattern_done = 0;
int recv_deterministic = 0;
int send_deterministic = 0;