alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

degen: learn to work on generalized-Co-Büchi as well

Browse source 
* spot/twaalgos/degen.hh, spot/twaalgos/degen.cc: Adjust
degeneralize() and degeneralize_tba() to work on generalized-co-Büchi.
* NEWS: Mention this.
* spot/twaalgos/cobuchi.hh, spot/twaalgos/cobuchi.cc (to_nca): Use
degeneralization on generalized-co-Büchi.
* spot/twaalgos/postproc.cc: Use degeneralization for generalized
co-Büchi as well.
* bin/autfilt.cc: Improve chain products of co-Büchi automata by using
generalization if too many colors are needed.
* tests/core/prodchain.test, tests/python/pdegen.py: Add test cases.
This commit is contained in:
Alexandre Duret-Lutz 2022-09-07 14:36:23 +02:00
parent fe3ebd370b
commit bdac53511a
9 changed files with 169 additions and 81 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -114,6 +114,9 @@ New in spot 2.10.6.dev (not yet released)
to obtain a simple model checker (that returns true or false,
without counterexample).
- degeneralize() and degeneralize_tba() learned to work on
generalized-co-Büchi as well.
- product() learned that the product of two co-Büchi automata
is a co-Büchi automaton. And product_or() learned that the
"or"-product of two Büchi automata is a Büchi automaton.

32
bin/autfilt.cc
View file

@ -713,10 +713,12 @@ ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
return p.run(aut);
}
static spot::twa_graph_ptr ensure_tba(spot::twa_graph_ptr aut)
static spot::twa_graph_ptr
ensure_tba(spot::twa_graph_ptr aut,
spot::postprocessor::output_type type = spot::postprocessor::Buchi)
{
spot::postprocessor p;
p.set_type(spot::postprocessor::Buchi);
p.set_type(type);
p.set_pref(spot::postprocessor::Any);
p.set_level(spot::postprocessor::Low);
return p.run(aut);
@ -726,12 +728,14 @@ static spot::twa_graph_ptr ensure_tba(spot::twa_graph_ptr aut)
static spot::twa_graph_ptr
product(spot::twa_graph_ptr left, spot::twa_graph_ptr right)
{
if ((type == spot::postprocessor::Buchi)
&& (left->num_sets() + right->num_sets() >
spot::acc_cond::mark_t::max_accsets()))
// Are we likely to fail because of too many colors?
if ((left->num_sets() + right->num_sets() >
spot::acc_cond::mark_t::max_accsets())
&& (type == spot::postprocessor::Buchi
|| type == spot::postprocessor::CoBuchi))
{
left = ensure_tba(left);
right = ensure_tba(right);
left = ensure_tba(left, type);
right = ensure_tba(right, type);
}
return spot::product(left, right);
}
@ -739,12 +743,14 @@ product(spot::twa_graph_ptr left, spot::twa_graph_ptr right)
static spot::twa_graph_ptr
product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right)
{
if ((type == spot::postprocessor::Buchi)
&& (left->num_sets() + right->num_sets() >
spot::acc_cond::mark_t::max_accsets()))
// Are we likely to fail because of too many colors?
if ((left->num_sets() + right->num_sets() >
spot::acc_cond::mark_t::max_accsets())
&& (type == spot::postprocessor::Buchi
|| type == spot::postprocessor::CoBuchi))
{
left = ensure_tba(left);
right = ensure_tba(right);
left = ensure_tba(left, type);
right = ensure_tba(right, type);
}
return spot::product_or(left, right);
}
@ -988,7 +994,7 @@ parse_opt(int key, char* arg, struct argp_state*)
if (!opt->included_in)
opt->included_in = aut;
else
opt->included_in = spot::product_or(opt->included_in, aut);
opt->included_in = ::product_or(opt->included_in, aut);
}
break;
case OPT_INHERENTLY_WEAK_SCCS:

