determinize: don't emit colors for temporary braces

Related to issue #298.

* spot/twaalgos/determinize.cc: Recognize braces that are temporary
to avoid emitting colors when they become empty.
* tests/python/298.py: New file, showing a reduction of colors.
* tests/Makefile.am: Add it.
* tests/core/ltlsynt.test: Adjust expected output (now smaller).
* tests/core/genltl.test: Adjust one expected output (now larger).
* NEWS: Mention the issue.

NEWS

@@ -170,6 +170,9 @@ New in spot 2.9.5.dev (not yet released)
     performing an (unnecessary) second iteration even when the first
     one failed to reduce the automaton.  (Issue #442)
 
+  - tgba_determinize() could create parity automata using more colors
+    than necessary.
+
 New in spot 2.9.5 (2020-11-19)
 
   Bugs fixed:

spot/twaalgos/determinize.cc

@@ -94,7 +94,8 @@ namespace spot
     // default constructor
     safra_state();
     safra_state(state_t state_number, bool acceptance_scc = false);
-    safra_state(const safra_build& s, const compute_succs& cs, unsigned& color);
+    safra_state(const safra_build& s, const compute_succs& cs, unsigned& color,
+                unsigned topbrace);
     // Compute successor for transition ap
     safra_state
     compute_succ(const compute_succs& cs, const bdd& ap, unsigned& color) const;
@@ -102,7 +103,7 @@ namespace spot
     merge_redundant_states(const std::vector<std::vector<char>>& implies);
     unsigned
     finalize_construction(const std::vector<int>& buildbraces,
-                          const compute_succs& cs);
+                          const compute_succs& cs, unsigned topbrace);
 
     // each brace points to its parent.
     // braces_[i] is the parent of i
@@ -593,6 +594,7 @@ namespace spot
     safra_build& ss = cs.ss;
     ss.braces_ = braces_; // copy
     ss.nodes_.clear();
+    unsigned topbrace = braces_.size();
     for (const auto& node: nodes_)
       {
         for (const auto& t: cs.aut->out(node.first))
@@ -612,7 +614,7 @@ namespace spot
               ss.update_succ(node.second, t.dst, t.acc);
           }
       }
-    return safra_state(ss, cs, color);
+    return safra_state(ss, cs, color, topbrace);
   }
 
   // When a node a implies a node b, remove the node a.
@@ -643,7 +645,7 @@ namespace spot
   // Return the emitted color, red or green
   unsigned
   safra_state::finalize_construction(const std::vector<int>& buildbraces,
-                                     const compute_succs& cs)
+                                     const compute_succs& cs, unsigned topbrace)
   {
     unsigned red = -1U;
     unsigned green = -1U;
@@ -698,11 +700,15 @@ namespace spot
             // Step A5 renumber braces
             ++decr;
 
-            // Step A3 emit red
+            // Any brace above topbrace was added while constructing
-            red = std::min(red, 2*b);
+            // this successor, so it should not emit any red.
+            if (b < topbrace)
+              // Step A3 emit red
+              red = std::min(red, 2*b);
           }
         else if (cs.empty_green[b] & is_green)
           {
+            assert(b < topbrace);
             // Step A4 emit green
             green = std::min(green, 2*b+1);
           }
@@ -745,12 +751,13 @@ namespace spot
 
   safra_state::safra_state(const safra_build& s,
                            const compute_succs& cs,
-                           unsigned& color)
+                           unsigned& color,
+                           unsigned topbrace)
   : nodes_(s.nodes_.begin(), s.nodes_.end())
   {
     if (cs.use_simulation)
       merge_redundant_states(cs.implies);
-    color = finalize_construction(s.braces_, cs);
+    color = finalize_construction(s.braces_, cs, topbrace);
   }
 
   bool

tests/Makefile.am

@@ -376,6 +376,7 @@ TESTS_ipython = \
 # do not consider part of the documentation: those have to start
 # with a _.
 TESTS_python = \
+  python/298.py \
   python/341.py \
   python/_altscc.ipynb \
   python/_autparserr.ipynb \

tests/core/genltl.test

@@ -195,7 +195,7 @@ cat >exp<<EOF
 "ms-phi-r=2",1,28
 "ms-phi-s=0",1,3
 "ms-phi-s=1",1,7
-"ms-phi-s=2",1,375
+"ms-phi-s=2",1,387
 "ms-phi-h=0",1,1
 "ms-phi-h=1",2,3
 "ms-phi-h=2",4,7

tests/core/ltlsynt.test

@@ -23,44 +23,39 @@
 set -e
 
 cat >exp <<EOF
-parity 19;
+parity 17;
-0 1 0 8,9 "INIT";
+0 1 0 7,8 "INIT";
-9 3 1 1,2;
+8 3 1 1,2;
-2 1 0 12,13;
+2 1 0 11,12;
-13 5 1 1,4;
+12 5 1 1,4;
-4 1 0 8,15;
+4 1 0 7,15;
 15 3 1 5,6;
