From 885a535184b8f20a257a618899a2840b844ad097 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 6 Jan 2013 18:57:50 +0100 Subject: [PATCH] Rewrite the ltl2tgba bench using ltlcross * bench/ltl2tgba/sum.py: New file. * bench/ltl2tgba/.gitignore, bench/ltl2tgba/Makefile.am, bench/ltl2tgba/README, bench/ltl2tgba/algorithms, bench/ltl2tgba/big, bench/ltl2tgba/defs.in, bench/ltl2tgba/known, bench/ltl2tgba/small: Rewrite this benchmark completely. Also drop support of Wring and Modella, as we cannot get them to work reliably. * bench/ltl2tgba/formulae.ltl: Rewrite in Spot's syntax. * bench/ltl2tgba/lbtt2csv.pl, bench/ltl2tgba/ltl2baw.in, bench/ltl2tgba/parseout.pl: Delete these scripts, no longer needed. * configure.ac: Do not output ltl2baw.pl anymore. --- bench/ltl2tgba/.gitignore | 6 +- bench/ltl2tgba/Makefile.am | 38 ++++-- bench/ltl2tgba/README | 266 ++++++++++++++++-------------------- bench/ltl2tgba/algorithms | 115 ++++------------ bench/ltl2tgba/big | 60 +------- bench/ltl2tgba/defs.in | 20 +-- bench/ltl2tgba/formulae.ltl | 76 +++++------ bench/ltl2tgba/known | 45 +----- bench/ltl2tgba/lbtt2csv.pl | 132 ------------------ bench/ltl2tgba/ltl2baw.in | 222 ------------------------------ bench/ltl2tgba/parseout.pl | 91 ------------ bench/ltl2tgba/small | 60 +------- bench/ltl2tgba/sum.py | 130 ++++++++++++++++++ configure.ac | 6 +- 14 files changed, 355 insertions(+), 912 deletions(-) delete mode 100755 bench/ltl2tgba/lbtt2csv.pl delete mode 100644 bench/ltl2tgba/ltl2baw.in delete mode 100755 bench/ltl2tgba/parseout.pl create mode 100755 bench/ltl2tgba/sum.py diff --git a/bench/ltl2tgba/.gitignore b/bench/ltl2tgba/.gitignore index 56a141e28..4bd7b21f5 100644 --- a/bench/ltl2tgba/.gitignore +++ b/bench/ltl2tgba/.gitignore @@ -1,7 +1,7 @@ Makefile.in Makefile -*.cfg -*.txt +*.csv +*.json *.log defs -ltl2baw.pl +results.tex diff --git a/bench/ltl2tgba/Makefile.am b/bench/ltl2tgba/Makefile.am index 6ab3f7c3d..aae9fe999 100644 --- a/bench/ltl2tgba/Makefile.am +++ b/bench/ltl2tgba/Makefile.am @@ -3,22 +3,38 @@ EXTRA_DIST = \ big \ formulae.ltl \ known \ - parseout.pl \ small \ - lbtt2csv.pl -CLEAN_FILES = \ - big.cfg big.log big.txt \ - small.cfg small.log small.txt \ - known.cfg known.log known.txt + sum.py + +OUTPUTS = known small big +OUTCSV = $(OUTPUTS:=.csv) +OUTJSON = $(OUTPUTS:=.json) +OUTLOG = $(OUTPUTS:=.log) + +CLEANFILES = $(OUTCSV) $(OUTJSON) $(OUTLOG) \ + results.pdf results.aux results.log results.tex .PHONY = run -run: small.txt big.txt known.txt -deps = $(srcdir)/algorithms $(top_srcdir)/configure.ac $(top_builddir)/src/tgbatest/ltl2tgba +run: $(OUTJSON) -small.txt: $(srcdir)/small $(deps) +deps = $(srcdir)/algorithms \ + $(top_srcdir)/configure.ac \ + $(top_builddir)/src/bin/ltl2tgba + +small.json: $(srcdir)/small $(deps) $(srcdir)/small -big.txt: $(srcdir)/big $(deps) +big.json: $(srcdir)/big $(deps) $(srcdir)/big -known.txt: $(srcdir)/known $(srcdir)/formulae.ltl $(deps) +known.json: $(srcdir)/known $(srcdir)/formulae.ltl $(deps) $(srcdir)/known + +results.tex: $(srcdir)/sum.py $(OUTJSON) + v=`git describe --always --dirty 2>/dev/null || \ + echo $(PACKAGE_STRING)`; \ + $(srcdir)/sum.py $(OUTJSON) >$(@:.tex=.tmp) \ + --intro "Results assembled on `LANG=C date` with $$v."; \ + mv $(@:.tex=.tmp) $@ + +results.pdf: results.tex + pdflatex results.tex diff --git a/bench/ltl2tgba/README b/bench/ltl2tgba/README index 5bbb31ec2..3f36675ae 100644 --- a/bench/ltl2tgba/README +++ b/bench/ltl2tgba/README @@ -1,182 +1,156 @@ This directory contains benchmark scripts for LTL-to-Büchi translators. -They are all based on lbtt. + +==================== + 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 lbtt configuration of all the algorithms. More about these below. + 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 - Run lbtt on, respectively: - small formulae (size 10, 4 propositions) - big formulae (size 12..15, 8 propositions) - known formulae (96 formulae from formulae.ltl) + 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.cfg: the configuration file for lbtt - xxxx.log: the log of lbtt's execution (also output when the script runs) - xxxx.txt: the summary of the test (also output at the end of the script) + 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 -* ltl2baw.in -* ltl2baw.pl - - ltl2baw.pl is generated from ltl2baw.in by configure. This perl - script converts the intermediate generalized automata computed by - ltl2ba into a form usable by lbtt. + 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. - See ../emptchk/README for the sources. + A list of LTL formulae used by the `known' check. They come + from three sources: -* parseout.pl + @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} + } - This scripts is used to create *.txt files from *.log files. + @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} + } -==================== - ALGORITHMS & TOOLS -==================== + In the known benchmark, we use both positive and negated versions + of these formulae. -The page http://spot.lip6.fr/wiki/LtlTranslationBenchmark explains -all the keys used and the different tools involved in the benchmark. +* sym.py -Spot's configure script checks for the tools needed in the -benchmark, and the script in this directory should omit the tools -that are not available. + This script reads all the *.json files, and write out a LaTeX file + with summary tables. -===================== - Running the scripts -===================== - - 1) Install all the third-party translators that you want to check. - They must all be in $PATH and work from there. - - Two difficulties comes from Modella and wring2lbtt: - - * Modella 1.5.7 produces automata that are not readable by lbtt 1.1.2. - You have to fix the former as follows: - ---- modella1.5.7/modella_automa.c 2004-08-30 17:19:47.000000000 +0200 -+++ modella1.5.7.fixed/modella_automa.c 2005-04-14 15:07:46.632785000 +0200 -@@ -618,6 +618,7 @@ void print_LBA(LBA* b,FILE* output){ - if(b->R[j]->source==i){ - fprintf(output,"%d ",b->R[j]->dest); - print_form_prefix(b->R[j]->label,output); -+ fputc('\n',output); - } - fprintf(output,"-1 "); - - - * The automata produced by Wring are translated to the syntax - understood by lbtt using `wring2lbtt' (by the same author of - Modella). wring2lbtt suffers from the same "lbtt syntax" - problem described above, you have to fix this too before it - can be used. - - Also wring2lbtt requires a Wring directory in the directory - where it is run; that makes it harder to use as a normal tool - from $PATH. I use the following wrapper in my $PATH to work - around this. - -#!/bin/sh -cd ~/src/wring2lbtt && ./wring2lbtt "$@" - - This is OK because the filenames supplied by lbtt are absolute. - - 2) ./configure Spot, and build it. - - During the configure process you should see lines such as - -checking for lbt... lbt -checking for ltl2ba... ltl2ba -checking for modella... modella -checking for script4lbtt.py... script4lbtt.py -checking for spin... spin -checking for wring2lbtt... wring2lbtt - - If some tool is not found, the corresponding tests will be disabled. - You can also use variables such as LBT, LTL2BA, MODELLA, LTL2NBA, - SPIN, and WRING2LBTT to specify the location of any of these scripts - if it is not in $PATH. For instance - - ./configure LTL2NBA=/home/adl/src/ltlnba/script4lbtt.py - - 3) Run `make' to build Spot. - - 4) cd into bench/ltl2tgba/ and execute any of - ./small - ./big - or ./known - - Alternatively running `make run' (in that directory) will run all - three scripts. If you have a multicore processor, you may want - to run `make -j3 run' to run these three scripts in parallel. - None of the tested translators use more than one core. - - 5) Wait... - ======================= Reading the summaries ======================= -The files small.txt, big.txt, and known.txt contain a summary of the -results. Each algorithm is described on two lines formated as -follows. +The various outputs (CSV, JSON, our LaTeX) may use the following +column headers: - 10: Spot FM (degen) - 831 2422 188 | 521 157 | 3.01 | 165971 8723693 (188) +* 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 first line presents the name of the algorithm ("Spot FM (degen)") -and its number for lbtt (10). The number is useless. In this -example, "FM (degen)" means that the Couvreur/FM algorithm is used to -translate LTL formula into a TGBA that is then DEGENeralized, so you -effectively get a Büchi automaton, which you can compare with that -automata produced by other tools. You may want to look in the file -`algorithms' to see which options are used for each name, if the -naming is unclear. +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). -The second line display 9 values: - 1. the total number of states of all generated automata (831) - 2. the total number of transitions of all generated automata (2422) - 3. the total number of acceptance conditions of all generated automata (188) - 4. the total number of nondeterministic states in these automata (521) - 5. the total number of automata with some nondeterminisitic state (157) - 6. the cumulated translation time in seconds (3.01) - 7. the total number of states in the synchronized products (165971) - 8. the total number of transitions in the synchronized products (8723693) - 9. the number of translated formulae (188) +For all these values (except count), the sammler number the better. -For all these values (but the last!) the smaller number the better. -Notes: - - * Small translation times are not accurate because: - - a) most of the translators are run through scripts that translate - their input from and their output to the format understood by - lbtt. For fast translators, most of the time is spent through - these wrappers. (For instance Spot's ltl2tgba is run through - lbtt-translate, and depending on how Spot has been configured - w.r.t. to dynamic libraries, ltl2tgba itself is often a shell - script that run the real binary with the locally built libraries.) - - b) LBTT use the time() function to measure time, which usually - has only a 0.01s resolution. Multiply this 0.01s by the number - for formulae to get the possible error (e.g. for the above example - 188*0.01 = 1.88s, so the 3.01s should be interpreted as "within - 3.01-1.88 and 3.01+1.88). - - * Some tools will appear to have translated fewer automata than the - others. This normally indicates bugs in the translator (incorrect - output) or timeouts. In that case it is harder to compare the - results. (Normalizing the other values accordingly may not be - fair: maybe the translator precisely failed to translate the - largest automata.) +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 diff --git a/bench/ltl2tgba/algorithms b/bench/ltl2tgba/algorithms index 0f19b8891..f12f87f58 100644 --- a/bench/ltl2tgba/algorithms +++ b/bench/ltl2tgba/algorithms @@ -1,97 +1,30 @@ -cat >"$conffile" <%N" +test -n "$LTL2BA" && set "$@" "$LTL2BA -f %s >%N" +test -n "$LTL3BA" && set "$@" "$LTL3BA -f %s >%N" \ + "$LTL3BA -M -f %s >%N" \ + "$LTL3BA -S -f %s >%N" \ + "$LTL3BA -S -M -f %s >%N" -Algorithm -{ - Name = "ltl3ba -M" - Path = "lbtt-translate" - Parameters = "--spin '$LTL3BA -M'" - Enabled = $HAVE_LTL3BA -} +# Use -s to output a neverclaim, like the other tools. +set "$@" "$LTL2TGBA --det -s %s >%N" \ + "$LTL2TGBA --small -s %s >%N" -Algorithm -{ - Name = "ltl3ba -S" - Path = "lbtt-translate" - Parameters = "--spin '$LTL3BA -S'" - Enabled = $HAVE_LTL3BA -} - -Algorithm -{ - Name = "ltl3ba -M -S" - Path = "lbtt-translate" - Parameters = "--spin '$LTL3BA -M -S'" - Enabled = $HAVE_LTL3BA -} - -Algorithm -{ - Name = "Modella" - Path = "$MODELLA" - Parameters = "-o1 -g -e -r12" - Enabled = $HAVE_MODELLA -} - -Algorithm -{ - Name = "Wring (RewRule+BoolOpt+AutSempl), degen" - Path = "$WRING2LBTT" - Parameters = "-d --5" - Enabled = $HAVE_WRING2LBTT -} - -Algorithm -{ - Name = "Wring (RewRule+BoolOpt+AutSempl)" - Path = "$WRING2LBTT" - Parameters = "--5" - Enabled = $HAVE_WRING2LBTT -} - -Algorithm -{ - Name = "NBA" - Path = "$LTL2NBA" - Enabled = $HAVE_LTL2NBA -} -EOF +# If you want to add your own tool, you can add it here. +# See 'man ltlcross' for the list of %-escape you may use +# to specify input formula and output automaton. +# +# set "$@" "tool options %... > %..." -for type in tgba ba; do - for pref in any deterministic small; do - for level in high; do - cat >>$conffile <. . ./defs - -conffile=big.cfg -logfile=big.log -sumfile=big.txt - . "$srcdir/algorithms" -cat >>"$conffile" <&1 | tee big.log diff --git a/bench/ltl2tgba/defs.in b/bench/ltl2tgba/defs.in index 311577e00..3abaa021a 100644 --- a/bench/ltl2tgba/defs.in +++ b/bench/ltl2tgba/defs.in @@ -1,5 +1,5 @@ # -*- mode: shell-script; coding: utf-8 -*- -# Copyright (C) 2012 Laboratoire de Recherche et Développement +# Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -36,8 +36,8 @@ test -f "$srcdir/defs.in" || { top_builddir="@top_builddir@" LBT="@LBT@" -LBTT="@LBTT@" -LBTT_TRANSLATE="@LBTT_TRANSLATE@" +LTLCROSS="$top_builddir/src/bin/ltlcross@EXEEXT@" +RANDLTL="$top_builddir/src/bin/randltl@EXEEXT@" LTL2BA="@LTL2BA@" LTL3BA="@LTL3BA@" LTL2NBA="@LTL2NBA@" @@ -45,17 +45,3 @@ LTL2TGBA="@top_builddir@/src/bin/ltl2tgba@EXEEXT@" MODELLA="@MODELLA@" SPIN="@SPIN@" WRING2LBTT="@WRING2LBTT@" - -($LBTT --version) >/dev/null 2>&1 || { - echo "$LBTT not available. Try configuring with --with-included-lbtt." - exit 77 -} - -for var in LBT LTL2BA LTL3BA LTL2NBA MODELLA SPIN WRING2LBTT -do - if eval 'test -z "$'$var'"'; then - eval HAVE_$var=no - else - eval HAVE_$var=yes - fi -done diff --git a/bench/ltl2tgba/formulae.ltl b/bench/ltl2tgba/formulae.ltl index bd8036772..bbd761c3b 100644 --- a/bench/ltl2tgba/formulae.ltl +++ b/bench/ltl2tgba/formulae.ltl @@ -1,42 +1,3 @@ -U p0 p1 -U p0 U p1 p2 -V ! p0 V ! p1 ! p2 -| U t V f ! p0 V f U t p1 -U U t p0 V f p1 -U V f p0 p1 -& & U t U t p0 V f ! p0 & U t p0 V f V f ! p0 -& V f U t p0 U t V f ! p1 -| & V f U t p0 U t V f ! p1 & V f U t p1 U t V f ! p0 -V p0 | p0 p1 -| U X p0 X p1 X V ! p0 ! p1 -| U X p0 p1 X V ! p0 | ! p0 ! p1 -& V f | ! p0 U t p1 | U X p0 p1 X V ! p0 | ! p0 ! p1 -& V f | ! p0 U t p1 | U X p0 X p1 X V ! p0 ! p1 -V f | ! p0 U t p1 -U t & p0 X U ! p1 ! p2 -& U t V f ! p0 V f U t ! p1 -V f & U t p0 U t p1 -& U t p0 U t ! p0 -V & X p1 p2 X U V U p3 p0 p2 V p3 p2 -| | & V f | p1 V f U t p0 V f | p2 V f U t ! p0 V f p1 V f p2 -| | & V f | p1 U t V f p0 V f | p2 U t V f ! p0 V f p1 V f p2 -& & | U t & ! p1 U t V f ! p0 U t & ! p2 U t V f p0 U t ! p1 U t ! p2 -& & | U t & ! p1 V f U t ! p0 U t & ! p2 V f U t p0 U t ! p1 U t ! p2 -& V f | p1 X V f p0 V f | p2 X V f ! p0 -V f | p1 & X p0 X ! p0 -| U p0 p0 U p1 p0 -U p0 & p1 V f p2 -U p0 & p1 X U p2 p3 -U p0 & p1 X & p2 U t & p3 X U t & p4 X U t & p5 X U t p6 -U t & p0 X V f p1 -U t & p0 X & p1 X U t p2 -U t & p0 X U p1 p2 -| U t V f p0 U t V f p1 -V f | ! p0 U p1 p2 -U t & p0 X U t & p1 X U t & p2 X U t p3 -& & & & V f U t p0 V f U t p1 V f U t p2 V f U t p3 V f U t p4 -| | U p0 U p1 p2 U p1 U p2 p0 U p2 U p0 p1 -V f | ! p0 U p1 | V f p2 V f p3 [](!p0) <>p1 -> (!p0 U p1) [](p2 -> [](!p0)) @@ -92,3 +53,40 @@ V f | ! p0 U p1 | V f p2 V f p3 [] (p2 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U (p1 | [] (p0 -> (p3 & !p5 & X(!p5 U p4))))) !p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0) <>p2 -> (!p2 U (p2 & (!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0)))) +p0 U p1 +p0 U (p1 U p2) +!p0 R (!p1 R !p2) +(1 U (0 R !p0)) | (0 R (1 U p1)) +(1 U p0) U (0 R p1) +(0 R p0) U p1 +(1 U p0) & (1 U (1 U p0)) & (0 R !p0) & (0 R (0 R !p0)) +(0 R (1 U p0)) & (1 U (0 R !p1)) +((0 R (1 U p0)) & (1 U (0 R !p1))) | ((0 R (1 U p1)) & (1 U (0 R !p0))) +p0 R (p0 | p1) +(Xp0 U Xp1) | X(!p0 R !p1) +(Xp0 U p1) | X(!p0 R (!p0 | !p1)) +(0 R (!p0 | (1 U p1))) & ((Xp0 U p1) | X(!p0 R (!p0 | !p1))) +(0 R (!p0 | (1 U p1))) & ((Xp0 U Xp1) | X(!p0 R !p1)) +0 R (!p0 | (1 U p1)) +1 U (p0 & X(!p1 U !p2)) +(1 U (0 R !p0)) & (0 R (1 U !p1)) +0 R ((1 U p0) & (1 U p1)) +(1 U p0) & (1 U !p0) +(Xp1 & p2) R X(((p3 U p0) R p2) U (p3 R p2)) +((0 R (p1 | (0 R (1 U p0)))) & (0 R (p2 | (0 R (1 U !p0))))) | (0 R p1) | (0 R p2) +((0 R (p1 | (1 U (0 R p0)))) & (0 R (p2 | (1 U (0 R !p0))))) | (0 R p1) | (0 R p2) +(0 R (p1 | X(0 R p0))) & (0 R (p2 | X(0 R !p0))) +0 R (p1 | (Xp0 & X!p0)) +p0 | (p1 U p0) +p0 U (p1 & (0 R p2)) +p0 U (p1 & X(p2 U p3)) +p0 U (p1 & X(p2 & (1 U (p3 & X(1 U (p4 & X(1 U (p5 & X(1 U p6))))))))) +1 U (p0 & X(0 R p1)) +1 U (p0 & X(p1 & X(1 U p2))) +1 U (p0 & X(p1 U p2)) +(1 U (0 R p0)) | (1 U (0 R p1)) +0 R (!p0 | (p1 U p2)) +1 U (p0 & X(1 U (p1 & X(1 U (p2 & X(1 U p3)))))) +(0 R (1 U p0)) & (0 R (1 U p1)) & (0 R (1 U p2)) & (0 R (1 U p3)) & (0 R (1 U p4)) +(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1)) +0 R (!p0 | (p1 U ((0 R p2) | (0 R p3)))) diff --git a/bench/ltl2tgba/known b/bench/ltl2tgba/known index 9fd17230b..ff20c72e6 100755 --- a/bench/ltl2tgba/known +++ b/bench/ltl2tgba/known @@ -1,10 +1,7 @@ #!/bin/sh # -*- shell-script -*- -# Copyright (C) 2011 Laboratoire de Recherche et Developpement de +# Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement de # l'Epita (LRDE) -# Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. # # This file is part of Spot, a model checking library. # @@ -22,43 +19,7 @@ # along with this program. If not, see . . ./defs - -conffile=known.cfg -logfile=known.log -sumfile=known.txt -ltlfile=$srcdir/formulae.ltl - . "$srcdir/algorithms" -cat >>"$conffile" <&1 | +tee known.log diff --git a/bench/ltl2tgba/lbtt2csv.pl b/bench/ltl2tgba/lbtt2csv.pl deleted file mode 100755 index 28f5e0249..000000000 --- a/bench/ltl2tgba/lbtt2csv.pl +++ /dev/null @@ -1,132 +0,0 @@ -#! /usr/bin/perl -w - -# Copyright (C) 2012 Laboratoire de Recherche et Développement de -# l'Epita. -# -# This file is part of Spot, a model checking library. -# -# Spot is free software; you can redistribute it and/or modify it -# under the terms of the GNU General Public License as published by -# the Free Software Foundation; either version 3 of the License, or -# (at your option) any later version. -# -# Spot is distributed in the hope that it will be useful, but WITHOUT -# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -# License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . - - -# This script reads the output of the files "*.log" given in arguments -# and output it in a csv format on stdout. -# If you give the option `-p' as the first argument of this program, -# you'll get only the positive formulae, while `-n' gives the negative -# ones. If you give several of them, you'll get only the last you asked for. -# -# As an example: "./lbtt2csv.pl -n -n -p -n -p foo.log" will output only -# the positive formulae. - - -use strict; - -our $no_positive = undef; -our $no_negative = undef; - -# Get a block and return the number of states, transition of the -# automaton and of the product, and the time too. -sub work_on_formula_in_algo($) -{ - my ($content) = @_; - - my ($states) = ($$content =~ /number of states:\s+(\d+?)\n/ms); - my ($tr) = ($$content =~ /number of transitions:\s+(\d+)\n/ms); - my ($acc_set) = ($$content =~ /acceptance sets:\s+(\d+)\n/ms); - my ($det) = ($$content =~ /is deterministic:\s+(\w+)\n/ms); - my ($nb_det) = ($$content =~ /nondeterminism index:\s+(\d+)\n/ms); - my ($time) = ($$content =~ /time:\s+(\d+\.\d+)/ms); - $$content = $'; #' - - my ($product_st) = ($$content =~ /number of states:\s+(\d+)/ms); - my ($product_tr) = ($$content =~ /number of transitions:\s+(\d+)\n/ms); - - $$content =~ /Negated formula:\n/ms; - $$content = $'; #' - - return ($states, $tr, $acc_set, $det, - $nb_det, $time, $product_st, $product_tr); -} - - -# Take a string which starts with the line " XX: `Algo Name'" and -# contains all algorithm block. Then it prints all the information -# wanted in its block, for the positive and negated formula. -sub work_on_algorithm($$) -{ - my ($content, $formula) = @_; - - my ($nb) = ($content =~ /(\d+?):[^\n]+/ms); - $content = $'; #' - - # Get the number of state and transition of the automaton and the - # product and the computation time. - my ($states, $tr, $acc_set, $det, $nb_det, $time, $product_st, $product_tr) - = work_on_formula_in_algo(\$content); - - print "\"$formula\",$nb,$states,$tr,$acc_set,$det,$nb_det," - . "$time,$product_st,$product_tr\n" unless defined $no_positive; - - # Now let's repeat with the negated formula. - ($states, $tr, $acc_set, $det, $nb_det, $time, $product_st, $product_tr) - = work_on_formula_in_algo(\$content); - - print "\"! $formula\",$nb,$states,$tr,$acc_set,$det,$nb_det," - . "$time,$product_st,$product_tr\n" unless defined $no_negative; -} - -# Take a string which is a concatenation of the lines of a round. -# In fact, we received from "LTL formula..." to "...Model". -# So we have to clean a little before working. -sub work_on_whole_round($) -{ - my ($round) = @_; - - $round =~ s/ parse tree.*?\n//ms; - - $round =~ /.*?\n\s+formula:\s+(.*?)\n/ms; - my $formula = $1; - $round = $'; #' - - - - $round =~ s{\n\n(.*?)(?=\n\n)}< - work_on_algorithm ($1, $formula); - >gse; -} - -while ($ARGV[0] eq '-n' or $ARGV[0] eq '-p') -{ - $no_negative = undef; - $no_positive = undef; - $no_negative = "true" if $ARGV[0] eq '-p'; - $no_positive = "true" if $ARGV[0] eq '-n'; - shift; -} - -my $round_re = qr/LTL formula:.*?Model/sm; - -local $/ = undef; -while (my $content = <>) -{ - # The content starting with "Round 1" and ending before the - # "Statistics after round ...". - $content =~ /Round/m; - $content = "Round" . $'; #' - $content =~ /Statistics after round /m; - $content = $`; - - $content =~ s<$round_re>< - work_on_whole_round($&); - >gse; -} diff --git a/bench/ltl2tgba/ltl2baw.in b/bench/ltl2tgba/ltl2baw.in deleted file mode 100644 index e0c5f6de8..000000000 --- a/bench/ltl2tgba/ltl2baw.in +++ /dev/null @@ -1,222 +0,0 @@ -#!/usr/bin/env @PERL@ - -# Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. -# -# This file is part of Spot, a model checking library. -# -# Spot is free software; you can redistribute it and/or modify it -# under the terms of the GNU General Public License as published by -# the Free Software Foundation; either version 3 of the License, or -# (at your option) any later version. -# -# Spot is distributed in the hope that it will be useful, but WITHOUT -# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -# License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . - -use warnings; - -# Usage: -# ------ -# -# This script converts the intermediate generalized automata computed -# by ltl2ba into a form usable by lbtt. This is useful for statistics. -# -# It can also be used to simplify a formula using ltl2ba, and then hand -# the simplified formula over to spot. (This can be used to compare -# Spot's formulae simplification and ltl2ba's.) -# -# ltl2baw.pl --ltl2ba='options-A' options-B -# run `ltl2ba options-B', extract the optimized generalized automata, -# and pass this automata to `ltl2tgba options-A'. -# e.g., ltl2baw.pl --ltl2ba=-t -f 'a U b' -# will convert ltl2ba's generalized automata for `a U b' into -# a form readable by lbtt. -# -# ltl2baw.pl options-B -# this is a shorthand for `ltl2baw.pl --ltl2ba=-t options-B', -# e.g., ltl2baw.pl -f 'a U b' -# -# ltl2baw.pl --spot='options-A' options-B -# run `ltl2ba options-B', extract the simplified formula -# and pass this formula to `ltl2tgba options-A'. -# e.g., ltl2baw.pl ---spot=-f -f '(a U b) <-> true' -# will use the Couvreur/FM algorithm to translate the formula -# simplified by ltl2ba -# -# The initial state problem: -# -------------------------- -# ltl2ba create a Transition-based Generalized Büchi Automaton in one -# of its intermediate steps. Unlike Spot's TGBAs, ltl2ba's TGBAs can -# have multiple initial state. This is a problem when using lbtt, -# because lbtt accepts only one initial state. When we detect such a -# situation, we create a new state whose successors are the union of -# the successors of all the initial states, and use this new state as -# initial state. Then we try to remove the original initial states: -# we can do this for states that have no input transition. - -use constant { - PROLOGUE => 1, - INIT_STATES => 2, - STATES => 3, - EPILOGUE => 4, -}; - -sub dquote(@) -{ - return map { "\"$_\"" } @_; -} - -my $arg = $ARGV[0]; -my $output_formula = 0; - -if ($arg =~ '^--ltl2ba=(.*)$') - { - open(LTL2TGBA, "| @top_builddir@/src/tgbatest/ltl2tgba $1 -X -"); - shift; - } -elsif ($arg =~ '--spot=(.*)$') - { - $output_formula = 1; - open(LTL2TGBA, "| @top_builddir@/src/tgbatest/ltl2tgba $1 -F -"); - shift; - } -else - { - open(LTL2TGBA, "| @top_builddir@/src/tgbatest/ltl2tgba -t -X -"); - } - -END { - # This also waits for ltl2tgba's termination. - close(LTL2TGBA) || die "error closing pipe to ltl2tgba"; -} - -my @args = dquote @ARGV; -open(LTL2BA, "@LTL2BA@ -d @args |") || die "failed to run ltl2ba"; - -my $state = PROLOGUE; - -my @init_states = (); -my $current_state; -my %states; -my %dests; -my %acc; -my $normalized; - -while () - { - chomp; - # print "$state: $_\n"; - if ($state == PROLOGUE) - { - $normalized = $1 - if m,Normlzd:\s*(.*?)\s*\*/,; - $state = INIT_STATES - if /Generalized Buchi automaton after simplification/; - } - elsif ($state == INIT_STATES) - { - next if /^init\s*:/; - if (/^\s*\d+\s*$/) - { - my $n = scalar($&); - push @init_states, $n; - $dests{$n} = 0; - } - else - { - $state = STATES; - } - } - # Not an elif. - if ($state == STATES) - { - if (/^state\s+(\d+)/) - { - $current_state = scalar($1); - } - elsif (/^(.+)\s+->\s+(\d+)\s+:\s+{(.*)}\s*$/) - { - my ($cond, $dest, $acc) = ($1, $2, $3); - ++$dests{$dest} if exists $dests{$dest}; - my @acc = dquote(split(',', $acc)); - $acc{$_} = 1 foreach (@acc); - push @{$states{$current_state}}, [$dest, $cond, "@acc"]; - } - else - { - $state = EPILOGUE; - } - } - } - -die "parse error ($state)\n" - unless $state == EPILOGUE; - -sub print_state($) -{ - my ($src) = @_; - foreach my $v (@{$states{$src}}) - { - my ($dst, $cond, $acc) = @$v; - print LTL2TGBA "\"$src\", \"$dst\", \"$cond\", $acc;\n"; - } -} - -if ($output_formula) - { - print LTL2TGBA $normalized; - } -else - { - print LTL2TGBA "acc = @{[keys %acc]};\n"; - - if ($#init_states > 0) - { - # Create a fake initial state, and try to remove the old ones. - # See the `The initial state problem' summary at the top of - # this file. - @succ = map { - my @out = @{$states{$_}}; - delete $states{$_} if $dests{$_} == 0; - @out; - } @init_states; - @init_states = ('init'); - $states{'init'} = \@succ; - } - elsif ($#init_states < 0) - { - print LTL2TGBA "\"false\", \"false\", \"false\", ;"; - exit 0; - } - my $s = $init_states[0]; - print_state($s); - delete $states{$s}; - - foreach my $src (keys %states) - { - print_state($src); - } - } - -### Setup "GNU" style for perl-mode and cperl-mode. -## Local Variables: -## perl-indent-level: 2 -## perl-continued-statement-offset: 2 -## perl-continued-brace-offset: 0 -## perl-brace-offset: 0 -## perl-brace-imaginary-offset: 0 -## perl-label-offset: -2 -## cperl-indent-level: 2 -## cperl-brace-offset: 0 -## cperl-continued-brace-offset: 0 -## cperl-label-offset: -2 -## cperl-extra-newline-before-brace: t -## cperl-merge-trailing-else: nil -## cperl-continued-statement-offset: 2 -## End: diff --git a/bench/ltl2tgba/parseout.pl b/bench/ltl2tgba/parseout.pl deleted file mode 100755 index 9f7d49040..000000000 --- a/bench/ltl2tgba/parseout.pl +++ /dev/null @@ -1,91 +0,0 @@ -#!/usr/bin/env perl - -# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement de -# l'Epita. -# Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. -# -# This file is part of Spot, a model checking library. -# -# Spot is free software; you can redistribute it and/or modify it -# under the terms of the GNU General Public License as published by -# the Free Software Foundation; either version 3 of the License, or -# (at your option) any later version. -# -# Spot is distributed in the hope that it will be useful, but WITHOUT -# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -# License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . - -use warnings; - -my $line = 0; -my $tool = 0; -my ($a, $b, $acc, $time, $det, $ndindex); - -my $prefix = 'All formulae'; -$prefix = 'Pos. formulae' if $ARGV[0] eq '-p'; -$prefix = 'Neg. formulae' if $ARGV[0] eq '-n'; -shift if $ARGV[0] eq '-n' or $ARGV[0] eq '-p'; - -sub sep($) -{ - $n = shift; - $n =~ s/(\d{1,3}?)(?=(\d{3})+$)/$1\\,/g; - return $n; -} - -format STDOUT3 = -@<<<<<<<<<<<<<<<<<<<<< & @>>>>>> & @>>>>>> & @>>>>>> & @>> & @>>>>>>>>> & @>>>>>>>>>>> \\ % @>> -$tool, sep($a), sep($b), sep($ndindex), sep($1-$det), sep($2), sep($3), sep($1) -. - -format STDOUT2 = -||<:>@>>||@<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<||<)>@>>>>>||<)>@>>>>>||<)>@>>>||<)>@#####.##||<)>@>>>>>>>>||<)>@>>>>>>>>||<)>@>>|| -$num, $tool, $a, $b, $acc, $time, $2, $3, $1 -. - -format STDOUT = -@>>: @<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<< -$num, $tool - @>>>>> @>>>>> @>>> | @>>>>> @>> | @#####.## | @>>>>>>>> @>>>>>>>> (@>>) -$a, $b, $acc, $ndindex, $1-$det, $time, $2, $3, $1 -. - -$~ = STDOUT2 if (exists $ENV{'WIKIOUTPUT'}); -$~ = STDOUT3 if (exists $ENV{'LATEXOUTPUT'}); - -my %impl; - -while (<>) -{ - last if /^ Failures to compute/; - - if (/^\s{4}(\d+):\s`(.+)'\s*(?:\(disabled\))?\s*$/) - { - $impl{$1} = $2 unless exists $impl{$1}; - } - if (/$prefix\s*\|\s*([^|\s]*)\s*\|\s*([^|\s]*)\s*\|\s*([^|\s]*)\s*\|\s*([^|\s]*)\s*\|$/o) - { - $acc = $1; - $time = $2 || 0; - $det = $3 || 0; - $ndindex = $4; - } - next unless /$prefix\s+\|\s*([^|\s]*)\s*\|\s*([^|\s]*)\s*\|\s*([^|\s]*)\s*\|$/o; - if ($line % 2) - { - $num = $line >> 1; - $tool = $impl{$num}; - write; - } - else - { - ($a, $b) = ($2, $3); - } - ++$line; -} diff --git a/bench/ltl2tgba/small b/bench/ltl2tgba/small index b1ff44d1b..e242d44ee 100755 --- a/bench/ltl2tgba/small +++ b/bench/ltl2tgba/small @@ -1,10 +1,7 @@ #!/bin/sh # -*- shell-script -*- -# Copyright (C) 2011 Laboratoire de Recherche et Developpement de +# Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement de # l'Epita (LRDE) -# Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. # # This file is part of Spot, a model checking library. # @@ -22,58 +19,7 @@ # along with this program. If not, see . . ./defs - -conffile=small.cfg -logfile=small.log -sumfile=small.txt - . "$srcdir/algorithms" -cat >>"$conffile" <&1 | tee small.log diff --git a/bench/ltl2tgba/sum.py b/bench/ltl2tgba/sum.py new file mode 100755 index 000000000..edc5eac3b --- /dev/null +++ b/bench/ltl2tgba/sum.py @@ -0,0 +1,130 @@ +#!/usr/bin/env python3 +import json +import argparse + +def latex_escape_char(ch): + if ch in '#$%&_{}': + return '\\' + ch + elif ch in '~^': + return '\\' + ch + '{}' + elif ch == '\\': + return '\\textbackslash' + else: + return ch + +def latex_escape(x): + if type(x) == str: + return ''.join(latex_escape_char(ch) for ch in x) + return map(latex_escape, x) + +def rot(x): + if type(x) == str: + return '\\rot{' + x + '}' + return map(rot, x) + + +def process_file(filename): + data = json.load(open(filename)) + + ncols = len(data['fields']) + ntools = len(data['tools']) + datacols = range(2, ncols) + fields = { name:index for index,name in enumerate(data["fields"]) } + toolcol = fields['tool'] + inputcol = fields['input'] + + # Index results by tool, then input + results = { t:{} for t in range(0, ntools) } + for l in data["results"]: + results[l[toolcol]][l[inputcol]] = l + + for i in range(0, ntools): + # Remove any leading directory, and trailing %... + name = data["tools"][i] + name = name[name.rfind('/', 0, name.find(' ')) + 1:] + data["tools"][i] = latex_escape(name[0:name.find('%')]) + + print(r''' +\section*{\texttt{%s}} +\subsection*{Cumulative summary}''' % filename) + + print('\\begin{tabular}{l' + ('r' * (ncols - 1)) + '}\n', + " & ".join(rot(latex_escape(["tool", "count"] + data["fields"][2:]))), + "\\\\") + for i in range(0, ntools): + # Compute sums over each column. + sums = [("%6.2f" if j == 9 else "%6d") % + (sum([x[j] for x in results[i].values()])) + for j in datacols] + print("\\texttt{%-18s} & %3d & " + % (data["tools"][i], len(results[i])), " & ".join(sums), "\\\\") + print(r'\end{tabular}') + + print(r'''\subsection*{Cross comparison} + +How many times did the left tool produce an automaton strictly bigger +than the top tool? Bigger means more states, or equal number of +states and more transitions. + +''') + + header = '\\begin{tabular}{l' + for i in data["tools"]: + header += 'c' + header += '}' + + statescol = fields['states'] + transcol = fields['transitions'] + + print(header) + for left in data["tools"]: + print("&", rot("\\texttt{%s}" % left), end=' ') + print(r'\\') + for left in range(0, ntools): + print("\\texttt{%-18s}" % data["tools"][left], end=' ') + for top in range(0, ntools): + x = 0 + for k,ct in results[top].items(): + if k in results[left]: + cl = results[left][k] + if (cl[statescol] > ct[statescol] + or (cl[statescol] == ct[statescol] + and cl[transcol] > ct[transcol])): + x += 1 + print("&", x, end=' ') + print(r"\\") + print(r'\end{tabular}') + + +def main(): + p = argparse.ArgumentParser(description="Process ltlcross' output", + epilog="Report bugs to .") + p.add_argument('filenames', + help="name of the JSON file to read", + nargs='+') + p.add_argument('--intro', + help="introductory text for the LaTeX output", + default='') + args = p.parse_args() + + print(r'''\documentclass{article} +\usepackage[a4paper,landscape,margin=2cm]{geometry} +\usepackage{adjustbox} +\usepackage{array} + +\newcolumntype{R}[2]{% + >{\adjustbox{angle=#1,lap=\width-(#2)}\bgroup}% + l% + <{\egroup}% +} +\newcommand*\rot{\multicolumn{1}{R{45}{1em}}}% no optional argument here, please! + +\begin{document} +''') + print(args.intro) + for filename in args.filenames: + process_file(filename) + print(r'\end{document}') + + +main() diff --git a/configure.ac b/configure.ac index b7633d0bd..f22cea840 100644 --- a/configure.ac +++ b/configure.ac @@ -1,5 +1,5 @@ -# Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de +# Recherche et Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), Université # Pierre et Marie Curie. @@ -171,8 +171,6 @@ AC_CONFIG_FILES([ wrap/python/tests/Makefile tools/x-to-1 ]) -AC_CONFIG_FILES([bench/ltl2tgba/ltl2baw.pl:bench/ltl2tgba/ltl2baw.in], - [chmod +x bench/ltl2tgba/ltl2baw.pl]) AC_CONFIG_FILES([doc/dot], [chmod +x doc/dot]) AC_CONFIG_FILES([wrap/python/tests/run], [chmod +x wrap/python/tests/run]) AC_OUTPUT