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

ltltest: get rid of equals.cc

Browse source 
* src/ltltest/equals.cc: Delete.
* src/ltltest/Makefile.am: Adjust.
* src/ltltest/unabbrevwm.test: Rewrite using ltlfilt.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-09 23:18:55 +01:00
parent 6a2aad6259
commit c85ba787e8
3 changed files with 12 additions and 213 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ltltest/unabbrevwm.test
View file

@ -25,7 +25,12 @@
set -e
# This caused a segfault at some point
run 0 ../unabbrevwm \
'(!((G(p0)) U ((F(p0)) M ((F(X(p1))) & ((p2) W (G(p2))))))) M (F(p0))' \
'(Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2)))))))'
# Removing W,M in this formula caused a segfault at some point.
run 0 ../../bin/ltlfilt --remove-wm >out <<EOF
(!((G(p0)) U ((F(p0)) M ((F(X(p1))) & ((p2) W (G(p2))))))) M (F(p0))
(Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2)))))))
EOF
# The first formula will be simplified to the second, so after uniq
# the output should have one line.
test `uniq out | wc -l` = 1