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

提问于 2024-04-25T18:59:30+08:00

浏览次

0

如何在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投影 .

3 回答

2
一种方法是将约束放入签名中：
```
sig A{r1:B->C, r2:C}{
  r2 = r1[B]
}
```
回复于 2024-04-25T18:59:30+08:00
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 / ternary中的select13
回复于 2024-04-25T18:59:30+08:00
0

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

事实{all a：A，c：C | （a-> c）在r2中如果某些b：B | r1}中的（a-> b-> c）

回复于 2024-04-25T18:59:30+08:00

相关问题