mc: snake_case the checkers

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 874875a..7bc9774 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -150,7 +150,7 @@ static void MC_report_crash(int status)
   else
     XBT_INFO("No core dump was generated by the system.");
   XBT_INFO("Counter-example execution trace:");
-  for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
+  for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
   simgrid::mc::dumpRecordPath();
   simgrid::mc::session->log_state();
@@ -164,7 +164,7 @@ static void MC_report_assertion_error()
   XBT_INFO("*** PROPERTY NOT VALID ***");
   XBT_INFO("**************************");
   XBT_INFO("Counter-example execution trace:");
-  for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
+  for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
   simgrid::mc::dumpRecordPath();
   simgrid::mc::session->log_state();

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 96f377a..1089f65 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -117,7 +117,7 @@ void Session::restore_initial_state()
 
 void Session::log_state()
 {
-  mc_model_checker->getChecker()->logState();
+  mc_model_checker->getChecker()->log_state();
 
   if (not _sg_mc_dot_output_file.get().empty()) {
     fprintf(dot_output, "}\n");

diff --git a/src/mc/checker/Checker.hpp b/src/mc/checker/Checker.hpp
index 96a1f20..c71f17e 100644 (file)
--- a/src/mc/checker/Checker.hpp
+++ b/src/mc/checker/Checker.hpp
@@ -48,18 +48,19 @@ public:
   /** Show the current trace/stack
    *
    *  Could this be handled in the Session/ModelChecker instead? */
-  virtual RecordTrace getRecordTrace() = 0;
+  virtual RecordTrace get_record_trace() = 0;
 
   /** Generate a textual execution trace of the simulated application */
-  virtual std::vector<std::string> getTextualTrace() = 0;
+  virtual std::vector<std::string> get_textual_trace() = 0;
 
   /** Log additional information about the state of the model-checker */
-  virtual void logState() = 0;
+  virtual void log_state() = 0;
 
 protected:
-  Session& getSession() { return *session_; }
+  Session& get_session() { return *session_; }
 };
 
+// External constructors so that the types (and the types of their content) remain hidden
 XBT_PUBLIC Checker* createLivenessChecker(Session& session);
 XBT_PUBLIC Checker* createSafetyChecker(Session& session);
 XBT_PUBLIC Checker* createCommunicationDeterminismChecker(Session& session);

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 24bdad1..31d3df5 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -282,7 +282,7 @@ CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& s) : C
 
 CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default;
 
-RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
+RecordTrace CommunicationDeterminismChecker::get_record_trace() // override
 {
   RecordTrace res;
   for (auto const& state : stack_)
@@ -290,7 +290,7 @@ RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
   return res;
 }
 
-std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
+std::vector<std::string> CommunicationDeterminismChecker::get_textual_trace() // override
 {
   std::vector<std::string> trace;
   for (auto const& state : stack_) {
@@ -302,7 +302,7 @@ std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // o
   return trace;
 }
 
-void CommunicationDeterminismChecker::logState() // override
+void CommunicationDeterminismChecker::log_state() // override
 {
   if (_sg_mc_comms_determinism && not this->recv_deterministic && this->send_deterministic) {
     XBT_INFO("******************************************************");
@@ -315,7 +315,7 @@ void CommunicationDeterminismChecker::logState() // override
     XBT_INFO("******************************************************");
     XBT_INFO("%s", this->send_diff);
   }
-  XBT_INFO("Expanded states = %lu", expandedStatesCount_);
+  XBT_INFO("Expanded states = %lu", expanded_states_count_);
   XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
   XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
   XBT_INFO("Send-deterministic : %s", not this->send_deterministic ? "No" : "Yes");
@@ -331,7 +331,7 @@ void CommunicationDeterminismChecker::prepare()
   incomplete_communications_pattern.resize(maxpid);
 
   std::unique_ptr<simgrid::mc::State> initial_state =
-      std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
+      std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
 
   XBT_DEBUG("********* Start communication determinism verification *********");
 
@@ -451,7 +451,7 @@ void CommunicationDeterminismChecker::real_run()
 
       /* Create the new expanded state */
       std::unique_ptr<simgrid::mc::State> next_state =
-          std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
+          std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
 
       /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at
        * least, data are transferred). These communications  are incomplete and they cannot be analyzed and compared
@@ -459,7 +459,7 @@ void CommunicationDeterminismChecker::real_run()
       bool compare_snapshots = all_communications_are_finished() && this->initial_communications_pattern_done;
 
       if (_sg_mc_max_visited_states != 0)
-        visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots);
+        visited_state = visited_states_.addVisitedState(expanded_states_count_, next_state.get(), compare_snapshots);
       else
         visited_state = nullptr;
 