16
spot/twaalgos/cobuchi.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2018, 2021 Laboratoire de Recherche et Développement
// Copyright (C) 2017-2018, 2021, 2022 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -26,6 +26,7 @@
#include <spot/twa/acc.hh>
#include <spot/twa/bddprint.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/degen.hh>
#include <spot/twaalgos/powerset.hh>
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/sccinfo.hh>
@ -338,23 +339,26 @@ namespace spot
twa_graph_ptr
to_nca(const_twa_graph_ptr aut, bool named_states)
{
if (aut->acc().is_co_buchi())
const acc_cond& acc = aut->acc();
if (acc.is_co_buchi())
return make_twa_graph(aut, twa::prop_set::all());
if (auto weak = weak_to_cobuchi(aut))
return weak;
if (acc.is_generalized_co_buchi())
return degeneralize_tba(aut);
const acc_cond::acc_code& code = aut->get_acceptance();
std::vector<acc_cond::rs_pair> pairs;
if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity())
if (acc.is_streett_like(pairs) || acc.is_parity())
return nsa_to_nca(aut, named_states);
else if (code.is_dnf())
return dnf_to_nca(aut, named_states);
auto tmp = make_twa_graph(aut, twa::prop_set::all());
tmp->set_acceptance(aut->acc().num_sets(),
aut->get_acceptance().to_dnf());
tmp->set_acceptance(acc.num_sets(), code.to_dnf());
return to_nca(tmp, named_states);
}
@ -683,6 +687,8 @@ namespace spot
return make_twa_graph(aut, twa::prop_set::all());
if (auto weak = weak_to_cobuchi(aut))
return weak;
if (aut->acc().is_generalized_co_buchi())
return degeneralize_tba(aut);
}
const acc_cond::acc_code& code = aut->get_acceptance();

9
spot/twaalgos/cobuchi.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
// Copyright (C) 2017-2019, 2022 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -92,8 +92,8 @@ namespace spot
/// original language, and is a superset iff the original language
/// can not be expressed using a co-Büchi acceptance condition.
///
/// The implementation dispatches between dnf_to_nca, nsa_to_nca,
/// and a trivial implementation for weak automata.
/// The implementation dispatches between dnf_to_nca(), nsa_to_nca(),
/// degeneralize_tba(), and a trivial implementation for weak automata.
SPOT_API twa_graph_ptr
to_nca(const_twa_graph_ptr aut, bool named_states = false);
@ -126,7 +126,8 @@ namespace spot
/// can not be expressed using a co-Büchi acceptance condition.
///
/// The implementation dispatches between dnf_to_dca, nsa_to_dca,
/// and a trivial implementation for deterministic weak automata.
/// degeneralize(), and a trivial implementation for deterministic
/// weak automata.
SPOT_API twa_graph_ptr
to_dca(const_twa_graph_ptr aut, bool named_states = false);
}

54
spot/twaalgos/degen.cc
View file

