CfaBase.xcore metamodel description

Table of contents

Package cern.plcverif.base.models.cfa.cfabase

Abstract class NamedElement

Abstract superclass for elements with mandatory names.

Extends: EObject

Attributes:

  • name [1..1]: EString
    • Name of the element (unique identifier in the scope of the containing element, used as FQN segment).
  • displayName [1..1]: EString
    • Name of the element (used for human-readable representation).
@GenModel(documentation="Abstract superclass for elements with mandatory names.")
abstract class NamedElement {
                @GenModel(documentation="Name of the element (unique identifier in the scope of the 
        containing element, used as FQN segment).")
    String [1] name
    @GenModel(documentation="Name of the element (used for human-readable representation).")
    String [1] displayName
}

Abstract class Freezable

Abstract superclass for elements that can be frozen. Freezing an element delivers the message that it should not be modified or removed during model transformations.

Extends: EObject

Attributes:

  • frozen : EBoolean
@GenModel(documentation="Abstract superclass for elements that can be frozen. Freezing an element 
    delivers the message that it should not be modified or removed during model transformations.")
abstract class Freezable {
    boolean frozen
        }

Abstract class CfaNetworkBase

Class to represent a network of control flow automata (CFA).

Extends: NamedElement

Operations:

@GenModel(documentation="Class to represent a network of control flow automata (CFA).")
abstract class CfaNetworkBase extends NamedElement {
    op AutomatonBase getMainAutomaton() { throw new UnsupportedOperationException("Must be overridden by the subclasses."); }
}

Abstract class AutomatonBase

Class to represent a control flow automaton.

Extends: NamedElement, Annotable

References:

  • locations [0..*]: Location
    • Locations defined in the automaton.
    • Containment: contains
    • Opposite: Location.parentAutomaton
  • initialLocation [1..1]: Location
    • The initial location of the automaton.
    • Containment: refers
  • endLocation [1..1]: Location
    • The final location of the automaton.
    • Containment: refers
  • transitions [0..*]: Transition
    • Transitions contained in the automaton.
    • Containment: contains
    • Opposite: Transition.parentAutomaton
  • annotations [0..*]: AutomatonAnnotation
    • Annotations of the automaton. Used for code generation and traceability.
    • Containment: contains
    • Opposite: AutomatonAnnotation.parentAutomaton

Operations:

  • getContainer() : CfaNetworkBase
    • Returns the CFA network containing this automaton. Should be realized in subclasses.
@GenModel(documentation="Class to represent a control flow automaton.")
abstract class AutomatonBase extends NamedElement, Annotable {
    @GenModel(documentation="Returns the CFA network containing this automaton. Should be realized in subclasses.")
    op CfaNetworkBase getContainer() { throw new UnsupportedOperationException("Must be overridden by the subclasses."); }
    @GenModel(documentation="Locations defined in the automaton.")
    contains Location[*] locations opposite parentAutomaton
        @GenModel(documentation="The initial location of the automaton.")
    refers Location [1] initialLocation
        @GenModel(documentation="The final location of the automaton.")
    refers Location [1] endLocation
    @GenModel(documentation="Transitions contained in the automaton.")
    contains Transition[*] transitions opposite parentAutomaton
    @GenModel(documentation="Annotations of the automaton. Used for code generation and traceability.")
    contains AutomatonAnnotation[*] annotations opposite parentAutomaton 
}

Class Location

Class to represent a CFA control location.

Extends: NamedElement, Freezable, Annotable

References:

  • parentAutomaton [1..1]: AutomatonBase
    • Automaton which contains the location.
    • Containment: container
    • Opposite: AutomatonBase.locations
  • incoming [0..*]: Transition
    • Incoming transitions of the location.
    • Containment: refers
    • Opposite: Transition.target
  • outgoing [0..*]: Transition
    • Outgoing transitions of the location.
    • Containment: refers
    • Opposite: Transition.source
  • annotations [0..*]: LocationAnnotation
    • Annotations of the location. Used for code generation and traceability.
    • Containment: contains
    • Opposite: LocationAnnotation.parentLocation
@GenModel(documentation="Class to represent a CFA control location.")
class Location extends NamedElement, Freezable, Annotable {
    @GenModel(documentation="Automaton which contains the location.")
    container AutomatonBase [1] parentAutomaton opposite locations
    @GenModel(documentation="Incoming transitions of the location.")
    refers Transition[*] incoming opposite target
    @GenModel(documentation="Outgoing transitions of the location.")
    refers Transition[*] outgoing opposite source
    @GenModel(documentation="Annotations of the location. Used for code generation and traceability.")
    contains LocationAnnotation[*] annotations opposite parentLocation 
}

Abstract class Transition

Abstract superclass to represent a generic CFA transition. Subclasses are AssignmentTransition and CallTransition, each implemented for both CFA declarations and instances.

Extends: NamedElement, Freezable, Annotable

References:

  • parentAutomaton [1..1]: AutomatonBase
    • Automaton which contains the transition.
    • Containment: container
    • Opposite: AutomatonBase.transitions
  • source [1..1]: Location
    • Source location of the transition.
    • Containment: refers
    • Opposite: Location.outgoing
  • target [1..1]: Location
    • Target location of the transition.
    • Containment: refers
    • Opposite: Location.incoming
  • condition [1..1]: Expression (unresolved)
    • Condition of the transition.
    • Containment: contains
  • annotations [0..*]: TransitionAnnotation
    • Annotations of the transition. Used for code generation and traceability.
    • Containment: contains
    • Opposite: TransitionAnnotation.parentTransition
@GenModel(documentation="Abstract superclass to represent a generic CFA transition. Subclasses are 
    AssignmentTransition and CallTransition, each implemented for both CFA declarations and instances.")
abstract class Transition extends NamedElement, Freezable, Annotable {
    @GenModel(documentation="Automaton which contains the transition.")
    container AutomatonBase [1] parentAutomaton opposite transitions
    @GenModel(documentation="Source location of the transition.")
    refers Location [1] source opposite outgoing
    @GenModel(documentation="Target location of the transition.")
    refers Location [1] target opposite incoming
    @GenModel(documentation="Condition of the transition.")
    contains Expression [1] condition
    @GenModel(documentation="Annotations of the transition. Used for code generation and traceability.")
    contains TransitionAnnotation[*] annotations opposite parentTransition 
}

Class ElseExpression

Special expression to denote 'none of the conditions of the other outgoing transitions is true'. If this is the guard of the only transition leaving a location, it is equivalent to the 'true' literal.

Extends: Expression (unresolved), ExplicitlyTyped (unresolved)

@GenModel(documentation="Special expression to denote 'none of the conditions 
of the other outgoing transitions is true'. If this is the guard of the only 
transition leaving a location, it is equivalent to the 'true' literal.")
class ElseExpression extends Expression, ExplicitlyTyped {
}

Class ArrayDimension

Represents a dimension of an array type. A dimension may be undefined, that is, of unknown size, although this is not supported in most of the CFA transformation libraries. Array indices may be negative. The array indices are expected to be signed 16-bit integers.

Extends: EObject

Attributes:

  • defined : EBoolean
    • If true, de values of 'lowerBound' and 'upperBound' specify the smallest and largest index that can be used to index this dimension of the corresponding array. Otherwise the array can be indexed with any value or expression, because the size is assumed to be unknown or arbitrary.
  • lowerIndex : EInt
    • Inclusive lower bound for the index used for this dimension. May be negative. Should not be used if 'defined' is false.
    • Default value: -1
  • upperIndex : EInt
    • Inclusive upper bound for the index used for this dimension. May be negative. Should not be used if 'defined' is false.
    • Default value: -1

Operations:

  • getSize() : EInt
    • The number of elements in this dimension of the corresponding array. Throws an exception if called on an array of undefined size.
  • isValidIndex(index : ELong) : EBoolean
    • Returns true if the specified index may be used as an index in this dimension.
  • dimensionEquals(other : ArrayDimension) : EBoolean
    • Returns true if the specified dimension has the same features as the current one.
@GenModel(documentation="Represents a dimension of an array type. A dimension may be undefined, that is, of 
    unknown size, although this is not supported in most of the CFA transformation libraries. Array indices 
    may be negative. The array indices are expected to be signed 16-bit integers.")
class ArrayDimension {
    @GenModel(documentation="If true, de values of 'lowerBound' and 'upperBound' specify the smallest and largest 
        index that can be used to index this dimension of the corresponding array. Otherwise the array can be
        indexed with any value or expression, because the size is assumed to be unknown or arbitrary.")
    boolean defined
    @GenModel(documentation="Inclusive lower bound for the index used for this dimension. May be negative. 
        Should not be used if 'defined' is false.")
    int lowerIndex = "-1"
    @GenModel(documentation="Inclusive upper bound for the index used for this dimension. May be negative. 
        Should not be used if 'defined' is false.")
    int upperIndex = "-1"
    @GenModel(documentation="The number of elements in this dimension of the corresponding array. Throws an 
        exception if called on an array of undefined size.")
    op int getSize() {
        if (defined) {
            return upperIndex - lowerIndex + 1;
        }
        else {
            throw new InvalidUndefinedArrayOperation("Undefined arrays do not have a size.");
        }
    }
    @GenModel(documentation="Returns true if the specified index may be used as an index in this dimension.")
    op boolean isValidIndex(long index) {
        if (isDefined) {
            return index >= lowerIndex && index <= upperIndex;
        }
        else {
            return true;
        }
    }
    @GenModel(documentation="Returns true if the specified dimension has the same features as the current one.")
    op boolean dimensionEquals(ArrayDimension other) {
        return defined == other.defined && lowerIndex == other.lowerIndex && upperIndex == other.upperIndex;
    }
}

Class ArrayType

Represents an array type. Multidimensional arrays must be represented as arrays of arrays.

Extends: Type (unresolved)

References:

  • elementType [1..1]: Type (unresolved)
    • Containment: contains
  • dimension [1..1]: ArrayDimension
    • Containment: contains

Operations:

  • dataTypeEquals(other : Type (unresolved)) : EBoolean
    • Two array types are equal if they have the same dimensions and the same type of elements.
@GenModel(documentation="Represents an array type. Multidimensional arrays must be represented as arrays of arrays.")
class ArrayType extends Type {
    contains Type [1] elementType
    contains ArrayDimension [1] dimension 
    @GenModel(documentation="Two array types are equal if they have the same dimensions and the same type of elements.")
    op boolean dataTypeEquals(Type other) {
        if (other instanceof ArrayType) {
            return elementType.dataTypeEquals(other.elementType) && dimension.dimensionEquals(other.dimension)
        }
        return false
    }
}

Abstract class Annotation

Abstract superclass for any kind of annotations.

Extends: EObject

@GenModel(documentation="Abstract superclass for any kind of annotations.")
abstract class Annotation {}

Interface Annotable

Extends: EObject

Operations:

  • getAnnotations() : EEList
interface Annotable {
    op EEList<? extends Annotation> getAnnotations()
}

Abstract class AutomatonAnnotation

Abstract superclass for all automaton annotations.

Extends: Annotation

References:

@GenModel(documentation="Abstract superclass for all automaton annotations.")
abstract class AutomatonAnnotation extends Annotation {
    container AutomatonBase [1] parentAutomaton opposite annotations
}

Class BlockAutomatonAnnotation

Automaton annotation to represent a specific block in PLC code.

Extends: AutomatonAnnotation

Attributes:

  • blockType [0..1]: EString
  • name [1..1]: EString
  • stateful : EBoolean
    • Default value: true
@GenModel(documentation="Automaton annotation to represent a specific block in PLC code.")
class BlockAutomatonAnnotation extends AutomatonAnnotation {
    String [0..1] blockType
    String [1] name
    boolean stateful = "true"
}

Abstract class LocationAnnotation

Abstract superclass for all location annotations.

Extends: Annotation

References:

  • parentLocation [1..1]: Location
    • Containment: container
    • Opposite: Location.annotations
@GenModel(documentation="Abstract superclass for all location annotations.")
abstract class LocationAnnotation extends Annotation {
    container Location [1] parentLocation opposite annotations
}

Class IfLocationAnnotation

Location annotation to represent an IF statement that starts at the given location.

Extends: LocationAnnotation

References:

  • endsAt [1..1]: Location
    • The location where the two paths merge again.
    • Containment: refers
  • then [1..1]: Transition
    • The transition which is followed in case the condition is true.
    • Containment: refers
@GenModel(documentation="Location annotation to represent an IF statement that starts at the given location.")
class IfLocationAnnotation extends LocationAnnotation {
    @GenModel(documentation="The location where the two paths merge again.")    
    refers Location [1] endsAt
    @GenModel(documentation="The transition which is followed in case the condition is true.")
    refers Transition [1] then
}

Class SwitchLocationAnnotation

Location annotation to represent a SWITCH statement that starts at the given location.

Extends: LocationAnnotation

References:

  • endsAt : Location
    • The location where the paths of the cases merge again.
    • Containment: refers
  • cases [0..*]: CaseLocationAnnotation
    • The annotations marking the locations where the paths of each case start.
    • Containment: refers
    • Opposite: CaseLocationAnnotation.switchAnnotation
  • elseCase : CaseLocationAnnotation
    • The annotation marking the location where the path of the default or else case starts.
    • Containment: refers
  • selectionExpr : Expression (unresolved)
    • The selection expression used to choose the path of execution.
    • Containment: contains
@GenModel(documentation="Location annotation to represent a SWITCH statement that starts at the given location.")
class SwitchLocationAnnotation extends LocationAnnotation {
    @GenModel(documentation="The location where the paths of the cases merge again.")    
    refers Location endsAt
    @GenModel(documentation="The annotations marking the locations where the paths of each case start.")    
    refers CaseLocationAnnotation[] cases opposite switchAnnotation
    @GenModel(documentation="The annotation marking the location where the path of the default or else case starts.")
    refers CaseLocationAnnotation elseCase
    @GenModel(documentation="The selection expression used to choose the path of execution.")
    contains Expression selectionExpr
}

Class CaseLocationAnnotation

Location annotation to represent a CASE statement that starts at the given location.

Extends: LocationAnnotation

References:

@GenModel(documentation="Location annotation to represent a CASE statement that starts at the given location.")
class CaseLocationAnnotation extends LocationAnnotation {
    refers SwitchLocationAnnotation switchAnnotation opposite cases
}

Abstract class LoopLocationAnnotation

Location annotation to represent an abstract loop statement that starts at the given location.

Extends: LocationAnnotation

References:

  • loopBodyEntry [1..1]: Transition
    • The transition which transfers control from loop administration to the actual body.
    • Containment: refers
  • loopNextCycle [1..1]: Transition
    • The transition which transfers control from the loop body back to the beginning of the cycle.
    • Containment: refers
  • loopExit [1..1]: Transition
    • The transition which transfers control out of the loop.
    • Containment: refers
@GenModel(documentation="Location annotation to represent an abstract loop statement that starts at the given location.")
abstract class LoopLocationAnnotation extends LocationAnnotation {
    @GenModel(documentation="The transition which transfers control from loop administration to the actual body.")
    refers Transition [1] loopBodyEntry
    @GenModel(documentation="The transition which transfers control from the loop body back to the beginning of the cycle.")
    refers Transition [1] loopNextCycle
    @GenModel(documentation="The transition which transfers control out of the loop.")
    refers Transition [1] loopExit
}

Class WhileLoopLocationAnnotation

Location annotation to represent a WHILE loop statement that starts at the given location.

Extends: LoopLocationAnnotation

@GenModel(documentation="Location annotation to represent a WHILE loop statement that starts at the given location.")
class WhileLoopLocationAnnotation extends LoopLocationAnnotation {
}

Class RepeatLoopLocationAnnotation

Location annotation to represent a REPEAT loop statement that starts at the given location.

Extends: LoopLocationAnnotation

@GenModel(documentation="Location annotation to represent a REPEAT loop statement that starts at the given location.")
class RepeatLoopLocationAnnotation extends LoopLocationAnnotation {
}

Class LabelledLocationAnnotation

Location annotation to represent a labeled statement at the given location.

Extends: LocationAnnotation

Attributes:

  • labelName [1..1]: EString
@GenModel(documentation="Location annotation to represent a labeled statement at the given location.")
class LabelledLocationAnnotation extends LocationAnnotation {
    String [1] labelName
}

Class LineNumberAnnotation

Location annotation to represent the original line number corresponding to the location.

Extends: LocationAnnotation

Attributes:

  • fileName [1..1]: EString
    • Default value: unknown
  • lineNumber : EInt
@GenModel(documentation="Location annotation to represent the original line number corresponding to the location.")
class LineNumberAnnotation extends LocationAnnotation {
    String [1] fileName = "unknown"
    int lineNumber
}

Class AssertionAnnotation

Location annotation to represent an assertion, i.e., a Boolean expression that shall always be satisfied.

Extends: LocationAnnotation

Attributes:

  • name [0..1]: EString

References:

  • invariant [1..1]: Expression (unresolved)
    • Containment: contains
@GenModel(documentation="Location annotation to represent an assertion, i.e., a Boolean expression that shall always be satisfied.")
class AssertionAnnotation extends LocationAnnotation {
    contains Expression [1] invariant
    String [0..1] name }

Abstract class TransitionAnnotation

Abstract superclass for all transition annotations.

Extends: Annotation

References:

@GenModel(documentation="Abstract superclass for all transition annotations.")
abstract class TransitionAnnotation extends Annotation {
    container Transition [1] parentTransition opposite annotations
}

Class GotoTransitionAnnotation

Transition annotation to represent a GOTO statement that is represented by the given transition.

Extends: TransitionAnnotation

Attributes:

  • targetLabel [1..1]: EString
@GenModel(documentation="Transition annotation to represent a GOTO statement that is represented by the given transition.")
class GotoTransitionAnnotation extends TransitionAnnotation {
    String [1] targetLabel
}

Class ContinueTransitionAnnotation

Transition annotation to represent a CONTINUE statement that is represented by the given transition.

Extends: TransitionAnnotation

@GenModel(documentation="Transition annotation to represent a CONTINUE statement that is represented by the given transition.")
class ContinueTransitionAnnotation extends TransitionAnnotation {
}

Class ExitTransitionAnnotation

Transition annotation to represent a EXIT statement that is represented by the given transition.

Extends: TransitionAnnotation

@GenModel(documentation="Transition annotation to represent a EXIT statement that is represented by the given transition.")
class ExitTransitionAnnotation extends TransitionAnnotation {
}

Class BlockReturnTransitionAnnotation

Transition annotation to represent a RETURN statement that is represented by the given transition.

Extends: TransitionAnnotation

@GenModel(documentation="Transition annotation to represent a RETURN statement that is represented by the given transition.")
class BlockReturnTransitionAnnotation extends TransitionAnnotation {
}

Enum DataDirection

Represents the possible modes in which a field or variable should be interpreted or used. Used by DirectionFieldAnnotation and DirectionVariableAnnotation. INPUT and INOUT fields or variables are initialized nondeterministically in the main automaton, unless overridden by settings.

Literals:

  • INPUT
  • OUTPUT
  • INOUT
  • LOCAL
  • TEMP
  • PARAMETER 
@GenModel(documentation="Represents the possible modes in which a field or variable should be interpreted 
    or used. Used by DirectionFieldAnnotation and DirectionVariableAnnotation. INPUT and INOUT fields or
    variables are initialized nondeterministically in the main automaton, unless overridden by settings.")
enum DataDirection {
    INPUT, OUTPUT, INOUT, LOCAL, TEMP, PARAMETER
}

results matching ""

    No results matching ""