diff --git a/src/mc/checker/CommunicationDeterminismChecker.hpp b/src/mc/checker/CommunicationDeterminismChecker.hpp
index 66181d8..c10d60f 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.hpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.hpp
@@ -21,12 +21,13 @@ public:
   explicit CommunicationDeterminismChecker(Session& session);
   ~CommunicationDeterminismChecker();
   void run() override;
-  RecordTrace getRecordTrace() override;
-  std::vector<std::string> getTextualTrace() override;
+  RecordTrace get_record_trace() override;
+  std::vector<std::string> get_textual_trace() override;
+
 private:
   void prepare();
   void real_run();
-  void logState() override;
+  void log_state() override;
   void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking);
   void restoreState();
 public:
@@ -38,8 +39,8 @@ public:
 private:
   /** Stack representing the position in the exploration graph */
   std::list<std::unique_ptr<simgrid::mc::State>> stack_;
-  simgrid::mc::VisitedStates visitedStates_;
-  unsigned long expandedStatesCount_ = 0;
+  simgrid::mc::VisitedStates visited_states_;
+  unsigned long expanded_states_count_ = 0;
 
   bool initial_communications_pattern_done = false;
   bool recv_deterministic                  = true;

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 2f7a6a9..89f2581 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -70,7 +70,7 @@ static bool evaluate_label(xbt_automaton_exp_label_t l, std::vector<int> const&
 Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs)
 {}
 
-std::shared_ptr<const std::vector<int>> LivenessChecker::getPropositionValues()
+std::shared_ptr<const std::vector<int>> LivenessChecker::get_proposition_values()
 {
   std::vector<int> values;
   unsigned int cursor = 0;
@@ -87,13 +87,13 @@ int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::Visi
   return simgrid::mc::snapshot_compare(s1, s2);
 }
 
-std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::Pair* pair)
+std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc::Pair* pair)
 {
   std::shared_ptr<VisitedPair> new_pair = std::make_shared<VisitedPair>(
     pair->num, pair->automaton_state, pair->atomic_propositions,
     pair->graph_state);
 
-  auto res = boost::range::equal_range(acceptancePairs_, new_pair.get(),
+  auto res = boost::range::equal_range(acceptance_pairs_, new_pair.get(),
                                        simgrid::mc::DerefAndCompareByActorsCountAndUsedHeap());
 
   if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) {
@@ -104,22 +104,22 @@ std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::
         || this->compare(pair_test.get(), new_pair.get()) != 0)
       continue;
     XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
-    explorationStack_.pop_back();
+    exploration_stack_.pop_back();
     if (dot_output != nullptr)
-      fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previousPair_, pair_test->num,
-              this->previousRequest_.c_str());
+      fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num,
+              this->previous_request_.c_str());
     return nullptr;
   }
 
-  acceptancePairs_.insert(res.first, new_pair);
+  acceptance_pairs_.insert(res.first, new_pair);
   return new_pair;
 }
 
-void LivenessChecker::removeAcceptancePair(int pair_num)
+void LivenessChecker::remove_acceptance_pair(int pair_num)
 {
-  for (auto i = acceptancePairs_.begin(); i != acceptancePairs_.end(); ++i)
+  for (auto i = acceptance_pairs_.begin(); i != acceptance_pairs_.end(); ++i)
     if ((*i)->num == pair_num) {
-      acceptancePairs_.erase(i);
+      acceptance_pairs_.erase(i);
       break;
     }
 }
