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