Start moving classes into the mc/api directory

diff --git a/MANIFEST.in b/MANIFEST.in
index 3c9f694..19701b6 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -2335,14 +2335,16 @@ include src/mc/ModelChecker.cpp
 include src/mc/ModelChecker.hpp
 include src/mc/Session.cpp
 include src/mc/Session.hpp
-include src/mc/Transition.cpp
-include src/mc/Transition.hpp
-include src/mc/TransitionComm.cpp
-include src/mc/TransitionComm.hpp
 include src/mc/VisitedState.cpp
 include src/mc/VisitedState.hpp
 include src/mc/api.cpp
 include src/mc/api.hpp
+include src/mc/api/State.cpp
+include src/mc/api/State.hpp
+include src/mc/api/Transition.cpp
+include src/mc/api/Transition.hpp
+include src/mc/api/TransitionComm.cpp
+include src/mc/api/TransitionComm.hpp
 include src/mc/checker/Checker.hpp
 include src/mc/checker/CommunicationDeterminismChecker.cpp
 include src/mc/checker/CommunicationDeterminismChecker.hpp
@@ -2392,8 +2394,6 @@ include src/mc/mc_record.hpp
 include src/mc/mc_replay.hpp
 include src/mc/mc_safety.hpp
 include src/mc/mc_smx.cpp
-include src/mc/mc_state.cpp
-include src/mc/mc_state.hpp
 include src/mc/remote/AppSide.cpp
 include src/mc/remote/AppSide.hpp
 include src/mc/remote/Channel.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index a753c9d..a7f0a6d 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -5,8 +5,8 @@
 
 #include "src/mc/ModelChecker.hpp"
 #include "src/mc/Session.hpp"
-#include "src/mc/Transition.hpp"
-#include "src/mc/TransitionComm.hpp"
+#include "src/mc/api/Transition.hpp"
+#include "src/mc/api/TransitionComm.hpp"
 #include "src/mc/checker/Checker.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 286f9e2..02cb8a7 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -11,8 +11,8 @@
 #include "smpi/smpi.h"
 #include "src/smpi/include/private.hpp"
 #endif
+#include "src/mc/api/State.hpp"
 #include "src/mc/mc_private.hpp"
-#include "src/mc/mc_state.hpp"
 #include "xbt/log.h"
 #include "xbt/system_error.hpp"
 

diff --git a/src/mc/VisitedState.hpp b/src/mc/VisitedState.hpp
index 4fe702f..e58bc08 100644 (file)
--- a/src/mc/VisitedState.hpp
+++ b/src/mc/VisitedState.hpp
@@ -6,7 +6,7 @@
 #ifndef SIMGRID_MC_VISITED_STATE_HPP
 #define SIMGRID_MC_VISITED_STATE_HPP
 
-#include "src/mc/mc_state.hpp"
+#include "src/mc/api/State.hpp"
 #include "src/mc/sosp/Snapshot.hpp"
 
 #include <cstddef>

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 7a2676b..ebdc965 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -10,9 +10,9 @@
 #include <vector>
 
 #include "simgrid/forward.h"
+#include "src/mc/api/State.hpp"
 #include "src/mc/mc_forward.hpp"
 #include "src/mc/mc_record.hpp"
-#include "src/mc/mc_state.hpp"
 #include "xbt/automaton.hpp"
 #include "xbt/base.h"
 

diff --git a/src/mc/mc_state.cpp b/src/mc/api/State.cpp
similarity index 96%
rename from src/mc/mc_state.cpp
rename to src/mc/api/State.cpp
index 9871c79..875d4fb 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/api/State.cpp
@@ -3,7 +3,7 @@
 /* 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 "src/mc/mc_state.hpp"
+#include "src/mc/api/State.hpp"
 #include "src/mc/Session.hpp"
 #include "src/mc/api.hpp"
 #include "src/mc/mc_config.hpp"
@@ -28,7 +28,7 @@ State::State() : num_(++expended_states_)
   /* Stateful model checking */
   if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
     auto snapshot_ptr = api::get().take_snapshot(num_);
-    system_state_ = std::shared_ptr<simgrid::mc::Snapshot>(snapshot_ptr);
+    system_state_     = std::shared_ptr<simgrid::mc::Snapshot>(snapshot_ptr);
     if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
       copy_incomplete_comm_pattern();
       copy_index_comm_pattern();
@@ -113,5 +113,5 @@ void State::copy_index_comm_pattern()
     this->communication_indices_.push_back(list_process_comm.index_comm);
 }
 
-}
-}
+} // namespace mc
+} // namespace simgrid

diff --git a/src/mc/mc_state.hpp b/src/mc/api/State.hpp
similarity index 96%
rename from src/mc/mc_state.hpp
rename to src/mc/api/State.hpp
index 739a402..acba0b9 100644 (file)
--- a/src/mc/mc_state.hpp
+++ b/src/mc/api/State.hpp
@@ -6,9 +6,9 @@
 #ifndef SIMGRID_MC_STATE_HPP
 #define SIMGRID_MC_STATE_HPP
 
-#include "src/mc/Transition.hpp"
-#include "src/mc/sosp/Snapshot.hpp"
+#include "src/mc/api/Transition.hpp"
 #include "src/mc/mc_comm_pattern.hpp"
+#include "src/mc/sosp/Snapshot.hpp"
 
 namespace simgrid {
 namespace mc {
@@ -39,7 +39,6 @@ public:
   std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern_;
   std::vector<unsigned> communication_indices_;
 
-
   /* Returns a positive number if there is another transition to pick, or -1 if not */
   int next_transition() const;
 
@@ -58,7 +57,7 @@ private:
   void copy_incomplete_comm_pattern();
   void copy_index_comm_pattern();
 };
-}
-}
+} // namespace mc
+} // namespace simgrid
 
 #endif

