twaalgos: implement restrict_dead_end_edges_here()
Discussed in issue #587. * spot/twaalgos/deadends.cc, spot/twaalgos/deadends.hh: New files. * spot/twaalgos/Makefile.am, python/spot/impl.i: Add them. * tests/core/deadends.test, tests/python/deadends.py: New files. * tests/Makefile.am: Add them. * spot/twa/acc.cc, spot/twa/acc.hh (keep_one_inf_per_branch): New method. * bin/autfilt.cc: Learn option --restrict-dead-end-edges. * NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz
parent
f03e32619a
commit
31511e042a
11 changed files with 588 additions and 1 deletions
|
|
@ -1845,6 +1845,86 @@ namespace spot
|
|||
return force_inf_rec(&back(), rem);
|
||||
}
|
||||
|
||||
namespace
|
||||
{
|
||||
static acc_cond::acc_code keep_one_inf_per_branch_rec
|
||||
(const acc_cond::acc_word* pos, bool inf_seen)
|
||||
{
|
||||
auto start = pos - pos->sub.size;
|
||||
switch (pos->sub.op)
|
||||
{
|
||||
case acc_cond::acc_op::And:
|
||||
{
|
||||
auto cur = --pos;
|
||||
auto res = acc_cond::acc_code::t();
|
||||
// Make a first pass to find Inf(...)
|
||||
if (!inf_seen)
|
||||
do
|
||||
{
|
||||
if (cur->sub.op == acc_cond::acc_op::Inf)
|
||||
{
|
||||
res = acc_cond::acc_code::inf(cur[-1].mark.lowest());
|
||||
inf_seen = true;
|
||||
break;
|
||||
}
|
||||
cur -= cur->sub.size + 1;
|
||||
}
|
||||
while (cur > start);
|
||||
// Now process the rest.
|
||||
do
|
||||
{
|
||||
if (pos->sub.op != acc_cond::acc_op::Inf)
|
||||
{
|
||||
auto tmp =
|
||||
keep_one_inf_per_branch_rec(pos, inf_seen) &
|
||||
std::move(res);
|
||||
std::swap(tmp, res);
|
||||
}
|
||||
pos -= pos->sub.size + 1;
|
||||
}
|
||||
while (pos > start);
|
||||
return res;
|
||||
}
|
||||
case acc_cond::acc_op::Or:
|
||||
{
|
||||
--pos;
|
||||
auto res = acc_cond::acc_code::f();
|
||||
do
|
||||
{
|
||||
auto tmp =
|
||||
keep_one_inf_per_branch_rec(pos, inf_seen) | std::move(res);
|
||||
std::swap(tmp, res);
|
||||
pos -= pos->sub.size + 1;
|
||||
}
|
||||
while (pos > start);
|
||||
return res;
|
||||
}
|
||||
case acc_cond::acc_op::Fin:
|
||||
return acc_cond::acc_code::fin(pos[-1].mark);
|
||||
case acc_cond::acc_op::Inf:
|
||||
if (inf_seen)
|
||||
return acc_cond::acc_code::t();
|
||||
else
|
||||
return acc_cond::acc_code::inf(pos[-1].mark.lowest());
|
||||
case acc_cond::acc_op::FinNeg:
|
||||
case acc_cond::acc_op::InfNeg:
|
||||
SPOT_UNREACHABLE();
|
||||
return {};
|
||||
}
|
||||
SPOT_UNREACHABLE();
|
||||
return {};
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
acc_cond::acc_code
|
||||
acc_cond::acc_code::keep_one_inf_per_branch() const
|
||||
{
|
||||
if (is_t() || is_f())
|
||||
return *this;
|
||||
return keep_one_inf_per_branch_rec(&back(), false);
|
||||
}
|
||||
|
||||
acc_cond::mark_t
|
||||
acc_cond::acc_code::used_sets() const
|
||||
{
|
||||
|
|
|
|||
|
|
@ -1391,6 +1391,13 @@ namespace spot
|
|||
/// \brief For all `x` in \a m, replaces `Fin(x)` by `false`.
|
||||
acc_code force_inf(mark_t m) const;
|
||||
|
||||
/// \brief Rewrite an acceptance condition by keeping at most
|
||||
/// one Inf(x) on each dijunctive branch.
|
||||
///
|
||||
/// For instance `(Fin(0)&Inf(1)&(Inf(2)|Fin(3))) | Inf(4)&Inf(5)`
|
||||
/// will become `(Fin(0)&Inf(1) | Inf(4)`
|
||||
acc_code keep_one_inf_per_branch() const;
|
||||
|
||||
/// \brief Return the set of sets appearing in the condition.
|
||||
acc_cond::mark_t used_sets() const;
|
||||
|
||||
|
|
@ -1992,6 +1999,16 @@ namespace spot
|
|||
return code_.inf_satisfiable(inf);
|
||||
}
|
||||
|
||||
/// \brief Rewrite an acceptance condition by keeping at most
|
||||
/// one Inf(x) on each disjunctive branch.
|
||||
///
|
||||
/// For instance `(Fin(0)&Inf(1)&(Inf(2)|Fin(3))) | Inf(4)&Inf(5)`
|
||||
/// will become `(Fin(0)&Inf(1) | Inf(4)`
|
||||
acc_cond keep_one_inf_per_branch() const
|
||||
{
|
||||
return {num_sets(), code_.keep_one_inf_per_branch()};
|
||||
}
|
||||
|
||||
/// \brief Check potential acceptance of an SCC.
|
||||
///
|
||||
/// Assuming that an SCC intersects all sets in \a
|
||||
|
|
|
|||
|
|
@ -39,6 +39,7 @@ twaalgos_HEADERS = \
|
|||
copy.hh \
|
||||
cycles.hh \
|
||||
dbranch.hh \
|
||||
deadends.hh \
|
||||
degen.hh \
|
||||
determinize.hh \
|
||||
dot.hh \
|
||||
|
|
@ -114,6 +115,7 @@ libtwaalgos_la_SOURCES = \
|
|||
contains.cc \
|
||||
cycles.cc \
|
||||
dbranch.cc \
|
||||
deadends.cc \
|
||||
degen.cc \
|
||||
determinize.cc \
|
||||
dot.cc \
|
||||
|
|
|
|||
181
spot/twaalgos/deadends.cc
Normal file
181
spot/twaalgos/deadends.cc
Normal file
|
|
@ -0,0 +1,181 @@
|
|||
// -*- 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/>.
|
||||
|
||||
#include "config.h"
|
||||
|
||||
#include <vector>
|
||||
#include <spot/twaalgos/deadends.hh>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
namespace
|
||||
{
|
||||
// Gather a disjunction of labels that appears on the edges of a
|
||||
// dead-end state that have to be seen in order to make an
|
||||
// accepting cycle.
|
||||
static bdd
|
||||
gather_useful_labels(const const_twa_graph_ptr& aut,
|
||||
acc_cond::mark_t used_in_cond,
|
||||
unsigned state)
|
||||
{
|
||||
// First, simplify the acceptance condition c based on the set
|
||||
// of colors occurring around the state.
|
||||
auto c = aut->get_acceptance();
|
||||
acc_cond::mark_t used_on_no_edge = used_in_cond;
|
||||
acc_cond::mark_t used_on_all_edges = used_in_cond;
|
||||
for (auto& e: aut->edges())
|
||||
{
|
||||
used_on_no_edge -= e.acc;
|
||||
used_on_all_edges &= e.acc;
|
||||
}
|
||||
|
||||
// if x appears on all edges, then
|
||||
// Fin(x) = false and Inf(x) = true
|
||||
if (used_on_all_edges)
|
||||
c = c.remove(used_on_all_edges, false);
|
||||
// if x appears on no edge at all, then
|
||||
// Fin(x) = true and Inf(x) = false
|
||||
if (used_on_no_edge)
|
||||
c = c.remove(used_on_no_edge, true);
|
||||
|
||||
if (c.is_f())
|
||||
return bddfalse;
|
||||
if (c.is_t())
|
||||
return bddtrue;
|
||||
|
||||
auto d = c.keep_one_inf_per_branch();
|
||||
|
||||
// Now look for edges that are useful to the simplified
|
||||
// acceptance condition.
|
||||
// We consider an edge as useful if its colors satisfy at
|
||||
// least one Fin(x) or Inf(x) in the acceptance.
|
||||
bdd useful = bddfalse;
|
||||
for (auto& e: aut->out(state))
|
||||
if (d.accepting(e.acc))
|
||||
useful |= e.cond;
|
||||
return useful;
|
||||
}
|
||||
}
|
||||
|
||||
twa_graph_ptr
|
||||
restrict_dead_end_edges_here(twa_graph_ptr& aut)
|
||||
{
|
||||
// We don't have anything to do if the automaton is deterministic.
|
||||
if (aut->prop_universal())
|
||||
return aut;
|
||||
if (!aut->is_existential())
|
||||
throw std::runtime_error
|
||||
("restrict_dead_end_edges_here() does not support alternation");
|
||||
unsigned ns = aut->num_states();
|
||||
// Find the states that are dead ends, i.e., that
|
||||
// have only themselves as successors.
|
||||
std::vector<bool> dead_end_states(ns, true);
|
||||
// Also record the disjunction of all self-loops around each
|
||||
// state.
|
||||
std::vector<bdd> self_loops(ns, bddfalse);
|
||||
for (auto& e: aut->edges())
|
||||
if (e.src == e.dst)
|
||||
self_loops[e.src] |= e.cond;
|
||||
else
|
||||
dead_end_states[e.src] = false;
|
||||
|
||||
// If the automaton is weak, we can consider every label of
|
||||
// the dead-end state as useful.
|
||||
bool is_weak = aut->prop_weak().is_true();
|
||||
|
||||
// This will hold the labels of the useful self-loops of the the
|
||||
// dead-end states. But we don't want to initialize it until we
|
||||
// need it.
|
||||
std::vector<bdd> dead_end_useful(is_weak ? 0U : ns, bddfalse);
|
||||
std::vector<bool> dead_end_useful_computed(is_weak ? 0U : ns, false);
|
||||
acc_cond::mark_t used_in_cond = aut->get_acceptance().used_sets();
|
||||
|
||||
std::vector<bdd> label_unions(ns, bddfalse);
|
||||
bool created_false_labels = false;
|
||||
bool nondeterministic_for_sure = false;
|
||||
for (unsigned s = 0; s < ns; ++s)
|
||||
{
|
||||
// compute a union of labels per dead-end destination
|
||||
for (auto& e: aut->out(s))
|
||||
if (e.src != e.dst && dead_end_states[e.dst])
|
||||
label_unions[e.dst] |= e.cond;
|
||||
|
||||
// Iterate over all edges (SRC,COND,DST), find those such that
|
||||
// (1) DST is a dead-end,
|
||||
// (2) Lab(DST,DST))⇒Lab(SRC,SRC)
|
||||
// (3) UsefulLab(DST)⇒Lab(SRC,DST)⇒Lab(SRC,SRC)
|
||||
//
|
||||
// where Lab(X,Y) is the union of all labels between X and Y
|
||||
// And UsefulLab(DST) are the labeled of the "useful" self
|
||||
// loops of DST (see gather_useful_labels).
|
||||
for (auto& e: aut->out(s))
|
||||
if (e.src != e.dst && dead_end_states[e.dst])
|
||||
{
|
||||
if (bdd u = label_unions[e.dst], sl = self_loops[e.src];
|
||||
bdd_implies(u, sl) && bdd_implies(self_loops[e.dst], sl))
|
||||
{
|
||||
// Find the edges of DST that are necessary to an
|
||||
// accepting loop, and gather their labels.
|
||||
bdd d;
|
||||
if (is_weak)
|
||||
{
|
||||
d = self_loops[e.dst];
|
||||
}
|
||||
else
|
||||
{
|
||||
if (!dead_end_useful_computed[e.dst])
|
||||
{
|
||||
dead_end_useful[e.dst] =
|
||||
gather_useful_labels(aut, used_in_cond, e.dst);
|
||||
dead_end_useful_computed[e.dst] = true;
|
||||
}
|
||||
d = dead_end_useful[e.dst];
|
||||
}
|
||||
if (bdd_implies(d, u))
|
||||
{
|
||||
// Restrict the dead-end transition's label.
|
||||
bdd cond = e.cond;
|
||||
cond &= d;
|
||||
if (cond != e.cond)
|
||||
{
|
||||
e.cond = cond;
|
||||
if (cond == bddfalse)
|
||||
created_false_labels = true;
|
||||
else
|
||||
nondeterministic_for_sure = true;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
// reset unions before next iteration
|
||||
for (auto& e: aut->out(s))
|
||||
label_unions[e.dst] = bddfalse;
|
||||
}
|
||||
// Note that restricting those label will never make the automaton
|
||||
// deterministic. In fact, it could make the automaton
|
||||
// non-deterministic. Additionally, completeness will not be
|
||||
// changed. This is because the restricted Lab(SRC,DST) still
|
||||
// implies Lab(SRC,SRC).
|
||||
if (nondeterministic_for_sure)
|
||||
aut->prop_universal(false);
|
||||
if (created_false_labels)
|
||||
aut->merge_edges();
|
||||
return aut;
|
||||
}
|
||||
|
||||
}
|
||||
51
spot/twaalgos/deadends.hh
Normal file
51
spot/twaalgos/deadends.hh
Normal file
|
|
@ -0,0 +1,51 @@
|
|||
// -*- 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/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include <spot/twa/twagraph.hh>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief restrict labels from "dead-end edges"
|
||||
///
|
||||
/// A dead-end edge is an edge between two states S₁ and S₂ such
|
||||
/// that S₂ has only itself as successor. I.e., once a run goes
|
||||
/// through this "dead-end" edge, it gets stuck in S₂.
|
||||
///
|
||||
/// Let Lab(S,D) denote the disjunction of all labels between S and
|
||||
/// D. Let UsefulLab(D,D) be the disjunction of labels of any
|
||||
/// subset of self-loops of D that will intersect all accepting
|
||||
/// cycles around D (one way to compute this subset is to simplify
|
||||
/// the acceptance condition with keep_one_inf_per_branch(), and
|
||||
/// then keep each edge that satisfy it).
|
||||
///
|
||||
/// Now, if the following implications are satisfied
|
||||
///
|
||||
/// ⎧ UsefulLab(D,D) ⇒ Lab(S,D) ⇒ Lab(S,S),<br/>
|
||||
/// ⎨ <br/>
|
||||
/// ⎩ Lab(D,D) ⇒ Lab(S,S).<br/>
|
||||
///
|
||||
/// then any edge between S and D, labeled by ℓ⊆Lab(S,D)
|
||||
/// can be replaced by ℓ∩UsefulLab(D,D).
|
||||
///
|
||||
/// This algorithm has no effect on deterministic automata (where
|
||||
/// it is not possible that Lab(S,D) ⇒ Lab(S,S)).
|
||||
SPOT_API twa_graph_ptr
|
||||
restrict_dead_end_edges_here(twa_graph_ptr& aut);
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue