util/Natural 合金中的意外行为

Question

我尝试了 Alloy4 的以下 sn-p，发现自己对 util/Natural 模块的行为感到困惑。 cmets 更详细地解释了意外情况。我希望有人能解释为什么会这样。

module weirdNatural
private open util/natural as nat

//Somehow, using number two obtained from incrementing one works as I expect, (ie, there is no 
//number greater than it in {0,1,2}. but using number two obtained from the natrual/add function
//seems to work differently. why is that?

let twoViaAdd = nat/add[nat/One, nat/One]
let twoViaInc = nat/inc[nat/One]

pred biggerAdd {
    some x: nat/Natural | nat/gt[x, twoViaAdd]
}

pred biggerInc {
    some y: nat/Natural | nat/gt[y, twoViaInc]
}

//run biggerAdd for 10 but 3 Natural //does not work well, it does find a number gt2 in {0,1,2}
run biggerInc for 10 but 3 Natural //works as expected, it finds a number gt2 in {0,1,2,3}, but not in {0,1,2}

Answer 1

感谢您提交此错误报告。你是绝对正确的，这是一种奇怪的行为。

Alloy4.2 对整数的处理方式进行了一些更改；即Alloy4.2中的+和-运算符总是被解释为集合并/差，所以必须使用内置函数plus/minus来表示算术加/减。另一方面，util/natural 模块（错误地）尚未更新为使用最新语法，这是您遇到的奇怪行为的根本原因（特别是 nat/add 函数使用旧的+ 运算符而不是plus，而nat/inc 没有）。

要解决此问题，您可以

• 1. 打开util/natural模块（从主菜单中选择“File -> Open Sample Models”）
  2. 编辑文件并将<a> + <b> 的两次出现替换为plus[<a>, <b>]
  3. 将新文件保存在与您的模型 als 文件相同的文件夹中（例如，作为“my_nat.als”）
  4. 从您的主模块打开它（例如，open my_nat as nat）

或

• 下载最新的unofficial version 已修复此错误（您可能需要手动删除 Alloy 临时文件夹以确保 Alloy Analyzer 未使用旧（缓存）版本的 util/natural 库）。