subset - 在合金中获取签名子集

Question

我想知道是否有办法在 Alloy 的给定签名中提取集合的子集。然后将提取的集合用于定义模型的某些事实。

假设以下模型：

abstract sig Status{}
one sig Status1 extends Status{}
one sig Status2 extends Status{}

sig A {
     status: one Status
}

sig B {
     setA: set A
}

fun SubsetOfSetAinB [b: B] : set A {
    //have some kind of operation here 
    //that returns a subset of b.setA where b.setA.status in Status1
}

感谢您的时间。

标签： subsetmodelingalloyrequirements

Answer 1

您应该能够通过设置的交集来获得它，例如b.setA & Status1.~status.