tests: add some test to cover autcross' univ-edges removal
* tests/core/ltl3ba.test: Here.
This commit is contained in:
parent
531252119c
commit
3d412fbb78
1 changed files with 8 additions and 3 deletions
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
# -*- 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).
|
||||
#
|
||||
# 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))
|
||||
EOF
|
||||
randltl -n 30 2
|
||||
) | ltlcross -D 'ltl3ba -H1' 'ltl3ba -H2' 'ltl3ba -H3' ltl2tgba \
|
||||
--ambiguous --strength --csv=output.csv
|
||||
) > file.ltl
|
||||
|
||||
ltlcross -F file.ltl -D 'ltl3ba -H1' 'ltl3ba -H2' 'ltl3ba -H3' ltl2tgba \
|
||||
--ambiguous --strength --verbose --csv=output.csv
|
||||
|
||||
grep _x output.csv && exit 1
|
||||
|
||||
|
|
@ -59,6 +61,9 @@ while read l; do
|
|||
test "x$first" = "x$l" || exit 1
|
||||
done)
|
||||
|
||||
ltldo 'ltl3ba -H1' -F file.ltl |
|
||||
autcross --language-complemented 'autfilt --dualize' --verbose
|
||||
|
||||
# The name of the HOA is preserved
|
||||
case `ltldo 'ltl3ba -H' -f xxx --stats=%m` in
|
||||
*xxx*);;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue