return false; // Comm transitions are INDEP with non-comm transitions
}
+
+bool CommWaitTransition::reversible_race(const Transition* other) const
+{
+ xbt_assert(type_ == Type::COMM_WAIT, "Unexpected transition type %s", to_c_str(type_));
+
+ // If the other event is a communication event, then we are not reversible; otherwise we are reversible.
+ return other->type_ != Transition::Type::COMM_ASYNC_SEND && other->type_ != Transition::Type::COMM_ASYNC_RECV;
+}
+
CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, unsigned comm_, aid_t sender_,
aid_t receiver_, unsigned mbox_)
: Transition(Type::COMM_TEST, issuer, times_considered)
{
return xbt::string_printf("TestComm(from %ld to %ld, mbox=%u)", sender_, receiver_, mbox_);
}
+
bool CommTestTransition::depends(const Transition* other) const
{
if (other->type_ < type_)
return false; // Comm transitions are INDEP with non-comm transitions
}
+bool CommTestTransition::reversible_race(const Transition* other) const
+{
+ xbt_assert(type_ == Type::COMM_TEST, "Unexpected transition type %s", to_c_str(type_));
+ return true; // CommTest is always enabled
+}
+
CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, int tag_)
: Transition(Type::COMM_ASYNC_RECV, issuer, times_considered), comm_(comm_), mbox_(mbox_), tag_(tag_)
{
return false; // Comm transitions are INDEP with non-comm transitions
}
+bool CommRecvTransition::reversible_race(const Transition* other) const
+{
+ xbt_assert(type_ == Type::COMM_ASYNC_RECV, "Unexpected transition type %s", to_c_str(type_));
+
+ return true; // CommRecv is always enabled
+}
+
CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, int tag_)
: Transition(Type::COMM_ASYNC_SEND, issuer, times_considered), comm_(comm_), mbox_(mbox_), tag_(tag_)
{
return false; // Comm transitions are INDEP with non-comm transitions
}
+bool CommSendTransition::reversible_race(const Transition* other) const
+{
+ xbt_assert(type_ == Type::COMM_ASYNC_SEND, "Unexpected transition type %s", to_c_str(type_));
+
+ return true; // CommSend is always enabled
+}
+
} // namespace simgrid::mc