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

new conversion for Streett->GBA

Browse source 
* src/twaalgos/totgba.hh, src/twaalgos/totgba.cc: Implement
the new function.
* NEWS: Mention this new function.
* src/bin/man/spot-x.x: Document SPOT_STREETT_CONV_MIN.
* src/tests/ltl2dstar4.test: Add tests.
* src/tests/Makefile.am: Add it.
* src/bin/autfilt.cc: Do do call remove_fin explicitely
when --tgba is used, let the postprocessor do it.
* src/twa/acc.hh: Add shift operators for acceptance marks.
* src/twaalgos/remfin.cc: Use the new algorithm.
* src/twaalgos/sccinfo.cc, src/twaalgos/sccinfo.hh: Add
a new method to supply the acceptance sets visited by an SCC.
This commit is contained in:
Alexandre Duret-Lutz 2015-07-10 19:02:21 +02:00
parent c0ffe5cdff
commit d8a1dafad1
11 changed files with 419 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

18
NEWS
View file

@ -13,6 +13,24 @@ New in spot 1.99.1a (not yet released)
translation of one PSL formula and its now takes) now takes only
75s.
* streett_to_generalized_buchi() is a new function that implements
what its name suggests, with some SCC-based optimizations over the
naive definition. It is used by the to_generalized_buchi() and
remove_fin() function when the input automaton is a Streett
automaton with more than 3 pairs (this threeshold can be changed
via the SPOT_STREETT_CONV_MIN environment variable -- see the
spot-x(7) man page for details).
This is mainly useful to ltlcross, which has to get rid of "Fin"
acceptance to perform its checks. As an example, the Streett
automaton generatated by ltl2dstar (configured with ltl2tgba) for
the formula
!((GFa -> GFb) & (GFc -> GFd))
has 4307 states and 14 pairs. The new algorithm can translate it
into a TGBA with 9754 states and 7 acceptance sets, while the
default approch used for converting any acceptance to TGBA would
produce 250967 states and 7 acceptance sets.
* Bugs fixed:
- p[+][:*2] was not detected as belonging to siPSL
- scc_filter() would incorrectly remove Fin marks from

1
src/bin/autfilt.cc
View file

@ -460,7 +460,6 @@ parse_opt(int key, char* arg, struct argp_state*)
if (automaton_format == Spin)
error(2, 0, "--spin and --tgba are incompatible");
type = spot::postprocessor::TGBA;
opt_rem_fin = true;
break;
case ARGP_KEY_ARG:
jobs.emplace_back(arg, true);

44
src/bin/man/spot-x.x
View file

