+/* Search an enabled transition for the given process.
+ *
+ * This can be seen as an iterator returning the next transition of the process.
+ *
+ * We only consider the processes that are both
+ * - marked "to be interleaved" in their ProcessState (controlled by the checker algorithm).
+ * - which simcall can currently be executed (like a comm where the other partner is already known)
+ * Once we returned the last enabled transition of a process, it is marked done.
+ *
+ * Things can get muddled with the WAITANY and TESTANY simcalls, that are rewritten
+ * on the fly to a bunch of WAIT (resp TEST) transitions using the transition.argument
+ * field to remember what was the last returned sub-transition.
+ */