发现合金规格的意外实例

Question

我尝试了使用 Alloy 进行建模的第一步，但遇到了一个我无法理解的问题。我有以下规格：

module tour/AddressBook1

sig Name, Addr{}
sig Book {
    addr: Name->lone Addr
}

// operation: adds a (name, address) to the Book b, resulting in b'
pred add (b, b' : Book, n:Name, a:Addr) {
    b'.addr = b.addr + n->a
}

run add for 3 but 2 Book

到目前为止没有什么特别的。它实际上是 Daniel Jackson 的“软件抽象”一书的例子。

它本质上是对具有（名称，地址）对的书籍进行建模。 add-predicate 应该通过添加（可能已经存在的）（名称，地址）对来获取 Book-instance b 并从中创建另一个 Book-instance b'。

找到的前几个示例很简单且令人信服，但单击“下一步”按钮我最终得到了以下示例（上面的完整视图，下面书籍的等效投影）

我看到两本书，起始书 Book0 有两对 (Name0, Addr2) 和 (Name1, Addr1)。从注释中我们还可以看到，添加操作将添加新的二人组（Name1，Addr2）。当我现在查看结果书 Book1 时，我有 {(Name0, Addr0),(Name1, Addr2)} 而不是 {(Name0, Addr2),(Name1, Addr1),(Name1, Addr2)}

为什么这被视为法律实例？

（Alloy Analyzer 4.2，构建日期 2012-09-25 15:54 EDT）

Answer 1

这里有两件令人困惑的事情：

1. Book0 不参与操作。相反，Book1 具有b0 和b1 的角色。

2. 将n->a 添加到一本书并不能断言这是一个新地址。在该实例中，Book1 在add 之前和之后都有此地址。 这是因为操作

   b'.addr = b.addr + n->a
   

   使用设置联合。分解为一个更简单的例子：

   {1, 2} = {1} + {2}
   

   是真的。但是

   {1, 2} = {1, 2} + {2}
   

   也是如此。所以在最初的例子中，没有什么可以排除n->a 已经成为b.addr 的一部分。合金分析器只生成与给定约束一致的所有实例。

您可以通过在add 中添加断言来改进此示例：

    b.addr[n] != a