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

* src/tgbatest/ltlcross.test: More formulas from Joachim.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2014-08-21 23:06:33 +02:00
parent 408dc878e5
commit a72b84b0b4
1 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/tgbatest/ltlcross.test
View file

@ -25,8 +25,16 @@ ltl2tgba=../ltl2tgba
(
# A bug reported by Joachim Klein
echo 'G(Fa & ((a M b) U ((c U !d) M d)))'
# Some formulas supplied by Joachim Klein. The first two were
# incorrectly translated by ltl_to_tgba_fm(), while the other have
# shown some bugs in other translators.
cat <<EOF
G(Fa & ((a M b) U ((c U !d) M d)))
XF(p2 R (!Fp1 W p1))
X p0 || ((X p0) V <>p0)
p0 xor (p0 W X!p0)
p0 & (!p0 W Xp0)
EOF
# Random formulas
../../bin/randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15
) |