]> AND Public Git Repository - simgrid.git/blobdiff - src/mc/explo/LivenessChecker.hpp
Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Rename mc::Session into mc::api::RemoteApp
[simgrid.git] / src / mc / explo / LivenessChecker.hpp
index ea7c0e6fe480d8f113c16f791e2a815926e544ab..f47c4ec44ca6fee65c8c95d0875ebaff318a075a 100644 (file)
 #include <memory>
 #include <vector>
 
-namespace simgrid {
-namespace mc {
+namespace simgrid::mc {
 
 class XBT_PRIVATE Pair {
 public:
-  int num                               = 0;
-  bool search_cycle                     = false;
-  std::shared_ptr<State> graph_state    = nullptr; /* System state included */
-  xbt_automaton_state_t automaton_state = nullptr;
+  int num                           = 0;
+  bool search_cycle                 = false;
+  std::shared_ptr<State> app_state_ = nullptr; /* State of the application (including system state) */
+  xbt_automaton_state_t prop_state_ = nullptr; /* State of the property automaton */
   std::shared_ptr<const std::vector<int>> atomic_propositions;
   int requests             = 0;
   int depth                = 0;
@@ -39,19 +38,19 @@ class XBT_PRIVATE VisitedPair {
 public:
   int num;
   int other_num                      = 0;       /* Dot output for */
-  std::shared_ptr<State> graph_state = nullptr; /* System state included */
-  xbt_automaton_state_t automaton_state;
+  std::shared_ptr<State> app_state_  = nullptr; /* State of the application (including system state) */
+  xbt_automaton_state_t prop_state_;            /* State of the property automaton */
   std::shared_ptr<const std::vector<int>> atomic_propositions;
   std::size_t heap_bytes_used = 0;
-  int actors_count            = 0;
+  int actor_count_;
 
-  VisitedPair(int pair_num, xbt_automaton_state_t automaton_state,
-              std::shared_ptr<const std::vector<int>> atomic_propositions, std::shared_ptr<State> graph_state);
+  VisitedPair(int pair_num, xbt_automaton_state_t prop_state,
+              std::shared_ptr<const std::vector<int>> atomic_propositions, std::shared_ptr<State> app_state);
 };
 
 class XBT_PRIVATE LivenessChecker : public Exploration {
 public:
-  explicit LivenessChecker(Session* session);
+  explicit LivenessChecker(RemoteApp* remote_app);
   void run() override;
   RecordTrace get_record_trace() override;
   std::vector<std::string> get_textual_trace() override;
@@ -79,7 +78,6 @@ private:
   std::string previous_request_;
 };
 
-} // namespace mc
-} // namespace simgrid
+} // namespace simgrid::mc
 
 #endif