1

考虑以下地址簿示例的简单变体

sig Name, Addr {}
sig Book { addr : Name -> Addr } // no lone on Addr
pred show(b:Book) { some n : Name | #addr[b,n] > 1 }
run show for exactly 2 Book, exactly 2 Addr, exactly 2 Name

在某些模型实例中，我可以在评估器中得到以下结果

all b:Book | show[b]
--> yields false
some b:Book | show[b]
--> yields true
show[Book]
--> yields true

如果 show 是一个关系，那么人们可能会期望得到如下答案：{ true, false }。假设它是一个谓词，则返回一个布尔值。我本来希望 show[Book] 是上面普遍量化的表达式的简写。相反，它似乎是在使用存在量化来折叠结果。任何人都知道这可能是什么原因，或者对 show[Book] 的含义有另一种解释？

4

1 回答 1

1

（我不确定我的用词是否正确，如果这看起来很模糊，请耐心等待。）

请记住，Alloy 中所有表示个体的表达式都表示个体的集合，并且在语言中“个体 X”和“成员是个体 X 的单例集合”之间没有区别。（[后来的附录：]在更常用的术语中：Alloy 逻辑中的一般规则是所有值都是关系。二元关系是成对的集合，n 元关系的 n 元组集合，集合是一元关系和标量是单例集。参见软件抽象第 3.2.2 节中的讨论，或Greg Dennis 和 Rob Seater 的合金分析器 4 教程中的幻灯片“一切都是关系” 。）

鉴于您对 'show' 谓词的声明，很容易预期 'show' 的参数应该是一本书——或者更准确地说，是一组书的单例——然后进一步期待，如果参数实际上不是一个单例集（如show[Book]这里的表达式），那么系统将强制它成为一个单例集，或者用某种隐含的存在或全称量化来解释它。但是在声明pred show(b:Book) ...中，表达式b:Book只是命名了一个对象 b，它将是签名 Book 中的一组对象。（要要求 b 是一个单例集，写成。）对于 b = Book 和 b = Book$0 一样，对pred show(one b: Book) ...构成 of 主体的表达式求值。show

存在量化的出现是表达式核心的点运算符addr[b,n]（或等效地n.(b.addr)定义）方式的结果。实际上，如果您进行实验，您会发现只要有任何名称为所有书籍的集合都包含到两个不同地址的映射，即使在存在解释会失败的情况下。尝试将其添加到您的模型中，例如：

pred hmmmm { show[Book] and no b: Book | show[b] }
run hmmmm for exactly 2 Book, exactly 2 Addr, exactly 2 Name
于 2013-02-01T22:23:31.807 回答