From e1e9f960e62f467a72380e5dfa23a1bcbf7029ac Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 27 Jul 2023 09:48:00 +0200
Subject: [PATCH] tests: add some test to cover autcross' univ-edges removal

* tests/core/ltl3ba.test: Here.
---
 tests/core/ltl3ba.test | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/tests/core/ltl3ba.test b/tests/core/ltl3ba.test
index fdcebc926..acc68a2c5 100755
--- a/tests/core/ltl3ba.test
+++ b/tests/core/ltl3ba.test
@@ -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*);;