gf_guarantee_to_ba: save states using histories
This improves gf_guarantee_to_ba() on formulas GF(φ) where the automaton for F(φ) as several leading transiant SCCs. E.g., GF(a <-> XXXa) where we know get results that are as good as those of delag without loosing on the cases where delag's technique would actually produce two big automata. * spot/twaalgos/gfguarantee.cc: Implement this. * spot/twaalgos/gfguarantee.hh, NEWS: Document it. * tests/core/ltl2tgba2.test, tests/core/ltl3ba.test: Add test cases.
This commit is contained in:
Alexandre Duret-Lutz
parent
730c6bbca2
commit
7e9325866f
5 changed files with 221 additions and 26 deletions
28
NEWS
28
NEWS
|
|
@ -94,17 +94,27 @@ New in spot 2.5.3.dev (not yet released)
|
|||
simplified to {1} or {SERE} depending on whether SERE accepts
|
||||
the empty word or not.
|
||||
|
||||
- gf_guarantee_to_ba() is a specialized construction for
|
||||
translating formulas of the form GF(guarantee) to BA or DBA,
|
||||
and fg_safety_to_dca() is a specialized construction for
|
||||
translating formulas of the form FG(safety) to DCA. These
|
||||
are slight generalizations of some constructions proposed
|
||||
by J. Esparza, J. Křentínský, and S. Sickert (LICS'18).
|
||||
- gf_guarantee_to_ba() is a specialized construction for translating
|
||||
formulas of the form GF(guarantee) to BA or DBA, and
|
||||
fg_safety_to_dca() is a specialized construction for translating
|
||||
formulas of the form FG(safety) to DCA. These are generalizations
|
||||
of some constructions proposed by J. Esparza, J. Křentínský, and
|
||||
S. Sickert (LICS'18).
|
||||
|
||||
These are now used by the main translation routine, and can be
|
||||
disabled by passing -x '!gf-guarantee' to ltl2tgba. As an
|
||||
example, the translation of GF(a <-> XXb) to transition-based
|
||||
Büchi went from 9 to 5 states using that construction.
|
||||
disabled by passing -x '!gf-guarantee' to ltl2tgba. For example,
|
||||
here are the size of deterministic transition-based Büchi automata
|
||||
constructed from four GF(guarantee) formulas with two versions of
|
||||
Spot, and converted to other types of deterministic automata by
|
||||
other tools.
|
||||
|
||||
ltl2tgba -D rabinizer 4
|
||||
2.5 2.6 delag ltl2dra
|
||||
------------------------- ----------- -------------
|
||||
GF(a <-> XXa) 9 4 4 9
|
||||
GF(a <-> XXXa) 27 8 8 25
|
||||
GF(((a & Xb) | XXc) & Xd) 6 4 16 5
|
||||
GF((b | Fa) & (b R Xb)) 6 2 3 3
|
||||
|
||||
- Slightly improved log output for the SAT-based minimization
|
||||
functions. The CSV log files now include an additional column
|
||||
|
|
|
|||
|
|
@ -75,13 +75,113 @@ namespace spot
|
|||
if (!state_based)
|
||||
{
|
||||
bool is_det = is_deterministic(aut);
|
||||
bool initial_state_reachable = false;
|
||||
for (auto& e: aut->edges())
|
||||
if (e.dst == init)
|
||||
|
||||
// If the initial state is a trivial SCC, we will be able to
|
||||
// remove it by combining the transitions leading to the
|
||||
// terminal state on the transitions leaving the initial
|
||||
// state. However if some successor of the initial state is
|
||||
// also trivial, we might be able to remove it as well if we
|
||||
// are able to replay two step from the initial state: this
|
||||
// can be generalized to more depth and require computing some
|
||||
// history for each state (i.e., a common suffix to all finite
|
||||
// words leading to this state).
|
||||
std::vector<std::vector<bdd>> histories;
|
||||
bool initial_state_trivial = si.is_trivial(si.initial());
|
||||
|
||||
if (is_det && initial_state_trivial)
|
||||
{
|
||||
initial_state_reachable = true;
|
||||
break;
|
||||
// Compute the max number of steps we want to keep in
|
||||
// the history of each state. This is the largest
|
||||
// number of trivial SCCs you can chain from the initial
|
||||
// state.
|
||||
unsigned max_histories = 1;
|
||||
{
|
||||
std::vector<unsigned> depths(ns, 0U);
|
||||
for (unsigned d: si.succ(ns - 1))
|
||||
depths[d] = 2;
|
||||
for (int scc = ns - 2; scc >= 0; --scc)
|
||||
{
|
||||
if (!si.is_trivial(scc))
|
||||
continue;
|
||||
unsigned sccd = depths[scc];
|
||||
max_histories = std::max(max_histories, sccd);
|
||||
++sccd;
|
||||
for (unsigned d: si.succ(scc))
|
||||
depths[d] = std::max(depths[d], sccd);
|
||||
}
|
||||
}
|
||||
|
||||
unsigned numstates = aut->num_states();
|
||||
histories.resize(numstates);
|
||||
// Compute the one-letter history of each state. If all
|
||||
// transition entering a state have the same label, the history
|
||||
// is that label. Otherwise set it to bddfalse.
|
||||
for (auto& e: aut->edges())
|
||||
{
|
||||
std::vector<bdd>& hd = histories[e.dst];
|
||||
if (hd.empty())
|
||||
hd.push_back(e.cond);
|
||||
else if (hd[0] != e.cond)
|
||||
hd[0] = bddfalse;
|
||||
}
|
||||
// remove all bddfalse, and check if there is a chance to build
|
||||
// a larger history.
|
||||
bool should_continue = false;
|
||||
for (auto&h: histories)
|
||||
if (h.empty())
|
||||
continue;
|
||||
else if (h[0] == bddfalse)
|
||||
h.pop_back();
|
||||
else
|
||||
should_continue = true;
|
||||
// Augment those histories with more letters.
|
||||
unsigned historypos = 0;
|
||||
while (should_continue && historypos + 1 < max_histories)
|
||||
{
|
||||
++historypos;
|
||||
for (auto& e: aut->edges())
|
||||
{
|
||||
std::vector<bdd>& hd = histories[e.dst];
|
||||
if (hd.size() >= historypos)
|
||||
{
|
||||
std::vector<bdd>& hs = histories[e.src];
|
||||
if (hd.size() == historypos)
|
||||
{
|
||||
if (hs.size() >= historypos)
|
||||
hd.push_back(hs[historypos - 1]);
|
||||
else
|
||||
hd.push_back(bddfalse);
|
||||
}
|
||||
else if (hs.size() < historypos
|
||||
|| hd[historypos] != hs[historypos - 1])
|
||||
{
|
||||
hd[historypos] = bddfalse;
|
||||
}
|
||||
}
|
||||
}
|
||||
should_continue = false;
|
||||
for (unsigned n = 0; n < numstates; ++n)
|
||||
{
|
||||
auto& h = histories[n];
|
||||
//for (auto&h: histories)
|
||||
if (h.size() <= historypos)
|
||||
continue;
|
||||
else if (h[historypos] == bddfalse)
|
||||
h.pop_back();
|
||||
else
|
||||
should_continue = true;
|
||||
}
|
||||
}
|
||||
// std::cerr << "computed histories:\n";
|
||||
// for (unsigned n = 0; n < numstates; ++n)
|
||||
// {
|
||||
// std::cerr << n << ": [";
|
||||
// for (bdd b: histories[n])
|
||||
// bdd_print_formula(std::cerr, aut->get_dict(), b) << ", ";
|
||||
// std::cerr << '\n';
|
||||
// }
|
||||
}
|
||||
|
||||
unsigned nedges = aut->num_edges();
|
||||
unsigned new_init = -1U;
|
||||
// The loop might add new edges, but we just want to iterate
|
||||
|
|
@ -89,9 +189,14 @@ namespace spot
|
|||
for (unsigned edge = 1; edge <= nedges; ++edge)
|
||||
{
|
||||
auto& e = aut->edge_storage(edge);
|
||||
// Don't bother with terminal states, they won't be
|
||||
// reachable anymore.
|
||||
if (term[si.scc_of(e.src)])
|
||||
continue;
|
||||
// It will loop
|
||||
if (term[si.scc_of(e.dst)])
|
||||
{
|
||||
if (initial_state_reachable
|
||||
if (!initial_state_trivial
|
||||
// If the source state is the initial state, we
|
||||
// should not try to combine it with itself...
|
||||
|| e.src == init)
|
||||
|
|
@ -105,11 +210,55 @@ namespace spot
|
|||
// state of the automaton, we can get rid of it by
|
||||
// combining the edge reaching the terminal state
|
||||
// with the edges leaving the initial state.
|
||||
bdd econd = e.cond;
|
||||
bool first = true;
|
||||
//
|
||||
// However if we have some histories for e.src
|
||||
// (which implies that the automaton is
|
||||
// deterministic), we can try to replay that from
|
||||
// the initial state first.
|
||||
//
|
||||
// One problem with those histories, is that we do
|
||||
// not know how much of it to replay. It's possible
|
||||
// that we cannot find a matching transition (e.g. if
|
||||
// the history if "b" but the choices are "!a" or "a"),
|
||||
// and its also possible to that playing too much of
|
||||
// history will get us back the terminal state. In both
|
||||
// cases, we should try again with a smaller history.
|
||||
unsigned moved_init = init;
|
||||
if (is_det)
|
||||
{
|
||||
auto& h = histories[e.src];
|
||||
int hsize = h.size();
|
||||
for (int hlen = hsize - 1; hlen > 0; --hlen)
|
||||
{
|
||||
for (int pos = hlen - 1; pos >= 0; --pos)
|
||||
{
|
||||
for (auto& e: aut->out(moved_init))
|
||||
if (bdd_implies(h[pos], e.cond))
|
||||
{
|
||||
if (term[si.scc_of(e.dst)])
|
||||
goto failed;
|
||||
moved_init = e.dst;
|
||||
goto moved;
|
||||
}
|
||||
// if we reach this place, we failed to follow
|
||||
// one step of the history.
|
||||
goto failed;
|
||||
moved:
|
||||
continue;
|
||||
}
|
||||
// we have successfully played all history
|
||||
// to a non-terminal state.
|
||||
break;
|
||||
failed:
|
||||
moved_init = init;
|
||||
continue;
|
||||
}
|
||||
}
|
||||
// Combine this edge with any compatible edge from
|
||||
// the initial state.
|
||||
for (auto& ei: aut->out(init))
|
||||
bdd econd = e.cond;
|
||||
bool first = true;
|
||||
for (auto& ei: aut->out(moved_init))
|
||||
{
|
||||
bdd cond = ei.cond & econd;
|
||||
if (cond != bddfalse)
|
||||
|
|
@ -196,12 +345,22 @@ namespace spot
|
|||
f = nest_f(f);
|
||||
}
|
||||
twa_graph_ptr aut = ltl_to_tgba_fm(f, dict, true);
|
||||
twa_graph_ptr reduced = minimize_obligation(aut, f, nullptr,
|
||||
!deterministic);
|
||||
twa_graph_ptr reduced = minimize_obligation(aut, f);
|
||||
if (reduced == aut)
|
||||
return nullptr;
|
||||
scc_info si(reduced);
|
||||
if (!is_terminal_automaton(reduced, &si, true))
|
||||
return nullptr;
|
||||
do_g_f_terminal_inplace(si, state_based);
|
||||
if (!deterministic)
|
||||
{
|
||||
scc_info si2(aut);
|
||||
if (!is_terminal_automaton(aut, &si2, true))
|
||||
return reduced;
|
||||
do_g_f_terminal_inplace(si2, state_based);
|
||||
if (aut->num_states() <= reduced->num_states())
|
||||
return aut;
|
||||
}
|
||||
return reduced;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -49,9 +49,10 @@ namespace spot
|
|||
///
|
||||
/// If the formula \a gf has the form GΦ where Φ matches either F(φ)
|
||||
/// or F(φ₁)|F(φ₂)|...|F(φₙ), we translate Φ into A_Φ and attempt to
|
||||
/// minimize it to a WDBA. If \a deterministic is not set, we keep
|
||||
/// the minimized automaton only if A_Φ is larger. If the resulting
|
||||
/// automaton is terminal, we then call g_f_terminal_inplace().
|
||||
/// minimize it to a WDBA W_Φ. If the resulting automaton is
|
||||
/// terminal, we then call g_f_terminal_inplace(W_Φ). If \a
|
||||
/// deterministic is not set, we keep the minimized automaton only
|
||||
/// if g_f_terminal_inplace(A_Φ) is larger.
|
||||
///
|
||||
/// Return nullptr if the input formula is not of the supported
|
||||
/// form.
|
||||
|
|
@ -59,7 +60,9 @@ namespace spot
|
|||
/// This construction generalizes a construction in the LICS'18
|
||||
/// paper of J. Esparza, J. Křetínský, and S. Sickert. This version
|
||||
/// will work if Φ represent a safety property, even if it is not a
|
||||
/// syntactic safety.
|
||||
/// syntactic safety. When building deterministic transition-based
|
||||
/// automata, it will also try to remove useless trivial components
|
||||
/// at the beginning of wdba(A_Φ).
|
||||
SPOT_API twa_graph_ptr
|
||||
gf_guarantee_to_ba_maybe(formula gf, const bdd_dict_ptr& dict,
|
||||
bool deterministic = true, bool state_based = false);
|
||||
|
|
|
|||
|
|
@ -360,3 +360,19 @@ p-patterns,20, 1,8, 1,8, 3,24, 3,24
|
|||
EOF
|
||||
|
||||
diff output expected
|
||||
|
||||
|
||||
# These four formulas appear in a NEWS entry for Spot 2.6
|
||||
cat >formulas <<EOF
|
||||
GF((a & XXa) | (!a & XX!a)), 4,8, 4,8, 6,14, 7,14
|
||||
GF((a & XXXa) | (!a & XXX!a)), 7,14, 8,16, 8,18, 15,30
|
||||
GF(((a & Xb) | XXc) & Xd), 4,60, 4,64, 4,68, 5,80
|
||||
GF((b | Fa) & (b R Xb)), 2,4, 2,4, 3,6, 3,12
|
||||
EOF
|
||||
|
||||
ltl2tgba -Fformulas/1 --stats='%f, %s,%t' |
|
||||
ltl2tgba -D -F-/1 --stats='%f,%>, %s,%t' |
|
||||
ltl2tgba -B -F-/1 --stats='%f,%>, %s,%t' |
|
||||
ltl2tgba -BD -F-/1 --stats='%f,%>, %s,%t' > output
|
||||
|
||||
diff formulas output
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
|
||||
# Copyright (C) 2016, 2017, 2018 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -39,8 +39,15 @@ export SPOT_HOA_TOLERANT
|
|||
# compatible with Spin's syntax.
|
||||
(
|
||||
echo _x
|
||||
# Some formula used by Spot's GF(guarantee) translation.
|
||||
cat <<EOF
|
||||
GF((a & XXa) | (!a & XX!a))
|
||||
GF((a & XXXa) | (!a & XXX!a))
|
||||
GF(((a & Xb) | XXc) & Xd)
|
||||
GF((b | Fa) & (b R Xb))
|
||||
EOF
|
||||
randltl -n 30 2
|
||||
) | ltlcross 'ltl3ba -H1' 'ltl3ba -H2' 'ltl3ba -H3' \
|
||||
) | ltlcross -D 'ltl3ba -H1' 'ltl3ba -H2' 'ltl3ba -H3' ltl2tgba \
|
||||
--ambiguous --strength --csv=output.csv
|
||||
|
||||
grep _x output.csv && exit 1
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue