Expr.xcore metamodel description

Table of contents

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:

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:

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

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

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

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

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

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

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:

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

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

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

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

@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) = 16
  • B32 (32) = 32
  • B64 (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
}

results matching ""

    No results matching ""