PRISM models can include formulas which are used to avoid duplication of code. A formula comprises a name (an identifier) and an expression. The formula name can then be used as shorthand for the expression anywhere an expression might usually be accepted. A formula is defined as follows:
It can then be used anywhere within that file, as for example in this command:
The effect is exactly as if the following had been typed:
Formulas defined in a model can also be used when specifying its properties.
During parsing of the model, expansion of formulas is done before module renaming so, if a module which uses formulas is renamed to another module, it is the contents of the formula which will be renamed, not the formula itself.
PRISM models can also contain labels. These are a way of identifying sets of states that are of particular interest. Labels can only be used when specifying properties but, for convenience, can be defined in model files as well as property files.
Labels differ from formulas in two other ways: firstly, they must be of Boolean type;
secondly, they are written using quotation marks ("..."), as illustrated in the following example:
Site hosted at the Department of Computer Science, University of Oxford