提取集合中具有特定属性(与特定值相关)的所有元素

Question

我正试图编写一个Alloy函数，以检索与函数参数相关的特定类型的所有元素(比如说，它们的一个"字段/属性"具有该值(。我尝试过各种方法，但都没有成功。

它有点像

fun get[a:A] : set X{
(x.name :> a)
}

但是这返回一组a，而我想要一组X

Answer 1

您可以更简单地做到这一点：

name.a

返回名称下映射到中某个元素的X集

检查与您的版本的等效性：

sig A { }
sig X {
name: set A
}
fun get [a:A] : set X{
((X <: name) :> a).A
}
fun get' [a:A] : set X{
name.a
}
check {
all a: A | get[a] = get'[a]
}

Answer 2

这很有效，希望对某人有用：

fun get[a:A] : set X{
((X <: name) :> a).A
}