From e1459ae1f3ca27cf74f3592980445151049defd1 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Thu, 14 Apr 2016 11:09:12 +0200 Subject: [PATCH] [mc] Move mc_global stuff into LivenessChecker This gets rid of initial_global_state in LivenessChecker. --- src/mc/LivenessChecker.cpp | 24 +++++++++++------------- src/mc/LivenessChecker.hpp | 2 ++ src/mc/mc_snapshot.h | 2 -- 3 files changed, 13 insertions(+), 15 deletions(-) diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index 81b9833447..8dae669664 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -139,8 +139,8 @@ std::shared_ptr LivenessChecker::insertAcceptancePair(simgrid::mc:: 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; } @@ -159,7 +159,7 @@ void LivenessChecker::removeAcceptancePair(int pair_num) void LivenessChecker::prepare(void) { - initial_global_state->prev_pair = 0; + this->previousPair_ = 0; std::shared_ptr> propos = this->getPropositionValues(); @@ -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", - 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); @@ -381,14 +381,14 @@ int LivenessChecker::main(void) 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", - 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); @@ -485,12 +485,10 @@ int LivenessChecker::run() MC_automaton_load(_sg_mc_property_file); XBT_DEBUG("Starting the liveness algorithm"); - simgrid::mc::initial_global_state = std::unique_ptr(new s_mc_global_t()); simgrid::mc::session->initialize(); this->prepare(); int res = this->main(); - simgrid::mc::initial_global_state = nullptr; return res; } diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp index 128722ba60..efac9ad815 100644 --- a/src/mc/LivenessChecker.hpp +++ b/src/mc/LivenessChecker.hpp @@ -90,6 +90,8 @@ private: unsigned long visitedPairsCount_ = 0; unsigned long expandedPairsCount_ = 0; unsigned long expandedStatesCount_ = 0; + int previousPair_ = 0; + std::string previousRequest_; }; } diff --git a/src/mc/mc_snapshot.h b/src/mc/mc_snapshot.h index 591acdd7bd..7befa377df 100644 --- a/src/mc/mc_snapshot.h +++ b/src/mc/mc_snapshot.h @@ -129,8 +129,6 @@ typedef struct XBT_PRIVATE s_mc_snapshot_stack { } 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; -- 2.20.1