mc: snake_case a class

[simgrid.git] / src / mc / checker / LivenessChecker.cpp

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index cd49a87..2f7a6a9 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -3,32 +3,16 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
-#include <cstring>
-
-#include <memory>
-#include <list>
-
-#include <boost/range/algorithm.hpp>
-
-#include <unistd.h>
-#include <sys/wait.h>
-
-#include <xbt/automaton.h>
-#include <xbt/dynar.h>
-#include <xbt/log.h>
-#include <xbt/sysdep.h>
-
-#include "src/mc/Session.hpp"
-#include "src/mc/Transition.hpp"
 #include "src/mc/checker/LivenessChecker.hpp"
+#include "src/mc/Session.hpp"
+#include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
-#include "src/mc/mc_private.hpp"
-#include "src/mc/mc_record.hpp"
-#include "src/mc/mc_replay.hpp"
 #include "src/mc/mc_request.hpp"
 #include "src/mc/mc_smx.hpp"
-#include "src/mc/remote/Client.hpp"
+
+#include <boost/range/algorithm.hpp>
+#include <cstring>
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification");
 
@@ -148,13 +132,13 @@ void LivenessChecker::replay()
   if(_sg_mc_checkpoint > 0) {
     simgrid::mc::Pair* pair = explorationStack_.back().get();
     if(pair->graph_state->system_state){
-      simgrid::mc::restore_snapshot(pair->graph_state->system_state);
+      pair->graph_state->system_state->restore(&mc_model_checker->process());
       return;
     }
   }
 
   /* Restore the initial state */
-  simgrid::mc::session->restoreInitialState();
+  simgrid::mc::session->restore_initial_state();
 
   /* Traverse the stack from the initial state and re-execute the transitions */
   int depth = 1;
@@ -277,7 +261,7 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth)
   for (auto const& s : this->getTextualTrace())
     XBT_INFO("  %s", s.c_str());
   simgrid::mc::dumpRecordPath();
-  simgrid::mc::session->logState();
+  simgrid::mc::session->log_state();
   XBT_INFO("Counter-example depth: %zu", depth);
 }
 
@@ -455,7 +439,7 @@ void LivenessChecker::run()
   }
 
   XBT_INFO("No property violation found.");
-  simgrid::mc::session->logState();
+  simgrid::mc::session->log_state();
 }
 
 Checker* createLivenessChecker(Session& s)