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