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.
This commit is contained in:
Alexandre Duret-Lutz
parent
9679032510
commit
e531da8d92
4 changed files with 160 additions and 21 deletions
17
ChangeLog
17
ChangeLog
|
|
@ -1,3 +1,20 @@
|
|||
2011-12-16 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||
|
||||
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 <adl@lrde.epita.fr>
|
||||
|
||||
Don't rely on the g++ version to include tr1/unordered_map and co.
|
||||
|
|
|
|||
|
|
@ -100,6 +100,7 @@ TESTS = \
|
|||
sccsimpl.test \
|
||||
obligation.test \
|
||||
wdba.test \
|
||||
babiak.test \
|
||||
randtgba.test \
|
||||
emptchk.test \
|
||||
emptchke.test \
|
||||
|
|
|
|||
115
src/tgbatest/babiak.test
Executable file
115
src/tgbatest/babiak.test
Executable file
|
|
@ -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 <<EOF
|
||||
(p6 V X(G(F(F(X X(F X(F((G X F p1)|((F p5)U p1))))U((F p4)&(!p2|(G p0))))))))
|
||||
(F((G 1)&(!p6 V X!p2)))V((F((G X(!p1 V!p3))V F!p2))U(X((G p3)U(p6 U p7))V X p5))
|
||||
(((F p0)V((F p3)&!p4))V((((!p0|!p5)V X!p5)V p6)U(p5|(!p3 U(G(p1 U p2))))))
|
||||
(G(((F((p3 &!p3)|(G((G!p2)V!p5))))|(p1 V!p4))U((X(G((F!p0)U!p6))U X!p2)|!p7)))
|
||||
X((X(!p1 V F!p6)V F!p4)U p2)&(F(G((0 U(F p6))U((p1 U(G(p4 U F p0)))U X p7))))
|
||||
(G(G(((F p5)U((((F!p1)V(p2 &!p4))|!p2)|((X!p7 U!p4)V(F(F((G p2)&p5))))))U p6)))
|
||||
EOF
|
||||
|
||||
cat > config <<EOF
|
||||
Algorithm
|
||||
{
|
||||
Name = "Spot/FM basic"
|
||||
Path = "${LBTT_TRANSLATE}"
|
||||
Parameters = "--spot '../ltl2tgba -F -f -t'"
|
||||
Enabled = yes
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Spot/FM, with reductions + degeneralization (neverclaim)"
|
||||
Path = "${LBTT_TRANSLATE}"
|
||||
Parameters = "--spin '../ltl2tgba -r4 -R3f -F -f -N'"
|
||||
Enabled = yes
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Spot/FM, with reducetion + WDBA + degeneralization (neverclaim)"
|
||||
Path = "${LBTT_TRANSLATE}"
|
||||
Parameters = "--spin '../ltl2tgba -r7 -R3 -f -x -N -F -Rm'"
|
||||
Enabled = yes
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Spot/FM, with reducetion + WDBA + degeneralization (DS)"
|
||||
Path = "${LBTT_TRANSLATE}"
|
||||
Parameters = "--spot '../ltl2tgba -r7 -R3 -f -x -DS -t -F -Rm'"
|
||||
Enabled = yes
|
||||
}
|
||||
|
||||
GlobalOptions
|
||||
{
|
||||
Rounds = 6
|
||||
Interactive = Never
|
||||
# Verbosity = 5
|
||||
# ComparisonCheck = no
|
||||
# ConsistencyCheck = no
|
||||
# IntersectionCheck = no
|
||||
}
|
||||
|
||||
# Not used, but LBTT seems to want it.
|
||||
FormulaOptions
|
||||
{
|
||||
Size = 1...13
|
||||
Propositions = 6
|
||||
|
||||
AbbreviatedOperators = Yes
|
||||
GenerateMode = Normal
|
||||
OutputMode = Normal
|
||||
PropositionPriority = 50
|
||||
|
||||
TruePriority = 1
|
||||
FalsePriority = 1
|
||||
|
||||
AndPriority = 10
|
||||
OrPriority = 10
|
||||
XorPriority = 0
|
||||
# EquivalencePriority = 0
|
||||
|
||||
BeforePriority = 0
|
||||
|
||||
DefaultOperatorPriority = 5
|
||||
}
|
||||
EOF
|
||||
|
||||
${LBTT} --formulafile=formulae
|
||||
rm config
|
||||
|
||||
|
||||
|
||||
|
|
@ -934,27 +934,6 @@ main(int argc, char** argv)
|
|||
const spot::tgba_tba_proxy* degeneralized = 0;
|
||||
const spot::tgba_sgba_proxy* state_labeled = 0;
|
||||
|
||||
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;
|
||||
|
||||
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");
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue