Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Start moving classes into the mc/api directory
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Fri, 11 Feb 2022 18:27:29 +0000 (19:27 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Fri, 11 Feb 2022 18:30:03 +0000 (19:30 +0100)
15 files changed:
MANIFEST.in
src/mc/ModelChecker.cpp
src/mc/Session.cpp
src/mc/VisitedState.hpp
src/mc/api.hpp
src/mc/api/State.cpp [moved from src/mc/mc_state.cpp with 96% similarity]
src/mc/api/State.hpp [moved from src/mc/mc_state.hpp with 96% similarity]
src/mc/api/Transition.cpp [moved from src/mc/Transition.cpp with 94% similarity]
src/mc/api/Transition.hpp [moved from src/mc/Transition.hpp with 100% similarity]
src/mc/api/TransitionComm.cpp [moved from src/mc/TransitionComm.cpp with 98% similarity]
src/mc/api/TransitionComm.hpp [moved from src/mc/TransitionComm.hpp with 97% similarity]
src/mc/checker/LivenessChecker.hpp
src/mc/checker/SafetyChecker.cpp
src/mc/mc_record.cpp
tools/cmake/DefinePackages.cmake

index 3c9f6948c5f1881c2caf70b6c7e2a4feb8730cbb..19701b642abf1f7a5f580c1f9e69a0cc35e93b6d 100644 (file)
@@ -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
index a753c9d3fa0ccb9f3ab1b7812d6a25967006d3e9..a7f0a6d057eaf5e06b253a9e4622855dffc04448 100644 (file)
@@ -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"
index 286f9e266ebb2d169760d8e3354461e5063891fb..02cb8a754d09c61f446b364b3519ab34b5fe7e06 100644 (file)
@@ -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"
 
index 4fe702f92141ef90531c59870c3995132c6e1f70..e58bc089e5e337402581dcfa5636e004969fc958 100644 (file)
@@ -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>
index 7a2676b531f691ad737e9e26d97cfccbff68d598..ebdc9656aa2364f845301306809153393da6d0fa 100644 (file)
@@ -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"
 
similarity index 96%
rename from src/mc/mc_state.cpp
rename to src/mc/api/State.cpp
index 9871c79be658f8ff8095be9c81153fd92f152661..875d4fb460ad6bdb6128ae78a0b33b58bd9da744 100644 (file)
@@ -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
similarity index 96%
rename from src/mc/mc_state.hpp
rename to src/mc/api/State.hpp
index 739a40252a9353866cdb2b9aecfd750b262988ea..acba0b99ac833dca87a23da3d8c09e81dc7b2279 100644 (file)
@@ -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
similarity index 94%
rename from src/mc/Transition.cpp
rename to src/mc/api/Transition.cpp
index 134452e310efdcf3f5e75ea9ecff0c00ed28fb09..40caa931a88383fd9c9fc3e8854ae16917bcbad2 100644 (file)
@@ -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
similarity index 98%
rename from src/mc/TransitionComm.cpp
rename to src/mc/api/TransitionComm.cpp
index 328c977cc529b245f150bddbefb718691d39929c..6cc54f84dcb73dc777647d5791b0f06f10fa5d6c 100644 (file)
@@ -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>
similarity index 97%
rename from src/mc/TransitionComm.hpp
rename to src/mc/api/TransitionComm.hpp
index e6fa6c9cae81650afd6453c23338af0e322eea30..e2103facc4c7cecbfa9585a4d07408618d7a4e0a 100644 (file)
@@ -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>
 
index 11388df20807a11f59f075262657006ea561de10..d2d34dfaa96bcba24fce31c72cc3d674e5e97e94 100644 (file)
@@ -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>
index 7362331d5c88f1b00a536e9da0131ccc443d5bf6..5eff4386873205b2cdbf37277a53299d60cf2590 100644 (file)
@@ -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"
index 02522b06cc2b49194c84962f371947e7e690e9f3..2456caca6a0d6dccc5642d81db8374373edc9c9f 100644 (file)
@@ -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");
index b4de54e65a06f39220c479021e4d70ce5fd02e4f..3ca374d45e81a3f32c451700dc73807e2aacaac8 100644 (file)
@@ -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
   )