Eliminate component definition/instantiation

This CIF to CIF transformation eliminates all component definitions and instantiations, by actually instantiating the component definitions.

Supported specifications

This transformation supports all CIF specifications.

Preprocessing

n/a

Implementation details

This transformation operates in three phases:

  • Phase 1: Find the component definitions without any component definitions and/or component instantiations in them.

  • Phase 2: Instantiate the component definitions found in phase 1, by putting the body of the definition in the place of the instantiation, in a component named after the component instantiation. Also removes the component definitions that were just instantiated, and introduces new local algebraic variables for the algebraic parameters.

  • Phase 3: Replace uses of component, event, and location parameters by the arguments provided for the instantiation.

For instance, the following specification:

group def P(alg int x):
  invariant x > 0;
end

p1: P(1);

alg int y = 2;
p2: P(y);

is transformed to the following specification:

group p1:
  alg int x = 1;
  invariant x > 0;
end

alg int y = 2;
group p2:
  alg int x = y;
  invariant x > 0;
end

Absolute references may be needed to express the results of this transformation. For instance:

const int x = 5;

group def X():
  invariant x = 5;
end

group a:
  x: X();
end

is transformed to the following specification:

const int x = 5;

group a:
  group x:
    invariant .x = 5;
  end
end

Note how the invariant in component a.x can not refer to constant x directly, as x refers to component a.x in that context. Therefore, the scope absolute reference .x is used instead.

Renaming

n/a

Size considerations

Since component definitions are shortcuts for components, eliminating them could result in an increase of the size of the specification.

Optimality

n/a

Annotations

This transformation does not add any new annotations. Each instantiated component gets the annotations of its component definition and instantiation. If a component definition is instantiated multiple times, this thus leads to a duplication of the annotations of that definition on its instantiated components. The annotations of automaton definitions that are not instantiated are removed. As each algebraic parameter becomes an algebraic variable when a component definition is instantiated, the variable get the annotations of the parameter.