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(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))))))'