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

sccfilter: some inherently-weak automata should have t acceptance

Browse source 
* spot/twaalgos/sccfilter.cc: If an inherently-weak automaton has
no rejecting cycle, reduce its acceptance to t instead of Büchi.
* spot/twa/acc.hh (operator==, operator<): Fix comparisons of
true acceptances.
* NEWS: Mention these two changes.
* spot/twaalgos/sccfilter.hh: Update documentation.
* spot/twaalgos/determinize.cc (tgba_determinize): The call
to scc_filter assume that the input BA is never reduced to t
acceptance.  Call scc_filter with an extra option to ensure that.
* spot/twaalgos/postproc.cc (do_scc_filter): Adjust to add the
extra option when we want to build Büchi or coBuchi.
(ensure_ba): Don't mark trivial SCCs as accepting.
* tests/core/complement.test, tests/core/dstar.test,
tests/core/ltlsynt.test, tests/core/readsave.test,
tests/core/wdba2.test, tests/python/_product_susp.ipynb,
tests/python/automata-io.ipynb, tests/python/dualize.py,
tests/python/highlighting.ipynb, tests/python/intrun.py,
tests/python/setacc.py, tests/python/simstate.py,
tests/python/stutter-inv.ipynb, tests/python/zlktree.py: Adjust test
cases.
This commit is contained in:
Alexandre Duret-Lutz 2023-11-17 13:41:19 +01:00
parent 13377542cd
commit 0e71dd70c1
20 changed files with 857 additions and 842 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/twaalgos/determinize.cc
View file

