fsm - NuSMV 中的交换指令

Question

我正在尝试在 NuSMV 中实现基本交换指令，所以我有局部变量 a1,tmp,a2 来执行逻辑

tmp = a1; a1 = a2; a2 = tmp

但是，我不知道如何next()在 NuSMV 中保持这种顺序，任何想法都会受到赞赏。