# Contents

# 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]; }