UtyExpr (Averest)

UtyExpr Type

Namespace: Averest.Quartz
Assembly: Averest.dll
Parent Module: UtyExprs
Base Type: obj
All Interfaces: IEquatable<UtyExpr> , IStructuralEquatable , IComparable<UtyExpr> , IComparable , IStructuralComparable

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.

Union cases

Union case	Description
`UtyAX UtyExpr` Full Usage: `UtyAX UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyAY UtyExpr` Full Usage: `UtyAY UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyAbs UtyExpr` Full Usage: `UtyAbs UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyAdd UtyExpr * UtyExpr` Full Usage: `UtyAdd UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyAlways UtyExpr` Full Usage: `UtyAlways UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyAny QName * QType * UtyExpr` Full Usage: `UtyAny QName * QType * UtyExpr` Parameters: Item : `QName * QType * UtyExpr`	Item : `QName * QType * UtyExpr`
`UtyAppend UtyExpr * UtyExpr` Full Usage: `UtyAppend UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyApply QName * UtyExpr list` Full Usage: `UtyApply QName * UtyExpr list` Parameters: Item : `QName * UtyExpr list`	Item : `QName * UtyExpr list`
`UtyArr UtyExpr list` Full Usage: `UtyArr UtyExpr list` Parameters: Item : `UtyExpr list`	Item : `UtyExpr list`
`UtyArr2Btv QName` Full Usage: `UtyArr2Btv QName` Parameters: Item : `QName`	Item : `QName`
`UtyArrAcc UtyExpr * UtyExpr` Full Usage: `UtyArrAcc UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyBitOfBtv UtyExpr * ConstExpr` Full Usage: `UtyBitOfBtv UtyExpr * ConstExpr` Parameters: Item : `UtyExpr * ConstExpr`	Item : `UtyExpr * ConstExpr`
`UtyBool2Btv UtyExpr` Full Usage: `UtyBool2Btv UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyBtv2Int UtyExpr` Full Usage: `UtyBtv2Int UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyBtv2Nat UtyExpr` Full Usage: `UtyBtv2Nat UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyBtvConst bool list` Full Usage: `UtyBtvConst bool list` Parameters: Item : `bool list`	Item : `bool list`
`UtyConcat UtyExpr * UtyExpr` Full Usage: `UtyConcat UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyConj UtyExpr * UtyExpr` Full Usage: `UtyConj UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyCont UtyExpr` Full Usage: `UtyCont UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyCos UtyExpr` Full Usage: `UtyCos UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyDisj UtyExpr * UtyExpr` Full Usage: `UtyDisj UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyDiv UtyExpr * UtyExpr` Full Usage: `UtyDiv UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyDrv UtyExpr` Full Usage: `UtyDrv UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyEX UtyExpr` Full Usage: `UtyEX UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyEY UtyExpr` Full Usage: `UtyEY UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyEqu UtyExpr * UtyExpr` Full Usage: `UtyEqu UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyEqv UtyExpr * UtyExpr` Full Usage: `UtyEqv UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyEventual UtyExpr` Full Usage: `UtyEventual UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyExists QName * QType * UtyExpr` Full Usage: `UtyExists QName * QType * UtyExpr` Parameters: Item : `QName * QType * UtyExpr`	Item : `QName * QType * UtyExpr`
`UtyExistsPath UtyExpr` Full Usage: `UtyExistsPath UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyExp(UtyExpr, UtyExpr)` Full Usage: `UtyExp(UtyExpr, UtyExpr)` Parameters: Item1 : `UtyExpr` Item2 : `UtyExpr`	Item1 : `UtyExpr` Item2 : `UtyExpr`
`UtyFalse` Full Usage: `UtyFalse`
`UtyFiniteStar UtyExpr` Full Usage: `UtyFiniteStar UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyFixEqus((FixSign * QName * UtyExpr) list, UtyExpr)` Full Usage: `UtyFixEqus((FixSign * QName * UtyExpr) list, UtyExpr)` Parameters: Item1 : `(FixSign * QName * UtyExpr) list` Item2 : `UtyExpr`	Item1 : `(FixSign * QName * UtyExpr) list` Item2 : `UtyExpr`
`UtyForall QName * QType * UtyExpr` Full Usage: `UtyForall QName * QType * UtyExpr` Parameters: Item : `QName * QType * UtyExpr`	Item : `QName * QType * UtyExpr`
`UtyForallPath UtyExpr` Full Usage: `UtyForallPath UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyITE UtyExpr * UtyExpr * UtyExpr` Full Usage: `UtyITE UtyExpr * UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr * UtyExpr`
`UtyImpl UtyExpr * UtyExpr` Full Usage: `UtyImpl UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyInside` Full Usage: `UtyInside`
`UtyInstant` Full Usage: `UtyInstant`
`UtyInt2Btv UtyExpr * UtyExpr` Full Usage: `UtyInt2Btv UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyInt2Real UtyExpr` Full Usage: `UtyInt2Real UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyIntConst bool list` Full Usage: `UtyIntConst bool list` Parameters: Item : `bool list`	Item : `bool list`
`UtyLeq UtyExpr * UtyExpr` Full Usage: `UtyLeq UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyLes UtyExpr * UtyExpr` Full Usage: `UtyLes UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyListConj QName * ConstExpr * ConstExpr * UtyExpr` Full Usage: `UtyListConj QName * ConstExpr * ConstExpr * UtyExpr` Parameters: Item : `QName * ConstExpr * ConstExpr * UtyExpr`	Item : `QName * ConstExpr * ConstExpr * UtyExpr`
`UtyListDisj QName * ConstExpr * ConstExpr * UtyExpr` Full Usage: `UtyListDisj QName * ConstExpr * ConstExpr * UtyExpr` Parameters: Item : `QName * ConstExpr * ConstExpr * UtyExpr`	Item : `QName * ConstExpr * ConstExpr * UtyExpr`
`UtyListSum QName * ConstExpr * ConstExpr * UtyExpr` Full Usage: `UtyListSum QName * ConstExpr * ConstExpr * UtyExpr` Parameters: Item : `QName * ConstExpr * ConstExpr * UtyExpr`	Item : `QName * ConstExpr * ConstExpr * UtyExpr`
`UtyLog2 UtyExpr` Full Usage: `UtyLog2 UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyMod UtyExpr * UtyExpr` Full Usage: `UtyMod UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyMul UtyExpr * UtyExpr` Full Usage: `UtyMul UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyNat2Btv UtyExpr * UtyExpr` Full Usage: `UtyNat2Btv UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyNat2Int UtyExpr` Full Usage: `UtyNat2Int UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyNat2Real UtyExpr` Full Usage: `UtyNat2Real UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyNatConst bool list` Full Usage: `UtyNatConst bool list` Parameters: Item : `bool list`	Item : `bool list`
`UtyNeg UtyExpr` Full Usage: `UtyNeg UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyNext UtyExpr` Full Usage: `UtyNext UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyOmegaStar UtyExpr` Full Usage: `UtyOmegaStar UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyPastAlways UtyExpr` Full Usage: `UtyPastAlways UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyPastEventual UtyExpr` Full Usage: `UtyPastEventual UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyPastStrongBefore UtyExpr * UtyExpr` Full Usage: `UtyPastStrongBefore UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyPastStrongNext UtyExpr` Full Usage: `UtyPastStrongNext UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyPastStrongUntil UtyExpr * UtyExpr` Full Usage: `UtyPastStrongUntil UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyPastStrongWhen UtyExpr * UtyExpr` Full Usage: `UtyPastStrongWhen UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyPastWeakBefore UtyExpr * UtyExpr` Full Usage: `UtyPastWeakBefore UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyPastWeakNext UtyExpr` Full Usage: `UtyPastWeakNext UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyPastWeakUntil UtyExpr * UtyExpr` Full Usage: `UtyPastWeakUntil UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyPastWeakWhen UtyExpr * UtyExpr` Full Usage: `UtyPastWeakWhen UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyPresent UtyExpr` Full Usage: `UtyPresent UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyRealConst double` Full Usage: `UtyRealConst double` Parameters: Item : `double`	Item : `double`
`UtyReplicate UtyExpr * ConstExpr` Full Usage: `UtyReplicate UtyExpr * ConstExpr` Parameters: Item : `UtyExpr * ConstExpr`	Item : `UtyExpr * ConstExpr`
`UtyReverse UtyExpr` Full Usage: `UtyReverse UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtySat UtyExpr * UtyExpr` Full Usage: `UtySat UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtySegment UtyExpr * ConstExpr * ConstExpr` Full Usage: `UtySegment UtyExpr * ConstExpr * ConstExpr` Parameters: Item : `UtyExpr * ConstExpr * ConstExpr`	Item : `UtyExpr * ConstExpr * ConstExpr`
`UtySin UtyExpr` Full Usage: `UtySin UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtySizeOf UtyExpr` Full Usage: `UtySizeOf UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyStrongBefore UtyExpr * UtyExpr` Full Usage: `UtyStrongBefore UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyStrongUntil UtyExpr * UtyExpr` Full Usage: `UtyStrongUntil UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyStrongWhen UtyExpr * UtyExpr` Full Usage: `UtyStrongWhen UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtySub UtyExpr * UtyExpr` Full Usage: `UtySub UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyTerminate` Full Usage: `UtyTerminate`
`UtyTrue` Full Usage: `UtyTrue`
`UtyTup UtyExpr list` Full Usage: `UtyTup UtyExpr list` Parameters: Item : `UtyExpr list`	Item : `UtyExpr list`
`UtyTup2Btv UtyExpr` Full Usage: `UtyTup2Btv UtyExpr` Parameters: Item : `UtyExpr`	Item : `UtyExpr`
`UtyTupAcc UtyExpr * ConstExpr` Full Usage: `UtyTupAcc UtyExpr * ConstExpr` Parameters: Item : `UtyExpr * ConstExpr`	Item : `UtyExpr * ConstExpr`
`UtyVar QName` Full Usage: `UtyVar QName` Parameters: Item : `QName`	Item : `QName`
`UtyWeakBefore UtyExpr * UtyExpr` Full Usage: `UtyWeakBefore UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyWeakUntil UtyExpr * UtyExpr` Full Usage: `UtyWeakUntil UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`
`UtyWeakWhen UtyExpr * UtyExpr` Full Usage: `UtyWeakWhen UtyExpr * UtyExpr` Parameters: Item : `UtyExpr * UtyExpr`	Item : `UtyExpr * UtyExpr`