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

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

n/a

### Size considerations

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

n/a