CfaInstance.xcore metamodel description
Table of contents
- AbstractVariable
- AbstractVariableRef
- ArrayElementInitialValue
- ArrayElementRef
- ArrayVariable
- AssignmentTransition
- AutomatonInstance
- Call
- CallTransition
- CfaNetworkInstance
- DirectionVariableAnnotation
- ForLoopLocationAnnotation
- FullyQualifiedName
- InternalGeneratedVariableAnnotation
- OriginalDataTypeVariableAnnotation
- ReturnValueVariableAnnotation
- Variable
- VariableAnnotation
- VariableAssignment
- VariableRef
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:
- container [1..1]: CfaNetworkInstance
- The CFA network instance containing this variable.
- Containment: container
- Opposite: CfaNetworkInstance.
variables
- fqn [1..1]: FullyQualifiedName
- The fully qualified name of this variable.
- Containment: contains
- annotations [0..*]: VariableAnnotation
- Annotations of the variable. Used for code generation and traceability.
- Containment: contains
- Opposite: VariableAnnotation.
parentVariable
@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:
- variables [0..*]: AbstractVariable
- Containment: contains
- Opposite: AbstractVariable.
container
- automata [0..*]: AutomatonInstance
- Automata in the network.
- Containment: contains
- Opposite: AutomatonInstance.
container
- mainAutomaton : AutomatonInstance
- Automaton which starts the execution.
- Containment: refers
@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:
- container [1..1]: CfaNetworkInstance
- Automaton system which this automaton belongs to.
- Containment: container
- Opposite: CfaNetworkInstance.
automata
@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:
- parentVariable [1..1]: AbstractVariable
- Containment: container
- Opposite: AbstractVariable.
annotations
@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
}