Eliminate the use of locations in expressions

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.

Supported specifications

This transformation supports a subset of CIF specifications. The following restrictions apply:

  • Component definitions and component instantiations are not supported.

Preprocessing

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):

Implementation details

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 true.

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_l1 and LOC_l2 represent locations l1 and l2, respectively.

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.

Renaming

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, LP2, 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.

Size considerations

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.

Optimality

This transformation introduces enumerations for the possible values of the location pointer variables. To eliminate the enumerations, apply the Convert enumerations to integers or Convert enumerations to constants CIF to CIF transformation.

Annotations

This transformation does not process, add, or remove any annotations.