Commit 7a65bdf6 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

specialized translation for GF(guarantee) and FG(safety)

This is adapted from a proposition in a paper by J. Esparza,
J. Křentínský, and S. Sickert, submitted to LICS'18.  We should add
proper references to the code and documentation once that paper is
accepted.

* spot/twaalgos/gfguarantee.cc, spot/twaalgos/gfguarantee.hh:
New files.
* spot/twaalgos/Makefile.am, python/spot/impl.i: Add them.
* spot/twa/fwd.hh: Add a forward declaration of bdd_dict_ptr.
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Make it
possible to call finalize() from the translator subclass.  Constify
all the do_* functions while we are there.
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Add
a "gf-guarantee" option to decide whether to use the new translation.
* bin/spot-x.cc: Document it.
* tests/core/dca2.test, tests/core/genltl.test,
tests/core/ltl2tgba2.test, tests/core/parity2.test,
tests/core/satmin.test, tests/python/automata.ipynb,
tests/python/sbacc.py: Adjust test cases.
* tests/python/except.py: Add a couple more tests.
parent 89f70479
Pipeline #1186 passed with stages
in 136 minutes and 33 seconds
......@@ -27,6 +27,19 @@ New in spot 2.5.2.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 in a submitted
paper.
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.
Bugs fixed:
- "autfilt --cobuchi --small/--det" would turn a transition-based
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et
// Copyright (C) 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -107,6 +107,14 @@ the determinization algorithm.") },
the determinization algorithm.") },
{ DOC("det-stutter", "Set to 0 to disable optimizations based on \
the stutter-invariance in the determinization algorithm.") },
// FIXME: Add bibliographic reference to their paper ASAP.
{ DOC("gf-guarantee", "Set to 0 to disable alternate constructions \
for GF(guarantee)->[D]BA and FG(safety)->DCA. Those constructions \
are based on work by J. Esparza, J. Křentínský, and S. Sickert. \
This is enabled by default for medium and high optimization \
levels. Unless we are building deterministic automata, the \
resulting automata are compared to the automata built using the \
more traditional pipeline, and only kept if they are better.") },
{ DOC("simul", "Set to 0 to disable simulation-based reductions. \
Set to 1 to use only direct simulation. Set to 2 to use only reverse \
simulation. Set to 3 to iterate both direct and reverse simulations. \
......
......@@ -131,6 +131,7 @@
#include <spot/twaalgos/lbtt.hh>
#include <spot/twaalgos/ltl2taa.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/gfguarantee.hh>
#include <spot/twaalgos/compsusp.hh>
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/magic.hh>
......@@ -571,6 +572,7 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/lbtt.hh>
%include <spot/twaalgos/ltl2taa.hh>
%include <spot/twaalgos/ltl2tgba_fm.hh>
%include <spot/twaalgos/gfguarantee.hh>
%include <spot/twaalgos/compsusp.hh>
%include <spot/twaalgos/determinize.hh>
%include <spot/twaalgos/dualize.hh>
......
// -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
// Copyright (C) 2014, 2015, 2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -23,6 +23,9 @@
namespace spot
{
class bdd_dict;
typedef std::shared_ptr<bdd_dict> bdd_dict_ptr;
class twa;
typedef std::shared_ptr<twa> twa_ptr;
typedef std::shared_ptr<const twa> const_twa_ptr;
......
......@@ -49,6 +49,7 @@ twaalgos_HEADERS = \
dualize.hh \
emptiness.hh \
emptiness_stats.hh \
gfguarantee.hh \
gv04.hh \
hoa.hh \
iscolored.hh \
......@@ -114,6 +115,7 @@ libtwaalgos_la_SOURCES = \
dtwasat.cc \
dualize.cc \
emptiness.cc \
gfguarantee.cc \
gv04.cc \
hoa.cc \
iscolored.cc \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2018 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/>.
#include "config.h"
#include "gfguarantee.hh"
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isweakscc.hh>
#include <spot/twaalgos/strength.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/minimize.hh>
#include <spot/twaalgos/dualize.hh>
namespace spot
{
namespace
{
// F(φ₁)&F(φ₂)&F(φ₃) ≡ F(φ₁ & F(φ₂ & F(φ₃))
// because we assume this is all under G.
static formula
nest_f(formula input)
{
assert(input.is(op::And));
formula res = formula::tt();
unsigned n = input.size();
do
{
--n;
assert(input[n].is(op::F));
res = formula::F(formula::And({input[n][0], res}));
}
while (n);
return res;
}
static twa_graph_ptr
do_g_f_terminal_inplace(scc_info& si, bool state_based)
{
twa_graph_ptr aut = std::const_pointer_cast<twa_graph>(si.get_aut());
if (!is_terminal_automaton(aut, &si, true))
throw std::runtime_error("g_f_terminal() expects a terminal automaton");
unsigned ns = si.scc_count();
std::vector<bool> term(ns, false);
for (unsigned n = 0; n < ns; ++n)
if (is_terminal_scc(si, n))
term[n] = true;
aut->prop_keep({ false, false, true, false, true, true });
aut->prop_state_acc(state_based);
aut->prop_inherently_weak(false);
aut->set_buchi();
unsigned init = aut->get_init_state_number();
if (!state_based)
{
for (auto& e: aut->edges())
if (term[si.scc_of(e.dst)])
{
e.dst = init;
e.acc = {0};
}
else
{
e.acc = {};
}
}
else
{
// Replace all terminal state by a single accepting state.
unsigned accstate = aut->new_state();
for (auto& e: aut->edges())
{
if (term[si.scc_of(e.dst)])
e.dst = accstate;
e.acc = {};
}
// This accepting state has the same output as the initial
// state.
for (auto& e: aut->out(init))
aut->new_edge(accstate, e.dst, e.cond, {0});
// This is not mandatory, but starting on the accepting
// state helps getting shorter accepting words.
aut->set_init_state(accstate);
}
aut->purge_unreachable_states();
return aut;
}
}
twa_graph_ptr
g_f_terminal_inplace(twa_graph_ptr aut, bool state_based)
{
scc_info si(aut);
return do_g_f_terminal_inplace(si, state_based);
}
twa_graph_ptr
gf_guarantee_to_ba_maybe(formula gf, const bdd_dict_ptr& dict,
bool deterministic, bool state_based)
{
if (!gf.is(op::G))
return nullptr;
formula f = gf[0];
if (!f.is(op::F))
{
// F(...)&F(...)&... is also OK.
if (!f.is(op::And))
return nullptr;
for (auto c: f)
if (!c.is(op::F))
return nullptr;
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);
scc_info si(reduced);
if (!is_terminal_automaton(aut, &si, true))
return nullptr;
do_g_f_terminal_inplace(si, state_based);
return reduced;
}
twa_graph_ptr
gf_guarantee_to_ba(formula gf, const bdd_dict_ptr& dict,
bool deterministic, bool state_based)
{
twa_graph_ptr res = gf_guarantee_to_ba_maybe(gf, dict,
deterministic, state_based);
if (!res)
throw std::runtime_error
("gf_guarantee_to_ba(): expects a formula of the form GF(guarantee)");
return res;
}
twa_graph_ptr
fg_safety_to_dca_maybe(formula fg, const bdd_dict_ptr& dict,
bool state_based)
{
if (!fg.is(op::F))
return nullptr;
formula g = fg[0];
if (!g.is(op::G))
{
// G(...)|G(...)|... is also OK.
if (!g.is(op::Or))
return nullptr;
for (auto c: g)
if (!c.is(op::G))
return nullptr;
}
formula gf = negative_normal_form(fg, true);
twa_graph_ptr res =
gf_guarantee_to_ba_maybe(gf, dict, true, state_based);
if (!res)
return nullptr;
return dualize(res);
}
twa_graph_ptr
fg_safety_to_dca(formula gf, const bdd_dict_ptr& dict,
bool state_based)
{
twa_graph_ptr res = fg_safety_to_dca_maybe(gf, dict, state_based);
if (!res)
throw std::runtime_error
("fg_safety_to_dca(): expects a formula of the form FG(safety)");
return res;
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2018 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/>.
#pragma once
#include <spot/misc/common.hh>
#include <spot/twa/fwd.hh>
#include <spot/tl/formula.hh>
#include <spot/tl/nenoform.hh>
namespace spot
{
/// \ingroup twa_misc
/// \brief Given a terminal automaton \a f_terminal recognizing
/// some formula F(φ), modify it to recognize GF(φ).
///
/// If \a state_based is set, the automaton all terminal states are
/// replaced by a unique accepting state that has the same outgoing
/// transitions as the initial state, and the initial state is
/// actually relocated to that accepting state. The latter point is
/// not necessary, but it favors shorter accepting cycles.
///
/// If \a state_based is not set, all transition going to terminal
/// states are made accepting and redirected to the initial state.
///
/// This construction is inspired by a similar construction in a
/// submitted paper by J. Esparza, J. Křetínský, & S. Sickert.
SPOT_API twa_graph_ptr
g_f_terminal_inplace(twa_graph_ptr f_terminal, bool state_based = false);
/// \ingroup twa_ltl
/// \brief Convert GF(φ) into a (D)BA if φ is a guarantee property.
///
/// 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().
///
/// Return nullptr if the input formula is not of the supported
/// form.
///
/// This construction generalized a similar construction in a
/// submitted paper by J. Esparza, J. Křetínský, & S. Sickert in the
/// sense that it will work if Φ represent a safety property, even
/// if it is not a syntactic safety.
SPOT_API twa_graph_ptr
gf_guarantee_to_ba_maybe(formula gf, const bdd_dict_ptr& dict,
bool deterministic = true, bool state_based = false);
/// \ingroup twa_ltl
/// \brief Convert GF(φ) into a (D)BA if φ is a guarantee property.
///
/// This is similar to gf_guarantee_to_ba_maybe() except it raises
/// an exception of the input formula is not of the supported form.
SPOT_API twa_graph_ptr
gf_guarantee_to_ba(formula gf, const bdd_dict_ptr& dict,
bool deterministic = true, bool state_based = false);
/// \ingroup twa_ltl
/// \brief Convert FG(φ) into a DCA if φ is a safety property.
///
/// This is the dual of gf_guarantee_to_ba_maybe(). See that
/// function for details.
///
/// Return nullptr if the input formula is not of the supported
/// form.
SPOT_API twa_graph_ptr
fg_safety_to_dca_maybe(formula fg, const bdd_dict_ptr& dict,
bool state_based);
/// \ingroup twa_ltl
/// \brief Convert FG(φ) into a DCA if φ is a safety property.
///
/// This is similar to fg_safety_to_dba_maybe() except it raises
/// an exception of the input formula is not of the supported form.
SPOT_API twa_graph_ptr
fg_safety_to_dca(formula fg, const bdd_dict_ptr& dict,
bool state_based = false);
}
......@@ -105,7 +105,7 @@ namespace spot
}
twa_graph_ptr
postprocessor::do_simul(const twa_graph_ptr& a, int opt)
postprocessor::do_simul(const twa_graph_ptr& a, int opt) const
{
if (!has_separate_sets(a))
return a;
......@@ -124,7 +124,7 @@ namespace spot
}
twa_graph_ptr
postprocessor::do_sba_simul(const twa_graph_ptr& a, int opt)
postprocessor::do_sba_simul(const twa_graph_ptr& a, int opt) const
{
if (ba_simul_ <= 0)
return a;
......@@ -143,7 +143,7 @@ namespace spot
}
twa_graph_ptr
postprocessor::do_degen(const twa_graph_ptr& a)
postprocessor::do_degen(const twa_graph_ptr& a) const
{
auto d = degeneralize(a,
degen_reset_, degen_order_,
......@@ -153,7 +153,7 @@ namespace spot
}
twa_graph_ptr
postprocessor::do_degen_tba(const twa_graph_ptr& a)
postprocessor::do_degen_tba(const twa_graph_ptr& a) const
{
return degeneralize_tba(a,
degen_reset_, degen_order_,
......@@ -162,7 +162,7 @@ namespace spot
}
twa_graph_ptr
postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg)
postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg) const
{
if (scc_filter_ == 0)
return a;
......@@ -176,7 +176,7 @@ namespace spot
}
twa_graph_ptr
postprocessor::do_scc_filter(const twa_graph_ptr& a)
postprocessor::do_scc_filter(const twa_graph_ptr& a) const
{
return do_scc_filter(a, scc_filter_ > 1);
}
......@@ -186,6 +186,36 @@ namespace spot
#define SBACC_ (pref_ & SBAcc)
#define COLORED_ (pref_ & Colored)
twa_graph_ptr
postprocessor::finalize(twa_graph_ptr tmp) const
{
if (COMP_)
tmp = complete(tmp);
bool want_parity = type_ & Parity;
if (want_parity && tmp->acc().is_generalized_buchi())
tmp = SBACC_ ? do_degen(tmp) : do_degen_tba(tmp);
if (SBACC_)
tmp = sbacc(tmp);
if (want_parity)
{
if (COLORED_)
colorize_parity_here(tmp);
parity_kind kind = parity_kind_any;
parity_style style = parity_style_any;
if ((type_ & ParityMin) == ParityMin)
kind = parity_kind_min;
else if ((type_ & ParityMax) == ParityMax)
kind = parity_kind_max;
if ((type_ & ParityOdd) == ParityOdd)
style = parity_style_odd;
else if ((type_ & ParityEven) == ParityEven)
style = parity_style_even;
change_parity_here(tmp, kind, style);
}
return tmp;
}
twa_graph_ptr
postprocessor::run(twa_graph_ptr a, formula f)
{
......@@ -199,38 +229,11 @@ namespace spot
state_based_ = true;
bool via_gba = (type_ == BA) || (type_ == TGBA) || (type_ == Monitor);
bool want_parity = (type_ & Parity) == Parity;
bool want_parity = type_ & Parity;
if (COLORED_ && !want_parity)
throw std::runtime_error("postprocessor: the Colored setting only works "
"for parity acceptance");
auto finalize = [&](twa_graph_ptr tmp)
{
if (COMP_)
tmp = complete(tmp);
if (want_parity && tmp->acc().is_generalized_buchi())
tmp = SBACC_ ? do_degen(tmp) : do_degen_tba(tmp);
if (SBACC_)
tmp = sbacc(tmp);
if (want_parity)
{
if (COLORED_)
colorize_parity_here(tmp);
parity_kind kind = parity_kind_any;
parity_style style = parity_style_any;
if ((type_ & ParityMin) == ParityMin)
kind = parity_kind_min;
else if ((type_ & ParityMax) == ParityMax)
kind = parity_kind_max;
if ((type_ & ParityOdd) == ParityOdd)
style = parity_style_odd;
else if ((type_ & ParityEven) == ParityEven)
style = parity_style_even;
change_parity_here(tmp, kind, style);
}
return tmp;
};
if (!a->is_existential() &&
// We will probably have to revisit this condition later.
// Currently, the intent is that postprocessor should never
......
......@@ -219,12 +219,13 @@ namespace spot
twa_graph_ptr run(twa_graph_ptr input, formula f = nullptr);
protected:
twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt);
twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt);
twa_graph_ptr do_degen(const twa_graph_ptr& input);
twa_graph_ptr do_degen_tba(const twa_graph_ptr& input);
twa_graph_ptr do_scc_filter(const twa_graph_ptr& a, bool arg);
twa_graph_ptr do_scc_filter(const twa_graph_ptr& a);
twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt) const;
twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt) const;
twa_graph_ptr do_degen(const twa_graph_ptr& input) const;
twa_graph_ptr do_degen_tba(const twa_graph_ptr& input) const;
twa_graph_ptr do_scc_filter(const twa_graph_ptr& a, bool arg) const;
twa_graph_ptr do_scc_filter(const twa_graph_ptr& a) const;
twa_graph_ptr finalize(twa_graph_ptr tmp) const;
output_type type_ = TGBA;
int pref_ = Small;
......
......@@ -24,6 +24,8 @@
#include <spot/misc/optionmap.hh>
#include <spot/tl/relabel.hh>
#include <spot/twaalgos/relabel.hh>
#include <spot/twaalgos/gfguarantee.hh>
#include <spot/twaalgos/isdet.hh>
namespace spot
{
......@@ -32,6 +34,7 @@ namespace spot
{
comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0;
relabel_bool_ = tls_impl_ = -1;
gf_guarantee_ = level_ != Low;
if (!opt)
return;
......@@ -45,6 +48,7 @@ namespace spot
skel_simul_ = opt->get("skel-simul", 1);
}
tls_impl_ = opt->get("tls-impl", -1);
gf_guarantee_ = opt->get("gf-guarantee", gf_guarantee_);
}
void translator::build_simplifier(const bdd_dict_ptr& dict)
......@@ -96,6 +100,8 @@ namespace spot
twa_graph_ptr translator::run(formula* f)
{
#define PREF_ (pref_ & (Small | Deterministic))
bool unambiguous = (pref_ & postprocessor::Unambiguous);
if (unambiguous && type_ == postprocessor::Monitor)
{
......@@ -153,12 +159,13 @@ namespace spot
simpl_->clear_as_bdd_cache();
twa_graph_ptr aut;
twa_graph_ptr aut2 = nullptr;
if (comp_susp_ > 0)
{
// FIXME: Handle unambiguous_ automata?
int skel_wdba = skel_wdba_;
if (skel_wdba < 0)
skel_wdba = (pref_ == postprocessor::Deterministic) ? 1 : 2;
skel_wdba = (pref_ & postprocessor::Deterministic) ? 1 : 2;
aut = compsusp(r, simpl_->get_dict(), skel_wdba == 0,
skel_simul_ == 0, early_susp_ != 0,
......@@ -166,6 +173,24 @@ namespace spot
}
else
{
if (gf_guarantee_ && PREF_ != Any)
{
bool det = unambiguous || (PREF_ == Deterministic);
bool sba = type_ == BA || (pref_ & SBAcc);
if ((type_ & (BA | Parity | Generic)) || type_ == TGBA)
aut2 = gf_guarantee_to_ba_maybe(r, simpl_->get_dict(), det, sba);
if (aut2 && (type_ & (BA | Parity)) && (pref_ & Deterministic))
return finalize(aut2);
if (!aut2 && (type_ & (Generic | Parity | CoBuchi)))
{
aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(), sba);
if (aut2
&& (type_ & (CoBuchi | Parity))
&& (pref_ & Deterministic))
return finalize(aut2);
}
}
bool exprop = unambiguous || level_ == postprocessor::High;
aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop,
true, false, false, nullptr, nullptr,
......@@ -173,6 +198,18 @@ namespace spot
}
aut = this->postprocessor::run(aut, r);
if (aut2)
{
aut2 = this->postprocessor::run(aut2, r);
unsigned s2 = aut2->num_states();
unsigned s1 = aut->num_states();
bool d2_more_det = !is_deterministic(aut) && is_deterministic(aut2);
if (((PREF_ == Deterministic) && d2_more_det)
|| (s2 < s1)
|| (s2 == s1