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

bin: add -0 option for LTL output

Browse source 
* src/bin/common_output.cc: Add option -0.
* src/tests/ltlfilt.test: Test it.
* NEWS: Document it.
This commit is contained in:
Alexandre Duret-Lutz 2015-05-11 17:17:15 +02:00
parent a44e1bf325
commit e026766219
3 changed files with 35 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/tests/ltlfilt.test
View file

@ -25,10 +25,12 @@
set -e
ltlfilt=../../bin/ltlfilt
checkopt()
{
cat >exp
run 0 ../../bin/ltlfilt "$@" formulas > out
run 0 $ltlfilt "$@" formulas > out
diff exp out
}
@ -168,7 +170,7 @@ p0 & GFp1 & FGp1
p0 | Gp1 | FG(p2 | Xp3)
EOF
run 0 ../../bin/ltlfilt -u --nnf --relabel-bool=pnn in >out
run 0 $ltlfilt -u --nnf --relabel-bool=pnn in >out
diff exp out
cat >exp <<EOF
@ -189,7 +191,7 @@ p0 && []<>p1 && <>[]p1
p0 || []p1 || <>[](p2 || Xp3)
EOF
run 0 ../../bin/ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out
run 0 $ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out
diff exp out
cat >exp <<EOF
@ -219,28 +221,40 @@ cat >exp <<EOF
#define p4 ((c=1))
(p0=1) * (p1=1) * ((p2=1) + (p3=1)) * (X(p4=0))
EOF
run 0 ../../bin/ltlfilt -p --wring -u --nnf --relabel=pnn --define in >out
run 0 $ltlfilt -p --wring -u --nnf --relabel=pnn --define in >out
diff exp out
run 0 $ltlfilt -0 in > out
perl -i -pe 's/\0/@\n/g' out
cat >exp <<EOF
a & c & Xb@
a & b & GF(a | c) & FG(a | c)@
b & GF(a | c) & FG(a | c)@
h | i | G(d & e) | FG(!c | Xf)@
b & e & (f | g) & !Xc@
b & GF(a | c) & !GF!(a | c)@
EOF
diff exp out
SPOT_STUTTER_CHECK=0 \
../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
$ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
test $? = 2
grep 'non-LTL' stderr
SPOT_STUTTER_CHECK=555 \
../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
$ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
test $? = 2
grep 'invalid' stderr
SPOT_STUTTER_CHECK=5 \
../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}'
$ltlfilt --stutter-invariant -f '!{a:b*:c}'
# This one was incorrectly diagnosed as stutter invariant because of a
# bug in the bitvectors.
../../bin/ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1
$ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1
../../bin/ltlfilt -c -o 'foo' -f a 2>stderr && exit 1
$ltlfilt -c -o 'foo' -f a 2>stderr && exit 1
grep 'ltlfilt: options --output and --count are incompatible' stderr
true