@@ -130,7 +130,7 @@ void LivenessChecker::replay()
 
   /* Intermediate backtracking */
   if(_sg_mc_checkpoint > 0) {
-    simgrid::mc::Pair* pair = explorationStack_.back().get();
+    simgrid::mc::Pair* pair = exploration_stack_.back().get();
     if(pair->graph_state->system_state){
       pair->graph_state->system_state->restore(&mc_model_checker->process());
       return;
@@ -142,8 +142,8 @@ void LivenessChecker::replay()
 
   /* Traverse the stack from the initial state and re-execute the transitions */
   int depth = 1;
-  for (std::shared_ptr<Pair> const& pair : explorationStack_) {
-    if (pair == explorationStack_.back())
+  for (std::shared_ptr<Pair> const& pair : exploration_stack_) {
+    if (pair == exploration_stack_.back())
       break;
 
     std::shared_ptr<State> state = pair->graph_state;
@@ -169,11 +169,11 @@ void LivenessChecker::replay()
           state.get());
       }
 
-      this->getSession().execute(state->transition);
+      this->get_session().execute(state->transition);
     }
 
     /* Update statistics */
-    visitedPairsCount_++;
+    visited_pairs_count_++;
     mc_model_checker->executed_transitions++;
 
     depth++;
@@ -186,7 +186,7 @@ void LivenessChecker::replay()
 /**
  * @brief Checks whether a given pair has already been visited by the algorithm.
  */
-int LivenessChecker::insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair, simgrid::mc::Pair* pair)
+int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pair, simgrid::mc::Pair* pair)
 {
   if (_sg_mc_max_visited_states == 0)
     return -1;
@@ -195,7 +195,7 @@ int LivenessChecker::insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair
     visited_pair =
         std::make_shared<VisitedPair>(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
 
-  auto range = boost::range::equal_range(visitedPairs_, visited_pair.get(),
+  auto range = boost::range::equal_range(visited_pairs_, visited_pair.get(),
                                          simgrid::mc::DerefAndCompareByActorsCountAndUsedHeap());
 
   for (auto i = range.first; i != range.second; ++i) {
@@ -218,18 +218,18 @@ int LivenessChecker::insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair
     return (*i)->other_num;
   }
 
-  visitedPairs_.insert(range.first, std::move(visited_pair));
-  this->purgeVisitedPairs();
+  visited_pairs_.insert(range.first, std::move(visited_pair));
+  this->purge_visited_pairs();
   return -1;
 }
 
-void LivenessChecker::purgeVisitedPairs()
+void LivenessChecker::purge_visited_pairs()
 {
-  if (_sg_mc_max_visited_states != 0 && visitedPairs_.size() > (std::size_t)_sg_mc_max_visited_states) {
+  if (_sg_mc_max_visited_states != 0 && visited_pairs_.size() > (std::size_t)_sg_mc_max_visited_states) {
     // Remove the oldest entry with a linear search:
-    visitedPairs_.erase(boost::min_element(visitedPairs_,
-      [](std::shared_ptr<VisitedPair> const a, std::shared_ptr<VisitedPair> const& b) {
-        return a->num < b->num; } ));
+    visited_pairs_.erase(
+        boost::min_element(visited_pairs_, [](std::shared_ptr<VisitedPair> const a,
+                                              std::shared_ptr<VisitedPair> const& b) { return a->num < b->num; }));
   }
 }
 
@@ -237,38 +237,38 @@ LivenessChecker::LivenessChecker(Session& s) : Checker(s)
 {
 }
 
-RecordTrace LivenessChecker::getRecordTrace() // override
+RecordTrace LivenessChecker::get_record_trace() // override
 {
   RecordTrace res;
-  for (std::shared_ptr<Pair> const& pair : explorationStack_)
+  for (std::shared_ptr<Pair> const& pair : exploration_stack_)
     res.push_back(pair->graph_state->getTransition());
   return res;
 }
 
-void LivenessChecker::logState() // override
+void LivenessChecker::log_state() // override
 {
-  XBT_INFO("Expanded pairs = %lu", expandedPairsCount_);
-  XBT_INFO("Visited pairs = %lu", visitedPairsCount_);
+  XBT_INFO("Expanded pairs = %lu", expanded_pairs_count_);
+  XBT_INFO("Visited pairs = %lu", visited_pairs_count_);
   XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
 }
 
-void LivenessChecker::showAcceptanceCycle(std::size_t depth)
+void LivenessChecker::show_acceptance_cycle(std::size_t depth)
 {
   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
   XBT_INFO("|             ACCEPTANCE CYCLE            |");
   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
   XBT_INFO("Counter-example that violates formula:");
-  for (auto const& s : this->getTextualTrace())
+  for (auto const& s : this->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
   simgrid::mc::dumpRecordPath();
   simgrid::mc::session->log_state();
   XBT_INFO("Counter-example depth: %zu", depth);
 }
 
-std::vector<std::string> LivenessChecker::getTextualTrace() // override
+std::vector<std::string> LivenessChecker::get_textual_trace() // override
 {
   std::vector<std::string> trace;
-  for (std::shared_ptr<Pair> const& pair : explorationStack_) {
+  for (std::shared_ptr<Pair> const& pair : exploration_stack_) {
     int req_num = pair->graph_state->transition.argument;
     smx_simcall_t req = &pair->graph_state->executed_req;
     if (req && req->call != SIMCALL_NONE)
@@ -278,13 +278,13 @@ std::vector<std::string> LivenessChecker::getTextualTrace() // override
   return trace;
 }
 
-std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state,
-                                               std::shared_ptr<const std::vector<int>> propositions)
+std::shared_ptr<Pair> LivenessChecker::create_pair(Pair* current_pair, xbt_automaton_state_t state,
+                                                   std::shared_ptr<const std::vector<int>> propositions)
 {
-  expandedPairsCount_++;
-  std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(expandedPairsCount_);
+  expanded_pairs_count_++;
+  std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(expanded_pairs_count_);
   next_pair->automaton_state      = state;
-  next_pair->graph_state          = std::shared_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
+  next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
   next_pair->atomic_propositions  = std::move(propositions);
   if (current_pair)
     next_pair->depth = current_pair->depth + 1;
@@ -307,20 +307,20 @@ void LivenessChecker::backtrack()
 {
   /* Traverse the stack backwards until a pair with a non empty interleave
      set is found, deleting all the pairs that have it empty in the way. */
-  while (not explorationStack_.empty()) {
-    std::shared_ptr<simgrid::mc::Pair> current_pair = explorationStack_.back();
-    explorationStack_.pop_back();
+  while (not exploration_stack_.empty()) {
+    std::shared_ptr<simgrid::mc::Pair> current_pair = exploration_stack_.back();
+    exploration_stack_.pop_back();
     if (current_pair->requests > 0) {
       /* We found a backtracking point */
       XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
-      explorationStack_.push_back(std::move(current_pair));
+      exploration_stack_.push_back(std::move(current_pair));
       this->replay();
       XBT_DEBUG("Backtracking done");
       break;
     } else {
       XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth);
       if (current_pair->automaton_state->type == 1)
-        this->removeAcceptancePair(current_pair->num);
+        this->remove_acceptance_pair(current_pair->num);
     }
   }
 }
@@ -334,9 +334,9 @@ void LivenessChecker::run()
   simgrid::mc::session->initialize();
 
   /* Initialize */
-  this->previousPair_ = 0;
+  this->previous_pair_ = 0;
 
-  std::shared_ptr<const std::vector<int>> propos = this->getPropositionValues();
+  std::shared_ptr<const std::vector<int>> propos = this->get_proposition_values();
 
   // For each initial state of the property automaton, push a
   // (application_state, automaton_state) pair to the exploration stack:
@@ -344,11 +344,11 @@ void LivenessChecker::run()
   xbt_automaton_state_t automaton_state;
   xbt_dynar_foreach (simgrid::mc::property_automaton->states, cursor, automaton_state)
     if (automaton_state->type == -1)
-      explorationStack_.push_back(this->newPair(nullptr, automaton_state, propos));
+      exploration_stack_.push_back(this->create_pair(nullptr, automaton_state, propos));
 
   /* Actually run the double DFS search for counter-examples */
-  while (not explorationStack_.empty()) {
-    std::shared_ptr<Pair> current_pair = explorationStack_.back();
+  while (not exploration_stack_.empty()) {
+    std::shared_ptr<Pair> current_pair = exploration_stack_.back();
 
     /* Update current state in buchi automaton */
     simgrid::mc::property_automaton->current_state = current_pair->automaton_state;
@@ -365,20 +365,20 @@ void LivenessChecker::run()
 
     std::shared_ptr<VisitedPair> reached_pair;
     if (current_pair->automaton_state->type == 1 && not current_pair->exploration_started) {
-      reached_pair = this->insertAcceptancePair(current_pair.get());
+      reached_pair = this->insert_acceptance_pair(current_pair.get());
       if (reached_pair == nullptr) {
-        this->showAcceptanceCycle(current_pair->depth);
+        this->show_acceptance_cycle(current_pair->depth);
         throw simgrid::mc::LivenessError();
       }
     }
 
     /* Pair already visited ? stop the exploration on the current path */
     if (not current_pair->exploration_started) {
-      int visited_num = this->insertVisitedPair(reached_pair, current_pair.get());
+      int visited_num = this->insert_visited_pair(reached_pair, current_pair.get());
       if (visited_num != -1) {
         if (dot_output != nullptr) {
-          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previousPair_, visited_num,
-                  this->previousRequest_.c_str());
+          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, visited_num,
+                  this->previous_request_.c_str());
           fflush(dot_output);
         }
         XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
@@ -392,14 +392,13 @@ void LivenessChecker::run()
     int req_num = current_pair->graph_state->transition.argument;
 
     if (dot_output != nullptr) {
-      if (this->previousPair_ != 0 && this->previousPair_ != current_pair->num) {
-        fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
-          this->previousPair_, current_pair->num,
-          this->previousRequest_.c_str());
-        this->previousRequest_.clear();
+      if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) {
+        fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, current_pair->num,
+                this->previous_request_.c_str());
+        this->previous_request_.clear();
       }
-      this->previousPair_ = current_pair->num;
-      this->previousRequest_ = simgrid::mc::request_get_dot_output(req, req_num);
+      this->previous_pair_    = current_pair->num;
+      this->previous_request_ = 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);
@@ -412,7 +411,7 @@ void LivenessChecker::run()
     /* Update stats */
     mc_model_checker->executed_transitions++;
     if (not current_pair->exploration_started)
-      visitedPairsCount_++;
+      visited_pairs_count_++;
 
     /* Answer the request */
     mc_model_checker->handle_simcall(current_pair->graph_state->transition);
@@ -424,7 +423,7 @@ void LivenessChecker::run()
     current_pair->exploration_started = true;
 
     /* Get values of atomic propositions (variables used in the property formula) */
-    std::shared_ptr<const std::vector<int>> prop_values = this->getPropositionValues();
+    std::shared_ptr<const std::vector<int>> prop_values = this->get_proposition_values();
 
     // For each enabled transition in the property automaton, push a
     // (application_state, automaton_state) pair to the exploration stack:
@@ -432,8 +431,7 @@ void LivenessChecker::run()
       xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(
           current_pair->automaton_state->out, i, xbt_automaton_transition_t);
       if (evaluate_label(transition_succ->label, *prop_values))
-          explorationStack_.push_back(this->newPair(
-            current_pair.get(), transition_succ->dst, prop_values));
+        exploration_stack_.push_back(this->create_pair(current_pair.get(), transition_succ->dst, prop_values));
      }
 
   }

diff --git a/src/mc/checker/LivenessChecker.hpp b/src/mc/checker/LivenessChecker.hpp
index b37b475..e90523c 100644 (file)
--- a/src/mc/checker/LivenessChecker.hpp
+++ b/src/mc/checker/LivenessChecker.hpp
@@ -58,30 +58,32 @@ public:
   explicit LivenessChecker(Session& session);
   ~LivenessChecker() = default;
   void run() override;
-  RecordTrace getRecordTrace() override;
-  std::vector<std::string> getTextualTrace() override;
-  void logState() override;
+  RecordTrace get_record_trace() override;
+  std::vector<std::string> get_textual_trace() override;
+  void log_state() override;
+
 private:
   int compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2);
-  std::shared_ptr<const std::vector<int>> getPropositionValues();
-  std::shared_ptr<VisitedPair> insertAcceptancePair(simgrid::mc::Pair* pair);
-  int insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair, simgrid::mc::Pair* pair);
-  void showAcceptanceCycle(std::size_t depth);
+  std::shared_ptr<const std::vector<int>> get_proposition_values();
+  std::shared_ptr<VisitedPair> insert_acceptance_pair(simgrid::mc::Pair* pair);
+  int insert_visited_pair(std::shared_ptr<VisitedPair> visited_pair, simgrid::mc::Pair* pair);
+  void show_acceptance_cycle(std::size_t depth);
   void replay();
-  void removeAcceptancePair(int pair_num);
-  void purgeVisitedPairs();
+  void remove_acceptance_pair(int pair_num);
+  void purge_visited_pairs();
   void backtrack();
-  std::shared_ptr<Pair> newPair(Pair* pair, xbt_automaton_state_t state, std::shared_ptr<const std::vector<int>> propositions);
+  std::shared_ptr<Pair> create_pair(Pair* pair, xbt_automaton_state_t state,
+                                    std::shared_ptr<const std::vector<int>> propositions);
 
   // A stack of (application_state, automaton_state) pairs for DFS exploration:
-  std::list<std::shared_ptr<Pair>> explorationStack_;
-  std::list<std::shared_ptr<VisitedPair>> acceptancePairs_;
-  std::list<std::shared_ptr<VisitedPair>> visitedPairs_;
-  unsigned long visitedPairsCount_ = 0;
-  unsigned long expandedPairsCount_ = 0;
-  unsigned long expandedStatesCount_ = 0;
-  int previousPair_ = 0;
-  std::string previousRequest_;
+  std::list<std::shared_ptr<Pair>> exploration_stack_;
+  std::list<std::shared_ptr<VisitedPair>> acceptance_pairs_;
+  std::list<std::shared_ptr<VisitedPair>> visited_pairs_;
+  unsigned long visited_pairs_count_   = 0;
+  unsigned long expanded_pairs_count_  = 0;
+  unsigned long expanded_states_count_ = 0;
+  int previous_pair_                   = 0;
+  std::string previous_request_;
 };
 
 }

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 6b1c4da..796bed5 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -38,7 +38,7 @@ static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* stat
   return snapshot_compare(s1, s2);
 }
 
