From: Gabriel Corona Date: Wed, 13 Apr 2016 13:10:48 +0000 (+0200) Subject: [mc] Remove mc_stats and move remaining stats in ModelChecker for now X-Git-Tag: v3_13~106^2~2 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/cf64c8ceb2027a65be8789e5fb36902e9274be4c?ds=sidebyside [mc] Remove mc_stats and move remaining stats in ModelChecker for now --- diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 0e29e9a0c4..0677f95aff 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -345,8 +345,8 @@ void CommunicationDeterminismChecker::logState() // override XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff); } XBT_INFO("Expanded states = %lu", expandedStatesCount_); - XBT_INFO("Visited states = %lu", mc_stats->visited_states); - XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions); + XBT_INFO("Visited states = %lu", mc_model_checker->visited_states); + XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions); if (simgrid::mc::initial_global_state != nullptr) XBT_INFO("Send-deterministic : %s", !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes"); @@ -418,7 +418,7 @@ int CommunicationDeterminismChecker::main(void) state->interleaveSize()); /* Update statistics */ - mc_stats->visited_states++; + mc_model_checker->visited_states++; if (stack_.size() <= (std::size_t) _sg_mc_max_depth && (req = MC_state_get_request(state)) != nullptr @@ -434,7 +434,7 @@ int CommunicationDeterminismChecker::main(void) if (dot_output != nullptr) req_str = simgrid::mc::request_get_dot_output(req, req_num); - mc_stats->executed_transitions++; + mc_model_checker->executed_transitions++; /* TODO : handle test and testany simcalls */ e_mc_call_type_t call = MC_CALL_TYPE_NONE; diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index e3688e292f..584337f5b5 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -224,7 +224,7 @@ void LivenessChecker::replay() /* Update statistics */ visitedPairsCount_++; - mc_stats->executed_transitions++; + mc_model_checker->executed_transitions++; depth++; @@ -306,7 +306,7 @@ void LivenessChecker::logState() // override Checker::logState(); XBT_INFO("Expanded pairs = %lu", expandedPairsCount_); XBT_INFO("Visited pairs = %lu", visitedPairsCount_); - XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions); + XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions); } void LivenessChecker::showAcceptanceCycle(std::size_t depth) @@ -399,8 +399,8 @@ int LivenessChecker::main(void) simgrid::mc::request_to_string( req, req_num, simgrid::mc::RequestType::simix).c_str()); - /* Update mc_stats */ - mc_stats->executed_transitions++; + /* Update stats */ + mc_model_checker->executed_transitions++; if (!current_pair->exploration_started) visitedPairsCount_++; diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 9aaffdd876..b5baea4270 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -111,9 +111,6 @@ void ModelChecker::start() process_->init(); - /* Initialize statistics */ - mc_stats = xbt_new0(s_mc_stats_t, 1); - if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0')) MC_init_dot_output(); diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index 394a8c1822..6619f25c87 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -81,6 +81,9 @@ private: void handle_waitpid(); void on_signal(const struct signalfd_siginfo* info); +public: + unsigned long visited_states = 0; + unsigned long executed_transitions = 0; }; } diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index e59dd97b95..5e106adb04 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -91,8 +91,8 @@ void SafetyChecker::logState() // override { Checker::logState(); XBT_INFO("Expanded states = %lu", expandedStatesCount_); - XBT_INFO("Visited states = %lu", mc_stats->visited_states); - XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions); + XBT_INFO("Visited states = %lu", mc_model_checker->visited_states); + XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions); } int SafetyChecker::run() @@ -110,7 +110,7 @@ int SafetyChecker::run() stack_.size(), state, state->num, state->interleaveSize()); - mc_stats->visited_states++; + mc_model_checker->visited_states++; // The interleave set is empty or the maximum depth is reached, // let's back-track. @@ -135,7 +135,7 @@ int SafetyChecker::run() if (dot_output != nullptr) req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument); - mc_stats->executed_transitions++; + mc_model_checker->executed_transitions++; /* Answer the request */ this->getSession().execute(state->transition); diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 630adb9fe8..1213e1c1b3 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -64,8 +64,6 @@ std::vector processes_time; simgrid::mc::State* mc_current_state = nullptr; char mc_replay_mode = false; -mc_stats_t mc_stats = nullptr; - /* Liveness */ namespace simgrid { @@ -189,8 +187,8 @@ void replay(std::list> const& stack) } /* Update statistics */ - mc_stats->visited_states++; - mc_stats->executed_transitions++; + mc_model_checker->visited_states++; + mc_model_checker->executed_transitions++; } diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 235a5beafb..ad313238e7 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -64,15 +64,6 @@ XBT_PRIVATE extern FILE *dot_output; XBT_PRIVATE void MC_show_deadlock(void); -/****************************** Statistics ************************************/ - -typedef struct mc_stats { - unsigned long visited_states; - unsigned long executed_transitions; -} s_mc_stats_t, *mc_stats_t; - -XBT_PRIVATE extern mc_stats_t mc_stats; - /********************************** Snapshot comparison **********************************/ //#define MC_DEBUG 1