在合金中获取签名子集答案

【问题标题】：Getting subsets of signatures in Alloy在合金中获取签名子集
【发布时间】：2021-03-07 12:40:39
【问题描述】：

我想知道是否有一种方法可以提取 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
}

感谢您的宝贵时间。

【问题讨论】：

标签： subset modeling alloy requirements

【解决方案1】：

您应该能够通过设置的交叉点来获取此信息，例如 b.setA & Status1.~status。

【讨论】：

那个方案是最优的

【解决方案2】：

你自己已经给出了答案:-)。您只缺少 5 个字符：

fun SubsetOfSetAinB [b: B] : set A {
    { x : b.setA | b.setA.status in Status1 }
}

{ vars | test(vars) } 的枚举对于很多问题非常有用。

【讨论】：