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

implement BA acceptance set reduction and enlargement

Browse source 
For issue #570.

* spot/twaalgos/cleanacc.hh,
spot/twaalgos/cleanacc.cc (reduce_buchi_acceptance_set_here,
enlarge_buchi_acceptance_set_here): New functions.
* bin/autfilt.cc: Add options --reduce-acceptance-set and
--enlarge-acceptance-set.
* tests/core/basetred.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2024-04-25 17:59:10 +02:00
parent ab7f4f51c4
commit be102e09d4
6 changed files with 311 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
NEWS
View file

@ -35,6 +35,10 @@ New in spot 2.11.6.dev (not yet released)
the automaton using a basis of disjoint labels. See
https://spot.lre.epita.fr/tut25.html for some motivation.
- autfilt learned --reduce-acceptance-set/--enlarge-acceptance-set
to heurisitcally remove/add to unnecessary acceptance marks in
Büchi automata. (Issue #570)
- ltlfilt has a new option --relabel-overlapping-bool=abc|pnn that
will replace boolean subformulas by fresh atomic propositions even
if those subformulas share atomic propositions.
@ -142,6 +146,11 @@ New in spot 2.11.6.dev (not yet released)
The above also impacts autfilt --included-in option.
- spot::reduce_buchi_acceptance_set_here() and
spot::enlarge_buchi_acceptance_set_here() will heuristically
remove/add unnecessary acceptance marks in Büchi automata.
(Issue #570.)
- Given a twa_word_ptr W and a twa_ptr A both sharing the same
alphabet, one can now write W->intersects(A) or A->intersects(W)
instead of the longuer W->as_automaton()->intersects(A) or

27
bin/autfilt.cc
View file

@ -102,6 +102,7 @@ enum {
OPT_DUALIZE,
OPT_DNF_ACC,
OPT_EDGES,
OPT_ENLARGE_ACCEPTANCE_SET,
OPT_EQUIVALENT_TO,
OPT_EXCLUSIVE_AP,
OPT_GENERALIZED_RABIN,
@ -139,6 +140,7 @@ enum {
OPT_PRODUCT_AND,
OPT_PRODUCT_OR,
OPT_RANDOMIZE,
OPT_REDUCE_ACCEPTANCE_SET,
OPT_REJ_SCCS,
OPT_REJECT_WORD,
OPT_REM_AP,
@ -278,6 +280,12 @@ static const argp_option options[] =
{ "nth", 'N', "RANGE", 0,
"assuming input automata are numbered from 1, keep only those in RANGE",
0 },
{ "enlarge-acceptance-set", OPT_ENLARGE_ACCEPTANCE_SET, nullptr, 0,
"enlarge the number of accepting transitions (or states if -S) in a "
"Büchi automaton", 0 },
{ "reduce-acceptance-set", OPT_REDUCE_ACCEPTANCE_SET, nullptr, 0,
"reduce the number of accepting transitions (or states if -S) in a "
"Büchi automaton", 0 },
/**************************************************/
RANGE_DOC_FULL,
WORD_DOC,
@ -705,6 +713,8 @@ static int opt_highlight_accepting_run = -1;
static bool opt_highlight_languages = false;
static bool opt_dca = false;
static bool opt_streett_like = false;
static bool opt_enlarge_acceptance_set = false;
static bool opt_reduce_acceptance_set = false;
static spot::twa_graph_ptr
ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
@ -899,12 +909,12 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_dnf_acc = true;
opt_cnf_acc = false;
break;
case OPT_STREETT_LIKE:
opt_streett_like = true;
break;
case OPT_EDGES:
opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
break;
case OPT_ENLARGE_ACCEPTANCE_SET:
opt_enlarge_acceptance_set = true;
break;
case OPT_EXCLUSIVE_AP:
opt->excl_ap.add_group(arg);
break;
@ -1164,6 +1174,9 @@ parse_opt(int key, char* arg, struct argp_state*)
randomize_st = true;
}
break;
case OPT_REDUCE_ACCEPTANCE_SET:
opt_reduce_acceptance_set = true;
break;
case OPT_REJ_SCCS:
opt_rej_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
opt_art_sccs_set = true;
@ -1215,6 +1228,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_STATES:
opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
break;
case OPT_STREETT_LIKE:
opt_streett_like = true;
break;
case OPT_STRIPACC:
opt_stripacc = true;
break;
@ -1670,6 +1686,11 @@ namespace
else if (opt_rem_unused_ap) // constrain(aut, true) already does that
aut->remove_unused_ap();
if (opt_enlarge_acceptance_set)
spot::enlarge_buchi_acceptance_set_here(aut, sbacc);
if (opt_reduce_acceptance_set)
spot::reduce_buchi_acceptance_set_here(aut, sbacc);
if (opt_split_edges)
aut = spot::split_edges(aut);
else if (opt_separate_edges)

133
spot/twaalgos/cleanacc.cc
View file

@ -18,6 +18,8 @@
#include "config.h"
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/genem.hh>
namespace spot
{
@ -668,4 +670,135 @@ namespace spot
{
return simplify_acceptance_here(make_twa_graph(aut, twa::prop_set::all()));
}
twa_graph_ptr
reduce_buchi_acceptance_set_here(twa_graph_ptr& aut, bool preserve_sbacc)
{
if (!aut->acc().is_buchi())
throw std::invalid_argument
("reduce_buchi_acceptance_set_here() expects a Büchi automaton");
if (!preserve_sbacc)
aut->prop_state_acc(trival::maybe());
aut->prop_weak(trival::maybe()); // issue #562
// For each accepting edge in the automaton, we will test if the
// acceptance mark can be removed. To test this, we have to make
// sure that no accepting cycle depends exclusively on this mark.
// We do so by temporary changing the mark of the current edge to
// {1}, and then using the following acceptance condition to
// ensure that there is no cycle that pass through {1} when we
// ignore all other edges with {0}.
acc_cond testacc = acc_cond(2, (acc_cond::acc_code::fin({0}) &
acc_cond::acc_code::inf({1})));
acc_cond::mark_t one{1};
acc_cond::mark_t zero{0};
acc_cond::mark_t none{};
scc_info si(aut, scc_info_options::TRACK_STATES);
if (!preserve_sbacc || !aut->prop_state_acc())
// transition-based version
for (auto& e: aut->edges())
{
if (e.acc == none) // nothing to remove
continue;
unsigned srcscc = si.scc_of(e.src);
if (srcscc != si.scc_of(e.dst)) // transient edge
{
e.acc = none;
}
else
{
e.acc = one;
if (generic_emptiness_check_for_scc(si, srcscc, testacc))
e.acc = none;
else
e.acc = zero;
}
}
else
// state-based version
for (unsigned s = 0, ns = aut->num_states(); s < ns; ++s)
{
acc_cond::mark_t acc = aut->state_acc_sets(s);
if (acc == none) // nothing to remove
continue;
for (auto& e: aut->out(s))
e.acc = one;
if (generic_emptiness_check_for_scc(si, si.scc_of(s), testacc))
acc = none;
for (auto& e: aut->out(s))
e.acc = acc;
}
return aut;
}
twa_graph_ptr
enlarge_buchi_acceptance_set_here(twa_graph_ptr& aut, bool preserve_sbacc)
{
if (!aut->acc().is_buchi())
throw std::invalid_argument
("enlarge_buchi_acceptance_set_here() expects a Büchi automaton");
if (!preserve_sbacc)
aut->prop_state_acc(trival::maybe());
aut->prop_weak(trival::maybe()); // issue #562
// For each edge not marked as accepting will test if an
// acceptance mark can be added. To test this, we have to make
// sure that no rejecting cycle goes through this edge.
// We do so my temporary changing the mark of the current edge to
// {1}, and then using the following acceptance condition to
// ensure that there is no accepting cycle that pass through {1}
// when we ignore all other edges with {0}.
acc_cond testacc =
acc_cond(2, acc_cond::acc_code::fin({0}) & acc_cond::acc_code::inf({1}));
acc_cond::mark_t one{1};
acc_cond::mark_t zero{0};
acc_cond::mark_t none{};
scc_info si(aut, scc_info_options::TRACK_STATES);
if (!preserve_sbacc || !aut->prop_state_acc())
// transition-based version
for (auto& e: aut->edges())
{
if (e.acc == zero) // nothing to add
continue;
unsigned srcscc = si.scc_of(e.src);
if (si.is_rejecting_scc(srcscc)) // nothing to add
continue;
if (srcscc != si.scc_of(e.dst)) // transient edge
{
e.acc = zero;
}
else
{
e.acc = one;
if (generic_emptiness_check_for_scc(si, srcscc, testacc))
e.acc = zero;
else
e.acc = none;
}
}
else
// state-based version
for (unsigned s = 0, ns = aut->num_states(); s < ns; ++s)
{
acc_cond::mark_t acc = aut->state_acc_sets(s);
if (acc == zero) // nothing to add
continue;
unsigned srcscc = si.scc_of(s);
if (si.is_rejecting_scc(srcscc)) // nothing to add
continue;
for (auto& e: aut->out(s))
e.acc = one;
if (generic_emptiness_check_for_scc(si, srcscc, testacc))
acc = zero;
for (auto& e: aut->out(s))
e.acc = acc;
}
return aut;
}
}

28
spot/twaalgos/cleanacc.hh
View file

@ -70,4 +70,32 @@ namespace spot
SPOT_API twa_graph_ptr
simplify_acceptance(const_twa_graph_ptr aut);
/// @}
/// \ingroup twa_acc_transform
/// \brief Reduce the acceptance set of a Büchi automaton
///
/// Iterate over all accepting transitions, and remove them from the
/// acceptance set if this does not change the language.
///
/// This modifies the automaton in place.
///
/// If the input has state-based acceptance, it might lose it,
/// unless \a preserve_sbacc is set.
SPOT_API twa_graph_ptr
reduce_buchi_acceptance_set_here(twa_graph_ptr& aut,
bool preserve_sbacc = false);
/// \ingroup twa_acc_transform
/// \brief Enlarge the acceptance set of a Büchi automaton
///
/// Iterate over all accepting transitions, and add them to the
/// acceptance set if this cannot change the language.
///
/// This modifies the automaton in place.
///
/// If the input has state-based acceptance, it might lose it,
/// unless \a preserve_sbacc is set.
SPOT_API twa_graph_ptr
enlarge_buchi_acceptance_set_here(twa_graph_ptr& aut,
bool preserve_sbacc = false);
}

1
tests/Makefile.am
View file

@ -224,6 +224,7 @@ TESTS_twa = \
core/568.test \
core/acc.test \
core/acc2.test \
core/basetred.test \
core/bdddict.test \
core/cube.test \
core/alternating.test \

116
tests/core/basetred.test Executable file
View file

@ -0,0 +1,116 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) by the Spot authors, see the AUTHORS file for details.
#
# 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
. ./defs
set -e
genaut --cycle-log-nba=3 > in1.hoa
test 3 -eq `grep -c '{0}' in1.hoa`
autfilt --reduce-acceptance-set in1.hoa > out1.hoa
autfilt --enlarge-acceptance-set in1.hoa > out1l.hoa
autfilt --reduce-acceptance-set out1l.hoa > out1r.hoa
autfilt --enlarge-acceptance-set out1r.hoa > out1rl.hoa
test 1 -eq `grep -c '{0}' out1.hoa`
test 9 -eq `grep -c '{0}' out1l.hoa`
test 1 -eq `grep -c '{0}' out1r.hoa`
diff out1l.hoa out1rl.hoa
autfilt --reduce-acceptance-set -S in1.hoa > out1b.hoa
autfilt --enlarge-acceptance-set -S in1.hoa > out1lb.hoa
autfilt --enlarge-acceptance-set -S out1b.hoa > out1lbb.hoa
test 1 -eq `grep -c '{0}' out1b.hoa`
test 3 -eq `grep -c '{0}' out1lb.hoa`
test 3 -eq `grep -c '{0}' out1lbb.hoa`
diff out1.hoa out1b.hoa
diff out1lb.hoa out1lbb.hoa
cat >in2.hoa <<EOF
HOA: v1
States: 3
Start: 0
AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
--BODY--
State: 0 {0}
[t] 0
[t] 1
[t] 2
State: 1 {0}
[t] 2
State: 2 {0}
[t] 0
--END--
EOF
autfilt --reduce-acceptance-set in2.hoa > out2.hoa
autfilt --reduce-acceptance-set -S in2.hoa > out2b.hoa
autfilt --enlarge-acceptance-set out2.hoa > out2l.hoa
autfilt --enlarge-acceptance-set -S out2b.hoa > out2bl.hoa
cat >ex2.hoa <<EOF
HOA: v1
States: 3
Start: 0
AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
--BODY--
State: 0
[t] 0 {0}
[t] 1
[t] 2
State: 1
[t] 2
State: 2
[t] 0 {0}
--END--
EOF
cat >ex2b.hoa <<EOF
HOA: v1
States: 3
Start: 0
AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0 {0}
[t] 0
[t] 1
[t] 2
State: 1
[t] 2
State: 2
[t] 0
--END--
EOF
diff out2.hoa ex2.hoa
diff out2b.hoa ex2b.hoa
diff out2l.hoa in2.hoa
diff out2bl.hoa in2.hoa
randaut -n 20 -b -a.7 2 |
autcross --language-preserved --verbose \
'autfilt --reduce-acceptance-set' \
'autfilt --enlarge-acceptance-set' \
'autfilt --enlarge-acceptance-set --reduce-acceptance-set'