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

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

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

fact {all a:A,c:C | (a->c) in r2 iff some b:B | (a->b->c) in r1 }

Answer 2

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

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

Answer 3

您可以根据 r2 定义 r1

open util/ternary

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

sig B{}
sig C{}

check { select13[r1] in r2 } for 3

如果您需要一种方法来大致获取三元组的第一个和最后一个，请使用 util/ternary

中的 select13

Projection over the first and last element in a ternary relation in Alloy