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

tests: add some test to cover autcross' univ-edges removal

Browse source 
* tests/core/ltl3ba.test: Here.
This commit is contained in:
Alexandre Duret-Lutz 2023-07-27 09:48:00 +02:00
parent 95379c18cc
commit e1e9f960e6
1 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

11
tests/core/ltl3ba.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2016-2018, 2021 Laboratoire de Recherche et # Copyright (C) 2016-2018, 2021, 2023 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -47,8 +47,10 @@ GF(((a & Xb) | XXc) & Xd)
GF((b | Fa) & (b R Xb)) GF((b | Fa) & (b R Xb))
EOF EOF
randltl -n 30 2 randltl -n 30 2
) | ltlcross -D 'ltl3ba -H1' 'ltl3ba -H2' 'ltl3ba -H3' ltl2tgba \ ) > file.ltl
--ambiguous --strength --csv=output.csv
ltlcross -F file.ltl -D 'ltl3ba -H1' 'ltl3ba -H2' 'ltl3ba -H3' ltl2tgba \
--ambiguous --strength --verbose --csv=output.csv
grep _x output.csv && exit 1 grep _x output.csv && exit 1
@ -59,6 +61,9 @@ while read l; do
test "x$first" = "x$l" || exit 1 test "x$first" = "x$l" || exit 1
done) done)
ltldo 'ltl3ba -H1' -F file.ltl |
autcross --language-complemented 'autfilt --dualize' --verbose
# The name of the HOA is preserved # The name of the HOA is preserved
case `ltldo 'ltl3ba -H' -f xxx --stats=%m` in case `ltldo 'ltl3ba -H' -f xxx --stats=%m` in
*xxx*);; *xxx*);;