1This directory contains benchmark scripts for LTL-to-B�chi translators.
2
3====================
4 QUICK INSTRUCTIONS
5====================
6
7Running 'make run' should run three benchmarks (you may want to use
8'make run -j3' if you have three cores or more), then summarize these
9into a LaTeX document that is then compiled to 'result.pdf'.
10
11The summary script requires python3 to be installed, and the LaTeX
12compilation obviously needs some LaTeX distribution.
13
14The three benchmarks features respectively 200, 200, and 184 formulae,
15to be translated (when these tools exist) by spin, ltl2ba, ltl3ba (4
16configurations) and ltl2tgba (2 configurations).  Each translation has
17a timeout set to 10 minutes, but with a total of 4672 translations to
18perform it can take a long time.  If you want to speed things up, you
19may edit the file 'algorithms' to remove tools or lower the timeout.
20
21
22==========
23 CONTENTS
24==========
25
26Here are the different scripts used, in case you want to customize
27this benchmark.
28
29* tools
30
31  The configuration of all the translators.  This is merely a script
32  that builds the command-line of ltlcross, to be run by the next
33  three scripts.  Most of the variables (like $SPIN, $LTL2BA, etc) are
34  defined by the 'defs' file, which is output by 'configure' after
35  checking for the presence of the said tools.
36
37  If you want to add your own tool to the mix, simply modify this
38  'tools' file.
39
40  The timeout value, common to the three benchmarks, is also set here.
41
42* small
43* big
44* known
45
46  Three scripts that run ltlcross on, respectively:
47    100 small formulae (size 10, 4 propositions) and their negations
48    100 big formulae (size 12..15, 8 propositions) and their negations
49    92 known formulae (produced by genltl, see below) and their negations
50
51  Each script generates 3 files:
52    xxxx.log: the log of ltlcross' execution, updated as the script goes
53    xxxx.csv: the results in CSV format
54    xxxx.json: the results in JSON format
55
56  The last two files are only output when ltlcross terminates, so if
57  you kill a script before it terminates only the xxxx.log file will
58  have been overwritten.
59
60
61The known LTL formulas are generated by genltl, and come from the following
62three papers:
63
64    @InProceedings{   dwyer.98.fmsp,
65      author        = {Matthew B. Dwyer and George S. Avrunin and James C.
66		      Corbett},
67      title         = {Property Specification Patterns for Finite-state
68		      Verification},
69      booktitle     = {Proceedings of the 2nd Workshop on Formal Methods in
70		      Software Practice (FMSP'98)},
71      publisher     = {ACM Press},
72      address       = {New York},
73      editor        = {Mark Ardis},
74      month         = mar,
75      year          = {1998},
76      pages         = {7--15}
77    }
78
79    @InProceedings{   etessami.00.concur,
80      author        = {Kousha Etessami and Gerard J. Holzmann},
81      title         = {Optimizing {B\"u}chi Automata},
82      booktitle     = {Proceedings of the 11th International Conference on
83		      Concurrency Theory (Concur'00)},
84      pages         = {153--167},
85      year          = {2000},
86      editor        = {C. Palamidessi},
87      volume        = {1877},
88      series        = {Lecture Notes in Computer Science},
89      address       = {Pennsylvania, USA},
90      publisher     = {Springer-Verlag}
91    }
92
93    @InProceedings{   somenzi.00.cav,
94      author        = {Fabio Somenzi and Roderick Bloem},
95      title         = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}},
96      booktitle     = {Proceedings of the 12th International Conference on
97		      Computer Aided Verification (CAV'00)},
98      pages         = {247--263},
99      year          = {2000},
100      volume        = {1855},
101      series        = {Lecture Notes in Computer Science},
102      address       = {Chicago, Illinois, USA},
103      publisher     = {Springer-Verlag}
104    }
105
106  In the known benchmark, we use both positive and negated versions
107  of these formulae, yielding 178 unique formulas.
108
109* sym.py
110
111  This script reads all the *.json files, and write out a LaTeX file
112  with summary tables.
113
114
115=======================
116 Reading the summaries
117=======================
118
119The various outputs (CSV, JSON, our LaTeX) use column headers
120that are described in doc/userdoc/ltlcross.html and also
121in the ltlcross man page.
122
123The summary tables produced by sum.py accumulate all these results for
124all formulae, tool by tool.  They display an additional column, called
125'count', giving the number of formulae successfully translated (the
126missing formulae correspond to timeouts).
127
128For all these values (except count), smaller numbers are better.
129
130
131More details about ltlcross (used to produce these outputs) can be
132found in its man page, and at http://spot.lrde.epita.fr/tools.html
133
134
135==============================================
136 Running differents configurations / toolsets
137==============================================
138
139Instead of modifying the 'tools' file, you can also set the TOOLS
140environment variable to point to another file.
141
142For instance try
143
144  TOOLS=./tools.sim make -j3 run
145
146to benchmark several simulation-related options.
147