From f6be0830500640375a8842e7f462c3b22e8650cc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 14 Dec 2020 22:48:51 +0100 Subject: [PATCH] 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 | 3 + spot/twaalgos/determinize.cc | 23 ++++-- tests/Makefile.am | 1 + tests/core/genltl.test | 2 +- tests/core/ltlsynt.test | 145 +++++++++++++---------------------- tests/python/298.py | 33 ++++++++ 6 files changed, 107 insertions(+), 100 deletions(-) create mode 100644 tests/python/298.py diff --git a/NEWS b/NEWS index db16d6baa..a193ea39d 100644 --- a/NEWS +++ b/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: diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index 4aeddc497..436b8303a 100644 --- a/spot/twaalgos/determinize.cc +++ b/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>& implies); unsigned finalize_construction(const std::vector& 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& 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 - red = std::min(red, 2*b); + // Any brace above topbrace was added while constructing + // 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 diff --git a/tests/Makefile.am b/tests/Makefile.am index cd3d3c01a..b033d75de 100644 --- a/tests/Makefile.am +++ b/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 \ diff --git a/tests/core/genltl.test b/tests/core/genltl.test index ef596e842..ed1785494 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -195,7 +195,7 @@ cat >exp<exp <exp <exp <exp < GFb' --verbose --algo=ps 2> out diff --git a/tests/python/298.py b/tests/python/298.py new file mode 100644 index 000000000..51f9f35a1 --- /dev/null +++ b/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 . + +# 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