Eliminate component definition/instantiation
This CIF to CIF transformation eliminates all component definitions and instantiations, by actually instantiating the component definitions.
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;
endAbsolute 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();
endis transformed to the following specification:
const int x = 5;
group a:
group x:
invariant .x = 5;
end
endNote 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.