Alloy中蕴含运算符与析取运算符的行为差异问题

我在Alloy中建模银行账户转账系统时遇到了困惑。我期望spec指定的轨迹属于总余额恒定的轨迹子集，但使用蕴含式spec implies always (total' = total)验证时会得到反例，而逻辑等价的not spec or always (total' = total)却找不到反例。已开启“prevent overflows”为“yes”，希望找出问题原因。

建模代码 #

sig User {
  var balance: one Int
}

var one abstract sig Message {}

var lone sig TransferEvent extends Message {
  var from: User,
  var to: User,
  var amount: Int,
}

pred transfer[from: User, amt: Int, to: User] {
  /* 前置条件: */
  { 
    0 <= amt
    amt <= balance[from]
    from != to
  }
  /* 后置条件: */
  {
    balance'[from] = minus[balance[from], amt]
    balance'[to] = plus[balance[to], amt]
    all k: User |
      (k != from and k != to) implies balance'[k] = balance[k]
  }
}

pred init {
  all u: User | balance[u] >= 0
}

// 一步操作要么是转账，要么是"停滞"步骤
pred step {
  { 
    some TransferEvent
    transfer[Message.from, Message.amount, Message.to]
  } or
  {
    no Message and balance = balance'
  }
}

// 行为是从满足init的状态出发，经过无限多"step"步骤可达的轨迹
pred spec {
  init
  always step
}

run spec for 3 but exactly 3 User, exactly 3 steps, 3 int


fun total: Int {
  sum u: User | balance[u]
}

assert Constant {
  (not spec) or (always (total' = total)) // 执行check Constant时无反例
  // (spec) => (always (total' = total)) // 会找到反例
}

check Constant for 3 int

问题原因分析 #

这是Alloy中时序逻辑蕴含式的语义差异导致的：

• 当使用spec => always (total' = total)时，Alloy模型检查器会尝试寻找满足spec但不满足always (total' = total)的轨迹。但这里的反例是虚假的：因为spec要求轨迹是无限的（always step），而Alloy在有限步验证时，会将截断的有限轨迹视为“潜在的无限轨迹”。此时always的语义被弱化，检查器会认为“后续可能出现违反守恒的步骤”，从而生成反例，但实际上你的step定义已经保证每一步都维持余额守恒。
• 当使用not spec or always (total' = total)时，逻辑上等价于蕴含式，但Alloy检查器的处理方式不同：它需要找到同时满足spec和not always (total' = total)的轨迹。由于spec要求无限步骤，而有限步验证下无法构造出真正违反守恒的无限轨迹，因此找不到反例。

修复建议 #

1. 限定验证的步数：在检查断言时明确指定步数，让always只检查有限步内的行为，避免虚假反例：

assert Constant {
  spec => always (total' = total)
}
check Constant for 3 int, 3 steps

2. 优化可变签名的定义：var one abstract sig Message {}和var lone sig TransferEvent的可变声明可能导致状态间Message实例的变化不受控，建议将转账参数直接作为step的输入，而非依赖可变签名：

pred step {
  (some from, to: User, amt: Int | transfer[from, amt, to]) or
  (balance = balance')
}

3. 明确前后条件的关联：将transfer谓词的前置条件和后置条件用蕴含式绑定，避免Alloy误解为无条件满足后置条件：

pred transfer[from: User, amt: Int, to: User] {
  (0 <= amt and amt <= balance[from] and from != to) => (
    balance'[from] = minus[balance[from], amt]
    and balance'[to] = plus[balance[to], amt]
    and all k: User | (k != from and k != to) implies balance'[k] = balance[k]
  )
}

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