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

minimize_wdba: use a product to decide accepting SCCs

Browse source 
Fixes #347.

* spot/twaalgos/minimize.cc, spot/twaalgos/minimize.hh: An SCC of the
determinized automaton is marked as accepting if it intersects any
accepting SCC of the original automaton.  This can be checked by
making a product.  As a consequence the output of minimize_wdba() now
always includes the original language, and minimize_obligation() only
needs a single containment check.
* NEWS: Mention this.
This commit is contained in:
Alexandre Duret-Lutz 2018-06-05 17:42:44 +02:00
parent 4afd1856a6
commit 730c6bbca2
3 changed files with 48 additions and 124 deletions
Download patch file Download diff file Expand all files Collapse all files

6
NEWS
View file

@ -130,6 +130,12 @@ New in spot 2.5.3.dev (not yet released)
the resulting TGBA makes it more likely that simulation-based
reductions will reduce it.
- When applied to automata that are not WDBA-realizable,
spot::minimize_wdba() was changed to produce an automaton
recognizing a language that includes the original one. As a
consequence spot::minimize_obligation() now only needs one
containement check instead of two.
- The LTL simplification routine learned the following reductions,
where f is any formula, and q is a "suspendable" formula (a.k.a.
both a pure eventuality and purely universal).

146
spot/twaalgos/minimize.cc
View file

