alloy - 如何对函数体使用集合推导

Question

假设我有以下签名:

sig A {}
sig B {}

sig P {
    a: A,
    b: B
}

我如何编写一个函数 f，例如，f 返回 P 的集合，其中每个成员的值为 x: A 表示它的 a 字段？

输入表达式{p: P | p.a = x} 进入评估器给我返回一个集合，但是当我尝试以这种方式定义 f

fun f(a: A) : set P {
    { p: P | p.a = a }
}

alloy 告诉我我犯了一个错误:

A type error has occurred This cannot be a legal relational join where left hand side is p (type = {this/P}) right hand side is a (type = {this/A})

Answer 1

问题是您用函数参数隐藏了 a 关系。如果将 f(a: A) 替换为 f(a': A)，它会起作用。或者，您可以使用 @ 运算符，它返回集合的全局值而不是局部值:

fun f(a: A) : set P {
    { p: P | p.@a = a }
}