@ -39,16 +39,40 @@ user time for solving the SAT problem, system time for solving the SAT
problem.
.TP
\fBSPOT_SATSOLVER\fR If set, this variable should indicate how to call
a SAT\-solver. This is used by the sat\-minimize option described
above. The default value is \f(CW"glucose -verb=0 -model %I >%O"\fR,
it is correct for glucose version 3.0 (for older versions, remove the
\fCW(-model\fR option). The escape sequences \f(CW%I\fR and
\f(CW%O\fR respectively denote the names of the input and output
files. These temporary files are created in the directory specified
by \fBSPOT_TMPDIR\fR or \fBTMPDIR\fR (see below). The SAT-solver
should follow the convention of the SAT Competition for its input and
output format.
\fBSPOT_SATSOLVER\fR
If set, this variable should indicate how to call a SAT\-solver. This
is used by the sat\-minimize option described above. The default
value is \f(CW"glucose -verb=0 -model %I >%O"\fR, it is correct for
glucose version 3.0 (for older versions, remove the \fCW(-model\fR
option). The escape sequences \f(CW%I\fR and \f(CW%O\fR respectively
denote the names of the input and output files. These temporary files
are created in the directory specified by \fBSPOT_TMPDIR\fR or
\fBTMPDIR\fR (see below). The SAT-solver should follow the convention
of the SAT Competition for its input and output format.
.TP
\fBSPOT_STREETT_CONV_MIN\fR
The number of Streett pairs above which conversion from Streett
acceptance to generalized-Büchi acceptance should be made with a
dedicated algorithm. By default this is 3, i.e., if a Streett
automaton with 3 acceptance pairs or more has to be converted into
generalized-Büchi, the dedicated algorithm is used. This algorithm is
close to the classical conversion from Streett to Büchi, but with
several tweaks. When this algorithm is not used, the standard
"Fin-removal" approach is used instead: first the acceptance condition
is converted into disjunctive normal form (DNF), then Fin acceptance
is removed like for Rabin automata, yielding a disjuction of
generalized Büchi acceptance, and the result is finally converted into
conjunctive normal form (CNF) to obtain a generalized Büchi
acceptance. Both algorithms have a worst-case size that is
exponential in the number of Streett pairs, but in practice the
dedicated algorithm works better for most Streett automata with 3 or
more pairs (and many 2-pair Streett automata as well, but the
difference here is less clear). Setting this variable to 0 will
disable the dedicated algorithm. Setting it to 1 will enable it for
all Streett automata, however we do not recommand setting it to less
than 2, because the "Fin-removal" approach is better for single-pair
Streett automata.
.TP
\fBSPOT_TMPDIR\fR, \fBTMPDIR\fR

1
src/tests/Makefile.am
View file

@ -219,6 +219,7 @@ TESTS_twa = \
ltl2dstar.test \
ltl2dstar2.test \
ltl2dstar3.test \
ltl2dstar4.test \
ltl2ta.test \
ltl2ta2.test \
randaut.test \

69
src/tests/ltl2dstar4.test Executable file
View file

@ -0,0 +1,69 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# 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/>.
# Do some quick translations to make sure the neverclaims produced by
# spot actually look correct! We do that by parsing them via ltlcross.
# ltl2neverclaim-lbtt.test does the same with LBTT if it is installed.
. ./defs
set -e
# Skip this test if ltl2dstar is not installed.
(ltl2dstar --version) || exit 77
ltlfilt=../../bin/ltlfilt
ltl2tgba=../../bin/ltl2tgba
ltlcross=../../bin/ltlcross
randltl=../../bin/randltl
autfilt=../../bin/autfilt
ltldo=../../bin/ltldo
STR='--automata=streett --output-format=hoa'
$ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-s $STR - - |
$autfilt --tgba --stats '%S %E %A %s %e %t %a %d' |
tee out
test "`cat out`" = '9 144 4 25 416 416 2 0'
$ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-s $STR - - |
SPOT_STREETT_CONV_MIN=1 $autfilt --tgba --stats '%S %E %A %s %e %t %a %d' |
tee out
test "`cat out`" = '9 144 4 25 482 482 2 0'
LTL2DSTAR="ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L"
# Generate 50 formulas for which the streett automaton has at least 3
# acceptance sets.
$randltl --ltl-priorities=W=0,M=0 -n 1000 3 |
$ltldo "$LTL2DSTAR ->%O" -F- --name=%f -H | tee streett |
$autfilt --acc-set=3.. --stats=%M | head -n 50 > formulas
# Add 50 formulas that use less acceptance sets
$autfilt streett --acc-set=0..2 --stats=%M | head -n 50 >> formulas
$ltlcross -F formulas --timeout=30 \
"$ltl2tgba -H %f >%O" \
"$LTL2DSTAR %O" \
"$LTL2DSTAR - | SPOT_STREETT_CONV_MIN=0 $autfilt --tgba -H >%O" \
"$LTL2DSTAR - | SPOT_STREETT_CONV_MIN=1 $autfilt --tgba -H >%O" \
--csv=out.csv

22
src/twa/acc.hh
View file

@ -167,6 +167,28 @@ namespace spot
return id ^ r.id;
}
mark_t operator<<(int i) const
{
return id << i;
}
mark_t& operator<<=(int i)
{
id <<= i;
return *this;
}
mark_t operator>>(int i) const
{
return id >> i;
}
mark_t& operator>>=(int i)
{
id >>= i;
return *this;
}
mark_t strip(mark_t y) const
{
// strip every bit of id that is marked in y

5
src/twaalgos/remfin.cc
View file

@ -21,6 +21,7 @@
#include "sccinfo.hh"
#include <iostream>
#include "cleanacc.hh"
#include "totgba.hh"
//#define TRACE
#ifdef TRACE
@ -110,6 +111,10 @@ namespace spot
twa_graph_ptr remove_fin(const const_twa_graph_ptr& aut)
{
auto maybe = streett_to_generalized_buchi_maybe(aut);
if (maybe)
return maybe;
if (!aut->acc().uses_fin_acceptance())
return std::const_pointer_cast<twa_graph>(aut);

10
src/twaalgos/sccinfo.cc
View file

@ -251,6 +251,16 @@ namespace spot
return res;
}
acc_cond::mark_t scc_info::acc_sets_of(unsigned scc) const
{
acc_cond::mark_t res = 0U;
for (auto src: states_of(scc))
for (auto& t: aut_->out(src))
if (scc_of(t.dst) == scc)
res |= t.acc;
return res;
}
std::vector<std::set<acc_cond::mark_t>> scc_info::used_acc() const
{
unsigned n = aut_->num_states();

1
src/twaalgos/sccinfo.hh
View file

@ -211,6 +211,7 @@ namespace spot
std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const;
acc_cond::mark_t acc_sets_of(unsigned scc) const;
std::vector<bool> weak_sccs() const;

248
src/twaalgos/totgba.cc
View file

@ -20,12 +20,48 @@
#include "totgba.hh"
#include "remfin.hh"
#include "cleanacc.hh"
#include "sccinfo.hh"
#include "twa/twagraph.hh"
#include <deque>
#include <tuple>
namespace spot
{
namespace
{
struct st2gba_state
{
acc_cond::mark_t pend;
unsigned s;
st2gba_state(unsigned st, acc_cond::mark_t bv = -1U):
pend(bv), s(st)
{
}
};
struct st2gba_state_hash
{
size_t
operator()(const st2gba_state& s) const
{
std::hash<acc_cond::mark_t> h;
return s.s ^ h(s.pend);
}
};
struct st2gba_state_equal
{
bool
operator()(const st2gba_state& left,
const st2gba_state& right) const
{
if (left.s != right.s)
return false;
return left.pend == right.pend;
}
};
typedef std::vector<acc_cond::mark_t> terms_t;
terms_t cnf_terms(const acc_cond::acc_code& code)
@ -55,12 +91,224 @@ namespace spot
}
// Specialized conversion for Streett -> TGBA
// ============================================
//
// Christof Löding's Diploma Thesis: Methods for the
// Transformation of ω-Automata: Complexity and Connection to
// Second Order Logic. Section 3.4.3, gives a transition
// from Streett with |Q| states to BA with |Q|*(4^n-3^n+2)
// states, if n is the number of acceptance pairs.
//
// Duret-Lutz et al. (ATVA'2009): On-the-fly Emptiness Check of
// Transition-based Streett Automata. Section 3.3 contains a
// conversion from transition-based Streett Automata to TGBA using
// the generalized Büchi acceptance to limit the explosion. It goes
// from Streett with |Q| states to (T)GBA with |Q|*(2^n+1) states.
// However the definition of the number of acceptance sets in that
// paper is suboptimal: only n are needed, not 2^n.
//
// This implements this second version.
twa_graph_ptr
streett_to_generalized_buchi(const const_twa_graph_ptr& in)
{
// While "t" is Streett, it is also generalized Büchi, so
// do not do anything.
if (in->acc().is_generalized_buchi())
return std::const_pointer_cast<twa_graph>(in);
int p = in->acc().is_streett();
if (p <= 0)
throw std::runtime_error("streett_to_generalized_buchi() should only be"
" called on automata with Streett acceptance");
// In Streett acceptance, inf sets are odd, while fin sets are
// even.
acc_cond::mark_t inf;
acc_cond::mark_t fin;
std::tie(inf, fin) = in->get_acceptance().used_inf_fin_sets();
assert((inf >> 1) == fin);
scc_info si(in);
// Compute the acceptance sets present in each SCC
unsigned nscc = si.scc_count();
std::vector<std::tuple<acc_cond::mark_t, acc_cond::mark_t, bool>> sccfi;
sccfi.reserve(nscc);
for (unsigned s = 0; s < nscc; ++s)
{
auto acc = si.acc_sets_of(s); // {0,1,2,3,4,6,7,9}
auto acc_fin = acc & fin; // {0, 2, 4,6}
auto acc_inf = acc & inf; // { 1, 3, 7,9}
auto fin_wo_inf = acc_fin - (acc_inf >> 1); // {4}
auto inf_wo_fin = acc_inf - (acc_fin << 1); // {9}
sccfi.emplace_back(fin_wo_inf, inf_wo_fin, acc_fin == 0U);
}
auto out = make_twa_graph(in->get_dict());
out->copy_ap_of(in);
out->prop_copy(in, {false, false, false, true});
out->set_generalized_buchi(p);
acc_cond::mark_t outall = out->acc().all_sets();
// Map st2gba pairs to the state numbers used in out.
typedef std::unordered_map<st2gba_state, unsigned,
st2gba_state_hash,
st2gba_state_equal> bs2num_map;
bs2num_map bs2num;
// Queue of states to be processed.
typedef std::deque<st2gba_state> queue_t;
queue_t todo;
st2gba_state s(in->get_init_state_number());
bs2num[s] = out->new_state();
todo.push_back(s);
bool sbacc = in->has_state_based_acc();
while (!todo.empty())
{
s = todo.front();
todo.pop_front();
unsigned src = bs2num[s];
unsigned scc_src = si.scc_of(s.s);
bool maybe_acc_scc = !si.is_rejecting_scc(scc_src);
acc_cond::mark_t scc_fin_wo_inf;
acc_cond::mark_t scc_inf_wo_fin;
bool no_fin;
std::tie(scc_fin_wo_inf, scc_inf_wo_fin, no_fin) = sccfi[scc_src];
for (auto& t: in->out(s.s))
{
acc_cond::mark_t pend = s.pend;
acc_cond::mark_t acc = 0U;
bool maybe_acc = maybe_acc_scc && (scc_src == si.scc_of(t.dst));
if (pend != -1U)
{
if (!maybe_acc)
continue;
// No point going to some place we will never leave
if (t.acc & scc_fin_wo_inf)
continue;
// For any Fin set we see, we want to see the
// corresponding Inf set.
pend |= (t.acc & fin) << 1;
pend -= t.acc & inf;
// Label this transition with all non-pending
// inf sets. The strip will shift everything
// to the correct numbers in the targets.
acc = (inf - pend).strip(fin) & outall;
// Adjust the pending sets to what will be necessary
// required on the destination state.
if (sbacc)
{
auto a = in->state_acc_sets(t.dst);
if (a & scc_fin_wo_inf)
continue;
pend |= (a & fin) << 1;
pend -= a & inf;
}
pend |= scc_inf_wo_fin;
}
else if (no_fin && maybe_acc)
{
assert(maybe_acc);
acc = outall;
}
st2gba_state d(t.dst, pend);
// Have we already seen this destination?
unsigned dest;
auto dres = bs2num.emplace(d, 0);
if (!dres.second)
{
dest = dres.first->second;
}
else // No, this is a new state
{
dest = dres.first->second = out->new_state();
todo.push_back(d);
}
out->new_edge(src, dest, t.cond, acc);
// Nondeterministically jump to level ∅. We need to do
// that only once per cycle. As an approximation, we
// only to that for transition where t.src >= t.dst as
// this has to occur at least once per cycle.
if (pend == -1U && (t.src >= t.dst) && maybe_acc && !no_fin)
{
acc_cond::mark_t pend = 0U;
if (sbacc)
{
auto a = in->state_acc_sets(t.dst);
if (a & scc_fin_wo_inf)
continue;
pend = (a & fin) << 1;
pend -= a & inf;
}
st2gba_state d(t.dst, pend | scc_inf_wo_fin);
// Have we already seen this destination?
unsigned dest;
auto dres = bs2num.emplace(d, 0);
if (!dres.second)
{
dest = dres.first->second;
}
else // No, this is a new state
{
dest = dres.first->second = out->new_state();
todo.push_back(d);
}
out->new_edge(src, dest, t.cond);
}
}
}
// for (auto s: bs2num)
// {
// std::cerr << s.second << " ("
// << s.first.s << ", ";
// if (s.first.pend == -1U)
// std::cerr << "-)\n";
// else
// std::cerr << s.first.pend << ")\n";
// }
return out;
}
twa_graph_ptr
streett_to_generalized_buchi_maybe(const const_twa_graph_ptr& in)
{
static int min = [&]() {
const char* c = getenv("SPOT_STREETT_CONV_MIN");
if (!c)
return 3;
errno = 0;
int val = strtol(c, nullptr, 10);
if (val < 0 || errno != 0)
throw std::runtime_error("unexpected value for SPOT_STREETT_CONV_MIN");
return val;
}();
if (min == 0 || min > in->acc().is_streett())
return nullptr;
else
return streett_to_generalized_buchi(in);
}
/// \brief Take an automaton with any acceptance condition and return
/// an equivalent Generalized Büchi automaton.
twa_graph_ptr
to_generalized_buchi(const const_twa_graph_ptr& aut)
{
auto maybe = streett_to_generalized_buchi_maybe(aut);
if (maybe)
return maybe;
auto res = remove_fin(cleanup_acceptance(aut));
if (res->acc().is_generalized_buchi())
return res;

11
src/twaalgos/totgba.hh
View file

@ -27,4 +27,15 @@ namespace spot
/// an equivalent Generalized Büchi automaton.
SPOT_API twa_graph_ptr
to_generalized_buchi(const const_twa_graph_ptr& aut);
/// \brief Convert Streett acceptance into generalized Büchi
/// acceptance.
SPOT_API twa_graph_ptr
streett_to_generalized_buchi(const const_twa_graph_ptr& in);
/// \brief Convert Streett acceptance into generalized Büchi
/// only if SPOT_STREET_CONF_MIN is set to a number of pairs
/// less than the number of pairs used by IN.
SPOT_API twa_graph_ptr
streett_to_generalized_buchi_maybe(const const_twa_graph_ptr& in);
}