This CIF to CIF transformation eliminates the use of locations in expressions (such as guards, invariants, and equations), by introducing location pointer variables for automata, and using them instead.
This transformation supports a subset of CIF specifications. The following restrictions apply:
Component definitions and component instantiations are not supported.
No preprocessing is currently performed by this CIF to CIF transformation. To increase the subset of specifications that can be transformed, apply the following CIF to CIF transformations (in the given order):
For each automaton with two or more locations, and for which a location is used (referred to) in an expression (such as a guard, invariant, or equation), a location pointer variable is introduced, with as value the current location of the automaton. The values for such a new variables are part of a newly created enumeration that has a value (an enumeration literal) for each location of the automaton. For automata with exactly one location, no location pointer variable is created.
To initialize the new location pointer variable, the variable itself is initialized to
any (meaning any value in its domain), and initialization predicates are added to all locations that could potentially be initial locations. For automata with exactly one initial state, the initial value of the location pointer variable is set directly, instead of using initialization predicates.
All edges in the automaton that change the current location of that automaton, get an additional assignment to update the location pointer variable.
All uses of the locations of the automaton in expressions (that is, all location reference expressions) are changed to equality binary expressions for the location pointer variable and the enumeration literal corresponding to the location. For references to a location of an automaton with exactly one location, all uses of this location are changed to
For instance, the following specification:
automaton x: event e; alg bool a = l1; location l1: initial; edge e goto l2; location l2: edge e; end
is transformed to the following specification:
automaton x: event e; alg bool a = LP = LOC_l1; disc LPE LP = LOC_l1; enum LPE = LOC_l1, LOC_l2; location l1: initial; edge e do LP := LOC_l2 goto l2; location l2: edge e; end
Location pointer variable
LP is added. It is initialized directly in the declaration, since there is exactly one initial location in this automaton. Enumeration
LPE is created to represent the possible values of the location pointer variable. Enumerations literals
LOC_l2 represent locations
The edge from location
l1 to location
l2 is extended with an update to the location pointer. The self loop in location
l2 is not extended, as the location does not change.
If the names of the location pointer variables that are introduced, conflict with already existing declarations, they are renamed. For instance, if
LP is already in use,
LP3, etc, are used instead. Similarly, renaming is performed for enumerations, and enumeration literals that conflict with already existing declarations. If renaming takes place, a warning is printed to the console.
The number of added location pointer variables is linear in the number of automata. The number of added initialization predicates for the location pointer variables is linear in the number of possible initial locations. The number of added enumerations is linear in the number of automata. The number of added enumeration literals is linear in the number of locations. The number of added updates is linear in the number of edges. The number of added equality binary expressions is linear in the number of location references.