-void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
+void SafetyChecker::check_non_termination(simgrid::mc::State* current_state)
 {
   for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
     if (snapshot_compare(state->get(), current_state) == 0) {
@@ -47,7 +47,7 @@ void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
       XBT_INFO("******************************************");
       XBT_INFO("Counter-example execution trace:");
-      for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
+      for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
         XBT_INFO("  %s", s.c_str());
       simgrid::mc::dumpRecordPath();
       simgrid::mc::session->log_state();
@@ -56,7 +56,7 @@ void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
     }
 }
 
-RecordTrace SafetyChecker::getRecordTrace() // override
+RecordTrace SafetyChecker::get_record_trace() // override
 {
   RecordTrace res;
   for (auto const& state : stack_)
@@ -64,7 +64,7 @@ RecordTrace SafetyChecker::getRecordTrace() // override
   return res;
 }
 
-std::vector<std::string> SafetyChecker::getTextualTrace() // override
+std::vector<std::string> SafetyChecker::get_textual_trace() // override
 {
   std::vector<std::string> trace;
   for (auto const& state : stack_) {
@@ -77,9 +77,9 @@ std::vector<std::string> SafetyChecker::getTextualTrace() // override
   return trace;
 }
 
-void SafetyChecker::logState() // override
+void SafetyChecker::log_state() // override
 {
-  XBT_INFO("Expanded states = %lu", expandedStatesCount_);
+  XBT_INFO("Expanded states = %lu", expanded_states_count_);
   XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
   XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
 }
@@ -109,11 +109,11 @@ void SafetyChecker::run()
     }
 
     // Backtrack if we are revisiting a state we saw previously
