488
C. E. Budde
Fig. 1: ci precision. Top: dfts (transient). Bottom: queues (steady-state).
outliers [17]. Whiskers are standard deviation, and white numbers indicate how
many runs yielded not-null estimates. Clearly, res algorithms outperform cmc
in the hardest cases: less than half of cmc runs in DFT-8 could build (wide) cis.
Second, we estimate the steady-state overflow probability in the last node
of tandem queues, on a Markovian case with 2 buffers [29], 3 buffers [28], and
a non-Markovian 3-buffers case [30]. We study how FIG—using --amono, seq,
and rst 3,4,5,7,9 —approximates each optimal ad hoc function and thresholds of
[29, 28, 30]. Experiments ran as before: the bottom plot of Fig. 1 shows that FIG’s
default (rst 3 with seq, legend “AUTO 3”) is always closest to the optimal.
Third, we compare FIG and modes in the original benchmark of the latter [5].
We do so for fe-seq, rst-seq, rst-es, using each tool’s default options.
We ran each benchmark instance 15 min, thrice per tool, in an Intel i7-6700
CPU with Linux x64 5.3.1. The scatter plots of Fig. 2 show the median of the ci
precisions. Sub-plots on the bottom-right are a zoom-ins in the range [10
−10 ,10
−5 ].
An (x,y) point is an instance whose median ci width was x for FIG 1.2 and y
for modes netcore-3.0.150, single threaded. A point over the solid diagonal line
means FIG built a narrower ci. A point on the upper boundary means that modes
built no cis in all runs. Dotted diagonal lines indicate cis twice as wide. Fig. 2
shows that both tools perform similarly, with a slight trend in favour of FIG.
This could be caused by modes operating on jani sta (translated from iosa
by FIG): modes must assign values to variables and then compare them to clocks.
Albeit modes is multi-threaded, these experiments ran on a single thread to
compare both tools on equal conditions. On the other hand, FIG also estimates
the probability of steady-state properties, for which there is no support in modes.
10 -16
10 -12
10 -8
10 -4
10 -16
10 -12
10 -8
10 -4
to
to
Fixed Effort (seq)
10 -16
10 -12
10 -8
10 -4
10 -16
10 -12
10 -8
10 -4
to
to
restart (seq)
10 -16
10 -12
10 -8
10 -4
10 -16
10 -12
10 -8
10 -4
to
to
restart (es)
oilpipes
database
tandem-queue
open-closed-queue
queue-with-breakdowns
Fig. 2: ci precision of FIG (x-axis) vs. modes (y-axis): medians of 3 runs × 15 min
C. E. Budde
Fig. 1: ci precision. Top: dfts (transient). Bottom: queues (steady-state).
outliers [17]. Whiskers are standard deviation, and white numbers indicate how
many runs yielded not-null estimates. Clearly, res algorithms outperform cmc
in the hardest cases: less than half of cmc runs in DFT-8 could build (wide) cis.
Second, we estimate the steady-state overflow probability in the last node
of tandem queues, on a Markovian case with 2 buffers [29], 3 buffers [28], and
a non-Markovian 3-buffers case [30]. We study how FIG—using --amono, seq,
and rst 3,4,5,7,9 —approximates each optimal ad hoc function and thresholds of
[29, 28, 30]. Experiments ran as before: the bottom plot of Fig. 1 shows that FIG’s
default (rst 3 with seq, legend “AUTO 3”) is always closest to the optimal.
Third, we compare FIG and modes in the original benchmark of the latter [5].
We do so for fe-seq, rst-seq, rst-es, using each tool’s default options.
We ran each benchmark instance 15 min, thrice per tool, in an Intel i7-6700
CPU with Linux x64 5.3.1. The scatter plots of Fig. 2 show the median of the ci
precisions. Sub-plots on the bottom-right are a zoom-ins in the range [10
−10 ,10
−5 ].
An (x,y) point is an instance whose median ci width was x for FIG 1.2 and y
for modes netcore-3.0.150, single threaded. A point over the solid diagonal line
means FIG built a narrower ci. A point on the upper boundary means that modes
built no cis in all runs. Dotted diagonal lines indicate cis twice as wide. Fig. 2
shows that both tools perform similarly, with a slight trend in favour of FIG.
This could be caused by modes operating on jani sta (translated from iosa
by FIG): modes must assign values to variables and then compare them to clocks.
Albeit modes is multi-threaded, these experiments ran on a single thread to
compare both tools on equal conditions. On the other hand, FIG also estimates
the probability of steady-state properties, for which there is no support in modes.
10 -16
10 -12
10 -8
10 -4
10 -16
10 -12
10 -8
10 -4
to
to
Fixed Effort (seq)
10 -16
10 -12
10 -8
10 -4
10 -16
10 -12
10 -8
10 -4
to
to
restart (seq)
10 -16
10 -12
10 -8
10 -4
10 -16
10 -12
10 -8
10 -4
to
to
restart (es)
oilpipes
database
tandem-queue
open-closed-queue
queue-with-breakdowns
Fig. 2: ci precision of FIG (x-axis) vs. modes (y-axis): medians of 3 runs × 15 min