我有一点合金规格如下：
sig class {parents : set class} fact f1{all p:class | not p in p.^parents} run{} for exactly 4 class
首先，我认为合金会将f1转换为布尔矩阵，然后对其执行闭包操作 . 但似乎它没有做这种翻译（看起来它在布尔矩阵创建之前运行了一些东西 . ） . 那么这个f1究竟是如何翻译的呢？它是否使用关系谓词？我对合金的翻译非常好奇 .
布尔矩阵用于表示Alloy中的表达式 . 因此，您从每个sig的一元矩阵，每个二元关系的二元矩阵，每个三元关系的三元矩阵等开始 . 然后，通过操纵（合成）您开始使用的那些矩阵来完成“复杂”表达式的翻译（例如，涉及关系代数运算符） . 对于每个Alloy运算符（例如，传递闭包（^），关系连接（ . ），in，not等），存在执行一堆矩阵运算的相应算法，使得正确地实现该运算符的语义 .
所以在这个例子中， all 量词首先展开，这意味着对于 class 类型的每个原子 p ，正文被翻译（类似于：
all
class
p
m0 = matrix（p）//返回与p对应的矩阵
m1 = matrix（parents）//返回与父对应的矩阵
m2 = ^ m1
m3 = m0.m2m3中
m4 = m0
m5 =不是m4
），最后，所有这些正文翻译都是AND .
1 回答
布尔矩阵用于表示Alloy中的表达式 . 因此，您从每个sig的一元矩阵，每个二元关系的二元矩阵，每个三元关系的三元矩阵等开始 . 然后，通过操纵（合成）您开始使用的那些矩阵来完成“复杂”表达式的翻译（例如，涉及关系代数运算符） . 对于每个Alloy运算符（例如，传递闭包（^），关系连接（ . ），in，not等），存在执行一堆矩阵运算的相应算法，使得正确地实现该运算符的语义 .
所以在这个例子中，
all量词首先展开，这意味着对于class类型的每个原子p，正文被翻译（类似于：m0 = matrix（p）//返回与p对应的矩阵
m1 = matrix（parents）//返回与父对应的矩阵
m2 = ^ m1
m3 = m0.m2
m3中
m4 = m0
m5 =不是m4
），最后，所有这些正文翻译都是AND .