# Union Models for Model Families: Efficient Reasoning over Space and Time
## 7 Results and Discussion
### Results for Property Checking (RT1)  
This section reports on our empirical results for the property checking reasoning task. Figure 25a illustrates \(\mathrm{T_{ind}}\), which is the total time performing property checking on each individual model, for all _SIZE_ and _INDV_ categories. Figure 25b reports on \(\mathrm{T_{MU}}\), which is the time needed to perform property checking on union models that capture individual models of different _SIZE_ and _INDV_. In addition, Figure 25c shows the time \(\mathrm{T_{construct}}\) needed to construct these union models. Figure 25d shows the time speedup with \(\mathrm{T_{construct}}\), i.e., _speedup_with_constrTime_ = \(T_{ind}\) /(\(T_{construct}\) + \(T_{MU}\)), while Figure 25e shows the speedup without considering \(\mathrm{T_{construct}}\), calculated as _speedup_without_constrTime_ = \(T_{ind}\) / \(T_{MU}\). Finally, Figure 25f highlights the time saving in minutes achieved by using \(M_{U}\) to perform property checking calculated as _TimeSaving_ = (\(T_{ind}-T_{MU}\)). Figure 25a-c shows that T\({}_{\rm ind}\), T\({}_{\rm MU}\), and T\({}_{\rm construct}\) increase when the size of models (i.e., _SIZE_) or the number of models in a family (i.e., _INDV_) increase. In addition, it can be noticed that the increase of T\({}_{\rm ind}\) is important for each _SIZE_ category, as the _INDV_ parameter grows from _INDV_ = S to _INDV_ = XL. For instance, with _SIZE_ = XL, we observe 30.85 s on average for _INDV_ = S to 765 s on average for _INDV_=XL. On the other hand, the increase of T\({}_{\rm MU}\) as _INDV_ grows is marginal for each _SIZE_ category. For example, for XL-sized models T\({}_{\rm MU}\) increases from 0.39 s (for _INDV_ = S) to 2.25 s (for _INDV_ = XL). Furthermore, it can be inferred from Figure 25d,e that the use of \(M_{U}\) for property checking achieves a noticeable time speedup compared to performing the same task on a set of individual models separately. For _speedup_with_constrTime_ (Figure 25d), the highest speedup (=131) was observed with a small number of individual models (i.e., _INDV_ = S) that are of a small size (i.e., _SIZE_ = S). The smallest speedup (=8) was observed when _INDV_ = M and _SIZE_ = XL. In addition, Figure 25d shows that there is a noticeable pattern of speedup degradation for each _INDV_ category as the number of elements per individual model (i.e., _SIZE_) increases. This is due in part to the increase of T\({}_{\rm construct}\) as the _SIZE_ increases. Nevertheless, the speedup never falls below 1, which means that even with very  
Figure 25: Results for property checking (RT1) for all _INDV_ and _SIZE_ categories. large models (with \(INDV=\) XL and \(SIZE=\) XL) the time to perform property checking on a group of such models (using \(M_{U}\)), considering the time to construct \(M_{U}\), is better than performing property checking on all individual models. Figure 25e shows that the time speedup becomes more significant when T\({}_{\text{construct}}\) is ignored, where the highest \(speedup\_without\_constrTim=1028\) is with models of \(SIZE=\) S and \(INDV=\) L. This high value of 1028, which is higher than the number of models in family (110), is caused in part because of a low denominator value with low resolution (e.g., 1028 = 308.4/0.3), as well as by the time taken by the Python environment to load before executing the code of each individual model, which is not negligible, particularly for small models. It is important to emphasize here that the erratic behavior of the time speedup with and without T\({}_{\text{construct}}\) across all categories of \(SIZE\) and \(INDV\) does not necessarily mean that one category is superior to the other. This is because speedup reflects the ratio between T\({}_{\text{ind}}\) and T\({}_{\text{MU}}\) (and T\({}_{\text{construct}}\) in case of calculating \(speedup\_with\_constrTime\)), and could fluctuate because of different densities of variability in the models.