-    if (visitedState_ != nullptr) {
+    if (visited_state_ != nullptr) {
       XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
-                visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num);
+                visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num);
 
-      visitedState_ = nullptr;
+      visited_state_ = nullptr;
       this->backtrack();
       continue;
     }
@@ -143,21 +143,21 @@ void SafetyChecker::run()
     mc_model_checker->executed_transitions++;
 
     /* Actually answer the request: let execute the selected request (MCed does one step) */
-    this->getSession().execute(state->transition);
+    this->get_session().execute(state->transition);
 
     /* Create the new expanded state (copy the state of MCed into our MCer data) */
     std::unique_ptr<simgrid::mc::State> next_state =
-        std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
+        std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
 
     if (_sg_mc_termination)
-      this->checkNonTermination(next_state.get());
+      this->check_non_termination(next_state.get());
 
     /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
     if (_sg_mc_max_visited_states > 0)
-      visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true);
+      visited_state_ = visited_states_.addVisitedState(expanded_states_count_, next_state.get(), true);
 
     /* If this is a new state (or if we don't care about state-equality reduction) */
-    if (visitedState_ == nullptr) {
+    if (visited_state_ == nullptr) {
 
       /* Get an enabled process and insert it in the interleave set of the next state */
       for (auto& remoteActor : mc_model_checker->process().actors()) {
@@ -175,7 +175,7 @@ void SafetyChecker::run()
 
     } else if (dot_output != nullptr)
       std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
-                   visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num,
+                   visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num,
                    req_str.c_str());
 
     stack_.push_back(std::move(next_state));
@@ -257,7 +257,7 @@ void SafetyChecker::backtrack()
       /* We found a back-tracking point, let's loop */
       XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num, stack_.size() + 1);
       stack_.push_back(std::move(state));
