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

ltldo: rename %R as %#

Browse source 
Fixes #189.

* bin/ltldo.cc: Here.
* tests/core/ltldo.test: Adjust and add test-case for %R.
* NEWS: Mention the change.
This commit is contained in:
Alexandre Duret-Lutz 2016-11-08 14:56:38 +01:00
parent 600b1f7e5c
commit 278b41f4bb
3 changed files with 20 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

15
NEWS
View file

@ -6,11 +6,18 @@ New in spot 2.1.2.dev (not yet released)
LTL over finite words) model checking to LTL model checking. This LTL over finite words) model checking to LTL model checking. This
is based on a transformation by De Giacomo & Vardi (IJCAI'13). is based on a transformation by De Giacomo & Vardi (IJCAI'13).
* "ltldo --stats=%R", which used to display the serial number of the
formula processed, was renamed to "ltldo --stats=%#" to free %R
for the following feature.
* autfilt, dstar2tgba, ltl2tgba, ltlcross, ltldo learned to time any * autfilt, dstar2tgba, ltl2tgba, ltlcross, ltldo learned to time any
task in a more precise way thanks to %R, %[LETTER]R option. User time, task in a more precise way thanks to %R, %[LETTER]R option. User
system time or children processing time or ... (see --help) can be or system time, for children or parent, can be measured
measured separately. A typical use-case is to exclude time spent separately. A typical use-case is "ltldo --stats='... %[c]R ...'
inside ltldo by keeping only time spent in each executed tool. ..." to measure the time spent in the tool ran by ltldo, excluding
that of ltldo. In all tools, the difference between %r
(wall-clock time) and %R (process time) can also be used to detect
unreliable measurements.
Library: Library:

4
bin/ltldo.cc
View file

@ -66,7 +66,7 @@ static const argp_option options[] =
static const argp_option more_o_format[] = static const argp_option more_o_format[] =
{ {
{ "%R", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, { "%#", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"serial number of the formula translated", 0 }, "serial number of the formula translated", 0 },
{ "%T", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, { "%T", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"tool used for translation", 0 }, "tool used for translation", 0 },
@ -262,7 +262,7 @@ namespace
: runner(dict), post(post) : runner(dict), post(post)
{ {
printer.add_stat('T', &cmdname); printer.add_stat('T', &cmdname);
printer.add_stat('R', &roundval); printer.add_stat('#', &roundval);
printer.add_stat('f', &inputf); printer.add_stat('f', &inputf);
} }

8
tests/core/ltldo.test
View file

@ -53,7 +53,7 @@ test "`echo 1,a,3,4 | ltldo -F-/2 ltl2tgba --stats='%<,%s,%>'`" = '1,2,3,4'
$genltl --and-gf=1..3 | $genltl --and-gf=1..3 |
run 0 $ltldo "{tgba}$ltl2tgba %f -H >%H" "{ba}$ltl2tgba >%N %f -s" \ run 0 $ltldo "{tgba}$ltl2tgba %f -H >%H" "{ba}$ltl2tgba >%N %f -s" \
--stats="%T,%R,%f,%s,%t,%e" >output --stats="%T,%#,%f,%s,%t,%e" >output
cat output cat output
cat >expected <<EOF cat >expected <<EOF
tgba,1,GFp1,1,2,2 tgba,1,GFp1,1,2,2
@ -146,3 +146,9 @@ grep ':.*empty input' stderr
$ltldo '{name} foo/bar/ltl2baextended' -f GFa 2>stderr && exit 1 $ltldo '{name} foo/bar/ltl2baextended' -f GFa 2>stderr && exit 1
grep 'error:.*foo/bar/ltl2baextended -f .*>.*' stderr grep 'error:.*foo/bar/ltl2baextended -f .*>.*' stderr
genltl --rv-counter=9 | ltldo ltl2tgba --stats='
print("%[up]R + %[uc]R + %[sp]R + %[sc]R - %R\n");
die if abs(%[up]R + %[uc]R + %[sp]R + %[sc]R - %R) > 0.02;' > code.pl
perl code.pl