Big bang in MC: app's observers are serialized, to become transitions in checker

[simgrid.git] / src / mc / Transition.hpp

diff --git a/src/mc/Transition.hpp b/src/mc/Transition.hpp
index 3cd9c4c..88929bc 100644 (file)
--- a/src/mc/Transition.hpp
+++ b/src/mc/Transition.hpp
@@ -8,6 +8,7 @@
 #define SIMGRID_MC_TRANSITION_HPP
 
 #include "simgrid/forward.h" // aid_t
+#include "src/kernel/actor/SimcallObserver.hpp"
 #include "src/mc/remote/RemotePtr.hpp"
 #include <string>
 
@@ -24,8 +25,13 @@ namespace mc {
  */
 class Transition {
   /* Textual representation of the transition, to display backtraces */
-  std::string textual_ = "";
   static unsigned long executed_transitions_;
+  static unsigned long replayed_transitions_;
+
+  friend State; // FIXME remove this once we have a proper class to handle the statistics
+
+protected:
+  std::string textual_ = "";
 
 public:
   aid_t aid_ = 0;
@@ -40,18 +46,63 @@ public:
    */
   int times_considered_ = 0;
 
+  Transition() = default;
+  Transition(aid_t issuer, int times_considered) : aid_(issuer), times_considered_(times_considered) {}
+
   void init(aid_t aid, int times_considered);
 
-  std::string to_string() const;
-  const char* to_cstring() const;
+  virtual std::string to_string(bool verbose = false);
+  const char* to_cstring(bool verbose = false);
 
   /* Moves the application toward a path that was already explored, but don't change the current transition */
-  RemotePtr<simgrid::kernel::actor::SimcallObserver> replay() const;
+  void replay() const;
+
+  virtual bool depends(Transition* other) { return true; }
 
   /* Returns the total amount of transitions executed so far (for statistics) */
   static unsigned long get_executed_transitions() { return executed_transitions_; }
+  /* Returns the total amount of transitions replayed so far while backtracing (for statistics) */
+  static unsigned long get_replayed_transitions() { return replayed_transitions_; }
+};
+
+class CommWaitTransition : public Transition {
+  double timeout_;
+  uintptr_t comm_;
+  aid_t sender_;
+  aid_t receiver_;
+  unsigned mbox_;
+  unsigned char* src_buff_;
+  unsigned char* dst_buff_;
+  size_t size_;
+
+public:
+  CommWaitTransition(aid_t issuer, int times_considered, char* buffer);
+  std::string to_string(bool verbose) override;
 };
 
+class CommRecvTransition : public Transition {
+  unsigned mbox_;
+  void* dst_buff_;
+
+public:
+  CommRecvTransition(aid_t issuer, int times_considered, char* buffer);
+  std::string to_string(bool verbose) override;
+};
+
+class CommSendTransition : public Transition {
+  unsigned mbox_;
+  void* src_buff_;
+  size_t size_;
+
+public:
+  CommSendTransition(aid_t issuer, int times_considered, char* buffer);
+  std::string to_string(bool verbose) override;
+};
+
+/** Make a new transition from serialized description */
+Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::SimcallObserver::Simcall simcall,
+                            char* buffer);
+
 } // namespace mc
 } // namespace simgrid