Home Articles

合金的配方翻译

Asked
Viewed 361 times
2

我有一点合金规格如下:

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

首先,我认为合金会将f1转换为布尔矩阵,然后对其执行闭包操作 . 但似乎它没有做这种翻译(看起来它在布尔矩阵创建之前运行了一些东西 . ) . 那么这个f1究竟是如何翻译的呢?它是否使用关系谓词?我对合金的翻译非常好奇 .

1 Answer

  • 3

    布尔矩阵用于表示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 .

Related