diff --git a/NEWS b/NEWS
index 4848b48b6b3ca2e0d74452740eb1621635fcbc99..6563ab45f13f4f707f3d988db5dbd1734cf0dc01 100644
--- a/NEWS
+++ b/NEWS
@@ -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
diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc
index 56476428e26ffffcde9afe86cef517019cacdfe4..7c4464b330b0b70a0e3d835310109f28b91a294a 100644
--- a/src/bin/autfilt.cc
+++ b/src/bin/autfilt.cc
@@ -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);
diff --git a/src/bin/man/spot-x.x b/src/bin/man/spot-x.x
index 7677d9a5b02a6be0b99c2618742816e4e402babb..e570d1228213b11a85c547c8ab8d518fd3431961 100644
--- a/src/bin/man/spot-x.x
+++ b/src/bin/man/spot-x.x
@@ -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
diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am
index 6f97d3f20016624fdb88772459f4ac4764154d11..aaa430374d4f573c8ab2288bd5434371843c40d1 100644
--- a/src/tests/Makefile.am
+++ b/src/tests/Makefile.am
@@ -219,6 +219,7 @@ TESTS_twa = \
ltl2dstar.test \
ltl2dstar2.test \
ltl2dstar3.test \
+ ltl2dstar4.test \
ltl2ta.test \
ltl2ta2.test \
randaut.test \
diff --git a/src/tests/ltl2dstar4.test b/src/tests/ltl2dstar4.test
new file mode 100755
index 0000000000000000000000000000000000000000..7acecfe96c1ee1075e4edbe4da74a87bf44eaa4f
--- /dev/null
+++ b/src/tests/ltl2dstar4.test
@@ -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 .
+
+# 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
diff --git a/src/twa/acc.hh b/src/twa/acc.hh
index 1ae38ff89ce1e1b0ec46e08dbc71c67602e2320b..06e83657486fa9e421021f191f2447e6836f63c2 100644
--- a/src/twa/acc.hh
+++ b/src/twa/acc.hh
@@ -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
diff --git a/src/twaalgos/remfin.cc b/src/twaalgos/remfin.cc
index bfafacaa5145d9893caf17c6281e59eca291a07d..228647dd5b507604aef40c43cfd70e8cd06ead72 100644
--- a/src/twaalgos/remfin.cc
+++ b/src/twaalgos/remfin.cc
@@ -21,6 +21,7 @@
#include "sccinfo.hh"
#include
#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(aut);
diff --git a/src/twaalgos/sccinfo.cc b/src/twaalgos/sccinfo.cc
index 99c23515d492053307578209c6029518ee35b9ee..5126dd3f7f9e4df337c80832591e11a42c89c328 100644
--- a/src/twaalgos/sccinfo.cc
+++ b/src/twaalgos/sccinfo.cc
@@ -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> scc_info::used_acc() const
{
unsigned n = aut_->num_states();
diff --git a/src/twaalgos/sccinfo.hh b/src/twaalgos/sccinfo.hh
index 5c03a03bbb6f5f1084c1ee32e068a9f2d9f1101b..fc1a0b8f636f2bb271a5a7389423a3611ad4ec70 100644
--- a/src/twaalgos/sccinfo.hh
+++ b/src/twaalgos/sccinfo.hh
@@ -211,6 +211,7 @@ namespace spot
std::set used_acc_of(unsigned scc) const;
+ acc_cond::mark_t acc_sets_of(unsigned scc) const;
std::vector weak_sccs() const;
diff --git a/src/twaalgos/totgba.cc b/src/twaalgos/totgba.cc
index d76896d29b1c1d696829cb175311787a5cd604f0..1d19b56f55cb869861efe2e9810d9f419133b61a 100644
--- a/src/twaalgos/totgba.cc
+++ b/src/twaalgos/totgba.cc
@@ -20,12 +20,48 @@
#include "totgba.hh"
#include "remfin.hh"
#include "cleanacc.hh"
+#include "sccinfo.hh"
#include "twa/twagraph.hh"
+#include
+#include
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 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 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(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> 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 bs2num_map;
+ bs2num_map bs2num;
+
+ // Queue of states to be processed.
+ typedef std::deque 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;
diff --git a/src/twaalgos/totgba.hh b/src/twaalgos/totgba.hh
index a40e5fbe130137eef8cf96a6193c0500201481cc..0903133543f47a455314f5ea7e4d076353be5d91 100644
--- a/src/twaalgos/totgba.hh
+++ b/src/twaalgos/totgba.hh
@@ -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);
}