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.