2

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

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}
4

1 回答 1

2

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

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

要解决此问题，您可以

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

或者

  • 下载修复此错误的最新非官方版本（您可能需要手动删除 Alloy 临时文件夹以确保 Alloy Analyzer 未使用旧（缓存）版本的 util/natural 库）。
于 2013-09-05T22:26:03.263 回答