.. _nmspec:

==================
Language Reference
==================

Nested model checking problems are specified in the simple language called **NML** and described in this section. The NM: language specify expressions that 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 <https://www.comp.nus.edu.sg/~pat/OnlineHelp/index.htm>`_). The property to be verified is the first assertion of the given model. The result is computed using `PAT <https://www.comp.nus.edu.sg/~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 <https://www.comp.nus.edu.sg/~pat/OnlineHelp/index.htm>`_) 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 <https://www.comp.nus.edu.sg/~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 but 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.