Commit d9fc75e9 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

Improve SCC simplification by removing implied acceptance conditions.

Spot 0.7.1 used to need 190 acceptance conditions to translate the
188 literature formulae.  With this patch we are down to 185.
That's not an impressive, but there are only ~20 formulae that
require more than 1 acceptance conditions; hence little room for
improvement.

* src/misc/bddlt.hh (bdd_hash): New function.
* src/misc/accconv.hh, src/misc/accconv.cc: New files.
* src/misc/Makefile.am: Add them.
* src/tgbaalgos/scc.cc (scc_map::build_map): Adjust
to record all combination of acceptance conditions occurring in a SCC.
* src/tgbaalgos/scc.hh (scc_map::scc::useful_acc): Update description.
* src/tgbaalgos/sccfilter.cc (scc_filter): Simplify acceptance
conditions that are always implied by another acceptance
conditions.  Previously, we only removed acceptance conditions
that where always present in accepting SCCs.
* src/tgbatest/sccsimpl.test: New file.
* src/tgbatest/Makefile.am (TESTS): Add it.
parent 9d232af8
2011-08-27 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Improve SCC simplification by removing implied acceptance conditions.
Spot 0.7.1 used to need 190 acceptance conditions to translate the
188 literature formulae. With this patch we are down to 185.
That's not an impressive, but there are only ~20 formulae that
require more than 1 acceptance conditions; hence little room for
improvement.
* src/misc/bddlt.hh (bdd_hash): New function.
* src/misc/accconv.hh, src/misc/accconv.cc: New files.
* src/misc/Makefile.am: Add them.
* src/tgbaalgos/scc.cc (scc_map::build_map): Adjust
to record all combination of acceptance conditions occurring in a SCC.
* src/tgbaalgos/scc.hh (scc_map::scc::useful_acc): Update description.
* src/tgbaalgos/sccfilter.cc (scc_filter): Simplify acceptance
conditions that are always implied by another acceptance
conditions. Previously, we only removed acceptance conditions
that where always present in accepting SCCs.
* src/tgbatest/sccsimpl.test: New file.
* src/tgbatest/Makefile.am (TESTS): Add it.
2011-08-26 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Refine yesterday's change to the degeneralization.
......
......@@ -30,6 +30,7 @@ nodist_misc_HEADERS = _config.h
DISTCLEANFILES = _config.h
misc_HEADERS = \
accconv.hh \
bareword.hh \
bddalloc.hh \
bddlt.hh \
......@@ -54,6 +55,7 @@ misc_HEADERS = \
noinst_LTLIBRARIES = libmisc.la
libmisc_la_SOURCES = \
accconv.cc \
bareword.cc \
bddalloc.cc \
bddop.cc \
......
// Copyright (C) 2011 Laboratoire de Recherche et Developpement 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.
#include <cassert>
#include "accconv.hh"
namespace spot
{
bdd acceptance_convertor::as_positive_product(bdd acc)
{
// Lookup in cache.
bdd_cache_t::const_iterator it = pos_prod_cache_.find(acc);
if (it != pos_prod_cache_.end())
return it->second;
// Split the sum
bdd res = bddtrue;
bdd all = acc;
while (all != bddfalse)
{
bdd one = bdd_satone(all);
all -= one;
// Lookup the subproduct in the cache.
it = pos_prod_cache_.find(one);
if (it != pos_prod_cache_.end())
{
res &= it->second;
continue;
}
// Otherwise, strip negative variables.
bdd pos = bddfalse;
bdd cur = one;
while (cur != bddfalse)
{
bdd low = bdd_low(cur);
if (low == bddfalse)
{
pos = bdd_ithvar(bdd_var(cur));
break;
}
cur = low;
}
assert(pos != bddfalse);
// Cache result for subproduct.
pos_prod_cache_[one] = pos;
// Augment final result.
res &= pos;
}
// Cache final result.
pos_prod_cache_[acc] = res;
return res;
};
bdd acceptance_convertor::as_full_product(bdd acc)
{
// Lookup in cache.
bdd_cache_t::const_iterator it = full_prod_cache_.find(acc);
if (it != full_prod_cache_.end())
return it->second;
bdd pos = as_positive_product(acc);
bdd res = bdd_exist(allneg_, pos) & pos;
// Cache final result.
full_prod_cache_[acc] = res;
return res;
}
}
// Copyright (C) 2011 Laboratoire de Recherche et Developpement 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.
#ifndef SPOT_MISC_ACCCONV_HH
# define SPOT_MISC_ACCCONV_HH
#include <bdd.h>
#include "misc/hash.hh"
#include "misc/bddlt.hh"
namespace spot
{
/// \brief Help class to convert between acceptance conditions to
/// other BDD formats.
class acceptance_convertor
{
public:
acceptance_convertor(bdd allneg)
: allneg_(allneg)
{
}
bdd as_positive_product(bdd acc);
bdd as_full_product(bdd acc);
protected:
bdd allneg_;
typedef Sgi::hash_map<bdd, bdd, bdd_hash> bdd_cache_t;
bdd_cache_t pos_prod_cache_;
bdd_cache_t full_prod_cache_;
};
}
#endif // SPOT_MISC_ACCCONV_HH
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
......@@ -38,6 +40,19 @@ namespace spot
return left.id() < right.id();
}
};
/// \brief Hash functor for BDDs.
/// \ingroup misc_tools
struct bdd_hash :
public std::unary_function<const bdd&, size_t>
{
size_t
operator()(const bdd& b) const
{
return b.id();
}
};
}
#endif // SPOT_MISC_BDDLT_HH
......@@ -25,6 +25,7 @@
#include "scc.hh"
#include "tgba/bddprint.hh"
#include "misc/escape.hh"
#include "misc/accconv.hh"
namespace spot
{
......@@ -139,6 +140,8 @@ namespace spot
void
scc_map::build_map()
{
acceptance_convertor conv(aut_->neg_acceptance_conditions());
// Setup depth-first search from the initial state.
{
self_loops_ = 0;
......@@ -267,7 +270,7 @@ namespace spot
conds.insert(cond);
bdd supp = bdd_support(cond);
bdd all = aut_->all_acceptance_conditions();
bdd useful = all - acc;
bdd useful = conv.as_full_product(acc);
while (threshold > root_.front().index)
{
assert(!root_.empty());
......@@ -276,7 +279,7 @@ namespace spot
acc |= root_.front().acc;
bdd lacc = arc_acc_.top();
acc |= lacc;
useful |= (all - lacc) | root_.front().useful_acc;
useful |= conv.as_full_product(lacc) | root_.front().useful_acc;
states.splice(states.end(), root_.front().states);
succs.insert(root_.front().succ.begin(),
root_.front().succ.end());
......@@ -447,15 +450,13 @@ namespace spot
res.dead_paths = d.dead_paths[init];
res.useless_scc_map.reserve(res.scc_total);
bdd useful_acc = bddfalse;
res.useful_acc = bddfalse;
for (unsigned n = 0; n < res.scc_total; ++n)
{
res.useless_scc_map[n] = !d.acc_paths[n];
if (m.accepting(n))
useful_acc |= m.useful_acc_of(n);
res.useful_acc |= m.useful_acc_of(n);
}
res.useful_acc = useful_acc;
return res;
}
......
......@@ -200,7 +200,16 @@ namespace spot
succ_type succ;
/// Trivial SCC have one state and no self-loops.
bool trivial;
/// Useful acceptance conditions.
/// \brief Set of acceptance combinations used in the SCC.
///
/// Note that the encoding used here differs from the
/// encoding used in automata.
/// If some transitions of the automaton are labeled by
/// Acc[a]&!Acc[b]&!Acc[c] | !Acc[a]&Acc[b]&!Acc[c]
/// an other transitions are labeled by
/// !Acc[a]&Acc[b]&!Acc[c] | !Acc[a]&!Acc[b]&Acc[c]
/// then useful_acc will contain
/// Acc[a]&Acc[b]&!Acc[c] | !Acc[a]&Acc[b]&Acc[c]
bdd useful_acc;
};
......
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -22,6 +22,7 @@
#include "tgba/tgbaexplicit.hh"
#include "reachiter.hh"
#include "tgbaalgos/scc.hh"
#include "misc/bddop.hh"
#include <sstream>
namespace spot
......@@ -131,31 +132,47 @@ namespace spot
scc_stats ss = build_scc_stats(sm);
bdd useful = ss.useful_acc;
if (useful == bddfalse)
// Even if no acceptance conditions are useful in a SCC,
// we need to keep at least one acceptance conditions
useful = bdd_satone(aut->all_acceptance_conditions());
bdd positive = bddtrue;
bdd cur = useful;
while (cur != bddfalse)
bdd negall = aut->neg_acceptance_conditions();
// Compute a set of useless acceptance conditions.
// If the acceptance combinations occurring in
// the automata are { a, ab, abc, bd }, then
// USEFUL contains (a&!b&!c&!d)|(a&b&!c&!d)|(a&b&c&!d)|(!a&b&!c&d)
// and we want to find that 'a' and 'b' are useless because
// they always occur with 'c'.
// The way we check if 'a' is useless that is to look whether
// USEFUL & (x -> a) == USEFUL for some other acceptance
// condition x.
bdd allconds = bdd_support(negall);
bdd allcondscopy = allconds;
bdd useless = bddtrue;
while (allconds != bddtrue)
{
bdd a = bdd_satone(cur);
cur -= a;
for (;;)
bdd a = bdd_ithvar(bdd_var(allconds));
bdd others = allcondscopy;
while (others != bddtrue)
{
if (bdd_low(a) == bddfalse)
bdd x = bdd_ithvar(bdd_var(others));
if (x != a)
{
positive &= bdd_ithvar(bdd_var(a));
break;
if ((useful & (x >> a)) == useful)
{
// a is useless
useful = bdd_exist(useful, a);
useless &= a;
allcondscopy = bdd_exist(allcondscopy, a);
break;
}
}
a = bdd_low(a);
others = bdd_high(others);
}
allconds = bdd_high(allconds);
}
bdd strip = bdd_exist(bdd_support(aut->all_acceptance_conditions()),
positive);
useful = bdd_exist(useful, strip);
// We never remove ALL acceptance conditions.
assert(negall == bddtrue || useless != bdd_support(negall));
useful = compute_all_acceptance_conditions(bdd_exist(negall, useless));
// In most cases we will create a tgba_explicit_string copy of the
// initial tgba, but this is not very space efficient as the
......@@ -168,7 +185,7 @@ namespace spot
if (af)
{
filter_iter<tgba_explicit_formula> fi(af, sm, ss.useless_scc_map,
useful, strip,
useful, useless,
remove_all_useless);
fi.run();
tgba_explicit_formula* res = fi.result();
......@@ -178,7 +195,7 @@ namespace spot
else
{
filter_iter<tgba_explicit_string> fi(aut, sm, ss.useless_scc_map,
useful, strip,
useful, useless,
remove_all_useless);
fi.run();
tgba_explicit_string* res = fi.result();
......
......@@ -97,6 +97,7 @@ TESTS = \
reduccmp.test \
reductgba.test \
scc.test \
sccsimpl.test \
obligation.test \
wdba.test \
randtgba.test \
......
#!/bin/sh
# Copyright (C) 2011 Laboratoire de Recherche et Developpement de
# l'Epita
#
# 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.
. ./defs
set -e
# This file tests the logic for simplifying superfluous
# acceptance conditions. Especially those whose presence
# are implied by others. This simplification is done as
# part of option -R3.
# The following automaton was generated for
# G((!p0 | !p2 | (!p1 W (!p1 & p3 & X(!p1 U p4)))) U p1)
# The formula does not really matter (except to show how
# such automata can occur). The important point is that the
# acceptance condition "p4", used a lot, is always present
# when "p1" is used. So the "p4" acceptance can be removed.
cat <<EOF > aut.txt
acc = "p4" "p1";
S1, S1, "p1", "p4" "p1";
S1, S1, "!p0 | !p2", "p4";
S1, S2, "p3", "p4";
S1, S3, "1", "p4";
S2, S1, "p1 & p4", "p4" "p1";
S2, S1, "(p4 & !p0) | (p4 & !p2)", "p4";
S2, S2, "p3 & p4", "p4";
S2, S2, "(!p1 & !p0) | (!p1 & !p2) | (!p1 & p3)",;
S2, S3, "p4", "p4";
S2, S4, "!p1",;
S3, S2, "!p1 & p3", "p4";
S3, S3, "!p1", "p4";
S4, S2, "!p1 & p3 & p4", "p4";
S4, S2, "!p1 & p3",;
S4, S3, "!p1 & p4", "p4";
S4, S4, "!p1",;
EOF
run 0 ../ltl2tgba -X -R3 -b aut.txt > out.txt
grep '^acc = "p1";$' out.txt
# Here, acceptances A and C can both be removed.
cat <<EOF > aut2.txt
acc = A B C D;
S1, S1, "a", A;
S1, S1, "b", A B;
S1, S1, "c", A B C;
S1, S1, "d", C D;
EOF
run 0 ../ltl2tgba -X -R3 -b aut2.txt > out2.txt
grep '^acc = "B" "D";$' out2.txt || grep '^acc = "D" "B";$' out2.txt || exit 1
# only 4 lines output, because the "b" and "c" lines have been merged.
test `wc -l < out2.txt` = 4
# Here, acceptances A and B can both be removed.
cat <<EOF > aut3.txt
acc = A B C D;
S1, S1, "a", A;
S1, S1, "b", A B;
S1, S1, "c", A B C;
S1, S1, "d", B D;
EOF
run 0 ../ltl2tgba -X -R3 -b aut3.txt > out3.txt
grep '^acc = "C" "D";$' out3.txt || grep '^acc = "D" "C";$' out3.txt || exit 1
# only 4 lines output, because the "a" and "b" lines have been merged.
test `wc -l < out3.txt` = 4
# No simplification possible here
cat <<EOF > aut4.txt
acc = A B C D;
S1, S1, "a", A;
S1, S1, "b", A B;
S1, S1, "c", A B C;
S1, S1, "d", B D;
S1, S1, "e", C D;
EOF
run 0 ../ltl2tgba -X -R3 -b aut4.txt > out4.txt
test `grep '^acc' out4.txt | wc -w` = 6
test `wc -l < out4.txt` = 6
# Make sure nothing wrong (like an assert())
# happens when no acceptance conditions are used.
cat <<EOF > aut5.txt
acc = ;
S1, S1, "a", ;
S1, S1, "b", ;
S1, S1, "c", ;
EOF
run 0 ../ltl2tgba -X -R3 -b aut5.txt > out5.txt
test `wc -l < out5.txt` = 2
# Here, one of A,B and one of C,D can be removed.
cat <<EOF > aut6.txt
acc = A B C D;
S1, S1, "a", A B;
S1, S1, "b", A B;
S1, S1, "c", C D;
S1, S1, "d", C D;
EOF
run 0 ../ltl2tgba -X -R3 -b aut6.txt > out6.txt
test `grep '^acc' out6.txt | wc -w` = 4
test `wc -l < out6.txt` = 3
# This automaton comes from the formula
# 1 U (p0 & (!p1 R ((1 U !p2) & (1 U !p3))))
# and and early implementation of our simplification
# missed the simplification.
cat <<EOF > aut7.txt
acc = ZZ "!p3" "!p2";
S1, S2, "p0 & !p2 & !p3 & !p1", ZZ "!p3" "!p2";
S1, S1, "!p0 | p1 | p2 | p3", "!p3" "!p2";
S1, S3, "p0 & p2 & !p3 & !p1", ZZ "!p3";
S1, S4, "p0 & p3 & !p2 & !p1", ZZ "!p2";
S1, S5, "(p0 & p2 & !p1) | (p0 & p3 & !p1)", ZZ;
S1, S6, "p0 & p1 & !p2 & !p3", ZZ "!p3" "!p2";
S1, S6, "(p0 & p1 & !p3) | (p0 & p2 & !p3)", ZZ "!p3";
S1, S6, "(p0 & p1 & !p2) | (p0 & p3 & !p2)", ZZ "!p2";
S1, S6, "(p0 & p1) | (p0 & p2) | (p0 & p3)", ZZ;
S2, S2, "1", ZZ "!p3" "!p2";
S3, S2, "!p2", ZZ "!p3" "!p2";
S3, S3, "p2", ZZ "!p3";
S4, S2, "!p3", ZZ "!p3" "!p2";
S4, S4, "p3", ZZ "!p2";
S5, S2, "!p2 & !p3", ZZ "!p3" "!p2";
S5, S3, "p2 & !p3", ZZ "!p3";
S5, S4, "p3 & !p2", ZZ "!p2";
S5, S5, "p2 | p3", ZZ;
S6, S2, "!p2 & !p3 & !p1", ZZ "!p3" "!p2";
S6, S3, "p2 & !p3 & !p1", ZZ "!p3";
S6, S4, "p3 & !p2 & !p1", ZZ "!p2";
S6, S5, "(p2 & !p1) | (p3 & !p1)", ZZ;
S6, S6, "p1 & !p2 & !p3", ZZ "!p3" "!p2";
S6, S6, "(p1 & !p3) | (p2 & !p3)", ZZ "!p3";
S6, S6, "(p1 & !p2) | (p3 & !p2)", ZZ "!p2";
S6, S6, "p1 | p2 | p3", ZZ;
EOF
run 0 ../ltl2tgba -X -R3 -b aut7.txt > out7.txt
# ZZ should disappear
grep ZZ out7.txt && exit 1
test `grep '^acc' out7.txt | wc -w` = 4
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment