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

Question

我正在尝试编写一个 Alloy 函数来检索与函数参数相关的特定类型的所有元素（让我说，它们的 "fields/attributes").我试过各种方法，none 成功了。

有点像

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

但是这个return一套A，而我想要一套X

Answer 1

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

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

Answer 2

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

name.a

returns 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]
}

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

Extract all elements of a set which have a certain attribute (are in relation with a certain value)

alloy