@ -42,7 +42,6 @@
#include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/bfssteps.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/remfin.hh>
@ -152,93 +151,6 @@ namespace spot
return res;
}
struct wdba_search_acc_loop final : public bfs_steps
{
wdba_search_acc_loop(const const_twa_ptr& det_a,
unsigned scc_n, scc_info& sm,
power_map& pm, const state* dest)
: bfs_steps(det_a), scc_n(scc_n), sm(sm), pm(pm), dest(dest)
{
seen(dest);
}
virtual const state*
filter(const state* s) override
{
s = seen(s);
if (sm.scc_of(std::static_pointer_cast<const twa_graph>(a_)
->state_number(s)) != scc_n)
return nullptr;
return s;
}
virtual bool
match(twa_run::step&, const state* to) override
{
return to == dest;
}
unsigned scc_n;
scc_info& sm;
power_map& pm;
const state* dest;
state_unicity_table seen;
};
bool
wdba_scc_is_accepting(const const_twa_graph_ptr& det_a, unsigned scc_n,
const const_twa_graph_ptr& orig_a, scc_info& sm,
power_map& pm)
{
// Get some state from the SCC #n.
const state* start = det_a->state_from_number(sm.one_state_of(scc_n));
// Find a loop around START in SCC #n.
wdba_search_acc_loop wsal(det_a, scc_n, sm, pm, start);
twa_run::steps loop;
const state* reached = wsal.search(start, loop);
assert(reached == start);
(void)reached;
// Build an automaton representing this loop.
auto loop_a = make_twa_graph(det_a->get_dict());
twa_run::steps::const_iterator i;
int loop_size = loop.size();
loop_a->new_states(loop_size);
int n;
for (n = 1, i = loop.begin(); n < loop_size; ++n, ++i)
{
loop_a->new_edge(n - 1, n, i->label);
i->s->destroy();
}
assert(i != loop.end());
loop_a->new_edge(n - 1, 0, i->label);
i->s->destroy();
assert(++i == loop.end());
loop_a->set_init_state(0U);
// Check if the loop is accepting in the original automaton.
bool accepting = false;
// Iterate on each original state corresponding to start.
const power_map::power_state& ps =
pm.states_of(det_a->state_number(start));
for (auto& s: ps)
{
// Construct a product between LOOP_A and ORIG_A starting in
// S. FIXME: This could be sped up a lot!
if (!product(loop_a, orig_a, 0U, s)->is_empty())
{
accepting = true;
break;
}
}
return accepting;
}
static twa_graph_ptr minimize_dfa(const const_twa_graph_ptr& det_a,
hash_set* final, hash_set* non_final)
{
@ -492,10 +404,38 @@ namespace spot
// (i.e., it is not the start of any accepting word).
scc_info sm(det_a);
if (input_is_det)
sm.determine_unknown_acceptance();
unsigned scc_count = sm.scc_count();
// SCCs of det_a are assumed accepting if any of their loop
// corresponds to an accepted word in the original automaton.
// If the automaton is the same as det_a, we can simply ask that
// to sm.
std::vector<char> is_accepting_scc(scc_count, 0);
if (input_is_det)
{
sm.determine_unknown_acceptance();
for (unsigned m = 0; m < scc_count; ++m)
is_accepting_scc[m] = sm.is_accepting_scc(m);
}
else
{
twa_graph_ptr prod = spot::product(a, det_a);
//print_dot(std::cerr, prod, "s");
const product_states* pmap =
prod->get_named_prop<product_states>("product-states");
assert(pmap);
scc_info sip(prod, scc_info_options::TRACK_STATES_IF_FIN_USED);
sip.determine_unknown_acceptance();
unsigned prod_scc_count = sip.scc_count();
for (unsigned m = 0; m < prod_scc_count; ++m)
if (sip.is_accepting_scc(m))
{
unsigned right_state = (*pmap)[sip.one_state_of(m)].second;
is_accepting_scc[sm.scc_of(right_state)] = true;
}
}
// SCC that have been marked as useless.
std::vector<bool> useless(scc_count);
// The "color". Even number correspond to
@ -534,14 +474,7 @@ namespace spot
}
else
{
// Regular SCCs are accepting if any of their loop
// corresponds to an accepted word in the original
// automaton. If the automaton is the same as det_a, we
// can simply ask that to sm.
bool acc_scc = input_is_det
? sm.is_accepting_scc(m)
: wdba_scc_is_accepting(det_a, m, a, sm, pm);
if (acc_scc)
if (is_accepting_scc[m])
{
is_useless = false;
d[m] = l & ~1; // largest even number inferior or equal
@ -608,10 +541,6 @@ namespace spot
// FIXME: we do not need to minimize the wdba to test realizability.
auto min_aut = minimize_wdba(aut);
if (!is_deterministic(aut)
&& !product(aut, remove_fin(dualize(min_aut)))->is_empty())
return false;
twa_graph_ptr aut_neg;
if (is_deterministic(aut))
{
@ -668,17 +597,6 @@ namespace spot
if (is_terminal_automaton(aut_f))
return min_aut_f;
// If the input was deterministic, then by construction
// min_aut_f accepts at least all the words of aut_f, so we do
// not need the reverse check. Otherwise, complement the
// minimized WDBA to test the reverse inclusion.
// (remove_fin() has a special handling of weak automata, and
// dualize also has a special handling of deterministic
// automata, so all these steps are quite efficient.)
if (!is_deterministic(aut_f)
&& !product(aut_f, remove_fin(dualize(min_aut_f)))->is_empty())
return std::const_pointer_cast<twa_graph>(aut_f);
// Build negation automaton if not supplied.
if (!aut_neg_f)
{

20
spot/twaalgos/minimize.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2018
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -64,17 +64,17 @@ namespace spot
/// Deterministic Büchi Automaton, and construct a minimal WDBA for
/// this language. This essentially chains three algorithms:
/// determinization, acceptance adjustment (Löding's coloring
/// algorithm), and minimization (using a Moore-like approache).
/// algorithm), and minimization (using a Moore-like approach).
///
/// If the input automaton does not represent a WDBA language,
/// the resulting automaton is still a WDBA, but it will not
/// be equivalent to the original automaton. Use the
/// minimize_obligation() function if you are not sure whether
/// it is safe to call this function.
///
/// Please see the following paper for a discussion of this
/// technique.
/// If the input automaton does not represent a WDBA language, the
/// resulting automaton is still a WDBA, but it will accept a
/// superset of the original language. Use the
/// minimize_obligation() function if you are not sure whether it is
/// safe to call this function.
///
/// The construction is inspired by the following paper, however we
/// guarantee that the output language is a subsets of the original
/// language while they don't.
/** \verbatim
@InProceedings{ dax.07.atva,
author = {Christian Dax and Jochen Eisinger and Felix Klaedtke},