+namespace simgrid {
+namespace mc {
+
+enum class CallType { NONE, SEND, RECV, WAIT, WAITANY };
+enum class CommPatternDifference { NONE, TYPE, RDV, TAG, SRC_PROC, DST_PROC, DATA_SIZE, DATA };
+enum class PatternCommunicationType {
+ none = 0,
+ send = 1,
+ receive = 2,
+};
+
+class PatternCommunication {
+public:
+ int num = 0;
+ RemotePtr<simgrid::kernel::activity::CommImpl> comm_addr{nullptr};
+ PatternCommunicationType type = PatternCommunicationType::send;
+ unsigned long src_proc = 0;
+ unsigned long dst_proc = 0;
+ std::string rdv;
+ std::vector<char> data;
+ int tag = 0;
+ int index = 0;
+
+ PatternCommunication dup() const
+ {
+ simgrid::mc::PatternCommunication res;
+ // num?
+ res.comm_addr = this->comm_addr;
+ res.type = this->type;
+ // src_proc?
+ // dst_proc?
+ res.dst_proc = this->dst_proc;
+ res.rdv = this->rdv;
+ res.data = this->data;
+ // tag?
+ res.index = this->index;
+ return res;
+ }
+};
+
+struct PatternCommunicationList {
+ unsigned int index_comm = 0;
+ std::vector<std::unique_ptr<simgrid::mc::PatternCommunication>> list;
+};
+
+static inline simgrid::mc::CallType MC_get_call_type(const s_smx_simcall* req)
+{
+ using simgrid::mc::CallType;
+ using simgrid::simix::Simcall;
+ switch (req->call_) {
+ case Simcall::COMM_ISEND:
+ return CallType::SEND;
+ case Simcall::COMM_IRECV:
+ return CallType::RECV;
+ case Simcall::COMM_WAIT:
+ return CallType::WAIT;
+ case Simcall::COMM_WAITANY:
+ return CallType::WAITANY;
+ default:
+ return CallType::NONE;
+ }
+}
+
+/********** Checker extension **********/
+
+struct CommDetExtension {
+ static simgrid::xbt::Extension<simgrid::mc::Checker, CommDetExtension> EXTENSION_ID;
+
+ CommDetExtension()
+ {
+ const unsigned long maxpid = api::get().get_maxpid();
+
+ initial_communications_pattern.resize(maxpid);
+ incomplete_communications_pattern.resize(maxpid);
+ }
+
+ std::vector<simgrid::mc::PatternCommunicationList> initial_communications_pattern;
+ std::vector<std::vector<simgrid::mc::PatternCommunication*>> incomplete_communications_pattern;
+
+ bool initial_communications_pattern_done = false;
+ bool recv_deterministic = true;
+ bool send_deterministic = true;
+ std::string send_diff;
+ std::string recv_diff;
+
+ void restore_communications_pattern(const simgrid::mc::State* state);
+ void deterministic_comm_pattern(aid_t process, const PatternCommunication* comm, bool backtracking);
+ void get_comm_pattern(smx_simcall_t request, CallType call_type, bool backtracking);
+ void complete_comm_pattern(RemotePtr<kernel::activity::CommImpl> const& comm_addr, aid_t issuer, bool backtracking);
+ void handle_comm_pattern(const Transition* transition, smx_simcall_t req, int value, bool backtracking);
+};
+simgrid::xbt::Extension<simgrid::mc::Checker, CommDetExtension> CommDetExtension::EXTENSION_ID;
+/********** State Extension ***********/
+
+class StateCommDet {
+ CommDetExtension* checker_;
+
+public:
+ std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern_;
+ std::vector<unsigned> communication_indices_;
+
+ static simgrid::xbt::Extension<simgrid::mc::State, StateCommDet> EXTENSION_ID;
+ explicit StateCommDet(CommDetExtension* checker) : checker_(checker)
+ {
+ copy_incomplete_comm_pattern();
+ copy_index_comm_pattern();
+ }