# Language Reference¶

Nested model checking problems are specified in the simple language called **NML** and described in this section. NML expressions can be evaluated to integer numbers. They are stored in text files with *.nm* extension.

## Model checking¶

The **model checking primitive** is used to evaluate the result of a model checking problem. The result is a non-negative integer number whose meaning depends on the type of the model. When checking a property over a non-probabilistic model, the result is 0 (not satisfied) or 1 (satisfied). When checking a property over a probabilistic model, the result is the min (alt. max) probability that the property is satisfied in per thousand. For example, a probability equal to 0.1234 is represented as 123. Model checking models are specified using the (P)CSP# language (see PAT documentation). The property to be verified is the first assertion of the given model. The result is computed using PAT.

mc(`<model>` ) |

where

`<model>` |
Path to a (P)CSP# model (.csp, .pcsp) |

## Meta model checking¶

The **meta model checking primitive** is used to evaluate the result of a meta model checking problem. Similarly to the model checking primitive, it returns an integer number. Meta model models are specified using the (P)CSP# language (see PAT documentation) extended with labeled place-holders of the form `[id]`

where `id`

is a label. These labeled place-holders can be used in place of integer constants (e.g., variable initial values, choice probabilities). A well-formed meta model checking call must bind all labeled place-holders of the given meta model with NML expressions. These bindings are specified in the *where* clause. When executed, the provided meta model is instantiated. A (P)CSP# model is obtained by substituting the occurrences of every labelled place-holder by the value of its binded expression. The property to be verified is the first assertion of the given model. The result is computed using PAT.

mcc(`<model>` where `<label>` = `<expr>` , `<label>` = `<expr>` , … ) |

where

`<model>` |
Path to a meta-(P)CSP# model (.mcsp, .mpcsp) |

`<label>` |
A label (e.g., x,y,word) |

`<expr>` |
A NML expression |

## Constant¶

Constants are introduced with simple and non-recursive *let*-expressions. The *let* clause of a *let*-expression specify bindings that associate labels to NML expressions. The result of a *let*-expression is the expression given by the *in* clause evaluated in the context where every binding in the *let* clause defines a constant, identified by its label, and that evaluates to the value of its expression.

let `<label>` = `<expr>` , `<label>` = `<expr>` , … in `<expr>` |

where

`<label>` |
A label (e.g., x,y,word) |

`<expr>` |
A NML expression |

## Arithmetic operation¶

The arithmetic operations supported in NML are binary operation (e.g., +,-,*,/,%) with standard semantics. The left-hand side and the right-hand side expressions are evaluated before the operation is performed.

`<expr>` `<op>` `<expr>` |

where

`<op>` |
An operator (+,-,*,/,% are supported) |

`<expr>` |
A NML expression |

## Number¶

Integer numbers such as `-5`

, `32`

, `0`

are well-formed NML expressions.