我有一个小的合金规格如下:
sig class {parents : set class}
fact f1{all p:class | not p in p.^parents}
run{} for exactly 4 class
首先,我认为合金会将 f1 转换为布尔矩阵,然后对其执行闭包操作。但它似乎没有进行这种翻译(看起来它在创建布尔矩阵之前运行了一些东西。)。那么这个 f1 究竟是如何翻译的呢?它使用关系谓词吗?我只是对合金的翻译很好奇。
我有一个小的合金规格如下:
sig class {parents : set class}
fact f1{all p:class | not p in p.^parents}
run{} for exactly 4 class
首先,我认为合金会将 f1 转换为布尔矩阵,然后对其执行闭包操作。但它似乎没有进行这种翻译(看起来它在创建布尔矩阵之前运行了一些东西。)。那么这个 f1 究竟是如何翻译的呢?它使用关系谓词吗?我只是对合金的翻译很好奇。
布尔矩阵用于表示合金中的表达式。因此,您从每个 sig 的一元矩阵、每个二元关系的二元矩阵、每个三元关系的三元矩阵等开始。然后,通过操作(组合)您开始使用的那些矩阵来完成“复杂”表达式的转换(例如,涉及关系代数运算符)。对于每个 Alloy 运算符(例如,传递闭包 (^)、关系连接 (.)、in、not 等),都有一个相应的算法执行一系列矩阵运算,以便正确实现该运算符的语义。
所以在这个例子中,all
量词首先被展开,这意味着对于每个p
类型class
的原子,身体被翻译(类似于:
),最后,所有这些正文翻译都是 AND'ed。