From d8f245a7de97b5a97ca246b758e7cd317b82fe55 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 17 Dec 2021 12:05:33 +0100 Subject: [PATCH] complement: fix a regression with 2.9.8 Reported by Reuben Rowe. * spot/twaalgos/complement.cc (complement): Remove the hard-coded simul=0 option on automata with >32 states. In 2.10 simul=0 now implies det-simul=0, causing the regression, and most importantly it is not needed anymore, because we have other threashold like simul-max and simul-trans-pruning in place. * tests/core/complement.test: Add Reuben's automaton as test case. * NEWS: Mention the fix. --- NEWS | 5 + spot/twaalgos/complement.cc | 9 +- tests/core/complement.test | 326 +++++++++++++++++++++++++++++++++++- 3 files changed, 334 insertions(+), 6 deletions(-) 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<