acc: make sure unit_propagate preserve the number of sets

* spot/twa/acc.hh: Here.
* tests/core/accsimpl.test, tests/core/ltl2tgba2.test: Add test cases.

spot/twa/acc.hh

@@ -1703,13 +1703,16 @@ namespace spot
       return is_parity(max, odd);
     }
 
-    /// \brief Remove redundant Fin and Inf. For example in
+    /// \brief Remove superfluous Fin and Inf by unit propagation.
-    /// Fin(0)|(Inf(0) & Fin(1)), Inf(0) is true iff Fin(0) is false so
+    ///
-    /// we can rewrite it as Fin(0)|Fin(1).
+    /// For example in `Fin(0)|(Inf(0) & Fin(1))`, `Inf(0)` is true
-    acc_cond
+    /// iff `Fin(0)` is false so we can rewrite it as `Fin(0)|Fin(1)`.
-    unit_propagation()
+    ///
+    /// The number of acceptance sets is not modified even if some do
+    /// not appear in the acceptance condition anymore.
+    acc_cond unit_propagation()
     {
-      return acc_cond(code_.unit_propagation());
+      return acc_cond(num_, code_.unit_propagation());
     }
 
     // Return (true, m) if there exist some acceptance mark m that

tests/core/accsimpl.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2018 Laboratoire de Recherche et Développement de
+# Copyright (C) 2018, 2020 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -51,3 +51,25 @@ EOF
 autfilt --simplify-acceptance 325 > 325s
 exp='3 Fin(0) | (Fin(1) & Inf(2))'
 test "$exp" = "`autfilt --stats='%a %g' 325s`"
+
+# This automaton used to cause some issue at some point, because
+# simplify_acceptance would simplify the acceptance condition without
+# removing the unnecessary set from the resulting automaton.
+cat >frenkin <<EOF
+HOA: v1
+States: 1
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 4 Fin(0) & (Fin(1) | (Inf(2)&Inf(3)))
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic stutter-invariant
+--BODY--
+State: 0
+[!0&1] 0
+[!0&!1] 0 {1 3}
+[0&1] 0 {0 1 2}
+[0&!1] 0 {0 1 2 3}
+--END--
+EOF
+autcross --language-preserved 'autfilt --simplify-acc' -F frenkin
+test 1,4,2 = "`autfilt --simplify-acc frenkin --stats=%s,%e,%a`"

tests/core/ltl2tgba2.test

@@ -441,4 +441,11 @@ ltl2tgba '!b & e U (a & b & c)' | grep '\[f\]' && exit 1
 ltl2tgba '!b & e U (a & b & c)' --stats=%w | grep 0 && exit 1
 ltl2tgba 'X!c & X(b & c & d & a U e)' | grep '\[f\]' && exit 1
 ltl2tgba 'X!c & X(b & c & d & a U e)' --stats=%w | grep 0 && exit 1
+
+# This caused issue at some point, because simplify_acceptance would
+# leave some undeclared acceptance set in the automaton, which would
+# cause simulation-based reduction to produce garbage output, which
+# would in turn cause the HOA printer to choke.
+ltlcross -f 'G(F(Gb ^ Fa) & FG!a)' 'ltl2tgba -G -D'
+
 :