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
            |  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

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! not ++ -- unary -
left * / %
left - +
left << >>
left <? >?
left < <= >= >
left == !=
left &
left ^
left |
left && and
left || or imply
right ?:
right = := += -= *= /= %= &= |= <<= >>= ^=
left forall exists sum

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 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:

OperatorAssignmentExampleMeaning
++=x += yx = x + y
--=x -= yx = x - y
**=x *= yx = x * y
//=x /= yx = x / y
%%=x %= yx = x % y
&&=x &= yx = x & y
^^=x ^= yx = x ^ y
||=x |= yx = x | y
<<<<=x <<= yx = x << y
>>>>=x >>= yx = x >> y

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, and clock rates.
  • 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];
}

Sum

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.

Floating Point Type Support

Statistical model checking (SMC) supports double precision floating point type double. The clock variables also have floating point values in SMC. Symbolic and statistical model checking can be applied on the same model provided that double and hybrid clock type variables do not influencing the model logic, i.e. they cannot be used in guard and invariant constraints (but can be used in ODE expressions).

The following is the list of builtin floating point functions (mostly imported from C math library, hence the C math manual can be consulted for more details):

  • int abs(int) — absolute value of integer argument.
  • double fabs(double) — absolute value of double argument.
  • double fmod(double x, double y) — remainder of the division opration x/y.
  • double fma(double x, double y, double z) — computes x*y+z as if to infinite precision.
  • double fmax(double x, double y) — the larger of the two arguments.
  • double fmin(double x, double y) — the smaller of the two arguments.
  • double exp(double x) — Euler's number raised to the given power: ex.
  • double exp2(double x) — 2 raised to the given power: 2x.
  • double expm1(double x) — Euler's number raised to the given power minus 1: ex-1.
  • double ln(double x) — logarithm to the base of Euler's number: loge(x).
  • double log(double x) — logarithm to the base of 10 log10(x) (this is different from C library, kept for backward compatibility reasons).
  • double log10(double x) — logarithm to the base of 10: log10(x).
  • double log2(double x) — logarithm to the base of 2: log2(x).
  • double log1p(double x) — logarithm to the base of Euler's number with argument plus 1 loge(1+x).
  • double pow(double x, int y) — raises to the specified integer power xy.
  • double pow(double x, double y) — raises to the specified floating point power xy.
  • double sqrt(double x) — computes square root.
  • double cbrt(double x) — computes cubic root.
  • double hypot(double x, double x) — computes hypotenuse of a right triangle: sqrt(x2+y2).
  • double sin(double x) — sine of an angle in radians.
  • double cos(double x) — cosine of an angle in radians.
  • double tan(double x) — tangent of an angle in radians.
  • double asin(double x) — arc sine in radians.
  • double acos(double x) — arc cosine in radians.
  • double atan(double x) — arc tangent in radians.
  • double atan2(double y, double x) — arc tangent of the ratio y/x in radians.
  • double sinh(double x) — hyperbolic sine: (exp(x)-exp(-x))/2.
  • double cosh(double x) — hyperbolic cosine: (exp(x)+exp(-x))/2.
  • double tanh(double x) — hyperbolic tangent: (exp(x)-exp(-x))/(exp(x)+exp(-x)).
  • double asinh(double x) — inverse hyperbolic sine.
  • double acosh(double x) — inverse hyperbolic cosine.
  • double atanh(double x) — inverse hyperbolic tangent.
  • double erf(double x) — Gauss error function (special non-elementary function of sigmoid).
  • double erfc(double x) — complement of a Gauss error function.
  • double tgamma(double x) — absolute value of the Gamma function (an extension of a factorial function Γ(n)=(n-1)!).
  • double lgamma(double x) — natural logarithm of the Gamma function.
  • double ceil(double x) — the ceiling function, the smallest integer value not less than x.
  • double floor(double x) — the floor function, the largest integer value not greater than x.
  • double trunc(double x) — nearest integer not greater in magnitude than x.
  • double round(double x) — nearest integer value to x rounding halfway cases away from zero.
  • int fint(double x) — converts floating point value into integer (works like trunc()).
  • double ldexp(double x, int y) — multiplies by a specified power of two: x*2y.
  • int ilogb(double x) — extracts unbiased exponent: trunc(log2(x+1)).
  • double logb(double x) — extracts unbiased exponent: trunc(log2(x+1)).
  • double nextafter(double from, double to) — a next representable floating point value of from in the direction of to.
  • double copysign(double x, double y) — floating point value with magnitude of x and sign of y.
  • bool signbit(double x) — true if the argument x is negative.<
  • double random(double max) — pseudo random number distributed uniformly over the interval [0,max).
  • double normal(double mean, double stddev) — pseudo random number distributed according to normal (Gaussian) distribution for a given mean and standard deviation stddev.

A few common constants and types can be declared as follows:

const int INT16_MIN     = -32768;
const int INT16_MAX     =  32767;
const int UINT16_MAX    =  65535;
const int INT32_MIN     = -2147483648;
const int INT32_MAX     =  2147483647;
const int UINT32_MAX    =  4294967295;
typedef int[INT32_MIN, INT32_MAX] int32_t;
typedef int[0, UINT32_MAX]        uint32_t;
const double M_PI       = 3.14159265358979312;  // Pi
const double M_PI_2     = 1.57079632679489656;  // Pi/2
const double M_PI_4     = 0.785398163397448279; // Pi/4
const double M_E        = 2.71828182845904509;  // Euler's number e
const double M_LOG2E    = 1.44269504088896339;  // log_2(e)
const double M_LOG10E   = 0.434294481903251817; // log_10(e)
const double M_LN2      = 0.693147180559945286; // log_e(2)
const double M_LN10     = 2.3025850929940459;   // log_e(10)
const double M_1_PI     = 0.318309886183790691; // 1/Pi
const double M_2_PI     = 0.636619772367581382; // 2/Pi
const double M_2_SQRTPI = 1.12837916709551256;  // 2/sqrt(Pi)
const double M_SQRT2    = 1.41421356237309515;  // sqrt(2)
const double M_SQRT1_2  = 0.707106781186547573; // 1/sqrt(2)