// actor which is executing the MutexWait is the owner of the mutex
if (pre_event_a_C.has_value() && mutex_wait->get_owner() == mutex_wait->aid_) {
const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_wait);
exC.insert(e_prime);
// actor which is executing the MutexWait is the owner of the mutex
if (pre_event_a_C.has_value() && mutex_wait->get_owner() == mutex_wait->aid_) {
const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_wait);
exC.insert(e_prime);