Sections

Sorts

Sorts are to be declared as a comma separated list, as below

    S,
    DATA

Functions

Function declarations have a list of types for the arguments separated by a '#', and a result type indicated with '->'.

    f : -> S
    f : DATA -> S
    f : S # DATA -> S

Functions can also be declared as infix- or prefix-operators. The name of an operator consists either of one or more operator symbols or of a normal function name enclosed in '.'. The places for the arguments of the operator are indicated in the declaration with a '_'.

    _&_ : B # B -> B
    _@*$^_ : B # B -> B
    _.and._ : B # B -> B
    !_ : B -> B
    .not._ : B -> B

These operators can be used as shown below.

    x & y
    x @*$^ y
    x .and. y
    ! x
    .not. y

Variables

Depending on the type of the module, the variable section lists the variables used either in the equations or in the process definitions. The type of variables is indicated with '->'.

    x : -> S

Equations

The definition of a function is given by means of equations. An equation is interpreted as a rule for a term rewrite system, in which the left hand side is rewritten to the right hand side. In the example below we give equations for the boolean and function.

[and1] and(false, false) = false
[and2] and(false, true) = false
[and3] and(true, false) = false
[and4] and(true, true) = true

Tags ([x]) on the left side of the equations are for documentation purposes only.

It is possible to use variables in an equation that are declared in the variables section. The variables get a value from the matching of terms with the left hand side in the rewrite process. These values are then substituted in the right hand side.

[and1] and(false, x) = false
[and2] and(true, x) = x

Equations can have conditions which have to be fulfilled before such equations can be applied. A condition is indicated with the keyword when followed by a comma separated list of equations.

[and1] and(x, y) = false when x = false
[and2] and(x, y) = false when y = false
[and3] and(true, true) = true

Atoms

Atom declarations have a list of types for the arguments separated by a '#'.

    a
    a : S
    a : DATA # S

Processes

Process declarations have a list of types for the arguments separated by a '#'.

    P
    P : S
    P : DATA # S

Sets

A sets section consists of sub-sections, each indicating the type of the sets declared in this sub-section.

    of atoms
        H = set-expression
    of S
        D = set-expression
        E = set-expression

A set expression can be one of the following constructions in which S and T denote set expressions.

sort  S

indicating all elements of the sort S

set  S

indicating all elements of the set S

enumeration  { e1 , e2 , ... , en }

An enumeration can contain placeholders.

	    H = {a(x), b(y) | x in S, y in DATA}

union  S + T

intersection  S . T

difference  S \ T

Communications

A communication consist of two communication partners separated by a '|' and the resulting action of that communication. Communication declarations can contain placeholders, in which case a communication can only take place if the communication partners have the same value for each placeholder. The values for the placeholders are substituted in the resulting communication action.

    a | b = c
    a(x) | b(x) = c(x) for x in S
    a(x) | b(y) = c(x, y) for x in S, y in S

Definitions

Process definitions consist of a process on the left hand side and its definitions on the right hand side. The process can have terms as arguments in which variables, defined in the variables section, may occur.

    P = process-expression
    P(x) = process-expression
    P(f(b), b(y)) = process-expression

Upon execution of a process, the process will be matched with the left hand side of the process definitions. The process will be replaced by an alternative composition of all the definitions for which the left hand side matches. If there is no matching process definition, a deadlock results. In the matching of the process, values for the variables will be determined, which will be substituted in the right hand side of the definition.

• process expression