Importation is a kind of tight coupling between models.
Strictly speaking, DCharts are not closed under importation. I.e., it may not be possible to find such a model so that it has exactly the same behavior as the original model but it has no importation state. A counter-example can be easily found. Suppose , which means model imports itself in state . This creates an infinite structure. It is impossible to find a non-recursive model with the same behavior.
If recursive importation is not considered, closure under importation can be proved with the algorithm described in section 4.2.9.
Proof The expanded model of non-recursive DCharts model is found by the following algorithm:
for in of
if is defined at then
import into according to the algorithm in section 4.2.9
Since is non-recursive, this algorithm always terminates in a finite number of steps. The model returned does not contain any importation state.
Obviously, is still a DCharts model. According to the semantics of dynamic importation (section 4.2.9), it has exactly the same behavior as .