Skip to main content.

Expressions

Most of the expression syntax of UPPAAL coincides with that of C, C++ and Java. E.g. assignments are done using the '=' operator (the older ':=' still works, but '=' is preferred). Notice that assignments are them self expressions.

The syntax of expressions is defined by the grammar for Expression.

Expression ::= ID
            |  NAT
            |  Expression '[' Expression ']'
            |  '(' Expression ')'
            |  Expression '++' | '++' Expression
            |  Expression '--' | '--' Expression
            |  Expression Assign Expression
            |  Unary Expression
            |  Expression Binary Expression
            |  Expression '?' Expression ':' Expression
            |  Expression '.' ID
	    |  Expression '(' Arguments ')'
	    |  'forall' '(' ID ':' Type ')' Expression
	    |  'exists' '(' ID ':' Type ')' Expression
            |  'deadlock' | 'true' | 'false'

Arguments  ::= [ Expression ( ',' Expression )* ]

Assign     ::= '=' | ':=' | '+=' | '-=' | '*=' | '/=' | '%='
            | '|=' | '&=' | '^=' | '<<=' | '>>='
Unary      ::= '+' | '-' | '!' | 'not'
Binary     ::= '<' | '<=' | '==' | '!=' | '>=' | '>'
            |  '+' | '-' | '*' | '/' | '%' | '&'
            |  '|' | '^' | '<<' | '>>' | '&&' | '||'
            |  '<?' | '>?' | 'or' | 'and' | 'imply'

Like in C++, assignment, preincrement and predecrement expressions evaluate to references to the first operand. The inline-if operator does in some cases (e.g. when both the true and false operands evaluate to compatible references) also evaluate to a reference, i.e., it is possible to use an inline-if on the left hand side of an assignment.

The use of the deadlock keyword is restricted to the requirement specification language.

Boolean Values

Boolean values are type compatible with integers. An integer value of 0 (zero) is evaluated to false and any other integer value is evaluated to true. The boolean value true evaluates to the integer value 1 and the boolean value false evaluates to the integer value 0. Notice: A comparison like 5 == true evaluates to false, since true evaluates to the integer value 1. This is consistent with C++.

Precedence

UPPAAL operators have the following associativity and precedence, listed from the highest to lowest. Operators borrowed from C keep the same precedence relationship with each other.

left () [] .
right! ++ -- unary -
left * / %
left - +
left << >>
left <? >?
left < <= >= >
left == !=
left &
left ^
left |
left &&
left ||
right ?:
right = := += -= *= /= %= &= |= <<= >>= ^=
right not
left and
left or imply
left forall exists

Operators

Anybody familiar with the operators in C, C++, Java or Perl should immediately feel comfortable with the operators in UPPAAL. Here we summarise the meaning of each operator.
() Parenthesis alter the evaluation order
[] Array lookup
. Infix lookup operator to access process scope
! Logical negation
++ Increment (can be used as both prefix and postfix operator)
-- Decrement (can be used as both prefix and --> --postfix operator)
- Integer subtraction (can also be used as unary negation)
+ Integer addition
* Integer multiplication
/ Integer division
% Modulo
<< Left bitshift
>> Right bitshift
<? Minimum
>? Maximum
< Less than
<= Less than or equal to
== Equality operator
!= Inequality operator
>= Greater than or equal to
> Greater than
& Bitwise and
^ Bitwise xor
| Bitwise or
&& Logical and
|| Logical or
?: If-then-else operator
not Logical negation
and Logical and
or Logical or
imply Logical implication
forall Forall quantifier
exists Exists quantifier

Notice that the keywords not, and and or behave the same as the !, &&, and || operators, except that the former have lower precedence.

Expressions Involving Clocks

When involving clocks, the actual expression syntax is restricted by the type checker. Expressions involving clocks are divided into three categories: Invariants, guards, and constraints:

  • An invariant is a conjunction of upper bounds on clocks and differences between clocks, where the bound is given by an integer expression.
  • A guard is a conjunction of bounds (both upper and lower) on clocks and differences between clocks, where the bound is given by an integer expression.
  • A constraint is any boolean combination (involving negation, conjunction, disjunction and implication) of bounds on clocks and differences between clocks, where the bound is given by an integer expression.

In addition, any of the three expressions can contain expressions (including disjunctions) over integers, as long as invariants and guards are still conjunctions at the top-level. The full constraint language is only allowed in the requirement specification language.

Out of Range Errors and Invalid Evaluations

An evaluation of an expression is invalid if out of range errors occur during evalution. This happens in the following situations:

  • Division by zero.
  • Shift operation with negative count.
  • Out of range assignment.
  • Out of range array index.
  • Assignment of a negative value to a clock.
  • Function calls with out of range arguments.
  • Function calls with out of range return values.

In case an invalid evaluation occurs during the computation of a successor, i.e., in the evaluation of a guard, synchronisation, assignment, or invariant, then the verification is aborted.

Quantifiers

An expression forall (ID : Type) Expr evaluates to true if Expr evaluates to true for all values ID of the type Type. An expression exists (ID : Type) Expr evaluates to true if Expr evaluates to true for some value ID of the type Type. In both cases, the scope of ID is the inner expression Expr, and Type must be a bounded integer or a scalar set.

Example

The following function can be used to check if all elements of the boolean array a have the value true.

bool alltrue(bool a[5])
{
  return forall (i : int[0,4]) a[i];
}