Search code examples
alloy

How to use a set comprehension for the body of a function

Suppose I have the following signatures:

sig A {}
sig B {}

sig P {
    a: A,
    b: B
}

How can I write a function f, say, such that f returns the set of P for which each member has the value x: A for its a field?

Entering the expression {p: P | p.a = x} into the evaluator gives me back a set, but when I try to define f in this manner

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

alloy tells me I've made an error:

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

Solution

  • The problem is that you shadowed the a relation with your function parameter. It works if you replace f(a: A) with f(a': A). Alternatively, you can use the @ operator, which returns the global instead of local value of a set: 

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