Functions and Relations

A function is a relation which does not map any given input to two or more different outputs. In Alloy, a function always returns a relation (possibly a relation that evaluates to a single Atom). See the discussion about using the fun command.