合金的公式翻译

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 = m0 in m3
• m5 = 不是 m4

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