Alloy6状态转换异常：订单Ok状态非法跳转问题排查

问题原因 #

1. Transitions Fact语法优先级错误
   原代码中transitions fact的写法always stutter or (some o: Order | order_success[o])存在语法问题：Alloy中always的优先级高于or，导致always仅作用于stutter，而非整个转换条件表达式。这意味着模型允许两种极端情况：要么全程保持状态不变，要么存在至少一次订单成功的转换，但其余步骤可以发生任何未被约束的状态变更——包括已处于Ok状态的订单跳回Pending或转为Err。

2. 未明确约束非Pending订单的状态稳定性
   虽然order_success断言中约束了非目标订单的状态保持不变，但由于transitions fact的语法错误，这个约束并没有被强制应用到所有状态转换步骤，导致验证器可以生成违反断言的反例。

改进建议 #

1. 修复Transitions Fact的语法 #

给整个转换条件添加括号，确保always作用于完整的stutter or (...)表达式，强制每个状态转换步骤只能是stutter或执行某个订单成功的动作：

fact transitions { 
    always (stutter or (some o: Order | order_success[o])) 
}

2. 强化订单状态稳定性约束 #

为了更严谨，可以显式添加fact，确保所有非Pending状态的订单无法变更状态：

fact "non-Pending orders cannot change status" {
    always all o: Order | o.status != Pending implies o.status' = o.status
}

或者直接在order_success断言中明确所有其他订单（包括Ok/Err状态）的状态保持不变（原代码中这部分已经存在，但语法修复后会生效）：

pred order_success[o: Order] {
    o.status = Pending
    o.status' = Ok
    all p: Order - o | p.status' = p.status
    all s: Sale | s.status' = s.status
}

3. 补充订单失败的转换规则（可选） #

如果业务逻辑允许订单从Pending转为Err，需要添加对应的转换断言并纳入transitions fact，例如：

pred order_failure[o: Order] {
    o.status = Pending
    o.status' = Err
    all p: Order - o | p.status' = p.status
    all s: Sale | s.status' = s.status
}

fact transitions { 
    always (stutter or (some o: Order | order_success[o]) or (some o: Order | order_failure[o])) 
}

内容的提问来源于stack exchange，提问作者Pablo Fernandez