alloy - 合金的公式翻译

Question

我有一个小的合金规格如下：

sig class {parents : set class}
fact f1{all p:class | not p in p.^parents}
run{} for exactly 4 class

首先，我认为合金会将 f1 转换为布尔矩阵，然后对其执行闭包操作。但它似乎没有进行这种翻译（看起来它在创建布尔矩阵之前运行了一些东西。）。那么这个 f1 究竟是如何翻译的呢？它使用关系谓词吗？我只是对合金的翻译很好奇。

Answer 1

布尔矩阵用于表示合金中的表达式。因此，您从每个 sig 的一元矩阵、每个二元关系的二元矩阵、每个三元关系的三元矩阵等开始。然后，通过操作（组合）您开始使用的那些矩阵来完成“复杂”表达式的转换（例如，涉及关系代数运算符）。对于每个 Alloy 运算符（例如，传递闭包 (^)、关系连接 (.)、in、not 等），都有一个相应的算法执行一系列矩阵运算，以便正确实现该运算符的语义。

所以在这个例子中，all量词首先被展开，这意味着对于每个p类型class的原子，身体被翻译（类似于：

• m0 = matrix(p) //返回p对应的矩阵
• m1 = matrix(parents) //返回父母对应的矩阵
• m2 = ^m1
• m3 = m0.m2
• m4 = m3 中的 m0
• m5 = 不是 m4

)，最后，所有这些正文翻译都是 AND'ed。