diff --git a/src/mc/Transition.cpp b/src/mc/api/Transition.cpp
similarity index 94%
rename from src/mc/Transition.cpp
rename to src/mc/api/Transition.cpp
index 134452e..40caa93 100644 (file)
--- a/src/mc/Transition.cpp
+++ b/src/mc/api/Transition.cpp
@@ -3,8 +3,7 @@
 /* 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 "src/mc/Transition.hpp"
-#include "src/mc/TransitionComm.hpp"
+#include "src/mc/api/Transition.hpp"
 #include "xbt/asserts.h"
 #include <simgrid/config.h>
 #if SIMGRID_HAVE_MC

diff --git a/src/mc/Transition.hpp b/src/mc/api/Transition.hpp
similarity index 100%
rename from src/mc/Transition.hpp
rename to src/mc/api/Transition.hpp

diff --git a/src/mc/TransitionComm.cpp b/src/mc/api/TransitionComm.cpp
similarity index 98%
rename from src/mc/TransitionComm.cpp
rename to src/mc/api/TransitionComm.cpp
index 328c977..6cc54f8 100644 (file)
--- a/src/mc/TransitionComm.cpp
+++ b/src/mc/api/TransitionComm.cpp
@@ -3,13 +3,13 @@
 /* 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 "src/mc/TransitionComm.hpp"
+#include "src/mc/api/TransitionComm.hpp"
 #include "xbt/asserts.h"
 #include <simgrid/config.h>
 #if SIMGRID_HAVE_MC
 #include "src/mc/ModelChecker.hpp"
 #include "src/mc/Session.hpp"
-#include "src/mc/mc_state.hpp"
+#include "src/mc/api/State.hpp"
 #endif
 
 #include <sstream>

diff --git a/src/mc/TransitionComm.hpp b/src/mc/api/TransitionComm.hpp
similarity index 97%
rename from src/mc/TransitionComm.hpp
rename to src/mc/api/TransitionComm.hpp
index e6fa6c9..e2103fa 100644 (file)
--- a/src/mc/TransitionComm.hpp
+++ b/src/mc/api/TransitionComm.hpp
@@ -8,7 +8,7 @@
 #define SIMGRID_MC_TRANSITION_COMM_HPP
 
 #include "src/kernel/actor/SimcallObserver.hpp"
-#include "src/mc/Transition.hpp"
+#include "src/mc/api/Transition.hpp"
 
 #include <string>
 

diff --git a/src/mc/checker/LivenessChecker.hpp b/src/mc/checker/LivenessChecker.hpp
index 11388df..d2d34df 100644 (file)
--- a/src/mc/checker/LivenessChecker.hpp
+++ b/src/mc/checker/LivenessChecker.hpp
@@ -7,8 +7,8 @@
 #ifndef SIMGRID_MC_LIVENESS_CHECKER_HPP
 #define SIMGRID_MC_LIVENESS_CHECKER_HPP
 
+#include "src/mc/api/State.hpp"
 #include "src/mc/checker/Checker.hpp"
-#include "src/mc/mc_state.hpp"
 #include "xbt/automaton.hpp"
 
 #include <list>

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 7362331..5eff438 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -3,10 +3,10 @@
 /* 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 "src/mc/checker/SafetyChecker.hpp"
 #include "src/mc/Session.hpp"
-#include "src/mc/Transition.hpp"
 #include "src/mc/VisitedState.hpp"
-#include "src/mc/checker/SafetyChecker.hpp"
+#include "src/mc/api/Transition.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"

diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp
index 02522b0..2456cac 100644 (file)
--- a/src/mc/mc_record.cpp
+++ b/src/mc/mc_record.cpp
@@ -6,14 +6,14 @@
 #include "src/mc/mc_record.hpp"
 #include "src/kernel/activity/CommImpl.hpp"
 #include "src/kernel/context/Context.hpp"
-#include "src/mc/Transition.hpp"
+#include "src/mc/api/Transition.hpp"
 #include "src/mc/mc_base.hpp"
 #include "src/mc/mc_replay.hpp"
 
 #if SIMGRID_HAVE_MC
+#include "src/mc/api/State.hpp"
 #include "src/mc/checker/Checker.hpp"
 #include "src/mc/mc_private.hpp"
-#include "src/mc/mc_state.hpp"
 #endif
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc, "Logging specific to MC record/replay facility");

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index b4de54e..3ca374d 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -552,7 +552,7 @@ set(MC_SRC_BASE
   src/mc/mc_config.cpp
   src/mc/mc_config.hpp
   src/mc/mc_global.cpp
-  src/mc/Transition.cpp
+  src/mc/api/Transition.cpp
   )
 
 set(MC_SRC
@@ -622,16 +622,16 @@ set(MC_SRC
   src/mc/mc_record.cpp
   src/mc/mc_private.hpp
   src/mc/mc_safety.hpp
-  src/mc/mc_state.hpp
-  src/mc/mc_state.cpp
   src/mc/VisitedState.cpp
   src/mc/VisitedState.hpp
   src/mc/mc_client_api.cpp
   src/mc/mc_smx.cpp
   src/mc/mc_exit.hpp
-  src/mc/Transition.hpp
-  src/mc/TransitionComm.cpp
-  src/mc/TransitionComm.hpp
+  src/mc/api/State.hpp
+  src/mc/api/State.cpp
+  src/mc/api/Transition.hpp
+  src/mc/api/TransitionComm.cpp
+  src/mc/api/TransitionComm.hpp
   src/mc/udpor_global.cpp
   src/mc/udpor_global.hpp
   )