This directory contains benchmark scripts for LTL-to-Büchi translators.
====================
QUICK INSTRUCTIONS
====================
Running 'make run' should run three benchmarks (you may want to use
'make run -j3' if you have three cores or more), then summarize these
into a LaTeX document that is then compiled to 'result.pdf'.
The summary script requires python3 to be installed, and the LaTeX
compilation obviously needs some LaTeX distribution.
The three benchmarks features respectively 200, 200, and 184 formulae,
to be translated (when these tools exist) by spin, ltl2ba, ltl3ba (4
configurations) and ltl2tgba (2 configurations). Each translation has
a timeout set to 10 minutes, but with a total of 4672 translations to
perform it can take a long time. If you want to speed things up, you
may edit the file 'algorithms' to remove tools or lower the timeout.
==========
CONTENTS
==========
Here are the different scripts used, in case you want to customize
this benchmark.
* algorithms
The configuration of all the translators. This is merely a script
that builds the command-line of ltlcross, to be run by the next
three scripts. Most of the $TOOL variables are defined by the
'defs' file, which is output by 'configure' after checking for
the presence of the said tools.
If you want to add your own tool to the mix, simply modify this file.
The timeout value, common to the three benchmarks, is also set here.
* small
* big
* known
Three scripts that run ltlcross on, respectively:
100 small formulae (size 10, 4 propositions) and their negations
100 big formulae (size 12..15, 8 propositions) and their negations
92 known formulae (from formulae.ltl) and their negations
Each script generates 3 files:
xxxx.log: the log of ltlcross' execution, updated as the script goes
xxxx.csv: the results in CSV format
xxxx.json: the results in JSON format
The last two files are only output when ltlcross terminates, so if
you kill a script before it terminates only the xxxx.log file will
have been overwritten.
* formulae.ltl
A list of LTL formulae used by the `known' check. They come
from three sources:
@InProceedings{ dwyer.98.fmsp,
author = {Matthew B. Dwyer and George S. Avrunin and James C.
Corbett},
title = {Property Specification Patterns for Finite-state
Verification},
booktitle = {Proceedings of the 2nd Workshop on Formal Methods in
Software Practice (FMSP'98)},
publisher = {ACM Press},
address = {New York},
editor = {Mark Ardis},
month = mar,
year = {1998},
pages = {7--15}
}
@InProceedings{ etessami.00.concur,
author = {Kousha Etessami and Gerard J. Holzmann},
title = {Optimizing {B\"u}chi Automata},
booktitle = {Proceedings of the 11th International Conference on
Concurrency Theory (Concur'00)},
pages = {153--167},
year = {2000},
editor = {C. Palamidessi},
volume = {1877},
series = {Lecture Notes in Computer Science},
address = {Pennsylvania, USA},
publisher = {Springer-Verlag}
}
@InProceedings{ somenzi.00.cav,
author = {Fabio Somenzi and Roderick Bloem},
title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}},
booktitle = {Proceedings of the 12th International Conference on
Computer Aided Verification (CAV'00)},
pages = {247--263},
year = {2000},
volume = {1855},
series = {Lecture Notes in Computer Science},
address = {Chicago, Illinois, USA},
publisher = {Springer-Verlag}
}
In the known benchmark, we use both positive and negated versions
of these formulae.
* sym.py
This script reads all the *.json files, and write out a LaTeX file
with summary tables.
=======================
Reading the summaries
=======================
The various outputs (CSV, JSON, our LaTeX) may use the following
column headers:
* input: formula translated (as a string in the CSV output, and as
an index into the input table in the JSON output)
* tool: tool used to translated this formula (idem)
* states: number of states of the resulting automaton
* edges: number of physical arcs between these states
* transitions: number of logical transitions from one state to the other
(for instance if the atomic propositions are 'a' and 'b', and
edge labeled by 'a' represents two transitions labeled by
'a&b' and 'a&!b')
* acc: number of acceptance sets used; it should always be one
in this automaton since we are producing (degeneralized)
Büchi automata.
* scc: number of strongly conncected components in the produced automaton
* nondetstates: number of nondeterministic states
* nondeterministic: 0 if the automaton is deterministic
(no nondeterministic state), 1 otherwise
* time: time required by the translation (although this is measured with
the highest-resolution clock available, it is "wall time", so it
can be affected by the machine's load).
* product_states: number of states in a product if the automaton with some
random Kripke structure (one unique Kripke structure is generated
for each formula and used with automata produced by all tools)
* product_transitions: number of transitions in that product
* product_scc: number of strongly connected componebts in that product
The summary tables produced by sum.py accumulate all these results for
all formulae, tool by tool. They display an additional column, called
'count', giving the number of formulae successfully translated (the
missing formulae correspond to timeouts).
For all these values (except count), the sammler number the better.
More details about ltlcross (used to produce these outputs) can be
found in its man page, and at http://spot.lip6.fr/userdoc/tools.html