@ -80,7 +80,8 @@ namespace spot
void fill_cache(unsigned s)
{
unsigned s1 = scc_of(s);
acc_cond::mark_t common = a_->acc().all_sets();
acc_cond::mark_t all_colors = a_->acc().all_sets();
acc_cond::mark_t common = all_colors;
acc_cond::mark_t union_ = {};
bool has_acc_self_loop = false;
bool is_true_state = false;
@ -97,7 +98,7 @@ namespace spot
std::get<2>(cache_[d]) &= t.acc;
// an accepting self-loop?
if ((t.dst == s) && a_->acc().accepting(t.acc))
if ((t.dst == s) && t.acc == all_colors)
{
has_acc_self_loop = true;
if (t.cond == bddtrue)
@ -330,9 +331,10 @@ namespace spot
bool skip_levels, bool ignaccsl,
bool remove_extra_scc)
{
if (!a->acc().is_generalized_buchi())
bool input_is_gba = a->acc().is_generalized_buchi();
if (!(input_is_gba || a->acc().is_generalized_co_buchi()))
throw std::runtime_error
("degeneralize() only works with generalized Büchi acceptance");
("degeneralize() only works with generalized (co)Büchi acceptance");
if (!a->is_existential())
throw std::runtime_error
("degeneralize() does not support alternation");
@ -347,7 +349,11 @@ namespace spot
// The result automaton is an SBA.
auto res = make_twa_graph(dict);
res->copy_ap_of(a);
if (input_is_gba)
res->set_buchi();
else
res->set_co_buchi();
acc_cond::mark_t all_colors = a->get_acceptance().used_sets();
if (want_sba)
res->prop_state_acc(true);
// Preserve determinism, weakness, and stutter-invariance
@ -396,9 +402,32 @@ namespace spot
std::vector<std::pair<unsigned, bool>> lvl_cache(a->num_states());
// Compute SCCs in order to use any optimization.
std::unique_ptr<scc_info> m = use_scc
? std::make_unique<scc_info>(a, scc_info_options::NONE)
: nullptr;
std::unique_ptr<scc_info> m = nullptr;
if (use_scc)
{
if (!input_is_gba)
{
// If the input is gen-co-Büchi, temporary pretend its
// generalized Büchi.
unsigned n = a->num_sets();
twa_graph_ptr amut = std::const_pointer_cast<twa_graph>(a);
amut->set_generalized_buchi(n);
try
{
m = std::make_unique<scc_info>(a, scc_info_options::NONE);
}
catch (...)
{
amut->set_generalized_co_buchi(n);
throw;
}
amut->set_generalized_co_buchi(n);
}
else
{
m = std::make_unique<scc_info>(a, scc_info_options::NONE);
}
}
// Initialize scc_orders
std::unique_ptr<scc_orders> orders = use_cust_acc_orders
@ -674,7 +703,7 @@ namespace spot
{
d.second = 0; // Make it go to the first level.
// Skip as many levels as possible.
if (!a->acc().accepting(acc) && skip_levels)
if (acc != all_colors && skip_levels)
{
if (use_cust_acc_orders)
{
@ -723,9 +752,10 @@ namespace spot
int use_lvl_cache, bool skip_levels, bool ignaccsl,
bool remove_extra_scc)
{
// If this already a degeneralized digraph, there is nothing we
// If this already a degeneralized twa, there is nothing we
// can improve.
if (a->is_sba())
if (const acc_cond& acc = a->acc();
a->prop_state_acc() && (acc.is_buchi() || acc.is_co_buchi()))
return std::const_pointer_cast<twa_graph>(a);
return degeneralize_aux<true>(a, use_z_lvl, use_cust_acc_orders,
@ -739,9 +769,9 @@ namespace spot
int use_lvl_cache, bool skip_levels, bool ignaccsl,
bool remove_extra_scc)
{
// If this already a degeneralized digraph, there is nothing we
// If this already a degeneralized twa, there is nothing we
// can improve.
if (a->acc().is_buchi())
if (a->acc().is_buchi() || a->acc().is_co_buchi())
return std::const_pointer_cast<twa_graph>(a);
return degeneralize_aux<false>(a, use_z_lvl, use_cust_acc_orders,

55
spot/twaalgos/degen.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2015, 2017-2020 Laboratoire de
// Copyright (C) 2012-2015, 2017-2020, 2022 Laboratoire de
// Recherche et Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -26,33 +26,36 @@ namespace spot
class scc_info;
/// \ingroup twa_acc_transform
/// \brief Degeneralize a spot::tgba into an equivalent sba with
/// only one acceptance condition.
/// \brief Degeneralize a generalized (co)Büchi automaton into an
/// equivalent (co)Büchi automaton.
///
/// This algorithm will build a new explicit automaton that has
/// at most (N+1) times the number of states of the original automaton.
/// There are two variants of the function. If the generalizd
/// (co)Büchi acceptance uses N colors, degeneralize() algorithm
/// will builds a state-based (co)Büchi automaton that has at most
/// (N+1) times the number of states of the original automaton.
/// degeneralize_tba() builds a transition-based (co)Büchi automaton
/// that has at most N times the number of states of the original
/// automaton.
///
/// When \a use_z_lvl is set, the level of the degeneralized
/// automaton is reset everytime an SCC is exited. If \a
/// use_cust_acc_orders is set, the degeneralization will compute a
/// custom acceptance order for each SCC (this option is disabled by
/// default because our benchmarks show that it usually does more
/// harm than good). If \a use_lvl_cache is set, everytime an SCC
/// is entered on a state that as already been associated to some
/// level elsewhere, reuse that level (set it to 2 to keep the
/// smallest number, 3 to keep the largest level, and 1 to keep the
/// first level found). If \a ignaccsl is set, we do not directly
/// jump to the accepting level if the entering state has an
/// accepting self-loop. If \a remove_extra_scc is set (the default)
/// we ensure that the output automaton has as many SCCs as the input
/// by removing superfluous SCCs.
/// Additional options control optimizations described in
/// \cite babiak.13.spin . When \a use_z_lvl is set, the level of
/// the degeneralized automaton is reset everytime an SCC is exited.
/// If \a use_cust_acc_orders is set, the degeneralization will
/// compute a custom acceptance order for each SCC (this option is
/// disabled by default because our benchmarks show that it usually
/// does more harm than good). If \a use_lvl_cache is set,
/// everytime an SCC is entered on a state that as already been
/// associated to some level elsewhere, reuse that level (set it to
/// 2 to keep the smallest number, 3 to keep the largest level, and
/// 1 to keep the first level found). If \a ignaccsl is set, we do
/// not directly jump to the accepting level if the entering state
/// has an accepting self-loop. If \a remove_extra_scc is set (the
/// default) we ensure that the output automaton has as many SCCs as
/// the input by removing superfluous SCCs.
///
/// Any of these three options will cause the SCCs of the automaton
/// \a a to be computed prior to its actual degeneralization.
///
/// The degeneralize_tba() variant produce a degeneralized automaton
/// with transition-based acceptance.
///
/// The mapping between each state of the resulting automaton
/// and the original state of the input automaton is stored in the
/// "original-states" named property of the produced automaton. Call
@ -70,6 +73,14 @@ namespace spot
/// Similarly, the property "degen-levels" keeps track of the degeneralization
/// levels. To retrieve it, call
/// `aut->get_named_prop<std::vector<unsigned>>("degen-levels")`.
///
/// As an alternative method to degeneralization, one may also
/// consider ACD transform. acd_transform() will never produce
/// larger automata than degenaralize_tba(), and
/// acd_transform_sbacc() produce smaller automata than
/// degeneralize() on the average. See \cite casares.22.tacas for
/// some comparisons.
///
/// \@{
SPOT_API twa_graph_ptr
degeneralize(const const_twa_graph_ptr& a, bool use_z_lvl = true,

23
spot/twaalgos/postproc.cc
View file

@ -236,7 +236,8 @@ namespace spot
if (COMP_)
tmp = complete(tmp);
bool want_parity = type_ & Parity;
if (want_parity && tmp->acc().is_generalized_buchi())
if (want_parity && (tmp->acc().is_generalized_buchi()
|| tmp->acc().is_generalized_co_buchi()))
tmp = choose_degen(tmp);
assert(!!SBACC_ == state_based_);
if (state_based_)
@ -402,10 +403,19 @@ namespace spot
if (PREF_ == Any)
{
if (type_ == Buchi)
if (type_ == Buchi
|| (type_ == CoBuchi && a->acc().is_generalized_co_buchi()))
{
a = choose_degen(a);
}
else if (type_ == CoBuchi)
{
a = to_nca(a);
if (state_based_ && a->prop_state_acc().is_true())
a = do_sba_simul(a, simul_);
else
a = do_simul(a, simul_);
}
return finalize(a);
}
@ -699,6 +709,8 @@ namespace spot
if (type_ == CoBuchi)
{
unsigned ns = sim->num_states();
bool weak = sim->prop_weak().is_true();
if (PREF_ == Deterministic)
sim = to_dca(sim);
else
@ -706,9 +718,14 @@ namespace spot
// if the input of to_dca/to_nca was weak, the number of
// states has not changed, and running simulation is useless.
if (level_ != Low && ns < sim->num_states())
if (!weak || (level_ != Low && ns < sim->num_states()))
{
if (state_based_ && sim->prop_state_acc().is_true())
sim = do_sba_simul(sim, simul_);
else
sim = do_simul(sim, simul_);
}
}
return finalize(sim);
}

35
tests/core/prodchain.test
View file

@ -26,9 +26,7 @@ shift
for i in 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 \
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42; do
ltl2tgba "{a[*$i]}[]->GFb" > $i.hoa
done
for i in *.hoa; do
set x "$@" --product $i
set x "$@" --product $i.hoa
shift
done
shift
@ -41,8 +39,9 @@ test "4,7,16,1" = `autfilt --stats=%s,%e,%t,%a result`
set x
shift
for i in *.hoa; do
set x "$@" --product-or $i
for i in 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 \
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42; do
set x "$@" --product-or $i.hoa
shift
done
shift
@ -55,28 +54,30 @@ shift
for i in 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 \
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42; do
ltl2tgba -D --cobuchi -S "{a[*$i]}<>->FGb" > $i.hoa
done
for i in *.hoa; do
set x "$@" --product $i
set x "$@" --product $i.hoa
shift
done
shift
autfilt -D --cobuchi --low -S "$@" > result
test "85,170,174,1" = `autfilt --stats=%s,%e,%t,%a result`
autfilt --cobuchi --high -D -S "$@" > result
test "44,47,92,1" = `autfilt --stats=%s,%e,%t,%a result`
: > stats
set x
shift
for i in *.hoa; do
set x "$@" --product-or $i
for i in 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 \
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42; do
ltl2tgba -D --cobuchi "{a[*$i]}<>->FGb" > $i.hoa
set x "$@" --product-or $i.hoa
shift
test $i -eq 1 && shift # remove the first --product
test 2,3,6,1 = `autfilt --high --small --cobuchi "$@" --stats=%s,%e,%t,%a`
test 3,5,10,1 = \
`autfilt --high --small --cobuchi "$@" | autfilt -S --stats=%s,%e,%t,%a`
done
shift
if [ $MAX_ACCSETS -eq 32 ]; then
autfilt --cobuchi -S "$@" 2> error && exit 1
autfilt "$@" 2> error && exit 1
grep 'Too many acceptance sets used' error
fi
# FIXME: implement degeneralization for generalized-co-Büchi
# autfilt --cobuchi --low -S "$@" > result
# test "45,89,180,1" = `autfilt --stats=%s,%e,%t,%a result`
true

13
tests/python/pdegen.py
View file

@ -149,6 +149,9 @@ tc.assertEqual(spot.is_partially_degeneralizable(de), [])
df = spot.partial_degeneralize(f, [0, 1])
df.equivalent_to(f)
tc.assertEqual(str(df.acc()), '(1, Fin(0))')
df2 = spot.degeneralize(f)
df.equivalent_to(f)
tc.assertEqual(str(df2.acc()), '(1, Fin(0))')
try:
df = spot.partial_degeneralize(f, [0, 1, 2])
@ -206,6 +209,16 @@ pdaut7 = spot.partial_degeneralize(aut7, sets)
tc.assertTrue(pdaut7.equivalent_to(aut7))
tc.assertEqual(daut7.num_states(), 10)
tc.assertEqual(pdaut7.num_states(), 10)
ddaut7 = spot.dualize(aut7)
ddaut7a = spot.scc_filter(spot.dualize(spot.degeneralize_tba(ddaut7)))
tc.assertTrue(ddaut7a.equivalent_to(aut7))
tc.assertEqual(ddaut7a.num_states(), daut7.num_states())
ddaut7b = spot.scc_filter(spot.dualize(spot.to_nca(ddaut7)))
tc.assertTrue(ddaut7b.equivalent_to(aut7))
tc.assertEqual(ddaut7b.num_states(), daut7.num_states())
ddaut7c = spot.scc_filter(spot.dualize(spot.to_dca(ddaut7)))
tc.assertTrue(ddaut7c.equivalent_to(aut7))
tc.assertEqual(ddaut7c.num_states(), daut7.num_states())
aut8 = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2"
acc-name: generalized-Buchi 5 Acceptance: 5 Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)