A Guide to Alloy
Glossary
(+)
Set-union operator.
(-)
Difference of two set.
(.*)
Transitive closure (reflexive).
(.^)
Transitive closure (non-reflexive).
all
Corresponds to forall.
assertion
These are assumptions about the model that you can ask the analyzer to find counter-examples 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).