-6 1 0 8,15;
+6 1 0 7,15;
-8 3 1 2;
+7 3 1 2;
 5 1 0 16,17;
 17 4 1 5,6;
 16 4 1 2;
-1 1 0 10,11;
+1 1 0 9,10;
-11 4 1 5,7;
+10 3 1 1,5;
-7 1 0 18,19;
+9 3 1 2,3;
-19 3 1 5,7;
+3 1 0 13,14;
-18 3 1 2,3;
-3 1 0 10,14;
 14 4 1 1,4;
-10 4 1 2,3;
+13 4 1 2,3;
-12 5 1 2,3;
+11 5 1 2,3;
-parity 16;
+parity 13;
 0 1 0 1,2 "INIT";
 2 1 1 3;
-3 2 0 4,5;
+3 3 0 4,5;
 5 1 1 6,7;
 7 1 0 8,9;
 9 1 1 10,11;
-11 1 0 8,12;
+11 1 0 8,9;
-12 1 1 10,11;
+8 3 1 3,12;
+12 2 0 4,5;
+4 2 1 3,12;
 10 2 0 8,9;
-8 3 1 3,13;
+6 1 0 13,4;
-13 3 0 4,5;
+13 1 1 6,10;
-4 1 1 3,13;
-6 2 0 14,15;
-15 2 1 3,13;
-14 1 1 10,16;
-16 1 0 14,15;
 1 1 1 3,6;
 parity 5;
 1 1 0 4,5 "INIT";
@@ -79,38 +74,24 @@ diff out exp
 
 cat >exp <<EOF
 REALIZABLE
-aag 31 1 3 1 26
+aag 16 1 2 1 13
 2
-4 49
+4 29
-6 57
+6 33
-8 59
+31
-63
+8 5 7
-10 7 9
+10 8 3
-12 5 10
+12 8 2
-14 12 3
+14 4 7
-16 12 2
+16 14 3
-18 4 10
+18 14 2
-20 18 3
+20 5 6
-22 18 2
+22 20 2
-24 6 9
+24 20 3
-26 5 24
+26 17 25
-30 26 3
+28 11 26
-32 4 24
+30 19 23
-34 32 2
+32 13 30
-36 32 3
-38 7 8
-40 5 38
-42 40 2
-44 40 3
-46 21 31
-48 15 46
-50 17 23
-52 35 43
-54 50 52
-56 27 54
-58 37 45
-60 27 52
-62 23 60
 i0 a
 o0 b
 EOF
@@ -119,36 +100,18 @@ diff out exp
 
 cat >exp <<EOF
 REALIZABLE
-aag 28 1 3 1 24
+aag 10 1 2 1 7
 2
-4 38
+4 18
-6 49
+6 20
-8 56
+14
-29
+8 4 7
-10 6 9
+10 5 6
-12 5 10
+12 11 9
-14 7 8
+14 2 13
-16 15 11
+16 4 9
-18 4 9
+18 3 17
-20 5 17
+20 2 17
-22 21 19
-24 2 23
-26 3 12
-28 27 25
-30 7 9
-32 4 30
-34 5 9
-36 35 33
-38 3 37
-40 6 11
-42 5 41
-44 43 19
-46 2 45
-48 27 47
-50 4 10
-52 5 14
-54 53 51
-56 3 55
 i0 a
 o0 b
 EOF
@@ -213,7 +176,7 @@ automaton has 9 states
 determinization done
 DPA has 12 states, 4 colors
 simplification done
-DPA has 11 states
+DPA has 10 states
 determinization and simplification took X seconds
 parity game solved in X seconds
 EOF
@@ -223,11 +186,11 @@ diff outx exp
 
 cat >exp <<EOF
 translating formula done in X seconds
-automaton has 3 states and 4 colors
+automaton has 2 states and 4 colors
 simplification done in X seconds
-DPA has 3 states
+DPA has 2 states
 split inputs and outputs done in X seconds
-automaton has 8 states
+automaton has 6 states
 parity game solved in X seconds
 EOF
 ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --verbose --algo=ps 2> out

tests/python/298.py

@@ -0,0 +1,33 @@
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita
+# (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+# Test for parts of Issue #298.
+
+import spot
+
+a1 = spot.automaton("""genltl --dac=51 | ltl2tgba --med |""")
+a1 = spot.degeneralize_tba(a1)
+r1 = spot.tgba_determinize(a1, True, False, False)
+assert r1.num_sets() == 3
+
+a2 = spot.automaton("""genltl --dac=51 | ltl2tgba --high |""")
+a2 = spot.degeneralize_tba(a2)
+r2 = spot.tgba_determinize(a2, True, False, False)
+# This used to fail in 2.9.5 and earlier.
+assert r2.num_sets() == 3