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 | Expression Assign Expression | Unary Expression | Expression Binary Expression | Expression '?' Expression ':' Expression | Expression '.' ID | Expression '(' Arguments ')' | 'forall' '(' ID ':' Type ')' Expression | 'exists' '(' ID ':' Type ')' Expression | 'sum' '(' 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 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++.
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 ! not ++ -- unary - left * / % left - + left << >> left <? >? left < <= >= > left == != left & left ^ left | left && and left || or imply right ?: right = := += -= *= /= %= &= |= <<= >>= ^= left forall exists sum
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 or structure type 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 sum Sum expression
Notice that the keywords not, and and or behave the same as the !, &&, and || operators, except that the former have lower precedence.
A few binary operators can be syntactically combined with assignment to produce a compact assignment expression:
Operator Assignment Example Meaning + += x += y x = x + y - -= x -= y x = x - y * *= x *= y x = x * y / /= x /= y x = x / y % %= x %= y x = x % y & &= x &= y x = x & y ^ ^= x ^= y x = x ^ y | |= x |= y x = x | y << <<= x <<= y x = x << y >> >>= x >>= y x = x >> y
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:
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.
An evaluation of an expression is invalid if out of range errors occur during evalution. This happens in the following situations:
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.
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.
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]; }
An expression sum (ID : Type) Expr evaluates to an integer and is equal to the sum of the expressions evaluated with ID ranging over the given type argument. Boolean or state predicates (in TCTL expressions only) are accepted but not clock constraints. The expressions must be side-effect free. The type must be a bounded integer or a scalar set.