UtyExpr is the data type for untyped expressions that are generated by the parser. The following remarks should help to understand the meaning of the operators and their arguments:

• UtyInstant, UtyInside, and UtyTerminate are constants generated by the keywords "instant", "inside", and "terminate" that hold when the body statement satisfies the corresponding control-flow predicates (see language report). The type checker replaces these by declaring boolean variables whose names are the keywords.
• UtyTrue,UtyFalse,UtyBtvConst,UtyNatConst,UtyIntConst,UtyRealConst represent constants for boolean values, bitvectors, nat, int and real numbers. bool list arguments of UtyBtvConst, UtyNatConst, and UtyIntConst represent bitvector constants, a natural number in radix-2 representation, and an integer in two's complement, respectively. The argument of UtyRealConst is the corresponding real constant.
• UtyVar qn represents a variable of any type with name qn.
• UtyNeg,UtyConj,UtyDisj,UtyImpl,UtyEqv are boolean operators that may also be applied to bitvectors of the same length.
• UtyEqu represents equality for all types (note that it is the same as UtyEqv for booleans, but different for bitvectors).
• UtyLes and UtyLeq are numeric comparison operators for nat, int and real.
• UtyAdd,UtySub,UtyMul,UtyDiv are arithmetic operations for nat, int, and real
• UtyMod is the remainder of a nat or int division.
• UtyAbs is the absolute value of an int expression.
• UtySat(B,e) saturates the nat or int-expression e: for a nat-expression e, it will be e if e is less than B, otherwise it is B-1. For an int-expression, it is -B if e is less than -B, B-1 if e is equal to or greater than B, and e otherwise.
• UtyDrv is the derivation operator to describe hybrid systems.
• UtySin and UtyCos are trigonometric operators for real expressions.
• UtyExp and UtyLog2 are the exponential funtions and logarithm to base 2 for both real and nat-expressions.
• UtyBitOfBtv(bv,n) extracts the n-th bit of bitvector expression bv, where n should be a nat/int constant.
• UtyAppend(bv1,bv2) concatenates the bitvectors bv1 and bv2.
• UtySegment([bL;...;b0],n2,n1) = [bn2;...;bn1] where L>=n2>=n1>=0 must hold (it is also allowed to use negative values for n2 or n1, in which case the length L-1 is added to correct this).
• UtyReverse reverses a given bitvector expression.
• UtyReplicate(b,n) replicates the boolean expression b n-times to generate a bitvector.
• UtyArrAcc(lhs,e) is an access to an element of array lhs with the index expression e.
• UtyTupAcc(e,n) extracts the n-th component of a tuple expression e, where e=(e0,...,eN).
• UtyArr[e0;...;eN] generates an array with expressions (e0,...,eN).
• UtyTup[e0;...;eN] generates a tuple expression (e0,...,eN) from a list of expressions.
• UtyPresent(t) checks whether the value of t is currently determined by an action of the program (then it is true) or whether it is determined by the reaction to absence.
• UtyCont(t) switches between the discrete an the continuous environment for hybrid systems. Note that double application of this operator is the identity.
• UtyITE(b,e1,e0) is a generic if-else operator that selects e1 if b holds, and is otherwise e0.
• UtyApply(f,[e1;...;eN]) denotes a function application with a macro function f defined in MacroDefs. MacroDefs should map the QName f to a pair ([x1;...;xN],t) so that the semantics is the expression t{x1:=e1}..{xN:=eN}.
• UtyBool2Btv, UtyNat2Btv, UtyInt2Btv, UtyArr2Btv, UtyTup2Btv, UtyBtv2Nat, UtyBtv2Int, UtyNat2Int, UtyNat2Real, and UtyInt2Real are type adaptors that embed an expression in another type. The second arguments of UtyNat2Btv and UtyInt2Btv are the lengths of the bitvectors that are to be generated.
• UtySizeOf(e) computes the number of bits required to store expression e (it only depends on the type of e).
• UtyListConj, UtyListDisj, and UtyListSum are generic conjunction, disjunction and addition. The argument is a tuple (xn,min,max,e) that expands to a list [e{xn:=min};...;e{xn:=max}] that is then combined with UtyConj, UtyDisj or UtyAdd, respectively.
• UtyNext,...,UtyPastWeakWhen are linear time temporal operators.
• UtyExistsPath and UtyForallPath are path quantifiers to state that in a state a path property holds for all paths leaving it or for at least one of them.
• UtyEX,UtyAX,UtyEY,UtyAY are modal operators for the mu-calculus representing existential and universal successors, and existential and universal predecessors.
• UtyFixEqus(eqL,e) represents a vector mu-calculus formula with equation system eqL and body expression e. Equations are of the form (si,xi,ei) where variable xi is equated to expression ei with as least or greatest fixpoint depending on si.
• UtyConcat(e1,e2) concatenates two omega-regular expressions.
• UtyFiniteStar(e) is finite Kleene star or a regular expression.
• UtyOmegaStar(e) is omega-repetition for an omega-regular expression
• ConstExpr is used as a synonym for UtyExpr in those cases, where the UtyExpr must be reducible to a constant after generic parameters have been instantiated.

a type for untyped substitutions