CfaInstance.xcore metamodel description

Table of contents

Package cern.plcverif.base.models.cfa.cfainstance

Class FullyQualifiedName

Class to represent a fully qualified name, composed of segments that should be unique in their scope.

Extends: EObject

Attributes:

  • identifiers [1..*]: EString
    • The sequence of segments or identifiers constituting the fully qualified name.

Operations:

  • toString() : EString
@GenModel(documentation="Class to represent a fully qualified name, composed of segments that should be unique in their scope.")
class FullyQualifiedName {
    @GenModel(documentation="The sequence of segments or identifiers constituting the fully qualified name.")
    String [1..*] identifiers
            op String toString() {
        return String.join("/", identifiers)
    }
}

Abstract class AbstractVariable

Represents a variable or array of the CFA. Note that variables are unique in the model, referencing them is possible via AbstractVariableRef instances, which may be copied. This element can be frozen (see Freezable).

Extends: ExplicitlyTyped (unresolved), NamedElement (unresolved), Freezable (unresolved), Annotable (unresolved)

References:

@GenModel(documentation="Represents a variable or array of the CFA. Note that variables are unique in the model, referencing
    them is possible via AbstractVariableRef instances, which may be copied. This element can be frozen (see Freezable).")
abstract class AbstractVariable extends ExplicitlyTyped, NamedElement, Freezable, Annotable {
    @GenModel(documentation="The CFA network instance containing this variable.")
    container CfaNetworkInstance [1] ^container opposite variables 
    @GenModel(documentation="The fully qualified name of this variable.")
    contains FullyQualifiedName [1] fqn
    @GenModel(documentation="Annotations of the variable. Used for code generation and traceability.")
    contains VariableAnnotation[*] annotations opposite parentVariable
}

Class Variable

Represents an elementary variable of the CFA. Note that variables are unique in the model, referencing them is possible via VariableRef instances, which may be copied. This element can be frozen (see Freezable).

Extends: AbstractVariable

References:

  • initialValue [1..1]: InitialValue (unresolved)
    • The initial value of this variable.
    • Containment: contains

Operations:

  • toString() : EString
@GenModel(documentation="Represents an elementary variable of the CFA. Note that variables are unique in the model, 
    referencing them is possible via VariableRef instances, which may be copied. This element can be frozen (see Freezable).")
class Variable extends AbstractVariable {
    @GenModel(documentation="The initial value of this variable.")
    contains InitialValue [1] initialValue
            op String toString() {
        return fqn.toString()
    }
}

Class ArrayVariable

Represents a (multidimensional) array variable of the CFA. Note that variables are unique in the model, referencing them is possible via ArrayElementRef instances, which may be copied. The type of an ArrayVariable is always the type of its elements. This element can be frozen (see Freezable).

Extends: AbstractVariable

References:

  • dimensions [1..*]: ArrayDimension (unresolved)
    • The dimension(s) of this array.
    • Containment: contains
  • initialValues [0..*]: ArrayElementInitialValue
    • The initial values of array elements. Use cern.plcverif.base.models.cfa.utils.ArrayInitialValueHelper to read and process the initial values of multidimensional arrays
    • Containment: contains

Operations:

  • toString() : EString
@GenModel(documentation="Represents a (multidimensional) array variable of the CFA. Note that variables are unique in the 
    model, referencing them is possible via ArrayElementRef instances, which may be copied. The type of an ArrayVariable
    is always the type of its elements. This element can be frozen (see Freezable).")
class ArrayVariable extends AbstractVariable {
    @GenModel(documentation="The dimension(s) of this array.")
    contains ArrayDimension [1..*] dimensions
    @GenModel(documentation="The initial values of array elements. Use cern.plcverif.base.models.cfa.utils.ArrayInitialValueHelper
        to read and process the initial values of multidimensional arrays")
    contains ArrayElementInitialValue [*] initialValues
            op String toString() {
        var String ret = fqn.toString() + "[";
        for (dimension : dimensions) {
            if (!ret.endsWith("[")) {
                ret += ","
            }
            ret += dimension.toString()
        }
        return ret + "]";
    }
}

Class ArrayElementInitialValue

Represents the initialization of an array element.

Extends: EObject

References:

  • indices [0..*]: Expression (unresolved)
    • The indices of the element to initialize.
    • Containment: contains
  • initialValue [1..1]: InitialValue (unresolved)
    • The initial value of the identified element.
    • Containment: contains
@GenModel(documentation="Represents the initialization of an array element.")
class ArrayElementInitialValue {
    @GenModel(documentation="The indices of the element to initialize.")
    contains Expression [*] indices
    @GenModel(documentation="The initial value of the identified element.")
    contains InitialValue [1] initialValue 
}

Abstract class AbstractVariableRef

Represents a reference to a variable or an element of an array.

Extends: LeftValue (unresolved), Freezable (unresolved)

Operations:

  • getVariable() : AbstractVariable
    • Returns the referenced variable.
  • getType() : Type (unresolved)
    • The type of an AbstractVariableRef is always the type of the referred variable.
@GenModel(documentation="Represents a reference to a variable or an element of an array.")
abstract class AbstractVariableRef extends LeftValue, Freezable {
    @GenModel(documentation="Returns the referenced variable.")
    op AbstractVariable getVariable() {
                        throw new AbstractMethodError();
    }
    @GenModel(documentation="The type of an AbstractVariableRef is always the type of the referred variable.")
    op Type getType() {
        return variable.^type
    }
}

Class VariableRef

Represents a reference to a simple variable.

Extends: AbstractVariableRef

References:

  • variable : Variable
    • The referenced variable.
    • Containment: refers

Operations:

  • toString() : EString
@GenModel(documentation="Represents a reference to a simple variable.")
class VariableRef extends AbstractVariableRef {
    @GenModel(documentation="The referenced variable.")
    refers Variable variable
            op String toString() {
        return variable.fqn.toString()
    }
}

Class ArrayElementRef

Represents a reference to an array element.

Extends: AbstractVariableRef

References:

  • variable : ArrayVariable
    • The referenced array.
    • Containment: refers
  • indices [1..*]: Expression (unresolved)
    • The indices identifying the array element. The array indices must have signed 16-bit integer types.
    • Containment: contains

Operations:

  • toString() : EString
@GenModel(documentation="Represents a reference to an array element.")
class ArrayElementRef extends AbstractVariableRef {
    @GenModel(documentation="The referenced array.")
    refers ArrayVariable variable
    @GenModel(documentation="The indices identifying the array element. The array indices must have signed 16-bit integer types.")
    contains Expression [1..*] indices
            op String toString() {
        var String ret = variable.fqn.toString() + "[";
        for (index : indices) {
            if (!ret.endsWith("[")) {
                ret += ","
            }
            ret += index.toString()
        }
        return ret + "]";
    }
}

Class CfaNetworkInstance

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

Extends: CfaNetworkBase (unresolved)

References:

@GenModel(documentation="Class to represent an instance of a network of control flow automata (CFA).")
class CfaNetworkInstance extends CfaNetworkBase {
    contains AbstractVariable [*] variables opposite ^container
    @GenModel(documentation="Automata in the network.")
    contains AutomatonInstance[] automata opposite ^container
    @GenModel(documentation="Automaton which starts the execution.")
    refers AutomatonInstance mainAutomaton
}

Class AutomatonInstance

Class to represent an instance of a control flow automaton.

Extends: AutomatonBase (unresolved)

References:

@GenModel(documentation="Class to represent an instance of a control flow automaton.")
class AutomatonInstance extends AutomatonBase {
    @GenModel(documentation="Automaton system which this automaton belongs to.")
    container CfaNetworkInstance [1] ^container opposite automata
}

Class AssignmentTransition

Class to represent a (potentially guarded) CFA instance transition with assignment.

Extends: Transition (unresolved)

References:

  • assignments [0..*]: VariableAssignment
    • Variable assignments to perform when the transition fires.
    • Containment: contains
@GenModel(documentation="Class to represent a (potentially guarded) CFA instance transition with assignment.")
class AssignmentTransition extends Transition {
    @GenModel(documentation="Variable assignments to perform when the transition fires.")
    contains VariableAssignment[] assignments
}

Class CallTransition

Class to represent a (potentially guarded) CFA instance transition with automaton call. Semantically, this is equivalent to copying the called automata here, replacing this transition.

Extends: Transition (unresolved)

References:

  • calls [0..*]: Call
    • The calls performed upon transition. If it contains multiple calls, it is a parallel composition. In that case, all input assignments are performed before any of the executions and all output assignments are performed after all executions.
    • Containment: contains
    • Opposite: Call.parentTransition
@GenModel(documentation="Class to represent a (potentially guarded) CFA instance transition with automaton call. 
    Semantically, this is equivalent to copying the called automata here, replacing this transition.")
class CallTransition extends Transition {
    @GenModel(documentation="The calls performed upon transition. If it contains multiple calls, it is a parallel composition.
        In that case, all input assignments are performed before any of the executions and all output assignments are 
        performed after all executions.")
    contains Call[] calls opposite parentTransition
}

Class Call

Class to represent a CFA automaton instance call.

Extends: EObject

References:

  • parentTransition [1..1]: CallTransition
    • Transition which contains the call.
    • Containment: container
    • Opposite: CallTransition.calls
  • calledAutomaton [1..1]: AutomatonInstance
    • Automaton to be executed.
    • Containment: refers
  • inputAssignments [0..*]: VariableAssignment
    • Input assignments of the called automaton. Performed in arbitrary order, before executing 'calledAutomaton'.
    • Containment: contains
  • outputAssignments [0..*]: VariableAssignment
    • Output assignments of the called automaton. Performed in arbitrary order, after executing 'calledAutomaton'.
    • Containment: contains
@GenModel(documentation="Class to represent a CFA automaton instance call.")
class Call {
    @GenModel(documentation="Transition which contains the call.")
    container CallTransition [1] parentTransition opposite calls
    @GenModel(documentation="Automaton to be executed.")
    refers AutomatonInstance [1] calledAutomaton
    @GenModel(documentation="Input assignments of the called automaton. Performed in arbitrary order, before executing 
        'calledAutomaton'.")
    contains VariableAssignment[] inputAssignments
    @GenModel(documentation="Output assignments of the called automaton. Performed in arbitrary order, after executing 
        'calledAutomaton'.")
    contains VariableAssignment[] outputAssignments
}

Class VariableAssignment

Class to represent a variable assignment in the CFA instance.

Extends: Freezable (unresolved)

References:

  • leftValue [1..1]: AbstractVariableRef
    • Containment: contains
  • rightValue [1..1]: Expression (unresolved)
    • Containment: contains
@GenModel(documentation="Class to represent a variable assignment in the CFA instance.")
class VariableAssignment extends Freezable {
    contains AbstractVariableRef [1] leftValue
    contains Expression [1] rightValue
}

Abstract class VariableAnnotation

Abstract superclass for variable annotations.

Extends: Annotation (unresolved)

References:

@GenModel(documentation="Abstract superclass for variable annotations.")
abstract class VariableAnnotation extends Annotation {
    container AbstractVariable [1] parentVariable opposite annotations
}

Class DirectionVariableAnnotation

Variable annotation to indicate mode in which the annotated variable should be interpreted or used.

Extends: VariableAnnotation

Attributes:

  • direction [1..1]: DataDirection (unresolved)
@GenModel(documentation="Variable annotation to indicate mode in which the annotated variable should be interpreted or used.")
class DirectionVariableAnnotation extends VariableAnnotation {
    DataDirection [1] direction
}

Class OriginalDataTypeVariableAnnotation

Variable annotation to trace the original data type of the variable in the PLC code.

Extends: VariableAnnotation

Attributes:

  • plcDataType [1..1]: EString
@GenModel(documentation="Variable annotation to trace the original data type of the variable in the PLC code.")
class OriginalDataTypeVariableAnnotation extends VariableAnnotation {
    String [1] plcDataType
}

Class ReturnValueVariableAnnotation

Variable annotation to indicate that the annotated variable is used to store return values of an automaton.

Extends: VariableAnnotation

@GenModel(documentation="Variable annotation to indicate that the annotated variable is used to store return values of an automaton.")
class ReturnValueVariableAnnotation extends VariableAnnotation {
}

Class InternalGeneratedVariableAnnotation

Variable annotation to indicate that the annotated variable was created for internal purposes and it does not correspond to any of the source program's fields/variables.

Extends: VariableAnnotation

@GenModel(documentation="Variable annotation to indicate that the annotated variable was created for internal purposes and it does not correspond to any of the source program's fields/variables.")
class InternalGeneratedVariableAnnotation extends VariableAnnotation {
}

Class ForLoopLocationAnnotation

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

Extends: LoopLocationAnnotation (unresolved)

References:

  • loopVariable : AbstractVariableRef
    • Containment: contains
  • loopVariableInit : Transition (unresolved)
    • Containment: refers
  • loopVariableIncrement : Transition (unresolved)
    • Containment: refers
@GenModel(documentation="Location annotation to represent a FOR loop statement that starts at the given location.")
class ForLoopLocationAnnotation extends LoopLocationAnnotation {
    contains AbstractVariableRef loopVariable
    refers Transition loopVariableInit
    refers Transition loopVariableIncrement
}

results matching ""

    No results matching ""