From e2fad2d7aef7bc1912d3c5333dac147f2f1cde75 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 11 Jul 2019 14:48:50 +0200
Subject: [PATCH] complement: fix handling of output_aborter with postproc

Reported by Salomon Sickert.

* spot/twaalgos/complement.cc: Make sure the output of postproc
is deterministic.
* tests/core/ltlcross.test: Add test case.
* NEWS: Mention the bug.
---
 NEWS                        | 8 +++++++-
 spot/twaalgos/complement.cc | 2 +-
 tests/core/ltlcross.test    | 8 +++++++-
 3 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/NEWS b/NEWS
index f1d409e34..e65aa08b9 100644
--- a/NEWS
+++ b/NEWS
@@ -1,6 +1,12 @@
 New in spot 2.8.0.dev (not yet released)
 
-  Nothing yet.
+  Bugs fixed:
+
+  - When complement() was called with an output_aborter, it could
+    return an alternating automaton on large automata.  This in turn
+    caused ltlcross to emit errors like "remove_alternation() only
+    works with weak alternating automata" or "product() does not
+    support alternating automata".
 
 New in spot 2.8 (2019-07-10)
 
diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc
index a6945b5a3..d2664ff31 100644
--- a/spot/twaalgos/complement.cc
+++ b/spot/twaalgos/complement.cc
@@ -534,7 +534,7 @@ namespace spot
     p.set_pref(spot::postprocessor::Deterministic);
     p.set_level(spot::postprocessor::Low);
     auto det = p.run(std::const_pointer_cast<twa_graph>(aut));
-    if (!det)
+    if (!det || !is_universal(det))
       return nullptr;
     return dualize(det);
   }
diff --git a/tests/core/ltlcross.test b/tests/core/ltlcross.test
index cbbe54489..1a5806ba8 100755
--- a/tests/core/ltlcross.test
+++ b/tests/core/ltlcross.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012, 2013, 2014, 2016 Laboratoire de Recherche et
+# Copyright (C) 2012-2014, 2016, 2019 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -59,3 +59,9 @@ ltlcross -D \
   "$ltl2tgba -t -taa -r4 %f > %T" \
   "$ltl2tgba -t -taa -r4 -c %f > %T" \
   "$ltl2tgba -t -taa -r4 -R3 -RDS %f > %T"
+
+
+# This case, reported by Salomon Sickert, used to break ltlcross in
+# Spot 2.8.  We use ltl2tgba twice so ltlcross build cross-products.
+ltlcross --verbose ltl2tgba ltl2tgba \
+-f '(G(F((a1)&(X(X(b1))))))&(G(F((a2)&(X(X(b2))))))&(G(F((a3)&(X(X(b3))))))'