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

合金告诉我我犯了一个错误：

发生类型错误 这不能是左侧是 p (type = {this/P}) 右侧是 a (type = {this/A}) 的合法关系连接

标签： alloy

Answer 1

问题是您掩盖了a与函数参数的关系。如果你f(a: A)用f(a': A). 或者，您可以使用@运算符，它返回集合的全局值而不是局部值：

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