168
A. Cimatti et al.
Fig. 3: Comparison on the bounded convex category (consistency checking on
the first row and compatibility checking on the second).
than TRICker (especially for Uppaal), the latter overall solves a significantly
larger amount of problems within the timeout, showing a clear improvement in
scalability. This can be seen also in the survival plots comparing the three tools
with the Virtual Best Solver (vbs for short). We can make similar considerations
for the bounded and general categories, shown respectively in Fig. 4 and Fig. 5.
(Note that for the general case, we could not evaluate Uppaal as it does not
support the verification of fairness properties.) We remark that we did not note
any kind of correlation between the number of signal or state dependencies in
the benchmarks and the time spent by the solver. Finally, Fig. 6 shows the
correlation between the memory (measured in MB) and the time (in seconds)
spent by TRICker on consistency and compatibility checking, respectively.
We also evaluated the parameter synthesis algorithm described in Sec. 4.
Since Uppaal currently does not support parameter synthesis for timed automata,
we could not include it in the comparison. We therefore compared TRICker with
Timed-nuXmv, for which we used the ParamIC3 parameter synthesis algorithm
described in [9]. The algorithm is based on the inverse method, i.e., it finds a
bad configuration for the parameters and it tries to generalize it, maximizing the
set of bad parameters removed from the current approximation of the region.
We took all the consistent benchmarks of the previous test sets, which amounts
to approximately 100 instances (note that for each instance of the class NcMp,
the number of parameters is ≈ 2 · N · M
7 ). The results of the comparison are
shown in Fig. 7; as in the previous cases, TRICker shows better performance and
7 recall that both the lower and the upper bounds are parameters.
A. Cimatti et al.
Fig. 3: Comparison on the bounded convex category (consistency checking on
the first row and compatibility checking on the second).
than TRICker (especially for Uppaal), the latter overall solves a significantly
larger amount of problems within the timeout, showing a clear improvement in
scalability. This can be seen also in the survival plots comparing the three tools
with the Virtual Best Solver (vbs for short). We can make similar considerations
for the bounded and general categories, shown respectively in Fig. 4 and Fig. 5.
(Note that for the general case, we could not evaluate Uppaal as it does not
support the verification of fairness properties.) We remark that we did not note
any kind of correlation between the number of signal or state dependencies in
the benchmarks and the time spent by the solver. Finally, Fig. 6 shows the
correlation between the memory (measured in MB) and the time (in seconds)
spent by TRICker on consistency and compatibility checking, respectively.
We also evaluated the parameter synthesis algorithm described in Sec. 4.
Since Uppaal currently does not support parameter synthesis for timed automata,
we could not include it in the comparison. We therefore compared TRICker with
Timed-nuXmv, for which we used the ParamIC3 parameter synthesis algorithm
described in [9]. The algorithm is based on the inverse method, i.e., it finds a
bad configuration for the parameters and it tries to generalize it, maximizing the
set of bad parameters removed from the current approximation of the region.
We took all the consistent benchmarks of the previous test sets, which amounts
to approximately 100 instances (note that for each instance of the class NcMp,
the number of parameters is ≈ 2 · N · M
7 ). The results of the comparison are
shown in Fig. 7; as in the previous cases, TRICker shows better performance and
7 recall that both the lower and the upper bounds are parameters.