Modest Language Reference - Modest Toolset

(This documentation of the Modest language is a work in progress. It will slowly be extended over time.)

Every Modest model is a process. A process consists of declarations and a process behaviour. Declarations and behaviour can include expressions.

Comments

All characters in a Modest file starting from // to the end of a line and from /* up to the next */ are ignored as comments.

Declarations

All the components of a Modest process must be declared explicitly.

Actions

An action can be an impatient (default), patient, binary or broadcast action. Impatient and patient actions use multi-way synchronisation by default, while binary actions use binary and broadcast actions use broadcast synchronisation. The synchronisation behaviour of impatient and patient actions can be modified by a par construct with synchronisation vectors. The difference between impatient and patient actions only affects deadlines given by the urgent construct.

action ia; // declares impatient action ia for multi-way synchronisation impatient action ib, ic; // declares impatient actions ib and ic for multi-way synchronisation patient action pa; // declares patient action pa for multi-way synchronisation binary action ba; // declares action ba for binary synchronisation broadcast action bb, bd; // declares actions bb and bd for broadcast synchronisation

Action names use lowercase letters only. Action names that consist of multiple words are written in snake case, e.g. act_now.

Exceptions

Exceptions are declared just like actions.

exception e; // declares exception e

Exception names use lowercase letters only. Exception names that consist of multiple words are written in snake case, e.g. division_by_zero.

Processes

A process can declare child processes that can be used in process call constructs.

// Declare a parameterless process named P with declarations Decl and behaviour Beh process P() { Decl Beh } // Declare a process named Q with two parameters i and x process Q(int(0..5) i, real x) { Decl Beh }

Process names are capitalised. If a process name consists of multiple words, it is written in upper camel case, e.g. ThisIsAProcessName.

Datatypes

Modest provides the ability to declare and use complex, including recursive, datatypes.

datatype coord = { real x, real y }; // declares a non-recursive datatype with members x and y datatype int_list = { int hd, int_list option tl }; // declares a recursive datatype for lists of integers

Datatype names use lowercase letters only. Datatype names that consist of multiple words are written in snake case as above.

Functions

User-defined functions can be used in expressions. They can be parameterised, and have read access to the variables of the scope of the process in which the function is declared and of all ancestor processes. Functions can be recursive, and mutually recursive. The syntax of a function declaration is

function type name(params) = e;

where type is the return type, name is an identifer, params is a list of formal parameters, and e is an expression of type type.

function int square(int n) = n * n; // squares function int fac(int n) = if n == 0 then 1 else n * fac(n - 1); // factorials // Create a list of integers containing all integers from n up to and including m function int_list option n_to_m(int n, int m) = if n > m then none else some(int_list { hd: n, tl: n_to_m(n + 1, m) });

Function names use lowercase letters only. Function names that consist of multiple words are written in snake case as above. Prefer the if-then-else syntax to the ternary operator syntax for choices in longer functions.

Constants

Constants can only have type int and real. The value of a constant can be omitted to create a parametric model. Constants can only be declared in the outermost scope of a model.

const int N = 5; // declares a constant named N of type int with value 5 const real PROB; // declares a constant named PROB of type real for parametric analysis

Constant names use uppercase letters only. Constant names that consist of multiple words are written in snake case, e.g. MAX_PROB.

Variables

Variables can have any valid type. They can be initialised to a constant expression of their type. If no intialisation is specified, a variable's initial value is the default value of its type.

int(0..N) i = 2; // declares a bounded integer variable named i with values from 0 to N with initial value 2 int[] option ia; // declares a variable named i of type int[] option with implicit initial value none

Variable names use lowercase letters only. Variable names that consist of multiple words are written in snake case, e.g. num_packets.

Properties

Properties must be named. They can only be declared in the outermost scope of a model.

property PrL = Pmax(<> (square(i) != 0)); property "Em" = Xmin(S(i), i == 2);

Property names are capitalised. If a property name consists of multiple words, it is either written as separate words in double quotes, e.g. "Max. Probability", or in upper camel case, e.g. MaxProbability.

The Modest Language