Expr.xcore metamodel description
Table of contents
- AtomicExpression
- BeginningOfCycle
- BinaryArithmeticExpression
- BinaryArithmeticOperator
- BinaryCtlExpression
- BinaryCtlOperator
- BinaryExpression
- BinaryLogicExpression
- BinaryLogicOperator
- BinaryLtlExpression
- BinaryLtlOperator
- BoolLiteral
- BoolType
- ComparisonExpression
- ComparisonOperator
- ElementaryType
- EndOfCycle
- ExplicitlyTyped
- Expression
- FloatLiteral
- FloatType
- FloatWidth
- InitialValue
- IntLiteral
- IntType
- LeftValue
- LibraryFunction
- LibraryFunctions
- Literal
- NaryExpression
- Nondeterministic
- StringLiteral
- StringType
- TemporalBoolType
- Type
- TypeConversion
- Typed
- UnaryArithmeticExpression
- UnaryArithmeticOperator
- UnaryCtlExpression
- UnaryCtlOperator
- UnaryExpression
- UnaryLogicExpression
- UnaryLogicOperator
- UnaryLtlExpression
- UnaryLtlOperator
- UninterpretedFunction
- UninterpretedSymbol
- UnknownType
Package cern.plcverif.base.models.expr
Abstract class Type
Represents data type that are contained by ExplicitlyTyped model elements and returned by Typed model elements. Instances of this class and any subclasses must be compared by value instead of by reference, as every ExplicitlyTyped instance will have its own copy.
Extends: EObject
Operations:
- dataTypeEquals(other : Type) :
EBoolean
- Returns true if the current type is considered equal to the other type.
@GenModel(documentation="Represents data type that are contained by ExplicitlyTyped model elements and
returned by Typed model elements. Instances of this class and any subclasses must be compared by
value instead of by reference, as every ExplicitlyTyped instance will have its own copy.")
abstract class Type {
@GenModel(documentation="Returns true if the current type is considered equal to the other type.")
op boolean dataTypeEquals(Type other) { throw new UnsupportedOperationException("Must be overridden by the subclasses."); }
}
Class UnknownType
Represents a data type that is currently unknown. Instances of this class are used with UninterpretedSymbols.
Extends: Type
Operations:
- dataTypeEquals(other : Type) :
EBoolean
- An unknown type is never equal to anything.
@GenModel(documentation="Represents a data type that is currently unknown. Instances of this class are
used with UninterpretedSymbols.")
class UnknownType extends Type {
@GenModel(documentation="An unknown type is never equal to anything.")
op boolean dataTypeEquals(Type other) {
return false;
}
}
Abstract class ElementaryType
The base class for all elementary (non-complex) types.
Extends: Type
@GenModel(documentation="The base class for all elementary (non-complex) types.")
abstract class ElementaryType extends Type {
}
Class IntType
Represents an integer type that can be signed or unsigned and has a bit width that includes the potential representation of the sign.
Extends: ElementaryType
Attributes:
- signed :
EBoolean
- Default value: true
- bits :
EInt
- Default value: 16
Operations:
- dataTypeEquals(other : Type) :
EBoolean
- Returns true if the other type is an IntType with the same sign and bit width.
- getUnsignedBits() :
EInt
- Returns the number of bits that can be used to represent nonnegative numbers
@GenModel(documentation="Represents an integer type that can be signed or unsigned and has a bit width that
includes the potential representation of the sign.")
class IntType extends ElementaryType {
boolean signed = "true"
int bits = "16"
@GenModel(documentation="Returns true if the other type is an IntType with the same sign and bit width.")
op boolean dataTypeEquals(Type other) {
if (other instanceof IntType) {
return (other.signed == this.signed && other.bits == this.bits);
}
return false;
}
@GenModel(documentation="Returns the number of bits that can be used to represent nonnegative numbers")
op int getUnsignedBits() {
if (signed) {
return bits - 1
} else {
return bits
}
}
}
Class FloatType
Represents a float type that has a bit width specified by a FloatWidth.
Extends: ElementaryType
Attributes:
- bits : FloatWidth
- Default value: 16
Operations:
- dataTypeEquals(other : Type) :
EBoolean
- Returns true if the other type is an FloatType with the same bit width.
@GenModel(documentation="Represents a float type that has a bit width specified by a FloatWidth.")
class FloatType extends ElementaryType {
FloatWidth bits = "16"
@GenModel(documentation="Returns true if the other type is an FloatType with the same bit width.")
op boolean dataTypeEquals(Type other) {
if (other instanceof FloatType) {
return (other.bits == this.bits);
}
return false;
}
}
Class TemporalBoolType
Represents a temporal Boolean type. A temporal Boolean cannot be evaluated without a model providing a behavior to check against.
Extends: ElementaryType
Operations:
- dataTypeEquals(other : Type) :
EBoolean
- Returns true if the other type is a TemporalBoolType.
@GenModel(documentation="Represents a temporal Boolean type. A temporal Boolean
cannot be evaluated without a model providing a behavior to check against.")
class TemporalBoolType extends ElementaryType {
@GenModel(documentation="Returns true if the other type is a TemporalBoolType.")
op boolean dataTypeEquals(Type other) {
return other instanceof TemporalBoolType;
}
}
Class BoolType
Represents a Boolean type.
Extends: TemporalBoolType
Operations:
- dataTypeEquals(other : Type) :
EBoolean
- Returns true if the other type is an BoolType.
@GenModel(documentation="Represents a Boolean type.")
class BoolType extends TemporalBoolType {
@GenModel(documentation="Returns true if the other type is an BoolType.")
op boolean dataTypeEquals(Type other) {
return other instanceof BoolType;
}
}
Class StringType
Represents a string type that has a maximum length.
Extends: ElementaryType
Attributes:
- maxLength :
EInt
- Maximum lenght of the string in characters.
- Default value: 255
Operations:
- dataTypeEquals(other : Type) :
EBoolean
- Returns true if the other type is an StringType with the same maximum length.
@GenModel(documentation="Represents a string type that has a maximum length.")
class StringType extends ElementaryType {
@GenModel(documentation="Maximum lenght of the string in characters.")
int maxLength = "255"
@GenModel(documentation="Returns true if the other type is an StringType with the same maximum length.")
op boolean dataTypeEquals(Type other) {
if (other instanceof StringType) {
return (other.maxLength == this.maxLength);
}
return false;
}
}
Interface Typed
Represents a model element that has a type (either contained or derived).
Extends: EObject
Operations:
- getType() : Type
- Returns the type of the implementing model element. The returned type is always contained, but not necessarily in the implementing element.
@GenModel(documentation="Represents a model element that has a type (either contained or derived).")
interface Typed {
@GenModel(documentation="Returns the type of the implementing model element. The returned type is
always contained, but not necessarily in the implementing element.")
op Type getType() }
Interface ExplicitlyTyped
Represents a model element whose type is explicitly specified.
Extends: Typed
References:
- type [1..1]: Type
- Stores the type of the implemented model element. The getter method overrides method getType() in the Typed interface.
- Containment: contains
@GenModel(documentation="Represents a model element whose type is explicitly specified.")
interface ExplicitlyTyped extends Typed {
@GenModel(documentation="Stores the type of the implemented model element. The getter method overrides
method getType() in the Typed interface.")
contains Type[1] ^type
}
Interface Expression
Represents an expression, that is, a node in an expression tree.
Extends: Typed
@GenModel(documentation="Represents an expression, that is, a node in an expression tree.")
interface Expression extends Typed {
}
Abstract class AtomicExpression
Generic representation for atomic expressions that will serve as the leaves of the expression tree.
Extends: Expression
Operations:
- getType() : Type
@GenModel(documentation="Generic representation for atomic expressions that will serve as the leaves of the expression tree.")
abstract class AtomicExpression extends Expression {
op Type getType() {
throw new UnsupportedOperationException();
}
}
Abstract class UnaryExpression
Generic representation for expressions of pattern 'f(A)' or '[op] A'
Extends: Expression
References:
- operand [1..1]: Expression
- Containment: contains
Operations:
- getType() : Type
- By default, unary expressions have the same type as their operands (to be overridden if this is not appropriate).
@GenModel(documentation="Generic representation for expressions of pattern 'f(A)' or '[op] A'")
abstract class UnaryExpression extends Expression {
contains Expression[1] operand
@GenModel(documentation="By default, unary expressions have the same type as their
operands (to be overridden if this is not appropriate).")
op Type getType() {
return operand.^type
}
}
Abstract class BinaryExpression
Generic representation for expressions of pattern 'A [op] B'.
Extends: Expression
References:
- leftOperand [1..1]: Expression
- Containment: contains
- rightOperand [1..1]: Expression
- Containment: contains
Operations:
- getType() : Type
- By default, binary expressions have to have operands of the same type the same type, so the type returned by this method will be one of their types. If any of the operands are of unknown type, the result is that UnknownType instance.
@GenModel(documentation="Generic representation for expressions of pattern 'A [op] B'.")
abstract class BinaryExpression extends Expression {
contains Expression[1] leftOperand
contains Expression[1] rightOperand
@GenModel(documentation="By default, binary expressions have to have operands of the same type
the same type, so the type returned by this method will be one of their types. If any of the
operands are of unknown type, the result is that UnknownType instance.")
op Type getType() {
val leftType = leftOperand.^type;
if (leftType instanceof UnknownType) {
return leftType;
}
val rightType = rightOperand.^type;
if (rightType instanceof UnknownType) {
return rightType;
}
if (leftType.dataTypeEquals(rightType) == false) {
throw new IllegalStateException("Binary operation has operands of different types.")
}
if (leftType instanceof BoolType && !(rightType instanceof BoolType)) {
return rightType;
}
return leftType;
}
}
Abstract class NaryExpression
Generic representation for expressions of pattern 'f(A, ..., B)'.
Extends: Expression
References:
- operands [1..*]: Expression
- Containment: contains
Operations:
- getType() : Type
@GenModel(documentation="Generic representation for expressions of pattern 'f(A, ..., B)'.")
abstract class NaryExpression extends Expression {
contains Expression[1..*] operands
op Type getType() {
throw new UnsupportedOperationException("Type is undefined for generic N-ary expressions.");
}
}
Abstract class LeftValue
generic representation for atomic expressions that represents pieces of data to which a value can be assigned.
Extends: AtomicExpression
@GenModel(documentation="generic representation for atomic expressions that represents pieces of
data to which a value can be assigned.")
abstract class LeftValue extends AtomicExpression {
}
Abstract class InitialValue
Generic representation for atomic expressions that can be initial values of a piece of data. Currently implemented by Literal and Nondeterministic.
Extends: AtomicExpression
@GenModel(documentation="Generic representation for atomic expressions that can be initial values
of a piece of data. Currently implemented by Literal and Nondeterministic.")
abstract class InitialValue extends AtomicExpression {
}
Abstract class Literal
Generic representation for atomic expressions that have a fixed value.
Extends: InitialValue, ExplicitlyTyped
@GenModel(documentation="Generic representation for atomic expressions that have a fixed value.")
abstract class Literal extends InitialValue, ExplicitlyTyped {
}
Class UninterpretedSymbol
Representation of a uninterpreted symbol or placeholder. The type is usually an UnknownType (if assigned by a factory) but as an ExplicitlyTyped element, it can be set to more specific types.
Extends: AtomicExpression, ExplicitlyTyped
Attributes:
- symbol [1..1]:
EString
@GenModel(documentation="Representation of a uninterpreted symbol or placeholder. The type is usually
an UnknownType (if assigned by a factory) but as an ExplicitlyTyped element, it can be set to more
specific types.")
class UninterpretedSymbol extends AtomicExpression, ExplicitlyTyped {
String [1] symbol
}
Class Nondeterministic
Representation a nondeterministic value of the specified type.
Extends: InitialValue, ExplicitlyTyped
@GenModel(documentation="Representation a nondeterministic value of the specified type.")
class Nondeterministic extends InitialValue, ExplicitlyTyped {
}
Class UnaryArithmeticExpression
Representation for arithmetic expressions of pattern '[arithOp] A', where [arithOp] is MINUS or BITWISE_NOT.
Extends: UnaryExpression
Attributes:
- operator : UnaryArithmeticOperator
@GenModel(documentation="Representation for arithmetic expressions of pattern '[arithOp] A',
where [arithOp] is MINUS or BITWISE_NOT.")
class UnaryArithmeticExpression extends UnaryExpression {
UnaryArithmeticOperator operator
}
Class BinaryArithmeticExpression
Representation for arithmetic expressions of pattern 'A [arithOp] B', where [arithOp] is PLUS, MINUS, MULTIPLICATION, DIVISION, MODULO, INTEGER_DIVISION, POWER, BITSHIFT, BITROTATE, BITWISE_OR, BITWISE_AND or BITWISE_XOR.
Extends: BinaryExpression
Attributes:
- operator : BinaryArithmeticOperator
@GenModel(documentation="Representation for arithmetic expressions of pattern 'A [arithOp] B',
where [arithOp] is PLUS, MINUS, MULTIPLICATION, DIVISION, MODULO, INTEGER_DIVISION, POWER,
BITSHIFT, BITROTATE, BITWISE_OR, BITWISE_AND or BITWISE_XOR.")
class BinaryArithmeticExpression extends BinaryExpression {
BinaryArithmeticOperator operator
}
Class ComparisonExpression
Representation for comparison expressions of pattern 'A [compOp] B', where [compOp] is EQUALS, NOT_EQUALS, LESS_THAN, GREATER_THAN, LESS_EQ or GREATER_EQ.
Extends: BinaryExpression, ExplicitlyTyped
Attributes:
- operator : ComparisonOperator
@GenModel(documentation="Representation for comparison expressions of pattern 'A [compOp] B',
where [compOp] is EQUALS, NOT_EQUALS, LESS_THAN, GREATER_THAN, LESS_EQ or GREATER_EQ.")
class ComparisonExpression extends BinaryExpression, ExplicitlyTyped {
ComparisonOperator operator
}
Class UnaryLogicExpression
Representation for logical expressions of pattern '[logicOp] A', where [logicOp] is NEG. Can only be used with BoolType arguments.
Extends: UnaryExpression
Attributes:
- operator : UnaryLogicOperator
@GenModel(documentation="Representation for logical expressions of pattern '[logicOp] A',
where [logicOp] is NEG. Can only be used with {@link BoolType} arguments.")
class UnaryLogicExpression extends UnaryExpression {
UnaryLogicOperator operator
}
Class BinaryLogicExpression
Representation for logical expressions of pattern 'A [logicOp] B', where [logicOp] is AND, OR, XOR or IMPLIES. Can only be used with BoolType arguments.
Extends: BinaryExpression
Attributes:
- operator : BinaryLogicOperator
Operations:
- getType() : Type
- Binary logic expressions have to have operands of BoolType, but they can be different with regard to the temporal attribute. If any of them is temporal, that type will be returned. If any of the operands are of unknown type, the result is that UnknownType instance.
@GenModel(documentation="Representation for logical expressions of pattern 'A [logicOp] B',
where [logicOp] is AND, OR, XOR or IMPLIES. Can only be used with {@link BoolType} arguments.")
class BinaryLogicExpression extends BinaryExpression {
BinaryLogicOperator operator
@GenModel(documentation="Binary logic expressions have to have operands of BoolType, but they can be
different with regard to the temporal attribute. If any of them is temporal, that type will be
returned. If any of the operands are of unknown type, the result is that UnknownType instance.")
op Type getType() {
val leftType = leftOperand.^type
if (leftType instanceof UnknownType) {
return leftType;
}
val rightType = rightOperand.^type
if (rightType instanceof UnknownType) {
return rightType
}
if (leftType instanceof BoolType && rightType instanceof BoolType) {
return leftType;
} else if ((leftType instanceof TemporalBoolType && rightType instanceof TemporalBoolType)) {
return if (rightType instanceof BoolType) leftType else rightType;
} else
throw new IllegalStateException("Invalid types for operands of binary boolean expression.")
}
}
Class UnaryCtlExpression
Representation for CTL expressions of pattern '[ctlOp] A', where [ctlOp] is AX, AF, AG, EX, EF or EG.
Extends: UnaryExpression, ExplicitlyTyped
Attributes:
- operator : UnaryCtlOperator
@GenModel(documentation="Representation for CTL expressions of pattern '[ctlOp] A',
where [ctlOp] is AX, AF, AG, EX, EF or EG.")
class UnaryCtlExpression extends UnaryExpression, ExplicitlyTyped {
UnaryCtlOperator operator
}
Class BinaryCtlExpression
Representation for CTL expressions of pattern 'A [ctlOp] B', where [ctlOp] is AU or EU.
Extends: BinaryExpression, ExplicitlyTyped
Attributes:
- operator : BinaryCtlOperator
@GenModel(documentation="Representation for CTL expressions of pattern 'A [ctlOp] B',
where [ctlOp] is AU or EU.")
class BinaryCtlExpression extends BinaryExpression, ExplicitlyTyped {
BinaryCtlOperator operator
}
Class UnaryLtlExpression
Representation for LTL expressions of pattern '[ltlOp] A', where [ltlOp] is X, F, G.
Extends: UnaryExpression, ExplicitlyTyped
Attributes:
- operator : UnaryLtlOperator
@GenModel(documentation="Representation for LTL expressions of pattern '[ltlOp] A',
where [ltlOp] is X, F, G.")
class UnaryLtlExpression extends UnaryExpression, ExplicitlyTyped {
UnaryLtlOperator operator
}
Class BinaryLtlExpression
Representation for LTL expressions of pattern 'A [ltlOp] B', where [ltlOp] is U or R.
Extends: BinaryExpression, ExplicitlyTyped
Attributes:
- operator : BinaryLtlOperator
@GenModel(documentation="Representation for LTL expressions of pattern 'A [ltlOp] B',
where [ltlOp] is U or R.")
class BinaryLtlExpression extends BinaryExpression, ExplicitlyTyped {
BinaryLtlOperator operator
}
Class TypeConversion
Representation for explicit type cast expressions. The type specified though ExplicitlyTyped is the target type.
Extends: UnaryExpression, ExplicitlyTyped
@GenModel(documentation="Representation for explicit type cast expressions. The type specified though
ExplicitlyTyped is the target type.")
class TypeConversion extends UnaryExpression, ExplicitlyTyped {
}
Class UninterpretedFunction
Representation for uninterpreted n-ary functions.
Extends: NaryExpression, ExplicitlyTyped
Attributes:
- symbol [1..1]:
EString
@GenModel(documentation="Representation for uninterpreted n-ary functions.")
class UninterpretedFunction extends NaryExpression, ExplicitlyTyped {
String [1] symbol
}
Class LibraryFunction
Representation for interpreted n-ary library functions.
Extends: NaryExpression, ExplicitlyTyped
Attributes:
- function : LibraryFunctions
@GenModel(documentation="Representation for interpreted n-ary library functions.")
class LibraryFunction extends NaryExpression, ExplicitlyTyped {
LibraryFunctions function
}
Class EndOfCycle
Predicate that is true if and only if the currently active location represents the end of the cyclic execution.
Extends: Expression, ExplicitlyTyped
@GenModel(documentation="Predicate that is true if and only if the currently active location represents the end of the cyclic execution.")
class EndOfCycle extends Expression, ExplicitlyTyped { }
Class BeginningOfCycle
Predicate that is true if and only if the currently active location represents the beginning of the cyclic execution.
Extends: Expression, ExplicitlyTyped
@GenModel(documentation="Predicate that is true if and only if the currently active location represents the beginning of the cyclic execution.")
class BeginningOfCycle extends Expression, ExplicitlyTyped {
}
Class IntLiteral
Representation for an integer literal value.
Extends: Literal
Attributes:
- value :
ELong
- Modifiers: Unsettable
@GenModel(documentation="Representation for an integer literal value.")
class IntLiteral extends Literal {
unsettable long value
}
Class FloatLiteral
Representation for a float literal value.
Extends: Literal
Attributes:
- value :
EDouble
- Modifiers: Unsettable
@GenModel(documentation="Representation for a float literal value.")
class FloatLiteral extends Literal {
unsettable double value
}
Class BoolLiteral
Representation for a boolean literal value.
Extends: Literal
Attributes:
- value :
EBoolean
- Modifiers: Unsettable
@GenModel(documentation="Representation for a boolean literal value.")
class BoolLiteral extends Literal {
unsettable boolean value
}
Class StringLiteral
Representation for a string literal value.
Extends: Literal
Attributes:
- value :
EString
- Modifiers: Unsettable
@GenModel(documentation="Representation for a string literal value.")
class StringLiteral extends Literal {
unsettable String value
}
Enum FloatWidth
Represents the allowed float widths. Literal and value is set accordingly.
Literals:
B16
(16) = 16B32
(32) = 32B64
(64) = 64
@GenModel(documentation="Represents the allowed float widths. Literal and value is set accordingly.")
enum FloatWidth {
B16 as "16" = 16,
B32 as "32" = 32,
B64 as "64" = 64
}
Enum UnaryArithmeticOperator
Representation of supported unary arithmetic operators.
Literals:
MINUS
BITWISE_NOT
@GenModel(documentation="Representation of supported unary arithmetic operators.")
enum UnaryArithmeticOperator {
MINUS, BITWISE_NOT
}
Enum BinaryArithmeticOperator
Representation of supported binary arithmetic operators. They can only be used on IntType and FloatType arguments. Additional restrictions apply.
Literals:
PLUS
: Addition operator.MINUS
: Subtraction operator.MULTIPLICATION
: Multiplication operator.DIVISION
: Division operator. Can only be used on FloatType arguments.MODULO
: Remainder operator. Produces the remainder after the quotient of its operands rounded toward 0. The result value is such that(a INTEGER_DIVISION b) MULTIPLICATION b + (a MODULO b)
The result is negative iff the left argument is negative. This semantics coincides with the Java semantics of remainder (%
) operator.INTEGER_DIVISION
: Integer division operator. Produces the quotient of its operands, rounded toward 0. The result is negative iff the divident is negative. Examples:5 MOD 3 = 5 MOD (-3) = 2
,(-5) MOD 3 = (-5) MOD (-3) = -2
. This semantics coincides with the Java semantics of division (/
) operator.POWER
: Power operator. Produces the left operand to the power of the right operand.BITSHIFT
: Bit shift operator. Shifts the left operand's bits towards the least significant bit by the amount specified by the right operand, if the right operand is positive. 0s are shifted in. Can only be used on IntType arguments.BITROTATE
: Bit rotation operator. Shifts the left operand's bits towards the least significant bit by the amount specified by the right operand, if the right operand is positive. The values shifted out on one side are shifted in from the other side. Can only be used on IntType arguments.BITWISE_OR
: Bitwise OR operation. Can only be used on IntType arguments.BITWISE_AND
: Bitwise AND operation. Can only be used on IntType arguments.BITWISE_XOR
: Bitwise XOR operation. Can only be used on IntType arguments.
@GenModel(documentation="Representation of supported binary arithmetic operators. They can only be used on {@link IntType} and {@link FloatType} arguments. Additional restrictions apply.")
enum BinaryArithmeticOperator {
@GenModel(documentation="Addition operator.")
PLUS,
@GenModel(documentation="Subtraction operator.")
MINUS,
@GenModel(documentation="Multiplication operator.")
MULTIPLICATION,
@GenModel(documentation="Division operator. Can only be used on {@link FloatType} arguments.")
DIVISION,
@GenModel(documentation="Remainder operator. Produces the remainder after the quotient of its operands rounded toward 0. The result value is such that {@code (a INTEGER_DIVISION b) MULTIPLICATION b + (a MODULO b)} The result is negative iff the left argument is negative. This semantics coincides with the Java semantics of remainder ({@code %}) operator.")
MODULO,
@GenModel(documentation="Integer division operator. Produces the quotient of its operands, rounded toward 0. The result is negative iff the divident is negative. Examples: {@code 5 MOD 3 = 5 MOD (-3) = 2}, {@code (-5) MOD 3 = (-5) MOD (-3) = -2}. This semantics coincides with the Java semantics of division ({@code /}) operator.")
INTEGER_DIVISION,
@GenModel(documentation="Power operator. Produces the left operand to the power of the right operand.")
POWER,
@GenModel(documentation="Bit shift operator. Shifts the left operand's bits towards the least significant bit by the amount specified by the right operand, if the right operand is positive. 0s are shifted in. Can only be used on {@link IntType} arguments.")
BITSHIFT,
@GenModel(documentation="Bit rotation operator. Shifts the left operand's bits towards the least significant bit by the amount specified by the right operand, if the right operand is positive. The values shifted out on one side are shifted in from the other side. Can only be used on {@link IntType} arguments.")
BITROTATE,
@GenModel(documentation="Bitwise OR operation. Can only be used on {@link IntType} arguments.")
BITWISE_OR,
@GenModel(documentation="Bitwise AND operation. Can only be used on {@link IntType} arguments.")
BITWISE_AND,
@GenModel(documentation="Bitwise XOR operation. Can only be used on {@link IntType} arguments.")
BITWISE_XOR
}
Enum ComparisonOperator
Representation of supported (binary) comparison operators.
Literals:
EQUALS
NOT_EQUALS
LESS_THAN
GREATER_THAN
LESS_EQ
GREATER_EQ
@GenModel(documentation="Representation of supported (binary) comparison operators.")
enum ComparisonOperator {
EQUALS,
NOT_EQUALS,
LESS_THAN,
GREATER_THAN,
LESS_EQ,
GREATER_EQ
}
Enum UnaryLogicOperator
Representation of supported unary logic operators.
Literals:
NEG
@GenModel(documentation="Representation of supported unary logic operators.")
enum UnaryLogicOperator {
NEG
}
Enum BinaryLogicOperator
Representation of supported binary logic operators. Can only be used on BoolType arguments.
Literals:
AND
OR
XOR
IMPLIES
@GenModel(documentation="Representation of supported binary logic operators. Can only be used on {@link BoolType} arguments.")
enum BinaryLogicOperator {
AND,
OR,
XOR,
IMPLIES }
Enum UnaryCtlOperator
Representation of supported unary CTL operators.
Literals:
AX
AF
AG
EX
EF
EG
@GenModel(documentation="Representation of supported unary CTL operators.")
enum UnaryCtlOperator {
AX,
AF,
AG,
EX,
EF,
EG
}
Enum BinaryCtlOperator
Representation of supported binary CTL operators.
Literals:
AU
EU
@GenModel(documentation="Representation of supported binary CTL operators.")
enum BinaryCtlOperator {
AU,
EU
}
Enum UnaryLtlOperator
Representation of supported unary LTL operators.
Literals:
X
F
G
@GenModel(documentation="Representation of supported unary LTL operators.")
enum UnaryLtlOperator {
X,
F,
G
}
Enum BinaryLtlOperator
Representation of supported binary LTL operators.
Literals:
U
R
@GenModel(documentation="Representation of supported binary LTL operators.")
enum BinaryLtlOperator {
U,
R }
Enum LibraryFunctions
Representation of supported library functions.
Literals:
SIN
: Sine of an angle specified as a radian measure. Takes one FloatType operand. Its type is the same as its operand's.COS
: Cosine of an angle specified as a radian measure. Takes one FloatType operand. Its type is the same as its operand's.TAN
: Tangent of an angle specified as a radian measure. Takes one FloatType operand. Its type is the same as its operand's.ASIN
: Arc sine. The result angle is specified as a radian measure. Takes one FloatType operand. Its type is the same as its operand's.ACOS
: Arc cosine. The result angle is specified as a radian measure. Takes one FloatType operand. Its type is the same as its operand's.ATAN
: Arc tangent. The result angle is specified as a radian measure. Takes one FloatType operand. Its type is the same as its operand's.SQRT
: Square root. Takes one FloatType operand. Its type is the same as its operand's.EXP
: Exponent of the given value (e^argument). Takes one FloatType operand. Its type is the same as its operand's.LN
: Natural logarithm. Takes one FloatType operand. Its type is the same as its operand's.LOG
: 10-base logarithm. Takes one FloatType operand. Its type is the same as its operand's.
@GenModel(documentation="Representation of supported library functions.")
enum LibraryFunctions {
@GenModel(documentation="Sine of an angle specified as a radian measure. Takes one FloatType operand. Its type is the same as its operand's.")
SIN,
@GenModel(documentation="Cosine of an angle specified as a radian measure. Takes one FloatType operand. Its type is the same as its operand's.")
COS,
@GenModel(documentation="Tangent of an angle specified as a radian measure. Takes one FloatType operand. Its type is the same as its operand's.")
TAN,
@GenModel(documentation="Arc sine. The result angle is specified as a radian measure. Takes one FloatType operand. Its type is the same as its operand's.")
ASIN,
@GenModel(documentation="Arc cosine. The result angle is specified as a radian measure. Takes one FloatType operand. Its type is the same as its operand's.")
ACOS,
@GenModel(documentation="Arc tangent. The result angle is specified as a radian measure. Takes one FloatType operand. Its type is the same as its operand's.")
ATAN,
@GenModel(documentation="Square root. Takes one FloatType operand. Its type is the same as its operand's.")
SQRT,
@GenModel(documentation="Exponent of the given value (e^argument). Takes one FloatType operand. Its type is the same as its operand's.")
EXP,
@GenModel(documentation="Natural logarithm. Takes one FloatType operand. Its type is the same as its operand's.")
LN,
@GenModel(documentation="10-base logarithm. Takes one FloatType operand. Its type is the same as its operand's.")
LOG
}