A behaviour description might look like this:

  enum MyEnumType { Value1, Value2 };

  MyEnumType myEnumVariable = MyEnumType.Value1;
  bool myBoolVariable = true;

  on myPort1.myEvent1():
    bool blocal = myBoolVariable;
    myBoolVariable = false;
    on myPort1.myEvent2(): illegal;

  void f(bool b)
    if (b) myPort2.myEvent5();
    else   { myPort2.myEvent5(); myBoolVariable = true; }

This behaviour section introduces a local enum type (MyEnumType), two variables (called myEnumVariable and myBoolVariable), a number of statements, and a function definition (void f(bool b)) with one parameter. Note that in a sub scope a local variable blocal is defined. The different constructs are handled in more detail below.

Variable Declarations

As demonstrated in the example above, variables can be defined in a behaviour description, both at top level and in a local scope. Variables must be given an initial value.

The top-level variables are often referred to as 'state variables'. Their scope extends to the complete behaviour description, including the body of functions defined in the behaviour.

Variables defined at other places have a scope which is restricted to the compound statement ({ …​. }) they are defined in.

State Variables

Declarative versus Imperative Statements

There are two 'kinds' of behavioural statements: 'declarative' and 'imperative'. The declarative part describes the trigger events and the conditions in which they have to be handled, while the imperative part describes the response that has to occur as result of a trigger.

Compound Statement

Statements of the same 'kind' can be grouped using curly braces:

  { Statement1; Statement2; Statement3; }

It results in a single 'compound statement', of the same 'kind' as its sub statements, and can be used as such. Note that the list of statements within the curly braces can be empty:

  { /* this is an empty statement sequence */ }

Declarative Statements

The triggers an interface or component has to handle and the conditions in which they occur are described as declarative statements. The conditions are expressed as 'guard statements', the triggers as 'on-event statements'.

Guard Statement

A guard statement looks like:

  [ myBooleanExpression ] myStatement

The square brackets ([ and ]) must contain a boolean expression expressing the validity of the guard. The statement following the guard can be either declarative or imperative.

On-event Statement

In an interface behaviour specification an on-event statement is expressed as:

  on myEvent: myStatement

The statement contains a keyword on, the name of an event introduced in the interface, a colon (:), and a statement, which can be either be declarative or imperative. A declarative statement must not contain further on-event statements: nesting these statements is not allowed.

Note that no event parameters must be specified in an interface.

In a component behaviour specification an on-event statement is expressed as:

  on myPort.myEvent(myParameter1): myStatement

where myPort is a port of the component with an interface type that contains event myEvent with one data parameter. Note that in a component behaviour specification data parameters have to be used where specified. On the trigger each data parameter must be a fresh variable, implicitly typed conform the event specification.

Imperative Statements

The response on a (guarded) trigger event are expressed in the imperative statement following the declarative part. All variable assignments, event actions, function calls, etc. are handled here.

Variable Declaration Statement

New variables can be declared as follows:

  myType myVariable = myInitialValueExpression;

where myType denotes a previously defined type, myVariable is a 'fresh' name, and myInitialValueExpression an expression of type myType.

After the variable has been declared it can be referred to as long as the referring place is in scope (scopes being introduced by compounds). 'Fresh' should be interpreted as follows:

  • No two variables with the same name can be declared in one scope.

  • A variable myVar that has been declared in a wider scope can be 'shadowed' by a variable declaration with the same name in a sub scope

Assignment Statement

A previously declared variable can change value using an assignment statement:

  myVariable = myValueExpression;

Action Statement

In handling the response on a trigger event, an event action can be called. The syntax in an interface declaration is:


where myEvent is the name of an out event introduced in the interface. Note that no event parameters must be specified.

In a component behaviour specification an action statement is expressed as:


where myPort is a port of the component with an interface type that contains event myEvent with one data parameter.

Note that the event in an action statement must be a void event. For a valued event the return value must be caught, so an assignment statement is the appropriate way to handle that:

  myVariable = myEvent;


  myVariable = myPort.myEvent(myParameterExpression);

in an interface or component behaviour respectively.

Function Call Statement

A function defined in a behavioral specification can be called with properly typed parameter expressions. Given a function declaration

  void myFunc(MyEnumType e, bool b) { /* ... */ }

a function call statement might look like:

  myFunc(myEnumExpression, myBooleanExpression);

Note that the function in a function call statement must be a void function. For a valued function the return value must be caught, so an assignment statement is the appropriate way to handle that:

  myVariable = myValuedFunc(myBooleanExpression);

Reply Statement

A valued trigger event will have to set the appropriate return value in its response handling. Setting that value (not returning yet) is denoted as:


Return Statement

A valued function has to return with a value of the appropriate type. This looks like:

  return myValuedExpression;

If Statement

Conditional handling of statements is supported by the if statement, which can have an optional else part:

  if (myBooleanExpression) myStatement1


  if (myBooleanExpression) myStatement1 else myStatement2

where if and else are keywords, and the parentheses are part of the construct. The expression between the parentheses must be a boolean expression. The statements myStatement1 and myStatement2 are arbitrary imperative statements.

Note that nested if statements are allowed, and that

  if (b1) if (b2) myStatement1 else myStatement2

will be interpreted as

  if (b1)
  { if (b2) myStatement1 else myStatement2 }

and not as

  if (b1)
  { if (b2) myStatement1 }
  else myStatement2

In other words: else binds to the closest if.


A function declaration introduces the signature of a function and its body. The signature is built up from the return type, the name of the function, and a list of typed parameters. The body is a compound statement in the imperative part of the language, so no on-event and guarded statements are allowed. It is allowed however to refer to action events and global state variables, and of course to the function parameters.

An example:

MyReturnType myFunc(bool myPar1, MyEnum myPar2)
  bool myLocalBool = myPar2;
  if (myPar1)
    myLocalBool = false;
  myGlobal = myPar2;
  return myRetuenValue;

This declares a function called myFunc with two parameters (of type bool and MyEnum respectively) and returning a value of type MyReturnType. In the function body a local variable is declared, a conditional action event is called, a global state variable is set, another function is called, and the return value is set.

Functions are allowed to be recursive, and also mutual recursive (function f calling function g and vice versa), under one condition: A recursive function must be "tail recursive"; this means that the recursive call must be the last statement in the function. The rationale for this restriction comes from the need for verification: the generic recursive case cannot be verified.