The checker now have a reference to the session

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index ecab76b..ce7b065 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -399,19 +399,19 @@ simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm
   simgrid::mc::Checker* checker;
   switch (algo) {
     case CheckerAlgorithm::CommDeterminism:
-      checker = simgrid::mc::createCommunicationDeterminismChecker();
+      checker = simgrid::mc::createCommunicationDeterminismChecker(session);
       break;
 
     case CheckerAlgorithm::UDPOR:
-      checker = simgrid::mc::createUdporChecker();
+      checker = simgrid::mc::createUdporChecker(session);
       break;
 
     case CheckerAlgorithm::Safety:
-      checker = simgrid::mc::createSafetyChecker();
+      checker = simgrid::mc::createSafetyChecker(session);
       break;
 
     case CheckerAlgorithm::Liveness:
-      checker = simgrid::mc::createLivenessChecker();
+      checker = simgrid::mc::createLivenessChecker(session);
       break;
 
     default:

diff --git a/src/mc/checker/Checker.hpp b/src/mc/checker/Checker.hpp
index 1fe6c64..ebc0448 100644 (file)
--- a/src/mc/checker/Checker.hpp
+++ b/src/mc/checker/Checker.hpp
@@ -26,8 +26,10 @@ namespace mc {
  *  have all the necessary features). */
 // abstract
 class Checker {
+  Session* session_;
+
 public:
-  explicit Checker() = default;
+  explicit Checker(Session* session) : session_(session) {}
 
   // No copy:
   Checker(Checker const&) = delete;
@@ -52,13 +54,15 @@ public:
 
   /** Log additional information about the state of the model-checker */
   virtual void log_state() = 0;
+
+  Session* get_session() { return session_; }
 };
 
 // External constructors so that the types (and the types of their content) remain hidden
-XBT_PUBLIC Checker* createLivenessChecker();
-XBT_PUBLIC Checker* createSafetyChecker();
-XBT_PUBLIC Checker* createCommunicationDeterminismChecker();
-XBT_PUBLIC Checker* createUdporChecker();
+XBT_PUBLIC Checker* createLivenessChecker(Session* session);
+XBT_PUBLIC Checker* createSafetyChecker(Session* session);
+XBT_PUBLIC Checker* createCommunicationDeterminismChecker(Session* session);
+XBT_PUBLIC Checker* createUdporChecker(Session* session);
 
 } // namespace mc
 } // namespace simgrid

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 47b7ad5..b0f373a 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -255,7 +255,7 @@ void CommunicationDeterminismChecker::complete_comm_pattern(RemotePtr<kernel::ac
   }
 }
 
-CommunicationDeterminismChecker::CommunicationDeterminismChecker() : Checker() {}
+CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session* session) : Checker(session) {}
 
 CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default;
 
@@ -533,9 +533,9 @@ void CommunicationDeterminismChecker::run()
   this->real_run();
 }
 
-Checker* createCommunicationDeterminismChecker()
+Checker* createCommunicationDeterminismChecker(Session* session)
 {
-  return new CommunicationDeterminismChecker();
+  return new CommunicationDeterminismChecker(session);
 }
 
 } // namespace mc

diff --git a/src/mc/checker/CommunicationDeterminismChecker.hpp b/src/mc/checker/CommunicationDeterminismChecker.hpp
index ca9f694..3c92f89 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.hpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.hpp
@@ -18,7 +18,7 @@ namespace mc {
 
 class XBT_PRIVATE CommunicationDeterminismChecker : public Checker {
 public:
-  explicit CommunicationDeterminismChecker();
+  explicit CommunicationDeterminismChecker(Session* session);
   ~CommunicationDeterminismChecker() override;
   void run() override;
   RecordTrace get_record_trace() override;

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index a1b2ca6..f5b5643 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -202,9 +202,7 @@ void LivenessChecker::purge_visited_pairs()
   }
 }
 
-LivenessChecker::LivenessChecker() : Checker()
-{
-}
+LivenessChecker::LivenessChecker(Session* session) : Checker(session) {}
 
 RecordTrace LivenessChecker::get_record_trace() // override
 {
@@ -408,9 +406,9 @@ void LivenessChecker::run()
   api::get().log_state();
 }
 
-Checker* createLivenessChecker()
+Checker* createLivenessChecker(Session* session)
 {
-  return new LivenessChecker();
+  return new LivenessChecker(session);
 }
 
 } // namespace mc

