From: Gabriel Corona Date: Wed, 13 Apr 2016 12:55:19 +0000 (+0200) Subject: [mc] Move mc_stats.expanded_states into the Checkers X-Git-Tag: v3_13~106^2~4 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/1930bee57857b8ccfbdaa457ea6748a49fc8d4f8 [mc] Move mc_stats.expanded_states into the Checkers --- diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index e5b383d922..0e29e9a0c4 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -344,7 +344,7 @@ void CommunicationDeterminismChecker::logState() // override XBT_INFO("******************************************************"); XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff); } - XBT_INFO("Expanded states = %lu", mc_stats->expanded_states); + XBT_INFO("Expanded states = %lu", expandedStatesCount_); XBT_INFO("Visited states = %lu", mc_stats->visited_states); XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions); if (simgrid::mc::initial_global_state != nullptr) @@ -376,7 +376,7 @@ void CommunicationDeterminismChecker::prepare() } std::unique_ptr initial_state = - std::unique_ptr(MC_state_new()); + std::unique_ptr(MC_state_new(++expandedStatesCount_)); XBT_DEBUG("********* Start communication determinism verification *********"); @@ -455,7 +455,7 @@ int CommunicationDeterminismChecker::main(void) /* Create the new expanded state */ std::unique_ptr next_state = - std::unique_ptr(MC_state_new()); + std::unique_ptr(MC_state_new(++expandedStatesCount_)); /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at least, data are transfered). @@ -465,7 +465,8 @@ int CommunicationDeterminismChecker::main(void) && initial_global_state->initial_communications_pattern_done; if (_sg_mc_visited == 0 - || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) { + || (visited_state = visitedStates_.addVisitedState( + expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) { /* Get enabled processes and insert them in the interleave set of the next state */ for (auto& p : mc_model_checker->process().simix_processes()) diff --git a/src/mc/CommunicationDeterminismChecker.hpp b/src/mc/CommunicationDeterminismChecker.hpp index 291d98ec4f..781c2ba143 100644 --- a/src/mc/CommunicationDeterminismChecker.hpp +++ b/src/mc/CommunicationDeterminismChecker.hpp @@ -34,6 +34,7 @@ private: /** Stack representing the position in the exploration graph */ std::list> stack_; simgrid::mc::VisitedStates visitedStates_; + unsigned long expandedStatesCount_ = 0; }; #endif diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index e5613cd6bf..e3688e292f 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -438,7 +438,7 @@ std::shared_ptr LivenessChecker::newPair(Pair* current_pair, xbt_automaton { std::shared_ptr next_pair = std::make_shared(++expandedPairsCount_); next_pair->automaton_state = state; - next_pair->graph_state = std::shared_ptr(MC_state_new()); + next_pair->graph_state = std::shared_ptr(MC_state_new(++expandedStatesCount_)); next_pair->atomic_propositions = std::move(propositions); if (current_pair) next_pair->depth = current_pair->depth + 1; diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp index 3cbfce31bf..128722ba60 100644 --- a/src/mc/LivenessChecker.hpp +++ b/src/mc/LivenessChecker.hpp @@ -89,6 +89,7 @@ private: std::list> visitedPairs_; unsigned long visitedPairsCount_ = 0; unsigned long expandedPairsCount_ = 0; + unsigned long expandedStatesCount_ = 0; }; } diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index b51d39adae..e59dd97b95 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -90,7 +90,7 @@ std::vector SafetyChecker::getTextualTrace() // override void SafetyChecker::logState() // override { Checker::logState(); - XBT_INFO("Expanded states = %lu", mc_stats->expanded_states); + XBT_INFO("Expanded states = %lu", expandedStatesCount_); XBT_INFO("Visited states = %lu", mc_stats->visited_states); XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions); } @@ -142,7 +142,7 @@ int SafetyChecker::run() /* Create the new expanded state */ std::unique_ptr next_state = - std::unique_ptr(MC_state_new()); + std::unique_ptr(MC_state_new(++expandedStatesCount_)); if (_sg_mc_termination && this->checkNonTermination(next_state.get())) { MC_show_non_termination(); @@ -150,7 +150,7 @@ int SafetyChecker::run() } if (_sg_mc_visited == 0 - || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) { + || (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true)) == nullptr) { /* Get an enabled process and insert it in the interleave set of the next state */ for (auto& p : mc_model_checker->process().simix_processes()) @@ -298,7 +298,7 @@ void SafetyChecker::init() XBT_DEBUG("Starting the safety algorithm"); std::unique_ptr initial_state = - std::unique_ptr(MC_state_new()); + std::unique_ptr(MC_state_new(++expandedStatesCount_)); XBT_DEBUG("**************************************************"); XBT_DEBUG("Initial state"); diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp index a9662be45b..71b5f67d92 100644 --- a/src/mc/SafetyChecker.hpp +++ b/src/mc/SafetyChecker.hpp @@ -38,6 +38,7 @@ private: std::list> stack_; simgrid::mc::VisitedStates visitedStates_; std::unique_ptr visitedState_; + unsigned long expandedStatesCount_ = 0; }; } diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp index 746a0f115d..6d0e87e7cc 100644 --- a/src/mc/VisitedState.cpp +++ b/src/mc/VisitedState.cpp @@ -39,7 +39,7 @@ static int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::Visi * \brief Save the current state * \return Snapshot of the current state. */ -VisitedState::VisitedState() +VisitedState::VisitedState(unsigned long state_number) { simgrid::mc::Process* process = &(mc_model_checker->process()); this->heap_bytes_used = mmalloc_get_bytes_used_remote( @@ -49,8 +49,8 @@ VisitedState::VisitedState() this->nb_processes = mc_model_checker->process().simix_processes().size(); - this->system_state = simgrid::mc::take_snapshot(mc_stats->expanded_states); - this->num = mc_stats->expanded_states; + this->system_state = simgrid::mc::take_snapshot(state_number); + this->num = state_number; this->other_num = -1; } @@ -76,10 +76,11 @@ void VisitedStates::prune() /** * \brief Checks whether a given state has already been visited by the algorithm. */ -std::unique_ptr VisitedStates::addVisitedState(simgrid::mc::State* graph_state, bool compare_snpashots) +std::unique_ptr VisitedStates::addVisitedState( + unsigned long state_number, simgrid::mc::State* graph_state, bool compare_snpashots) { std::unique_ptr new_state = - std::unique_ptr(new VisitedState()); + std::unique_ptr(new VisitedState(state_number)); graph_state->system_state = new_state->system_state; XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state.get(), new_state->num, graph_state->num); diff --git a/src/mc/VisitedState.hpp b/src/mc/VisitedState.hpp index 364c8bfa52..13691af2e3 100644 --- a/src/mc/VisitedState.hpp +++ b/src/mc/VisitedState.hpp @@ -23,7 +23,7 @@ struct XBT_PRIVATE VisitedState { int num = 0; int other_num = 0; // dot_output for - VisitedState(); + VisitedState(unsigned long state_number); ~VisitedState(); }; @@ -31,7 +31,7 @@ class XBT_PRIVATE VisitedStates { std::vector> states_; public: void clear() { states_.clear(); } - std::unique_ptr addVisitedState(simgrid::mc::State* graph_state, bool compare_snpashots); + std::unique_ptr addVisitedState(unsigned long state_number, simgrid::mc::State* graph_state, bool compare_snpashots); private: void prune(); }; diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 83083888f1..ae5e000deb 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -69,7 +69,6 @@ XBT_PRIVATE void MC_show_deadlock(void); typedef struct mc_stats { unsigned long state_size; unsigned long visited_states; - unsigned long expanded_states; unsigned long executed_transitions; } s_mc_stats_t, *mc_stats_t; diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index 8f675cf61d..50df4a3f11 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -28,13 +28,13 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc, /** * \brief Creates a state data structure used by the exploration algorithm */ -simgrid::mc::State* MC_state_new() +simgrid::mc::State* MC_state_new(unsigned long state_number) { simgrid::mc::State* state = new simgrid::mc::State(); state->processStates.resize(MC_smx_get_maxpid()); - state->num = ++mc_stats->expanded_states; + state->num = state_number; /* Stateful model checking */ - if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) || _sg_mc_termination){ + if((_sg_mc_checkpoint > 0 && (state_number % _sg_mc_checkpoint == 0)) || _sg_mc_termination){ state->system_state = simgrid::mc::take_snapshot(state->num); if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ MC_state_copy_incomplete_communications_pattern(state); diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h index 43554bffd0..599b0cb785 100644 --- a/src/mc/mc_state.h +++ b/src/mc/mc_state.h @@ -151,7 +151,7 @@ XBT_PRIVATE void replay(std::list> const& st } } -XBT_PRIVATE simgrid::mc::State* MC_state_new(void); +XBT_PRIVATE simgrid::mc::State* MC_state_new(unsigned long state_number); XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state); #endif