Spot 1.0 benchmarks
This page gives additional details about benchmarks included in a paper submitted to IJCCBS. Please direct further questions to mailto:adl@lrde.epita.fr.
Table of Contents
Link to the tools used
- spin 6.2.2
- lbt 1.2.2
- wring 1.1.0
- ltl2ba 1.1
- modella 1.5.9
- ltl2nba (no version)
- ltl3ba 1.0.1
- spot 1.0
Because of the special type of automaton output by Wring (generalized
Büchi with multiple initial states, and labels on states) we had to
write a small tool to perform the conversion to the LBTT format we use
as input. The script convwring.pl adds a fake initial state, and
move the label of all states onto their incoming transitions. People
willing to interface with Wring might also consider the Wring2lbtt
tool written by the Modella authors, but it seems to perform a
different conversion, producing automata that are way larger than
those we produce.
184 formulas from the literature
The file formulas.txt contains the 92 formulas mentioned in the paper. They can be converted into other syntaxes using Spot's ltlfilt tool.
The statistics presented in the paper are based on these formulas and their negation. They were computed by running ltlcross as follows:
% ltlfilt --nnf formulas.ltl |
ltlcross -T600 --csv=cmp.csv --json=cmp.json \
'spin -f %s >%N' \
'modella -r12 -g -e %L %T' \
'~/projs/ltl2nba/script4lbtt.py %L %T' \
'ltl2ba -f %s >%N' \
'ltl3ba -S -f %s >%N' \
'ltl3ba -M -f %s >%N' \
'ltl3ba -M -S -f %s >%N' \
'ltl2tgba --spin --deterministic %f >%N' \
'ltl2tgba --spin --small %f >%N' \
'lbt < %L > %T' \
'(cd ~/projs/Wring-1.1.0; ./ltl2aut.pl -f %w | ~/convwring.pl) > %T' \
'ltl2tgba --lbtt --deterministic %f >%T' \
'ltl2tgba --lbtt --small %f >%T' 2>&1 | tee cmp.trace
The initial ltlfilt --nnf puts the formulas into negative normal form; the
intended side effect is to remove the ->, xor and <-> operators
because these are not supported by ltl2nba. The -T600 option
limits each translation to 10 minute.
The resulting files:
cmp.traceshows the output of the run above, including any reported error (these errors are discussed in the "Bugs found" section below).cmp.csvcontains detailed statistics about all the automata produced, including errorscmp.jsoncontains the same information in another format (see theltlcrossdocumentation for usage)
The following hand-edited files remove the three lines where wring
failed to produce a correct automaton (read below), and the one line
where Modella produced a bogus automaton:
These final results can be explored interactively using an experimental web page. We are told that this page does not work on IE9, so if you have problems, consider using another browser such as Firefox or Chrome.
sum.pyis the script we used to convertcmd-ed.jsoninto the table displayed in the paper.
Bugs found while preparing this paper
Spin
There is a regression between Spin 6.2.2 and Spin 5.2.5 regarding the
simplification of atomic propositions. Spin 6.2.2 considers (a || true) to be an atomic proposition without trying to break it down.
As a consequence the resulting automaton which is still correct can
be bigger than necessary.
% spin-5.2.5 -f '(a || true) || []<>c'
never { /* (a || true) || []<>c */
accept_init:
T0_init:
if
:: (1) -> goto accept_all
fi;
accept_all:
skip
}
% spin-6.2.2 -f '(a || true) || []<>c'
never { /* (a || true) || []<>c */
T0_init:
if
:: ((a || true)) -> goto accept_all
:: ((c)) -> goto accept_S10
:: (1) -> goto T0_S10
fi;
accept_S10:
if
:: (1) -> goto T0_S10
fi;
T0_S10:
if
:: ((c)) -> goto accept_S10
:: (1) -> goto T0_S10
fi;
accept_all:
skip
}
Spin 6.2.3 (released on 2012-10-24) is affected as well.
Modella
Modella 1.5.9 fails to translate (G(F(p0) & F(G(!p1))) | (F(G(!p0)) & G(F(p1))) correctly.
Using Spot's ltlcross to perform the product between the automata translated from this
formula and its negation shows that the product is not empty.
% ltlcross -f '(G(F(p0) & F(G(!p1))) | (F(G(!p0)) & G(F(p1)))' 'modella %L %T' | & G F p0 F G ! p1 & F G ! p0 G F p1 Running [P0]: modella 'lck-i0-FU7v8W' 'lck-o0-XXGKJS' Running [N0]: modella 'lck-i0-iqXvpO' 'lck-o0-2y0h5J' Performing sanity checks and gathering statistics... error: P0*N0 is nonempty
Looking at the automaton for the positive version of the formula reveals that it includes the language of G(!p0).
Wring
Running Wring causes Perl to print error messages from time to time. E.g.:
% ./ltl2aut.pl -f '(!(G((p2=0) + (((p3=0) + (X((p1=0) U ((F(p0=1)) * (p4=1)))) + (X((p1=1) R (p4=0)))) U ((p1=1) + (G((p3=0) + (X((p1=0) U ((F(p0=1)) * (p4=1)))) + (X((p1=1) R (p4=0))))))))))' Use of freed value in iteration at Buechi.pm line 755.
% ./ltl2aut.pl -f '((p2=1) * (X(p1=1))) R (X((((p3=1) U (p0=1)) R (p2=1)) U ((p3=1) R (p2=1))))' Use of freed value in iteration at Buechi.pm line 718.
% ./ltl2aut.pl -f '(!((p0=1) U ((p1=1) * (X((p2=1) * ((TRUE) U ((p3=1) * (X((TRUE) U ((p4=1) * (X((TRUE) U ((p5=1) * (X((TRUE) U (p6=1))))))))))))))))' Use of freed value in iteration at Buechi.pm line 718.
and when this happens, no automaton is produced. Unfortunately these errors are not deterministic.
Thew NEWS file of Wring 1.1.0, dated 2001-06-22, states:
WARNING: Recent versions of Perl (including 5.6.0, 5.6.1, and 5.7.1) have a bug that sometimes causes the perl interpreter to crash when running Wring. The Perl maintainers have been notified. In the meanwhile, if you are considering upgrading from, say, 5.005, you may want to keep this in mind.
It is related? We are running Perl 5.14.2 and unfortunately installing the 13-year-old Perl 5.005 is too much of a burden today as it is no longer packaged by GNU/Linux distributions.
ltl3ba
ltl3ba 1.0.1 segfaults on the following formula:
% ltl3ba -f '!(X(!(Xa && !Xa) V (a || !(Xa && !Xa))))' segmentation fault
This is fixed in ltl3ba 1.0.2 (released on 2012-12-13).
The above formula was part of an experiment with a set of random formulas, that we did not include in the paper.