TODO workflow nets (PR draft created but blocked) clarify definition of "soundness" T_j always happens before T_k?