%STILL NOT DONE --- NEEDS FORMATTING
\appendix

\chapter{Glossary}
\pagestyle{empty}
\begin{description}
  \item[(+)] Set-union operator.
  \item[(-)] Difference of two set.
  \item[(.*)] Transitive closure (reflexive).
  \item[(.\^{})] Transitive closure (non-reflexive).
  \item[all] Corresponds to forall.
  \item[assertion] These are assumptions about the model that you can ask the analyzer to find counter-examples of.
  \item[check] Command given to Alloy to attempt to find counter examples of an assertion.
  \item[fact] These are constraints of the model that are assumed to always hold.
  \item[function] An expression that returns a result.
  \item[lone] Multiplicity symbol indicating zero or one.
  \item[module] Similar to package in Java and corresponding to the path to the .als file from the project directory.
  \item[one] Multiplicity symbol indicating exactly one.
  \item[predicate] consists of one or more constraints and can be used to represent operations.
  \item[run] Command to ask Alloy to find instances that satisfy a predicate.
  \item[signature] A signature in Alloy is similar to the signature of a schema (in Z) in that it defines the vocabulary for the model.
  \item[some] Multiplicity symbol indicating more than zero (corresponds to there exists).
\end{description}
