Get greater number in a field? Alloy model checker

Question

I want to return the greater number max(loc.x) in a field scope:

sig Locations{
 x: set Int           // all x locations visited
 xgreater: one Int    // greater location
}

fact{all loc:Locations| xgreater = greaterX[loc]} // get greater location


fun greaterX[loc:Locations]:Int{     // get the greater location
 max(loc.x)                          // HOW do I do this?
}

Any ideas? Thank you.

Answer 1

How about making it a predicate

pred greatest [locs: set Location, x: Location] {...}

with a constraint that there is no location in lock larger than the x?

(Note also that I've changed the signature name to Location: as with classes and types, the convention is to use the singular noun.)