(+)

Setunion operator.

()

Difference of two set.

(.*)

Transitive closure (reflexive).

(.^)

Transitive closure (nonreflexive).

all

Corresponds to forall.

assertion

These are assumptions about the model that you can ask the analyzer to find counterexamples of.

check

Command given to Alloy to attempt to find counter examples of an assertion.

fact

These are constraints of the model that are assumed to always hold.

function

An expression that returns a result.

lone

Multiplicity symbol indicating zero or one.

module

Similar to package in Java and corresponding to the path to the .als file from the project directory.

one

Multiplicity symbol indicating exactly one.

predicate

consists of one or more constraints and can be used to represent operations.

run

Command to ask Alloy to find instances that satisfy a predicate.

signature

A signature in Alloy is similar to the signature of a schema (in Z) in that it defines the vocabulary for the model.

some

Multiplicity symbol indicating more than zero (corresponds to there exists).
