Home Articles

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

Asked
Viewed 651 times
0

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

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

更具体的是,如果我有:

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

如何约束r2成为第一列和最后一列的r1投影 .

3 Answers

  • 2

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

    sig A{r1:B->C, r2:C}{
      r2 = r1[B]
    }
    
  • 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

  • 0

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

    事实{all a:A,c:C | (a-> c)在r2中如果某些b:B | r1}中的(a-> b-> c)

Related