[mc] Only #include LivenessChecker.hpp in LivenessChecker.cpp

diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp
index f94a9e1..b9e1475 100644 (file)
--- a/src/mc/LivenessChecker.hpp
+++ b/src/mc/LivenessChecker.hpp
@@ -29,8 +29,6 @@ SG_END_DECL()
 namespace simgrid {
 namespace mc {
 
-extern XBT_PRIVATE xbt_automaton_t property_automaton;
-
 struct XBT_PRIVATE Pair {
   int num = 0;
   bool search_cycle = false;

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index e0d636b..af180ca 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -30,7 +30,6 @@
 #include "src/mc/mc_private.h"
 #include "src/mc/mc_ignore.h"
 #include "src/mc/mc_exit.h"
-#include "src/mc/LivenessChecker.hpp"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
 

diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp
index 9874969..06192f2 100644 (file)
--- a/src/mc/mc_compare.cpp
+++ b/src/mc/mc_compare.cpp
@@ -15,7 +15,6 @@
 #include "src/internal_config.h"
 #include "src/mc/mc_forward.hpp"
 #include "src/mc/mc_safety.h"
-#include "src/mc/LivenessChecker.hpp"
 #include "src/mc/mc_private.h"
 #include "src/mc/mc_smx.h"
 #include "src/mc/mc_dwarf.hpp"

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 187a69b..6e9b7b6 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -31,10 +31,10 @@
 #include "src/mc/mc_request.h"
 #include "src/mc/mc_safety.h"
 #include "src/mc/mc_snapshot.h"
-#include "src/mc/LivenessChecker.hpp"
 #include "src/mc/mc_private.h"
 #include "src/mc/mc_unw.h"
 #include "src/mc/mc_smx.h"
+#include "src/mc/Checker.hpp"
 #endif
 
 #include "src/mc/mc_record.h"

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 556eaec..28c1533 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -112,6 +112,9 @@ XBT_PRIVATE void find_object_address(
 XBT_PRIVATE
 int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc::Snapshot* s2);
 
+// Move is somewhere else (in the LivenessChecker class, in the Session class?):
+extern XBT_PRIVATE xbt_automaton_t property_automaton;
+
 }
 }
 

diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp
index 19e7db4..a2f6ce4 100644 (file)
--- a/src/mc/mc_record.cpp
+++ b/src/mc/mc_record.cpp
@@ -30,7 +30,7 @@
 #include "src/mc/mc_private.h"
 #include "src/mc/mc_state.h"
 #include "src/mc/mc_smx.h"
-#include "src/mc/LivenessChecker.hpp"
+#include "src/mc/Checker.hpp"
 #endif
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc,

diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index 8c2e869..fbdd510 100644 (file)
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -19,7 +19,6 @@
 
 #include "src/mc/mc_comm_pattern.h"
 #include "src/mc/mc_safety.h"
-#include "src/mc/LivenessChecker.hpp"
 #include "src/mc/mc_private.h"
 #include "src/mc/Process.hpp"
 #include "src/mc/mc_smx.h"

diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp
index 9e857eb..984ca97 100644 (file)
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -24,7 +24,6 @@
 #include "src/mc/mc_protocol.h"
 #include "src/mc/mc_safety.h"
 #include "src/mc/mc_comm_pattern.h"
-#include "src/mc/LivenessChecker.hpp"
 #include "src/mc/mc_exit.h"
 #include "src/mc/Session.hpp"
 #include "src/mc/Checker.hpp"