+ // CommTest is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // MutexAsyncLock is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // MutexTest is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // MutexTrylock is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // MutexUnlock is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // TODO: Get the semantics correct here
+ const auto e1_action = E.get_transition_for_handle(e1)->type_;
+ return e1_action != Transition::Type::MUTEX_ASYNC_LOCK and e1_action != Transition::Type::MUTEX_UNLOCK;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // SemAsyncLock is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // SemUnlock is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // TODO: Get the semantics correct here
+ return false;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // Object access is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // Random is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // TestAny is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // TODO: We need to check if any of the transitions
+ // waited on occurred before `e1`