From d94efe9fe1cf0a72500562acc39073aa0f604bd6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 15 Oct 2018 21:35:09 +0200 Subject: [PATCH] implement is_liveness() and is_liveness_automaton() * spot/twaalgos/strength.cc, spot/twaalgos/strength.hh, spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Here. * bin/ltlfilt.cc (--liveness): New filter. * NEWS: Mention those. * tests/core/ltlfilt.test, tests/python/ltlsimple.py: Add test cases. --- NEWS | 11 ++++++----- bin/ltlfilt.cc | 6 ++++-- spot/tl/hierarchy.cc | 5 +++++ spot/tl/hierarchy.hh | 14 ++++++++++++-- spot/twaalgos/strength.cc | 12 ++++++++++++ spot/twaalgos/strength.hh | 13 +++++++++++-- tests/core/ltlfilt.test | 10 ++++++++++ tests/python/ltlsimple.py | 3 +++ 8 files changed, 63 insertions(+), 11 deletions(-) diff --git a/NEWS b/NEWS index f9f2098c8..01538e3e5 100644 --- a/NEWS +++ b/NEWS @@ -15,11 +15,8 @@ New in spot 2.6.2.dev (not yet released) Zielonka algorithm. Calude's quasi-polynomial time algorithm has been dropped as it was not used. - Build: - - - We no longer distribute the Python-based CGI script + javascript - code for the online translator. Its replacement has its own - repository: https://gitlab.lrde.epita.fr/spot/spot-web-app/ + - ltlfilt learned --liveness to match formulas representing liveness + properties. Library: @@ -64,6 +61,10 @@ New in spot 2.6.2.dev (not yet released) with arbitrary acceptance condition into a parity automaton, based on a last-appearance record (LAR) construction. + - The new function is_liveness() and is_liveness_automaton() can be + used to check whether a formula or an automaton represents a + liveness property. + Bugs fixed: - Running "ltl2tgba -B" on formulas of the type FG(safety) would diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 626f59da4..a5a872012 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -700,11 +700,12 @@ namespace if (matched && (obligation || recurrence || persistence || !opt->acc_words.empty() - || !opt->rej_words.empty())) + || !opt->rej_words.empty() + || liveness)) { spot::twa_graph_ptr aut = nullptr; - if (!opt->acc_words.empty() || !opt->rej_words.empty()) + if (!opt->acc_words.empty() || !opt->rej_words.empty() || liveness) { aut = ltl_to_tgba_fm(f, simpl.get_dict(), true); @@ -724,6 +725,7 @@ namespace break; } + matched &= !liveness || is_liveness_automaton(aut); } // Some combinations of options can be simplified. diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc index ec89ca14d..870a46ae6 100644 --- a/spot/tl/hierarchy.cc +++ b/spot/tl/hierarchy.cc @@ -469,4 +469,9 @@ namespace spot const op* vd = v.data(); return nesting_depth(f, vd, vd + v.size()); } + + bool is_liveness(formula f) + { + return is_liveness_automaton(ltl_to_tgba_fm(f, spot::make_bdd_dict())); + } } diff --git a/spot/tl/hierarchy.hh b/spot/tl/hierarchy.hh index 41d852d89..49b66aa6a 100644 --- a/spot/tl/hierarchy.hh +++ b/spot/tl/hierarchy.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement de -// l'Epita (LRDE) +// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement +// de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -184,4 +184,14 @@ namespace spot /// /// The string should be terminated by '\0' or ']'. SPOT_API unsigned nesting_depth(formula f, const char* opers); + + + /// \brief Check whether a formula represents a liveness property. + /// + /// A formula represents a liveness property if any finite prefix + /// can be extended into a word accepted by the formula. + /// + /// The test is done by conversion to automaton. If you already + /// have an automaton, use spot::is_liveness_automaton() instead. + SPOT_API bool is_liveness(formula f); } diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 6e39b06e5..1ef93a7c2 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -22,6 +22,9 @@ #include #include #include +#include +#include +#include using namespace std::string_literals; @@ -401,4 +404,13 @@ namespace spot std::string num = std::to_string(scc_num); return decompose_scc(sm, (accepting ? ('a' + num) : num).c_str()); } + + bool + is_liveness_automaton(const const_twa_graph_ptr& aut) + { + auto mon = minimize_monitor(scc_filter_states(aut)); + return mon->num_states() == 1 && is_complete(mon); + } + + } diff --git a/spot/twaalgos/strength.hh b/spot/twaalgos/strength.hh index 2e8a9a0f0..ec2cad656 100644 --- a/spot/twaalgos/strength.hh +++ b/spot/twaalgos/strength.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire +// Copyright (C) 2010, 2011, 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. @@ -104,7 +104,7 @@ namespace spot /// SCCs). /// /// A minimized WDBA (as returned by a successful run of - /// minimize_obligation()) represent safety property if it is a + /// minimize_obligation()) represents safety property if it is a /// safety automaton. /// /// \param aut the automaton to check @@ -115,6 +115,15 @@ namespace spot is_safety_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr); + /// \brief Whether the automaton represents a liveness property. + /// + /// An automaton represents a liveness property if after forcing the + /// acceptance condition to true, the resulting automaton accepts + /// all words. In other words, there is no prefix that cannot be + /// extended into an accepting word. + SPOT_API bool + is_liveness_automaton(const const_twa_graph_ptr& aut); + /// \brief Check whether an automaton is weak or terminal. /// /// This sets the "inherently weak", "weak", "very-weak" and diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index 3ab827c3f..d4d2092d5 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -127,6 +127,16 @@ Fb F(a & X(!a & b)) EOF +checkopt --liveness < GFb') +assert not spot.is_liveness('a & GFb')