156 K.-W. Liang et al.
Fig. 5.Counts for newly added elements with certain structure (Reg. - regulator,
Tgt. - regulated element,Orig. - baseline model elements,New- newly added ele-
ment). All models studied are listed on x-axis, and y-axis is the count of new elements
having certain structure. (Color figure online)
Fig. 6.(a) Results of statistical model checking of 20 properties in 68 different models.
Each entity in x-axis is a model, and each row is the estimated probability for the
corresponding property. (b) The Max and min difference from the baseline model of
each property.