CFA Instance

The CFA Instance metamodel defines a control-flow automata network at the level of instances. It defines global variables which are either elementary variables or arrays (with 1..n dimensions). All variables are accessible from any automaton instance. The automata contain locations and transitions. A transition can be assignment transition (containing 1..n variable assignments, with non-defined execution order) or call transition.

[info] Usage information

The CFA Instance metamodel is defined to make the CFA translation simpler to automata-based model checker backends by restricting the feature set of it.

CFA instance metamodel overview

The main concepts of the CFA instance metamodel are the following.

Automata structure.

• A network (CfaNetworkInstance) consists of one or more automaton instances, of which one is the so-called main automaton (CfaNetworkInstance.mainAutomaton). The initial location of this automaton will be the first active location. The network also contains all the variables available.
• An automaton instance (AutomatonInstance) contains transitions and locations.
• The transitions in the automaton instance can be assignment and call transitions. A transition can only fire if its source location is active and its guard (condition) is satisfied.
  • When an assignment transition fires, the attached (zero, one or many) variable assignments (VariableAssignment) will be performed.
  • When a call transition fires, the following steps are performed for each defined call (Call), in a non-defined order between the different calls:
    1. The input variable assignments (Call.inputAssignments) are performed,
    2. The callee automaton's initial location (initialLocation) will be active, with the callee context (calleeContext) defined in the call. The calleeContext is expected to be a reference to a field or array element with the callee's local data structure (AutomatonDeclaration.localDataStructure) as type.
    3. When the callee automaton reaches its end location (endLocation), the output variable assignments (Call.outputAssignments) are performed.
    4. If all calls of the call transition have finished, the active location will be the target location of the call transition (CallTransition.target).

Data handling.

• The variables (AbstractVariable) contained in the network can be atomic (single) variables or array variables.
  • A single variable (Variable) has one of the types defined in the expression metamodel (the CFA instance metamodel does not define any additional types, unlike the CFA declaration metamodel). It is mandatory to have initial values for the single variables.
  • An array variable (ArrayVariable) defines an array with one or more dimensions. Each dimension's range is defined by the corresponding ArrayDimension objects.
• Single variables can be referred by VariableRef. To refer to an element of an array variable, use the ArrayElementRef class. These two classes extend the abstract AbstractVariableRef class.

See more in the detailed metamodel documentation.

CFA instance inlining

Call transitions can be eliminated by inlining the calls (cern.plcverif.base.models.cfa.transformation.CallInliner) which will ensure that no call transition can be found in the automata network, furthermore there will be a single automaton instance in the network.

After inlining, a CFA instance model shall only contain assignment transitions and a single automaton instance, the main automaton (CfaNetworkInstance.mainAutomaton). If there are other automaton instances contained by the network, they are ineffective (i.e., the semantics of the model is equivalent to a model which only has the main automaton as the only defined automaton).

Factory

There is a CfaInstanceSafeFactory defined for the safer and more convenient object creation. See the description of ExprSafeFactory for the ideas and conventions behind this factory. Note that as CfaInstanceFactory extends ExpressionSafeFactory, the objects of the expression metamodel can be created via an instance of the CfaInstanceFactory class.

CFA declaration instantiation

Typically, CFA instance models are not build directly, but created by instantiating CFA declaration models. Use CfaInstantiationTrace.transformCfaNetwork() to create an instantiated CFA model. It will return a CfaInstantiationTrace that can be used to access the CFA instance, but also to provide bi-directional tracing between the instance and declaration models.

Utilities

The cern.plcverif.base.models.cfa package provides various additional utilities for expression handling.

• Serialization. The CfaToXmi and XmiToCfa classes provide serialization and deserialization from and to XMI format for CFAs.
• String representation. The CfaToString class provides textual representation of expressions for diagnostic purposes.
• CFA transformation.
  • The CallInliner class provides a way to transform the CFA instance network into an equivalent without any call transitions. It will inline all calls and remove all automata beside the main automaton.
  • The ElseEliminator class transforms the CFA instance network in such way that else expressions will not be present in the model. It will replace all else expressions with a concrete expression based on the guards of the other transitions leaving the same place.
• Validation. The CfaValidation.validate() can be used to validate a CFA model. It will check the model against the EMF metamodel's constraints, as well as for certain additional validation rules (implemented in CfaInstanceValidation and ExprValidation).
  • If called as validate(CfaNetworkBase), it will throw a CfaValidationException exception is the model violates any of the requirements.
  • If called as validate(CfaNetworkBase, IPlcverifLogger), it will not throw any exception, but it will log every violation to the given logger with error severity.
• Utility classes.
  • The ArrayInitialValueHelper helps determining the initial values of an array variable.
  • The CfaInstanceUtils utility class contain helpful static methods for handling CFA instance models, such as determining the list of assigned variables in a transition (getAssignedVarRefs()).
  • The EquatableCfaObject is an optimized version for EquatableEObject. (EquatableEObject is a wrapper for any EObject whose equals() method does not check reference equality, but it calls EcoreUtil.equals(), thus it is suitable for HashSet and HashMap.)
  • The CfaInstanceStatistics class can calculate and provide certain metrics for a CFA instance model, such as number of locations and transitions, total variable bit length, and size of potential state space.
  • The CfaUtils class provide various utility methods, mainly for handling (Reading and writing) annotations.
• Visualization. The CfaToDot.represent() method can be used to transform a CFA model into a Graphviz-compatible textual representation for visualization. The format can be altered by implementing the ICfaToDotFormat interface and pass it to the representCfi method. The format used is similar to the format of the CFA declaration visualization, except that obviously there are no data structures in the output for a CFA instance.