+namespace simgrid {
+namespace mc {
+
+enum class CallType { NONE, SEND, RECV, WAIT, WAITANY };
+enum class CommPatternDifference { NONE, TYPE, MBOX, TAG, SRC_PROC, DST_PROC, DATA_SIZE };
+enum class PatternCommunicationType {
+ none = 0,
+ send = 1,
+ receive = 2,
+};
+
+class PatternCommunication {
+public:
+ int num = 0;
+ uintptr_t comm_addr = 0;
+ PatternCommunicationType type = PatternCommunicationType::send;
+ unsigned long src_proc = 0;
+ unsigned long dst_proc = 0;
+ unsigned mbox = 0;
+ unsigned size = 0;
+ 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.mbox = this->mbox;
+ // tag?
+ res.index = this->index;
+ return res;
+ }
+};
+
+struct PatternCommunicationList {
+ unsigned int index_comm = 0;
+ std::vector<std::unique_ptr<simgrid::mc::PatternCommunication>> list;
+};
+
+/********** 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(const Transition* transition, bool backtracking);
+ void complete_comm_pattern(const CommWaitTransition* transition, bool backtracking);
+ void handle_comm_pattern(const Transition* transition, 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();
+ }