Skip to content
This repository has been archived by the owner on Feb 19, 2022. It is now read-only.

Latest commit

 

History

History
37 lines (28 loc) · 1.65 KB

README.md

File metadata and controls

37 lines (28 loc) · 1.65 KB

Alloy learning

Some examples and notes while learning Alloy modeling language.

Examples

See examples/

Glossary

  • (+) - 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).

Resources

License

MIT