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

org: document -0

Browse source 
* doc/org/ioltl.org: Add an example with xargs -0.
* src/bin/common_aoutput.hh (statistics): Do not print nullptr if %F is
empty.
This commit is contained in:
Alexandre Duret-Lutz 2015-05-11 19:53:41 +02:00
parent 2749702e75
commit 011a56846f
2 changed files with 31 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

34
doc/org/ioltl.org
View file

@ -146,13 +146,12 @@ used by [[http://www.ltl2dstar.de][ltl2dstar]].
All tools that output LTL/PSL formulas implement the following options: All tools that output LTL/PSL formulas implement the following options:
#+BEGIN_SRC sh :results verbatim :exports results #+BEGIN_SRC sh :results verbatim :exports results
ltlfilt --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d' genltl --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
-c, --count print only a count of matched formulas -0, --zero-terminated-output separate output formulas with \0 instead of \n
-n, --max-count=NUM output at most NUM formulas (for use with xargs -0)
-q, --quiet suppress all normal output
-8, --utf8 output using UTF-8 characters -8, --utf8 output using UTF-8 characters
--csv-escape quote the formula for use in a CSV file --csv-escape quote the formula for use in a CSV file
--format=FORMAT specify how each line should be output (default: --format=FORMAT specify how each line should be output (default:
@ -231,6 +230,33 @@ rm -f example-*.ltl
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
Option =-0= is useful if the list of formulas is passed to =xargs=.
=xargs= normally splits its input on white space (which are frequent
in LTL formulas), but you can use =xargs -0= to split the input on
null characters. So for instance the following two invocations have
nearly the same output:
#+BEGIN_SRC sh :results verbatim :exports both
genltl -0 --gh-q=1..4 | xargs -0 ltl2tgba --stats='%F,%f,%s'
genltl --gh-q=1..4 | ltl2tgba -F- --stats='%F,%f,%s'
#+END_SRC
#+RESULTS:
: ,Fp1 | Gp2,3
: ,(Fp1 | Gp2) & (Fp2 | Gp3),8
: ,(Fp1 | Gp2) & (Fp2 | Gp3) & (Fp3 | Gp4),18
: ,(Fp1 | Gp2) & (Fp2 | Gp3) & (Fp3 | Gp4) & (Fp4 | Gp5),42
: -,Fp1 | Gp2,3
: -,(Fp1 | Gp2) & (Fp2 | Gp3),8
: -,(Fp1 | Gp2) & (Fp2 | Gp3) & (Fp3 | Gp4),18
: -,(Fp1 | Gp2) & (Fp2 | Gp3) & (Fp3 | Gp4) & (Fp4 | Gp5),42
The only difference is that for the first command, =ltl2tgba= received
its formulas from the command-line arguments supplied by =xargs= (so
=%F= is empty as there is no input file), while in the second case the
formula where read from standard input (denoted by =-=).
# LocalWords: lbt LBT's filename UTF gfa GFa ltlfilt LBTT scheck # LocalWords: lbt LBT's filename UTF gfa GFa ltlfilt LBTT scheck
# LocalWords: utf associativity # LocalWords: utf associativity

2
src/bin/common_aoutput.hh
View file

@ -111,7 +111,7 @@ public:
const spot::ltl::formula* f, const spot::ltl::formula* f,
const char* filename, int loc, double run_time) const char* filename, int loc, double run_time)
{ {
filename_ = filename; filename_ = filename ? filename : "";
if (loc >= 0 && has('L')) if (loc >= 0 && has('L'))
{ {
std::ostringstream os; std::ostringstream os;