Cleanup work to make is_race_reversible() a method of Transition

That's someone less efficient as we need to retrieve the other's
transition in all cases where most Transition kind can compute the
answer without the other transition, but that should be more readable.

diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
index a7de9b9..d35c167 100644 (file)
--- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
+++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
@@ -29,7 +29,7 @@ bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution:
                                                   Execution::EventHandle e2)
 {
   using Action     = Transition::Type;
-  using Handler    = std::function<bool(const Execution&, Execution::EventHandle, const Transition*)>;
+  using Handler    = std::function<bool(const Execution&, const Transition*, const Transition*)>;
   using HandlerMap = std::unordered_map<Action, Handler>;
 
   const static HandlerMap handlers = {
@@ -53,9 +53,10 @@ bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution:
       {Action::TESTANY, &ReversibleRaceCalculator::is_race_reversible_TestAny},
       {Action::WAITANY, &ReversibleRaceCalculator::is_race_reversible_WaitAny}};
 
-  const auto* e2_action = E.get_transition_for_handle(e2);
-  if (const auto handler = handlers.find(e2_action->type_); handler != handlers.end()) {
-    return handler->second(E, e1, e2_action);
+  const auto* other_transition = E.get_transition_for_handle(e1);
+  const auto* t2 = E.get_transition_for_handle(e2);
+  if (const auto handler = handlers.find(t2->type_); handler != handlers.end()) {
+    return handler->second(E, other_transition, t2);
   } else {
     xbt_die("There is currently no specialized computation for the transition "
             "'%s' for computing reversible races in ODPOR, so the model checker cannot "
@@ -63,12 +64,12 @@ bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution:
             "that the transition be supported in SimGrid using ODPPR and consider "
             "using the other model-checking algorithms supported by SimGrid instead "
             "in the meantime",
-            e2_action->to_string().c_str());
+            t2->to_string().c_str());
   }
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle /*e1*/,
-                                                            const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, const Transition* /*other_transition*/,
+                                                            const Transition* /*t2*/)
 {
   // ActorJoin races with another event iff its target `T` is the same as
   // the actor executing the other transition. Clearly, then, we could not join
@@ -76,138 +77,139 @@ bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, Ex
   return false;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
-                                                                   const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock(const Execution&,
+                                                                   const Transition* /*other_transition*/,
+                                                                   const Transition* /*t2*/)
 {
   // BarrierAsyncLock is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_BarrierWait(const Execution& E, Execution::EventHandle e1,
-                                                              const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_BarrierWait(const Execution& E, const Transition* other_transition,
+                                                              const Transition* /*t2*/)
 {
   // If the other event is a barrier lock event, then we
   // are not reversible; otherwise we are reversible.
-  const auto e1_action = E.get_transition_for_handle(e1)->type_;
-  return e1_action != Transition::Type::BARRIER_ASYNC_LOCK;
+  const auto other_action = other_transition->type_;
+  return other_action != Transition::Type::BARRIER_ASYNC_LOCK;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, Execution::EventHandle /*e1*/,
-                                                           const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, const Transition* /*other_transition*/,
+                                                           const Transition* /*t2*/)
 {
   // CommRecv is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, Execution::EventHandle /*e1*/,
-                                                           const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, const Transition* /*other_transition*/,
+                                                           const Transition* /*t2*/)
 {
   // CommSend is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, Execution::EventHandle e1,
-                                                           const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, const Transition* other_transition,
+                                                           const Transition* /*t2*/)
 {
   // If the other event is a communication event, then we
   // are not reversible; otherwise we are reversible.
-  const auto e1_action = E.get_transition_for_handle(e1)->type_;
-  return e1_action != Transition::Type::COMM_ASYNC_SEND && e1_action != Transition::Type::COMM_ASYNC_RECV;
+  const auto other_action = other_transition->type_;
+  return other_action != Transition::Type::COMM_ASYNC_SEND && other_action != Transition::Type::COMM_ASYNC_RECV;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, Execution::EventHandle /*e1*/,
-                                                           const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, const Transition* /*other_transition*/,
+                                                           const Transition* /*t2*/)
 {
   // CommTest is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
-                                                                 const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&,
+                                                                 const Transition* /*other_transition*/,
+                                                                 const Transition* /*t2*/)
 {
   // MutexAsyncLock is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, Execution::EventHandle /*e1*/,
-                                                            const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, const Transition* /*other_transition*/,
+                                                            const Transition* /*t2*/)
 {
   // MutexTest is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle /*e1*/,
-                                                               const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, const Transition* /*other_transition*/,
+                                                               const Transition* /*t2*/)
 {
   // MutexTrylock is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle /*e1*/,
-                                                              const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, const Transition* /*other_transition*/,
+                                                              const Transition* /*t2*/)
 {
   // MutexUnlock is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
-                                                            const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, const Transition* /*other_transition*/,
+                                                            const Transition* /*t2*/)
 {
   // TODO: for now we over approximate the reversibility
 
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
-                                                               const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, const Transition* /*other_transition*/,
+                                                               const Transition* /*t2*/)
 {
   // SemAsyncLock is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle /*e1*/,
-                                                            const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, const Transition* /*other_transition*/,
+                                                            const Transition* /*t2*/)
 {
   // SemUnlock is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, Execution::EventHandle e1,
-                                                          const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, const Transition* other_transition,
+                                                          const Transition* /*t2*/)
 {
 
-  const auto e1_transition = E.get_transition_for_handle(e1);
-  if (e1_transition->type_ == Transition::Type::SEM_UNLOCK &&
-      static_cast<const SemaphoreTransition*>(e1_transition)->get_capacity() <= 1) {
+  if (other_transition->type_ == Transition::Type::SEM_UNLOCK &&
+      static_cast<const SemaphoreTransition*>(other_transition)->get_capacity() <= 1) {
     return false;
   }
-  xbt_assert(false, "SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe");
+  xbt_die("SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe");
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle /*e1*/,
-                                                               const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, const Transition* /*other_transition*/,
+                                                               const Transition* /*t2*/)
 {
   // Object access is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, Execution::EventHandle /*e1*/,
-                                                         const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, const Transition* /*other_transition*/,
+                                                         const Transition* /*t2*/)
 {
   // Random is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, Execution::EventHandle /*e1*/,
-                                                          const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, const Transition* /*other_transition*/,
+                                                          const Transition* /*t2*/)
 {
   // TestAny is always enabled
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, Execution::EventHandle /*e1*/,
-                                                          const Transition* /*e2*/)
+bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, const Transition* /*other_transition*/,
+                                                          const Transition* /*t2*/)
 {
   // TODO: We need to check if any of the transitions
   // waited on occurred before `e1`

diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.hpp b/src/mc/explo/odpor/ReversibleRaceCalculator.hpp
index 88c6839..1c67814 100644 (file)
--- a/src/mc/explo/odpor/ReversibleRaceCalculator.hpp
+++ b/src/mc/explo/odpor/ReversibleRaceCalculator.hpp
@@ -30,25 +30,25 @@ namespace simgrid::mc::odpor {
  * is only sensible in the context of a race
  */
 class ReversibleRaceCalculator final {
-  static bool is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_BarrierAsyncLock(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_BarrierWait(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_CommRecv(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_CommSend(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_CommWait(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_CommTest(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_MutexTest(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_MutexWait(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_SemWait(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_Random(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_TestAny(const Execution&, Execution::EventHandle e1, const Transition* e2);
-  static bool is_race_reversible_WaitAny(const Execution&, Execution::EventHandle e1, const Transition* e2);
+  static bool is_race_reversible_ActorJoin(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_BarrierAsyncLock(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_BarrierWait(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_CommRecv(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_CommSend(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_CommWait(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_CommTest(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_MutexAsyncLock(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_MutexTest(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_MutexTrylock(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_MutexUnlock(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_MutexWait(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_SemAsyncLock(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_SemUnlock(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_SemWait(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_ObjectAccess(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_Random(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_TestAny(const Execution&, const Transition* t1, const Transition* t2);
+  static bool is_race_reversible_WaitAny(const Execution&, const Transition* t1, const Transition* t2);
 
 public:
   static bool is_race_reversible(const Execution&, Execution::EventHandle e1, Execution::EventHandle e2);