@ -881,7 +881,7 @@ namespace spot
aut_tmp->copy_state_names_from(a);
if (use_simulation)
{
aut_tmp = spot::scc_filter(aut_tmp);
aut_tmp = spot::scc_filter(aut_tmp, true, nullptr, true);
auto aut2 = simulation(aut_tmp, &implications, trans_pruning);
if (pretty_print)
aut2->copy_state_names_from(aut_tmp);

27
spot/twaalgos/postproc.cc
View file

@ -47,13 +47,28 @@ namespace spot
namespace
{
static twa_graph_ptr
ensure_ba(twa_graph_ptr& a)
ensure_ba(twa_graph_ptr& a, bool no_trivial)
{
if (a->acc().is_t())
{
auto m = a->set_buchi();
for (auto& t: a->edges())
t.acc = m;
if (!no_trivial)
{
for (auto& t: a->edges())
t.acc = m;
}
else
{
scc_info si(a);
unsigned nc = si.scc_count();
for (unsigned i = 0; i < nc; ++i)
// Cannot use "is_accepting_scc" because the
// acceptance condition was already changed.
if (!si.is_trivial(i))
for (auto& e: si.edges_of(i))
const_cast<acc_cond::mark_t&>(e.acc) = m;
}
a->prop_state_acc(true);
}
return a;
}
@ -219,7 +234,7 @@ namespace spot
if (state_based_ && a->prop_state_acc().is_true())
return scc_filter_states(a, arg);
else
return scc_filter(a, arg);
return scc_filter(a, arg, nullptr, type_ == CoBuchi || type_ == Buchi);
}
twa_graph_ptr
@ -251,7 +266,7 @@ namespace spot
if (state_based_)
tmp = sbacc(tmp);
if (type_ == Buchi)
tmp = ensure_ba(tmp);
tmp = ensure_ba(tmp, level_ == High);
if (want_parity)
{
if (!acd_was_used_ || (COMP_ && !was_complete))
@ -480,7 +495,7 @@ namespace spot
// We just need to add an acceptance set if there is none.
dba_is_minimal = dba_is_wdba = true;
if (type_ == Buchi)
ensure_ba(dba);
ensure_ba(dba, level_ == High);
}
else
{

40
spot/twaalgos/sccfilter.cc
View file

@ -124,12 +124,14 @@ namespace spot
}
};
// Transform inherently weak automata into weak Büchi automata.
template <bool buchi, class next_filter = id_filter>
// Transform inherently weak automata into weak Büchi automata, or
// t automata.
template <bool buchi, bool keep_one_color, class next_filter = id_filter>
struct weak_filter: next_filter
{
acc_cond::mark_t acc_m = {0};
acc_cond::mark_t rej_m = {};
bool true_acc = false;
template<typename... Args>
weak_filter(scc_info* si, Args&&... args)
@ -141,6 +143,23 @@ namespace spot
if (si->get_aut()->acc().is_co_buchi())
rej_m = {0};
}
if (!keep_one_color)
{
unsigned ns = si->scc_count();
bool may_reject = false;
for (unsigned i = 0; i < ns; ++i)
if (!si->is_trivial(i) && !si->is_accepting_scc(i))
{
may_reject = true;
break;
}
if (!may_reject)
{
true_acc = true;
acc_m = {};
rej_m = {};
}
}
}
filtered_trans trans(unsigned src, unsigned dst,
@ -164,7 +183,9 @@ namespace spot
void fix_acceptance(const twa_graph_ptr& out)
{
if (buchi)
if (true_acc)
out->set_generalized_buchi(0);
else if (buchi)
out->set_buchi();
else
out->copy_acceptance_of(this->si->get_aut());
@ -216,8 +237,8 @@ namespace spot
//
// The above rules are made more complex with two flags:
//
// - If PreserveSBA is set, we have to tree a transition
// leaving an SCC as other transitions inside the SCC,
// - If PreserveSBA is set, we have to treat a transition
// leaving an SCC like other transitions inside the SCC,
// otherwise we will break the property that all
// transitions leaving the same state have identical set
// membership.
@ -442,7 +463,7 @@ namespace spot
twa_graph_ptr
scc_filter(const const_twa_graph_ptr& aut, bool remove_all_useless,
scc_info* given_si)
scc_info* given_si, bool keep_one_color)
{
twa_graph_ptr res;
scc_info* si = given_si;
@ -455,10 +476,13 @@ namespace spot
| scc_info_options::TRACK_STATES_IF_FIN_USED);
if (aut->acc().is_t() || aut->acc().is_co_buchi())
res =
scc_filter_apply<state_filter<weak_filter<false>>>(aut, si);
scc_filter_apply<state_filter<weak_filter<false, false>>>(aut, si);
else if (keep_one_color)
res =
scc_filter_apply<state_filter<weak_filter<true, true>>>(aut, si);
else
res =
scc_filter_apply<state_filter<weak_filter<true>>>(aut, si);
scc_filter_apply<state_filter<weak_filter<true, false>>>(aut, si);
}
else if (aut->acc().is_generalized_buchi())
{

17
spot/twaalgos/sccfilter.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015, 2018 Laboratoire de
// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015, 2018, 2023 Laboratoire de
// Recherche et Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -51,20 +51,25 @@ namespace spot
/// accepting SCC are accepting.
///
/// If the input is inherently weak, the output will be a weak
/// automaton with state-based acceptance. The acceptance condition
/// is set to Büchi unless the input was co-Büchi or t (in which
/// case we keep this acceptance).
/// automaton with state-based acceptance. If the automaton had no
/// rejecting SCC, the acceptance condition is set to "t".
/// Otherwise, the acceptance condition is set to Büchi unless the
/// input was co-Büchi (in which case we keep this acceptance).
///
/// If \a given_sm is supplied, the function will use its result
/// If \a given_si is supplied, the function will use its result
/// without computing a map of its own.
///
/// If \a keep_one_color is set, the output will keep at least color
/// if the input had colors. Normally scc_filter removes as many
/// colors as possible.
///
/// \warning Calling scc_filter on a TωA that is not inherently weak
/// and has the SBA property (i.e., transitions leaving accepting
/// states are all marked as accepting) may destroy this property.
/// Use scc_filter_states() instead.
SPOT_API twa_graph_ptr
scc_filter(const const_twa_graph_ptr& aut, bool remove_all_useless = false,
scc_info* given_si = nullptr);
scc_info* given_si = nullptr, bool keep_one_color = false);
/// \brief Prune unaccepting SCCs.
///