#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
# DÃ©veloppement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see .
# Check several options of ltlfilt
. ./defs || exit 1
set -e
ltlfilt=ltlfilt
checkopt()
{
cat >exp
run 0 $ltlfilt "$@" formulas > out
diff exp out
}
# The empty lines in the file are meant, we want to make sure that
# they are ignored.
cat >formulas < formulas2
mv formulas2 formulas
checkopt --ltl --from-ltlf=al <in < b) -> (c xor d)
EOF
cat >exp <out
diff exp out
cat >exp <(p0 || p2) && <>[](p0 || p2)
#define p0 (b)
#define p1 (a || c)
p0 && []<>p1 && <>[]p1
#define p0 (h || i)
#define p1 (d && e)
#define p2 (!c)
#define p3 (f)
p0 || []p1 || <>[](p2 || Xp3)
#define p0 ((c && !d) || (!c && d))
#define p1 ((a && !b) || (!a && b))
p0 || []p1
EOF
run 0 $ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out
diff exp out
cat >exp <(p0 || p2) && <>[](p0 || p2)
#define p0 (b)
#define p1 (a)
#define p2 (c)
p0 && []<>(p1 || p2) && <>[](p1 || p2)
#define p0 (h)
#define p1 (i)
#define p2 (d)
#define p3 (e)
#define p4 (c)
#define p5 (f)
p0 || p1 || [](p2 && p3) || <>[](!p4 || Xp5)
#define p0 (b)
#define p1 (e)
#define p2 (f)
#define p3 (g)
#define p4 (c)
p0 && p1 && (p2 || p3) && !Xp4
#define p0 (b)
#define p1 (a)
#define p2 (c)
p0 && []<>(p1 || p2) && ![]<>!(p1 || p2)
#define p0 (a)
#define p1 (b)
#define p2 (c)
#define p3 (d)
<>(p0 <-> p1) -> !(p2 <-> p3)
EOF
run 0 $ltlfilt -s -u --relabel=pnn --define in >out
diff exp out
toolong='((p2=0) * (p3=1))' # work around the 80-col check
cat >exp <out
diff exp out
run 0 $ltlfilt -0 in > out
perl -i -pe 's/\0/@\n/g' out
cat >exp < b) -> (c xor d)@
EOF
diff exp out
SPOT_STUTTER_CHECK=0 \
$ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
test $? = 2
grep 'non-LTL' stderr
SPOT_STUTTER_CHECK=555 \
$ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
test $? = 2
grep 'invalid' stderr
SPOT_STUTTER_CHECK=5 \
$ltlfilt --stutter-invariant -f '!{a:b*:c}'
# This one was incorrectly diagnosed as stutter invariant because of a
# bug in the bitvectors.
$ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1
$ltlfilt -c -o 'foo' -f a 2>stderr && exit 1
grep 'ltlfilt: options --output and --count are incompatible' stderr
out=`$ltlfilt -f 'G(a xor b) -> F(c <-> Xd)' --unabbreviate='^iF'`
exp='(1 U (c <-> Xd)) | !G!(a <-> b)'
test "$out" = "$exp"
$ltlfilt -f 'GF"a\"\\b"' > out
test "`cat out`" = 'GF"a\"\\b"'
$ltlfilt --lbt-input -f 'G F "a\"\\b"' -l > out
test "`cat out`" = 'G F "a\"\\b"'
$ltlfilt --size=foo=2..3 2>stderr && exit 1
grep 'invalid range.*should start with' stderr
cat >out < out.1
ltlfilt out/2 > out.2
diff out out.1
diff out out.2
true