Eliminate groups | CIF documentation

Supported specifications

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

Component definitions and component instantiations are not supported.

Furthermore, this transformation does not guarantee the correct result for specification with enumerations. See also the Renaming section below.

Preprocessing

To increase the subset of specifications that can be transformed, apply the following CIF to CIF transformations (in the given order) prior to using this transformation:

The following CIF to CIF transformations are automatically applied as preprocessing (in the given order), to increase the subset of CIF specifications that can be transformed:

Implementation details

All declarations, invariants, initialization predicates, marker predicates, and equations from the groups are lifted to the top level of the specification. The automata are lifted to the top level of the specification as well. Subsequently, the groups are removed.

In order to be able to track the origin of automata, declarations and invariants, they are named after their absolute names. For a group x, with a group y, with a constant z, the absolute name of the constant is x.y.z. The constant is lifted to the top level of the specification, and named x_y_z.

For instance, this specification:

group a:
  const int x = 5;
  invariant inv: x > 4;
end

group p:
  automaton q:
    event e;
    location;
  end
end

is transformed to the following specification:

const int a_x = 5;
invariant a_inv: a_x > 4;

automaton p_q:
  event e;
  location;
end

Renaming

Since declarations (and invariants) of the specification are merged with the declarations of the groups and with automata, renaming may be necessary to ensure uniquely named declarations. For instance, for a group x, with a group y, with a constant z, the absolute name of the constant is x.y.z. The constant is lifted to the top level of the specification, and renamed to x_y_z. However, if the specification already contains a declaration of another constant, automaton, etc named x_y_z, then the lifted constant is renamed to x_y_z2 instead. If that name is also already in use, it is renamed to x_y_z3, etc.

Whenever renaming takes place, a warning will be printed to the console.

Renaming of enumeration literals

Enumeration literals that are part of lifted enumeration declarations, are not renamed to their absolute names. To understand why this is necessary, consider:

group x:
  enum E = A, B;
end

automaton y:
  enum E = A, B;
  location:
    initial;
end

invariant x.A = y.A;

Here, group x and automaton y both have an enumeration E with enumeration literals A and B. The invariant of the specification compares the literals of the two different enumerations. This is allowed, since the enumerations are compatible (they have the same enumeration literals, with the same names, in the same order). If we were to rename the enumeration literals to absolute names as we lift them to the top level of the specification, the result would be:

enum x_E = x_A, x_B;

automaton y:
  enum E = A, B;
  location:
    initial;
end

invariant x_A = y.A;

Which would no longer be a valid specification, as enumerations x_E and y.E are no longer compatible (they have enumeration literals with different names). Since we leave the names of the enumeration literals as they are, the result of the transformation is:

enum x_E = A, B;

automaton y:
  enum E = A, B;
  location:
    initial;
end

invariant A = y.A;

which is still a correct specification, and has the same meaning as the original specification.

Now assume the following specification:

group x:
  enum E = A, B;
end

group y:
  enum E = A, B;
end

invariant x.A = y.A;

Here, the two enumerations are both in groups. If we lift them, we have two enumerations, with the same literals, which is not a valid CIF specification. As such, renaming can not be avoided, and the result of the transformation will be:

enum x_E = A, B;
enum y_E = A2, B2;

invariant A = A2;

This result is an invalid CIF specification. Whenever an enumeration literal is renamed, a warning is printed to the console, informing of the possibility that the resulting specification is invalid. As such, it is highly recommended to avoid such situations, and eliminate the enumerations prior to the elimination of the groups.

Size considerations

The groups are removed. Other objects are lifted, which essentially means they are moved. The size of the specification does not increase.

Optimality

n/a

Annotations

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