Alloy使用always时序约束建模时提示无实例问题咨询

为Payment对象设计Queued -> Processing -> Complete的状态流转形式化规约，用于Alloy可视化验证，初始编写的模型代码如下：

enum State {Queued, Processing, Complete}

sig Payment {
    var state: State
}

pred processPayment[p: Payment] {
    p.state = Queued // guard
    p.state' = Processing // action
}

pred completePayment[p: Payment] {
    p.state = Processing // guard
    p.state' = Complete // action
}

fact init {
    Payment.state = Queued
}

fact next {
    always (some p : Payment | processPayment[p] or completePayment[p])
}

run {} for 1 Payment

执行run {} for 1 Payment命令时始终无法生成有效实例，按照参考教程的说明，Payment初始为Queued、下一状态流转为Processing的场景本应满足约束，需要定位建模错误。

模型存在两个核心问题，直接导致求解器无法找到合法实例：

• 无限轨迹死锁：Alloy时态建模默认生成无限长的离散状态执行轨迹，但现有next事实强制要求所有时刻必须存在某个Payment触发processPayment或completePayment动作。两个动作都有严格前置条件：processPayment要求对象当前为Queued状态，completePayment要求对象当前为Processing状态。当Payment流转到Complete终态后，没有任何动作满足触发条件，不存在合法下一状态，轨迹在终态处终止，不符合无限轨迹要求，因此求解器判定无合法实例。
• 缺少框架条件约束：两个动作谓词仅约束了目标Payment的状态变化，未明确规定「除当前操作的Payment外，其余所有Payment的状态、其余模型关系在迁移前后保持不变」。缺少该约束时，求解器会允许未被提及的关系在状态迁移时任意变动，即使解决死锁问题，也会生成大量不符合业务逻辑的非法轨迹。

补充框架条件约束，同时在终态场景下允许空转（Stuttering）步保证轨迹无限延伸，修复后代码如下：

enum State {Queued, Processing, Complete}

sig Payment {
    var state: State
}

// 框架约束：除当前操作的Payment外，其余对象状态保持不变
pred frame[p: Payment] {
    all p2: Payment - p | p2.state' = p2.state
}

pred processPayment[p: Payment] {
    p.state = Queued // 前置守卫
    p.state' = Processing // 状态更新
    frame[p]
}

pred completePayment[p: Payment] {
    p.state = Processing // 前置守卫
    p.state' = Complete // 状态更新
    frame[p]
}

// 终态空转步：所有状态保持不变
pred stutter {
    all p: Payment | p.state' = p.state
}

fact init {
    all p: Payment | p.state = Queued
}

fact next {
    always (
        (some p: Payment | processPayment[p] or completePayment[p])
        or
        // 所有支付到达终态时，允许空转维持无限轨迹
        (all p: Payment | p.state = Complete and stutter)
    )
}

run {} for 1 Payment

修复后执行命令即可生成合法实例，可观察到单Payment实例依次从Queued流转为Processing、再流转为Complete，之后持续保持Complete状态的完整执行流程。

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