From e531da8d92488df408ebb8cdf6cdcdcb22d6c4f7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 16 Dec 2011 12:56:22 +0100 Subject: [PATCH] Perform WDBA minimization before degeneralization. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit There is no point in degeneralizing an automaton if it can be WDBA minimized. Doing so will only augment the number of states and slow down the powerset construction used by the WDBA minimization. * src/tgbatest/babiak.test: New file. It includes 5 formulae which Tomáš Babiak reported Spot 0.7.1 would take over one hour to translate if degeneralization and WDBA minimization were both requested. * src/tgbatest/Makefile.am (TESTS): Add it. * src/tgbatest/ltl2tgba.cc: Do WDBA minimization before degeneralization. The above formulae are now all translated in a few seconds. --- ChangeLog | 17 ++++++ src/tgbatest/Makefile.am | 1 + src/tgbatest/babiak.test | 115 +++++++++++++++++++++++++++++++++++++++ src/tgbatest/ltl2tgba.cc | 48 +++++++++------- 4 files changed, 160 insertions(+), 21 deletions(-) create mode 100755 src/tgbatest/babiak.test diff --git a/ChangeLog b/ChangeLog index db2a7ce03..137cffe36 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,20 @@ +2011-12-16 Alexandre Duret-Lutz + + Perform WDBA minimization before degeneralization. + + There is no point in degeneralizing an automaton if it can be WDBA + minimized. Doing so will only augment the number of states and + slow down the powerset construction used by the WDBA minimization. + + * src/tgbatest/babiak.test: New file. It includes 5 formulae + which Tomáš Babiak reported Spot 0.7.1 would take over one hour to + translate if degeneralization and WDBA minimization were both + requested. + * src/tgbatest/Makefile.am (TESTS): Add it. + * src/tgbatest/ltl2tgba.cc: Do WDBA minimization before + degeneralization. The above formulae are now all translated in a + few seconds. + 2011-12-16 Alexandre Duret-Lutz Don't rely on the g++ version to include tr1/unordered_map and co. diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index a0e69af54..f2fd0c53f 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -100,6 +100,7 @@ TESTS = \ sccsimpl.test \ obligation.test \ wdba.test \ + babiak.test \ randtgba.test \ emptchk.test \ emptchke.test \ diff --git a/src/tgbatest/babiak.test b/src/tgbatest/babiak.test new file mode 100755 index 000000000..ca2501412 --- /dev/null +++ b/src/tgbatest/babiak.test @@ -0,0 +1,115 @@ +#!/bin/sh +# Copyright (C) 2011 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 2 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 Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +# While running some benchmark, Tomáš Babiak found that Spot took too +# much time (i.e. >1h) to translate those six formulae. It turns out +# that the WDBA minimization was performed after the degeneralization +# algorithm, while this is not necessary (WDBA will produce a BA, so +# we may as well skip degeneralization). Translating these formulae +# in the test-suite ensure that they don't take too much time (the +# buildfarm will timeout if it does). + +. ./defs + +set -e + +cat >formulae < config <number_of_acceptance_conditions(); - if (echeck_inst - && degeneralize_opt == NoDegen - && n_acc > 1 - && echeck_inst->max_acceptance_conditions() < n_acc) - degeneralize_opt = DegenTBA; - - if (degeneralize_opt == DegenTBA) - { - a = degeneralized = new spot::tgba_tba_proxy(a); - } - else if (degeneralize_opt == DegenSBA) - { - a = degeneralized = new spot::tgba_sba_proxy(a); - assume_sba = true; - } - else if (labeling_opt == StateLabeled) - { - a = state_labeled = new spot::tgba_sgba_proxy(a); - } - const spot::tgba* minimized = 0; if (opt_minimize) { @@ -983,6 +962,33 @@ main(int argc, char** argv) } } + unsigned int n_acc = a->number_of_acceptance_conditions(); + if (echeck_inst + && degeneralize_opt == NoDegen + && n_acc > 1 + && echeck_inst->max_acceptance_conditions() < n_acc) + { + degeneralize_opt = DegenTBA; + assume_sba = false; + } + + if (!assume_sba && !opt_monitor) + { + if (degeneralize_opt == DegenTBA) + { + a = degeneralized = new spot::tgba_tba_proxy(a); + } + else if (degeneralize_opt == DegenSBA) + { + a = degeneralized = new spot::tgba_sba_proxy(a); + assume_sba = true; + } + else if (labeling_opt == StateLabeled) + { + a = state_labeled = new spot::tgba_sgba_proxy(a); + } + } + if (opt_monitor) { tm.start("Monitor minimization");