diff --git a/NEWS b/NEWS index 12176da5e..80c4a2ed1 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,11 @@ New in spot 2.10.2.dev (not yet released) (e.g. co-Büchi) and where the initial state was in a rejecting SCC, sbacc() could output a superflous state. (Issue #492) + - Compared to 2.9.8, complement() (and many functions using it) was + slower and produced larger outputs on some automata with more than + 32 states due to an optimization of the determinization being + unintentionally disabled. + New in spot 2.10.2 (2021-12-03) Bugs fixed: diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc index 20be9c3eb..8db33225a 100644 --- a/spot/twaalgos/complement.cc +++ b/spot/twaalgos/complement.cc @@ -522,11 +522,10 @@ namespace spot m.set("det-max-states", aborter->max_states()); m.set("det-max-edges", aborter->max_edges()); } - if (aut->num_states() > 32) - { - m.set("ba-simul", 0); - m.set("simul", 0); - } + // In addition to the above options, the simulation-based + // optimization of the determinization is already restricted by + // the default values of simul-max and simul-trans-pruning. + // (See spot-x(7) for details.) spot::postprocessor p(&m); p.set_type(spot::postprocessor::Generic); p.set_pref(spot::postprocessor::Deterministic); diff --git a/tests/core/complement.test b/tests/core/complement.test index 35931f82c..eb3902d28 100755 --- a/tests/core/complement.test +++ b/tests/core/complement.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015-2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2015-2019, 2021 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -157,4 +157,328 @@ HOA: v1 States: 8 Start: 0 AP: 3 "a" "b" "c" Acceptance: 3 Fin(0) | EOF autfilt --complement pos.hoa >neg.hoa autfilt -q --intersect=pos.hoa neg.hoa && exit 1 + + +# The following automaton, generated by the Cyclist theorem prover was +# sent by Reuben Rowe to show a regression between Spot 2.9.8 and Spot +# 2.10. In the latter version, complementation was slower and larger, +# because the simulation-based optimization of the determinization was +# turned off. Here we do not check the runtime, but we can check the output +# size, which should be 4 and not 153. +cat >large.hoa<