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

fix python/dca.test for VPATH builds

Browse source 
* tests/python/dca.test: Do not assume the run script is in the source
directory.
This commit is contained in:
Alexandre Duret-Lutz 2017-11-22 09:49:03 +01:00
parent 61602a3bba
commit cc00898514
1 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

19
tests/python/dca.test
View file

@ -23,7 +23,10 @@ set -e
# Skip this test if ltl2dstar is not installed. # Skip this test if ltl2dstar is not installed.
(ltl2dstar --version) || exit 77 (ltl2dstar --version) || exit 77
cat >ba_formulas << 'EOF' DIR=dca.dir
mkdir -p $DIR
cat >$DIR/ba_formulas << 'EOF'
FG((Xc & XXa) <-> !(b xor (c M b))) FG((Xc & XXa) <-> !(b xor (c M b)))
F!FGFb F!FGFb
XF(b & Ga) XF(b & Ga)
@ -40,7 +43,7 @@ XF((!c R a) W !Fb)
(!a <-> !(c <-> Gb)) M 1 (!a <-> !(c <-> Gb)) M 1
((0 R a) M c) M ((b xor Fb) M F(b -> a)) ((0 R a) M c) M ((b xor Fb) M F(b -> a))
EOF EOF
cat >dsa_formulas <<'EOF' cat >$DIR/dsa_formulas <<'EOF'
(!b U b) U X(!a -> Fb) (!b U b) U X(!a -> Fb)
1 U (a xor b) 1 U (a xor b)
X(!(!b | (a M b)) -> XXa) X(!(!b | (a M b)) -> XXa)
@ -48,11 +51,11 @@ X(!(!b | (a M b)) -> XXa)
F(XF!a & (Fb U !a)) F(XF!a & (Fb U !a))
EOF EOF
while read ba_f; do while read ba_f; do
$srcdir/../run "$srcdir/dca.py" "$ba_f" > ba ../run "$srcdir/dca.py" "$ba_f" > ba
while read dsa_f; do while read dsa_f; do
ltldo -f "$dsa_f" "ltl2dstar --automata=streett\ ltldo -f "$dsa_f" "ltl2dstar --automata=streett\
--ltl2nba=spin:ltl2tgba@-Ds" -H | autfilt --product=ba > input.hoa --ltl2nba=spin:ltl2tgba@-Ds" -H | autfilt --product=ba > $DIR/input.hoa
autfilt --dca input.hoa > res.hoa autfilt --dca $DIR/input.hoa > $DIR/res.hoa
autfilt input.hoa --equivalent-to res.hoa autfilt $DIR/input.hoa --equivalent-to $DIR/res.hoa
done <dsa_formulas done <$DIR/dsa_formulas
done <ba_formulas done <$DIR/ba_formulas