alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Adjust parseout.pl to the new LBTT output.

Browse source 
* bench/ltl2tgba/parseout.pl: Adjust to output nondeterministic
indices and number of nondeterministic automata.
* bench/ltl2tgba/README: Update explanations.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-21 13:46:44 +02:00
parent f2b188d9ec
commit faed4e8be2
2 changed files with 52 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

59
bench/ltl2tgba/README
View file

@ -128,38 +128,51 @@ checking for wring2lbtt... wring2lbtt
======================= =======================
The files small.txt, big.txt, and known.txt contain a summary of the The files small.txt, big.txt, and known.txt contain a summary of the
results. Each algorithm is described as two lines formated as results. Each algorithm is described on two lines formated as
follows. follows.
6: Spot FM (degen) 10: Spot FM (degen)
834 / 2419 / 188 / 2.86 166579 / 8749162 (188) 831 2422 188 | 521 157 | 3.01 | 165971 8723693 (188)
The first line presents the name of the algorithm ("Spot FM (degen)") The first line presents the name of the algorithm ("Spot FM (degen)")
and its number for lbtt (6). The number is useless. In this example, and its number for lbtt (10). The number is useless. In this
"FM (degen)" means that the Couvreur/FM algorithm is used to translate example, "FM (degen)" means that the Couvreur/FM algorithm is used to
LTL formula into a TGBA that is then DEGENeralized. You may want to translate LTL formula into a TGBA that is then DEGENeralized, so you
look in the file `algorithms' to see which options are used for each effectively get a Büchi automaton, which you can compare with that
name, if the naming is unclear. 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 second line display 7 values: The second line display 9 values:
1. the total number of states of all generated automata (834) 1. the total number of states of all generated automata (831)
2. the total number of transitions of all generated automata (2419) 2. the total number of transitions of all generated automata (2422)
3. the total number of acceptance conditions of all generated automata (188) 3. the total number of acceptance conditions of all generated automata (188)
4. the cumulated translation time in seconds (2.86) 4. the total number of nondeterministic states in these automata (521)
5. the total number of states in the synchronized products (166579) 5. the total number of automata with some nondeterminisitic state (157)
6. the total number of transitions in the synchronized products (8749162) 6. the cumulated translation time in seconds (3.01)
7. the number of translated formulae (188) 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 (but the last!) the smaller number the better.
Notes: Notes:
* Small translation times are not accurate because most of the * Small translation times are not accurate because:
translators are run through scripts that translate their input
from and their output to the format understood by lbtt. For fast a) most of the translators are run through scripts that translate
translators, most of the time is spent through these wrappers. their input from and their output to the format understood by
(For instance Spot's ltl2tgba is run through lbtt-translate, and lbtt. For fast translators, most of the time is spent through
depending on how Spot has been configured w.r.t. to dynamic these wrappers. (For instance Spot's ltl2tgba is run through
libraries, ltl2tgba itself is often a shell script that run the lbtt-translate, and depending on how Spot has been configured
real binary with the locally built libraries.) 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 * Some tools will appear to have translated fewer automata than the
others. This normally indicates bugs in the translator (incorrect others. This normally indicates bugs in the translator (incorrect

24
bench/ltl2tgba/parseout.pl
View file

@ -1,6 +1,6 @@
#!/usr/bin/env perl #!/usr/bin/env perl
# Copyright (C) 2011 Laboratoire de Recherche et Développement de # Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement de
# l'Epita. # l'Epita.
# Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -27,7 +27,11 @@ use warnings;
my $line = 0; my $line = 0;
my $tool = 0; my $tool = 0;
my ($a, $b, $acc, $time); 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';
sub sep($) sub sep($)
{ {
@ -37,8 +41,8 @@ sub sep($)
} }
format STDOUT3 = format STDOUT3 =
@<<<<<<<<<<<<<<<<<<<<< & @>>>>>> & @>>>>>> & @>>>>>>>>> & @>>>>>>>>>>> \\ % @>> @<<<<<<<<<<<<<<<<<<<<< & @>>>>>> & @>>>>>> & @>>>>>> & @>> & @>>>>>>>>> & @>>>>>>>>>>> \\ % @>>
$tool, sep($a), sep($b), sep($2), sep($3), sep($1) $tool, sep($a), sep($b), sep($ndindex), sep($1-$det), sep($2), sep($3), sep($1)
. .
format STDOUT2 = format STDOUT2 =
@ -49,8 +53,8 @@ $num, $tool, $a, $b, $acc, $time, $2, $3, $1
format STDOUT = format STDOUT =
@>>: @<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<< @>>: @<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
$num, $tool $num, $tool
@>>>>> / @>>>>> / @>>> / @#####.## @>>>>>>>> / @>>>>>>>> (@>>) @>>>>> @>>>>> @>>> | @>>>>> @>> | @#####.## | @>>>>>>>> @>>>>>>>> (@>>)
$a, $b, $acc, $time, $2, $3, $1 $a, $b, $acc, $ndindex, $1-$det, $time, $2, $3, $1
. .
$~ = STDOUT2 if (exists $ENV{'WIKIOUTPUT'}); $~ = STDOUT2 if (exists $ENV{'WIKIOUTPUT'});
@ -60,16 +64,20 @@ my %impl;
while (<>) while (<>)
{ {
last if /^ Failures to compute/;
if (/^\s{4}(\d+):\s`(.+)'\s*(?:\(disabled\))?\s*$/) if (/^\s{4}(\d+):\s`(.+)'\s*(?:\(disabled\))?\s*$/)
{ {
$impl{$1} = $2 unless exists $impl{$1}; $impl{$1} = $2 unless exists $impl{$1};
} }
if (/All formulae\s*\|\s*([^|]*?)\s*\|\s*([^|]*?)\s*\|$/) if (/$prefix\s*\|\s*([^|\s]*)\s*\|\s*([^|\s]*)\s*\|\s*([^|\s]*)\s*\|\s*([^|\s]*)\s*\|$/o)
{ {
$acc = $1; $acc = $1;
$time = $2 || 0; $time = $2 || 0;
$det = $3 || 0;
$ndindex = $4;
} }
next unless /All formulae\s+\|\s*(.*?)\s*\|\s*(.*?)\s*\|\s*(.*?)\s*\|/; next unless /$prefix\s+\|\s*([^|\s]*)\s*\|\s*([^|\s]*)\s*\|\s*([^|\s]*)\s*\|$/o;
if ($line % 2) if ($line % 2)
{ {
$num = $line >> 1; $num = $line >> 1;