Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Concatenate nested namespaces (sonar).
[simgrid.git] / src / mc / ModelChecker.hpp
index e7bff26..c4b1894 100644 (file)
@@ -15,8 +15,7 @@
 #include <memory>
 #include <set>
 
-namespace simgrid {
-namespace mc {
+namespace simgrid::mc {
 
 /** State of the model-checker (global variables for the model checker)
  */
@@ -27,7 +26,9 @@ class ModelChecker {
   // This is the parent snapshot of the current state:
   PageStore page_store_{500};
   std::unique_ptr<RemoteProcess> remote_process_;
-  Checker* checker_ = nullptr;
+  Exploration* exploration_ = nullptr;
+
+  unsigned long visited_states_ = 0;
 
   // Expect MessageType::SIMCALL_TO_STRING or MessageType::SIMCALL_DOT_LABEL
   std::string simcall_to_string(MessageType type, aid_t aid, int times_considered);
@@ -50,30 +51,27 @@ public:
   void shutdown();
   void resume();
   void wait_for_requests();
-  Transition* handle_simcall(Transition const& transition, bool new_transition);
 
-  /* Interactions with the simcall observer */
-  bool simcall_is_visible(aid_t aid);
-  std::string simcall_dot_label(aid_t aid, int times_considered);
+  /** Let the application take a transition. A new Transition is created iff the last parameter is true */
+  Transition* handle_simcall(aid_t aid, int times_considered, bool new_transition);
 
+  /* Interactions with the simcall observer */
   XBT_ATTRIB_NORETURN void exit(int status);
 
-  bool checkDeadlock();
   void finalize_app(bool terminate_asap = false);
 
-  Checker* getChecker() const { return checker_; }
-  void setChecker(Checker* checker) { checker_ = checker; }
+  Exploration* get_exploration() const { return exploration_; }
+  void set_exploration(Exploration* exploration) { exploration_ = exploration; }
+
+  unsigned long get_visited_states() const { return visited_states_; }
+  void inc_visited_states() { visited_states_++; }
 
 private:
   void setup_ignore();
   bool handle_message(const char* buffer, ssize_t size);
   void handle_waitpid();
-
-public:
-  unsigned long visited_states = 0;
 };
 
-}
-}
+} // namespace simgrid::mc
 
 #endif