合金中三元关系中第一个和最后一个元素的投影

Question

如何在Alloy中的三元关系中投影第一列和最后一列？

假设我有r1: A->B->C，假设r1= (A0->B1->C1,A1->B1->C0, A2->B0->C2)，我如何定义r2: A->C为r2= (A0->C1,A1->C0, A2->C2)

更具体地说，如果我有：

sig A｛r1:B->C，r2:C｝

sig B｛｝

sig C｛｝

如何将r2约束为r1在第一列和最后一列上的投影。

Answer 1

一种方法是将约束放入签名中：

sig A{r1:B->C, r2:C}{
  r2 = r1[B]
} 

Answer 2

您可以根据r2 定义r1

open util/ternary
sig A{
    r2:C,
    r1:B->r2
}
sig B{}
sig C{}
check { select13[r1] in r2 } for 3

如果您需要一种通常获取三元组的第一个和最后一个的方法，请使用util/termary 中的select13

Answer 3

添加以下事实似乎也可以解决此问题：

事实{r2中的所有a:a，c:c|（a->c）当r1中的一些b:b|（a-->b->c）}