Some examples and notes while learning Alloy modeling language.
See examples/
- (+) - Set-union operator
- (-) - Difference of two sets
- (.*) - 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 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 scheme (in Z) in that it defines the vocabulary for the model.
- some - Multiplicity symbol indicating more than zero (corresponds to there exists).