-      this->restoreState();
+      this->restore_state();
       XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num, stack_.size());
       break;
     } else {
@@ -266,7 +266,7 @@ void SafetyChecker::backtrack()
   }
 }
 
-void SafetyChecker::restoreState()
+void SafetyChecker::restore_state()
 {
   /* Intermediate backtracking */
   simgrid::mc::State* last_state = stack_.back().get();
@@ -308,7 +308,7 @@ SafetyChecker::SafetyChecker(Session& s) : Checker(s)
   XBT_DEBUG("Starting the safety algorithm");
 
   std::unique_ptr<simgrid::mc::State> initial_state =
-      std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
+      std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Initial state");

diff --git a/src/mc/checker/SafetyChecker.hpp b/src/mc/checker/SafetyChecker.hpp
index f615e6f..1377934 100644 (file)
--- a/src/mc/checker/SafetyChecker.hpp
+++ b/src/mc/checker/SafetyChecker.hpp
@@ -25,19 +25,20 @@ public:
   explicit SafetyChecker(Session& session);
   ~SafetyChecker() = default;
   void run() override;
-  RecordTrace getRecordTrace() override;
-  std::vector<std::string> getTextualTrace() override;
-  void logState() override;
+  RecordTrace get_record_trace() override;
+  std::vector<std::string> get_textual_trace() override;
+  void log_state() override;
+
 private:
-  void checkNonTermination(simgrid::mc::State* current_state);
+  void check_non_termination(simgrid::mc::State* current_state);
   void backtrack();
-  void restoreState();
+  void restore_state();
 
   /** Stack representing the position in the exploration graph */
   std::list<std::unique_ptr<simgrid::mc::State>> stack_;
-  simgrid::mc::VisitedStates visitedStates_;
-  std::unique_ptr<simgrid::mc::VisitedState> visitedState_;
-  unsigned long expandedStatesCount_ = 0;
+  simgrid::mc::VisitedStates visited_states_;
+  std::unique_ptr<simgrid::mc::VisitedState> visited_state_;
+  unsigned long expanded_states_count_ = 0;
 };
 
 }

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 5e8fff4..3621458 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -89,7 +89,7 @@ void MC_show_deadlock()
   XBT_INFO("*** DEAD-LOCK DETECTED ***");
   XBT_INFO("**************************");
   XBT_INFO("Counter-example execution trace:");
-  for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
+  for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
   simgrid::mc::dumpRecordPath();
   simgrid::mc::session->log_state();

diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp
index 115695c..50d659c 100644 (file)
--- a/src/mc/mc_record.cpp
+++ b/src/mc/mc_record.cpp
@@ -98,7 +98,7 @@ std::string traceToString(simgrid::mc::RecordTrace const& trace)
 
 void dumpRecordPath()
 {
-  RecordTrace trace = mc_model_checker->getChecker()->getRecordTrace();
+  RecordTrace trace = mc_model_checker->getChecker()->get_record_trace();
   XBT_INFO("Path = %s", traceToString(trace).c_str());
 }