diff --git a/src/mc/checker/LivenessChecker.hpp b/src/mc/checker/LivenessChecker.hpp
index 39f899f..cb972c5 100644 (file)
--- a/src/mc/checker/LivenessChecker.hpp
+++ b/src/mc/checker/LivenessChecker.hpp
@@ -51,7 +51,7 @@ public:
 
 class XBT_PRIVATE LivenessChecker : public Checker {
 public:
-  explicit LivenessChecker();
+  explicit LivenessChecker(Session* session);
   void run() override;
   RecordTrace get_record_trace() override;
   std::vector<std::string> get_textual_trace() override;

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 42e8bc6..cefde1f 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -253,7 +253,7 @@ void SafetyChecker::restore_state()
   }
 }
 
-SafetyChecker::SafetyChecker() : Checker()
+SafetyChecker::SafetyChecker(Session* session) : Checker(session)
 {
   reductionMode_ = reduction_mode;
   if (_sg_mc_termination)
@@ -290,9 +290,9 @@ SafetyChecker::SafetyChecker() : Checker()
   stack_.push_back(std::move(initial_state));
 }
 
-Checker* createSafetyChecker()
+Checker* createSafetyChecker(Session* session)
 {
-  return new SafetyChecker();
+  return new SafetyChecker(session);
 }
 
 } // namespace mc

diff --git a/src/mc/checker/SafetyChecker.hpp b/src/mc/checker/SafetyChecker.hpp
index a16070e..4fc2d7e 100644 (file)
--- a/src/mc/checker/SafetyChecker.hpp
+++ b/src/mc/checker/SafetyChecker.hpp
@@ -23,7 +23,7 @@ class XBT_PRIVATE SafetyChecker : public Checker {
   ReductionMode reductionMode_ = ReductionMode::unset;
 
 public:
-  explicit SafetyChecker();
+  explicit SafetyChecker(Session* session);
   void run() override;
   RecordTrace get_record_trace() override;
   std::vector<std::string> get_textual_trace() override;

diff --git a/src/mc/checker/UdporChecker.cpp b/src/mc/checker/UdporChecker.cpp
index 8d3e8f7..a3e4265 100644 (file)
--- a/src/mc/checker/UdporChecker.cpp
+++ b/src/mc/checker/UdporChecker.cpp
@@ -11,7 +11,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to MC safety ver
 namespace simgrid {
 namespace mc {
 
-UdporChecker::UdporChecker() : Checker() {}
+UdporChecker::UdporChecker(Session* session) : Checker(session) {}
 
 void UdporChecker::run() {}
 
@@ -29,9 +29,9 @@ std::vector<std::string> UdporChecker::get_textual_trace()
 
 void UdporChecker::log_state() {}
 
-Checker* createUdporChecker()
+Checker* createUdporChecker(Session* session)
 {
-  return new UdporChecker();
+  return new UdporChecker(session);
 }
 
 } // namespace mc

diff --git a/src/mc/checker/UdporChecker.hpp b/src/mc/checker/UdporChecker.hpp
index 57dbe95..e20e7e2 100644 (file)
--- a/src/mc/checker/UdporChecker.hpp
+++ b/src/mc/checker/UdporChecker.hpp
@@ -15,7 +15,7 @@ namespace mc {
 
 class XBT_PRIVATE UdporChecker : public Checker {
 public:
-  explicit UdporChecker();
+  explicit UdporChecker(Session* session);
   void run() override;
   RecordTrace get_record_trace() override;
   std::vector<std::string> get_textual_trace() override;

diff --git a/src/mc/sosp/Snapshot.hpp b/src/mc/sosp/Snapshot.hpp
index a39b0d0..bc658e5 100644 (file)
--- a/src/mc/sosp/Snapshot.hpp
+++ b/src/mc/sosp/Snapshot.hpp
@@ -60,7 +60,7 @@ namespace mc {
 class XBT_PRIVATE Snapshot final : public AddressSpace {
 public:
   /* Initialization */
-  Snapshot(int num_state, RemoteProcess* get_remote_simulation = &mc_model_checker->get_remote_process());
+  Snapshot(int num_state, RemoteProcess* process = &mc_model_checker->get_remote_process());
 
   /* Regular use */
   bool on_heap(const void* address) const
@@ -73,7 +73,7 @@ public:
                    ReadOptions options = ReadOptions::none()) const override;
   Region* get_region(const void* addr) const;
   Region* get_region(const void* addr, Region* hinted_region) const;
-  void restore(RemoteProcess* get_remote_simulation) const;
+  void restore(RemoteProcess* process) const;
 
   // To be private
   int num_state_;
@@ -88,8 +88,8 @@ public:
 
 private:
   void add_region(RegionType type, ObjectInformation* object_info, void* start_addr, std::size_t size);
-  void snapshot_regions(RemoteProcess* get_remote_simulation);
-  void snapshot_stacks(RemoteProcess* get_remote_simulation);
+  void snapshot_regions(RemoteProcess* process);
+  void snapshot_stacks(RemoteProcess* process);
 };
 } // namespace mc
 } // namespace simgrid