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

bin: document %% for ltldo and ltlcross

Browse source 
I had no idea this was working...
Reported by Joachim Klein.

* src/bin/common_trans.cc: Document it.
* src/tests/ltlcross3.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2015-07-16 19:55:31 +02:00
parent a39ebcc8cc
commit 31f5ea75b2
2 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/bin/common_trans.cc
View file

@ -425,6 +425,7 @@ static const argp_option options[] =
{ "%O,%D", 0, 0, OPTION_DOC | OPTION_NO_USAGE, { "%O,%D", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the automaton is output as either (%O) HOA/never claim/LBTT, or (%D) " "the automaton is output as either (%O) HOA/never claim/LBTT, or (%D) "
"in LTL2DSTAR's format", 0 }, "in LTL2DSTAR's format", 0 },
{ "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 },
{ 0, 0, 0, 0, { 0, 0, 0, 0,
"If either %l, %L, or %T are used, any input formula that does " "If either %l, %L, or %T are used, any input formula that does "
"not use LBT-style atomic propositions (i.e. p0, p1, ...) will be " "not use LBT-style atomic propositions (i.e. p0, p1, ...) will be "

9
src/tests/ltlcross3.test
View file

@ -161,6 +161,11 @@ test 5 = `wc -l < out.csv`
check_csv out.csv check_csv out.csv
# Diagnose empty automata # Diagnose empty automata, and make sure %% is correctly replaced by %
run 1 ../../bin/ltlcross ': %f >%O' -f a 2>stderr run 1 ../../bin/ltlcross ': %f >%O; echo %%>foo' -f a 2>stderr
test 2 = `grep -c 'error: empty output.' stderr` test 2 = `grep -c 'error: empty output.' stderr`
cat foo
cat >expected<<EOF
%
EOF
diff foo expected