diff --git a/NEWS b/NEWS index 446769524..846bda49d 100644 --- a/NEWS +++ b/NEWS @@ -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 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 - task in a more precise way thanks to %R, %[LETTER]R option. User time, - system time or children processing time or ... (see --help) can be - measured separately. A typical use-case is to exclude time spent - inside ltldo by keeping only time spent in each executed tool. + task in a more precise way thanks to %R, %[LETTER]R option. User + or system time, for children or parent, can be measured + separately. A typical use-case is "ltldo --stats='... %[c]R ...' + ..." 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: diff --git a/bin/ltldo.cc b/bin/ltldo.cc index 81cc3da33..1664704ae 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -66,7 +66,7 @@ static const argp_option options[] = 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 }, { "%T", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "tool used for translation", 0 }, @@ -262,7 +262,7 @@ namespace : runner(dict), post(post) { printer.add_stat('T', &cmdname); - printer.add_stat('R', &roundval); + printer.add_stat('#', &roundval); printer.add_stat('f', &inputf); } diff --git a/tests/core/ltldo.test b/tests/core/ltldo.test index c005288e9..5dab1e4a3 100755 --- a/tests/core/ltldo.test +++ b/tests/core/ltldo.test @@ -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 | 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 >expected <stderr && exit 1 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