From 50fe34a55a093d7065b2ce6d722cdada557bd5f2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 15 Nov 2017 21:51:33 +0100 Subject: [PATCH] introduce is_obligation(f) This is not optimal yet because it still construct a minimal WDBA internally, but it's better than the previous way to call minimize_obligation() since it can avoid constructing the minimized automaton in a few more cases. * spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Introduce is_obligation(). * bin/ltlfilt.cc: Wire it to --obligation. * spot/twaalgos/minimize.cc: Implement is_wdba_realizable(), needed by the above. * tests/core/obligation.test: Test it. * bin/man/spot-x.x, NEWS: Document it. --- NEWS | 5 +++ bin/ltlfilt.cc | 6 +-- bin/man/spot-x.x | 17 ++++++++ spot/tl/hierarchy.cc | 83 ++++++++++++++++++++++++++++++++------ spot/tl/hierarchy.hh | 47 +++++++++++++++++---- spot/twaalgos/minimize.cc | 62 +++++++++++++++++++++++++--- tests/core/obligation.test | 23 ++++++++++- 7 files changed, 214 insertions(+), 29 deletions(-) diff --git a/NEWS b/NEWS index 4f537fd58..0320a6884 100644 --- a/NEWS +++ b/NEWS @@ -112,6 +112,11 @@ New in spot 2.4.2.dev (not yet released) will work either on f or its negation. (see https://spot.lrde.epita.fr/hierarchy.html for details). + - A new function spot::is_obligation() can be used to test whether a + formula is an obligation. This is used by ltlfilt --obligation, + and the algorithm used can be controled by the SPOT_O_CHECK + environment variable (see the spot-x(7) man page for details). + - The new function spot::is_colored() checks if an automaton is colored (i.e., every transition belongs to exactly one acceptance set) diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 1c07612d2..4df6d1f96 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -732,7 +732,7 @@ namespace // Because this is costly, we compute it later, so that we don't // have to compute it on formulas that have been discarded for // other reasons. - if (obligation) + if (obligation && (safety || guarantee)) { if (!aut) aut = ltl_to_tgba_fm(f, simpl.get_dict(), true); @@ -752,10 +752,10 @@ namespace matched &= !safety || is_safety_automaton(min, &si); } } - + else if (obligation) // just obligation, not safety or guarantee + matched &= is_obligation(f, aut); else if (persistence) matched &= spot::is_persistence(f); - else if (recurrence) matched &= spot::is_recurrence(f, aut); } diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x index 9f374815b..3f156ec28 100644 --- a/bin/man/spot-x.x +++ b/bin/man/spot-x.x @@ -99,6 +99,23 @@ in third-party tools that output incorrect HOA (e.g., declaring the automaton with property "univ-branch" when no universal branching is actually used) +.TP +\fBSPOT_O_CHECK\fR +Specifies the default algorithm that should be used +by the \f(CWis_obligation()\fR function. The value should +be one of the following: +.RS +.IP 1 +Make sure that the formula and its negation are +realizable by non-deterministic co-Büchi automata. +.IP 2 +Make sure that the formula and its negation are +realizable by deterministic Büchi automata. +.IP 3 +Make sure that the formula is realizable +by a weak and deterministic Büchi automata. +.RE + .TP \fBSPOT_OOM_ABORT\fR If this variable is set, Out-Of-Memory errors will \f(CWabort()\fR the diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc index 23ae83075..2e31148d5 100644 --- a/spot/tl/hierarchy.cc +++ b/spot/tl/hierarchy.cc @@ -35,7 +35,7 @@ namespace spot { static bool cobuchi_realizable(spot::formula f, - const const_twa_graph_ptr& aut) + const const_twa_graph_ptr& aut) { twa_graph_ptr cobuchi = nullptr; std::vector pairs; @@ -135,18 +135,18 @@ namespace spot return true; switch (algo_to_perform(true, aut != nullptr, algo)) - { + { case prcheck::PR_via_CoBuchi: - return cobuchi_realizable(f, - aut ? aut : ltl_to_tgba_fm(f, make_bdd_dict(), true)); + return cobuchi_realizable(f, aut ? aut : + ltl_to_tgba_fm(f, make_bdd_dict(), true)); case prcheck::PR_via_Rabin: - return detbuchi_realizable( - ltl_to_tgba_fm(formula::Not(f), make_bdd_dict(), true)); + return detbuchi_realizable(ltl_to_tgba_fm(formula::Not(f), + make_bdd_dict(), true)); case prcheck::PR_Auto: SPOT_UNREACHABLE(); - } + } SPOT_UNREACHABLE(); } @@ -158,22 +158,81 @@ namespace spot return true; switch (algo_to_perform(false, aut != nullptr, algo)) - { + { case prcheck::PR_via_CoBuchi: return cobuchi_realizable(formula::Not(f), - ltl_to_tgba_fm(formula::Not(f), make_bdd_dict(), true)); + ltl_to_tgba_fm(formula::Not(f), + make_bdd_dict(), true)); case prcheck::PR_via_Rabin: - return detbuchi_realizable( - aut ? aut : ltl_to_tgba_fm(f, make_bdd_dict(), true)); + return detbuchi_realizable(aut ? aut : + ltl_to_tgba_fm(f, make_bdd_dict(), true)); case prcheck::PR_Auto: SPOT_UNREACHABLE(); - } + } SPOT_UNREACHABLE(); } + + [[noreturn]] static void invalid_spot_o_check() + { + throw std::runtime_error("invalid value for SPOT_O_CHECK " + "(should be 1, 2, or 3)"); + } + + // This private function is defined in minimize.cc for technical + // reasons. + SPOT_LOCAL bool is_wdba_realizable(formula f, twa_graph_ptr aut = nullptr); + + bool + is_obligation(formula f, twa_graph_ptr aut, ocheck algo) + { + if (algo == ocheck::Auto) + { + static ocheck env_algo = []() + { + int val; + try + { + auto s = getenv("SPOT_O_CHECK"); + val = s ? std::stoi(s) : 0; + } + catch (const std::exception& e) + { + invalid_spot_o_check(); + } + if (val == 0) + return ocheck::via_WDBA; + else if (val == 1) + return ocheck::via_CoBuchi; + else if (val == 2) + return ocheck::via_Rabin; + else if (val == 3) + return ocheck::via_WDBA; + else + invalid_spot_o_check(); + }(); + algo = env_algo; + } + switch (algo) + { + case ocheck::via_WDBA: + return is_wdba_realizable(f, aut); + case ocheck::via_CoBuchi: + return (is_persistence(f, aut, prcheck::PR_via_CoBuchi) + && is_recurrence(f, aut, prcheck::PR_via_CoBuchi)); + case ocheck::via_Rabin: + return (is_persistence(f, aut, prcheck::PR_via_Rabin) + && is_recurrence(f, aut, prcheck::PR_via_Rabin)); + case ocheck::Auto: + SPOT_UNREACHABLE(); + } + SPOT_UNREACHABLE(); + } + + char mp_class(formula f) { if (f.is_syntactic_safety() && f.is_syntactic_guarantee()) diff --git a/spot/tl/hierarchy.hh b/spot/tl/hierarchy.hh index c0dd15a75..2f8181624 100644 --- a/spot/tl/hierarchy.hh +++ b/spot/tl/hierarchy.hh @@ -24,9 +24,9 @@ namespace spot { - /// Enum used to change the behaviour of is_persistence() or is_recurrence(). + /// Enum used to change the behavior of is_persistence() or is_recurrence(). /// - /// If PR_Auto, both methodes will first check the environment variable + /// If PR_Auto, both methods will first check the environment variable /// SPOT_PR_CHECK to see if one algorithm or the other is wanted /// to be forced. Otherwise, it will make the most appropriate decision. /// @@ -42,12 +42,12 @@ namespace spot /// if !f is cobuchi_realizable. enum class prcheck { - PR_Auto, - PR_via_CoBuchi, - PR_via_Rabin + PR_Auto, // FIXME: Remove the useless PR_ prefix since + PR_via_CoBuchi, // we already have a prcheck:: prefix. + PR_via_Rabin, }; - /// \brief Return true if \a f has the persistence property. + /// \brief Return true if \a f represents a persistence property. /// /// \param f the formula to check. /// \param aut the corresponding automaton (not required). @@ -57,7 +57,7 @@ namespace spot twa_graph_ptr aut = nullptr, prcheck algo = prcheck::PR_Auto); - /// \brief Return true if \a f has the recurrence property. + /// \brief Return true if \a f represents a recurrence property. /// /// Actually, it calls is_persistence() with the negation of \a f. /// @@ -69,6 +69,39 @@ namespace spot twa_graph_ptr aut = nullptr, prcheck algo = prcheck::PR_Auto); + /// Enum used to change the behavior of is_obligation(). + enum class ocheck + { + Auto, + via_CoBuchi, + via_Rabin, + via_WDBA, + }; + + /// \brief Return true if \a f has the recurrence property. + /// + /// Actually, it calls is_persistence() with the negation of \a f. + /// + /// \param f the formula to check. + /// \param aut the corresponding automaton (not required). + /// \param algo the algorithm to use. + /// + /// \a aut is constructed from f if not supplied. + /// + /// If \a algo is ocheck::via_WDBA, aut is converted into a WDBA + /// which is then checked for equivalence with aut. If \a algo is + /// ocheck::via_CoBuchi, we test that both f and !f are co-Büchi + /// realizable. If \a algo is ocheck::via_Rabin, we test that both + /// f and !f are DBA-realizable. + /// + /// Auto currently defaults to via_WDBA, unless the + /// SPOT_O_CHECK environment variable specifies + /// otherwise. + SPOT_API bool + is_obligation(formula f, + twa_graph_ptr aut = nullptr, + ocheck algo = ocheck::Auto); + /// \brief Return the class of \a f in the temporal hierarchy of Manna /// and Pnueli (PODC'90). /// diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index 33186597a..fcab083f7 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -46,6 +46,7 @@ #include #include #include +#include namespace spot { @@ -581,6 +582,54 @@ namespace spot return res; } + // Declared in tl/hierarchy.cc, but defined here because it relies on + // other internal functions from this file. + SPOT_LOCAL bool is_wdba_realizable(formula f, twa_graph_ptr aut = nullptr); + + bool is_wdba_realizable(formula f, twa_graph_ptr aut) + { + if (f.is_syntactic_obligation()) + return true; + + if (aut == nullptr) + aut = ltl_to_tgba_fm(f, make_bdd_dict(), true); + + if (!aut->is_existential()) + throw std::runtime_error + ("is_wdba_realizable() does not support alternation"); + + if ((f.is_syntactic_persistence() || aut->prop_weak()) + && (f.is_syntactic_recurrence() || is_deterministic(aut))) + return true; + + if (is_terminal_automaton(aut)) + return true; + + // FIXME: we do not need to minimize the wdba to test realizability. + auto min_aut = minimize_wdba(aut); + + if (!is_deterministic(aut) + && !product(aut, remove_fin(dualize(min_aut)))->is_empty()) + return false; + + twa_graph_ptr aut_neg; + if (is_deterministic(aut)) + { + aut_neg = remove_fin(dualize(aut)); + } + else + { + aut_neg = ltl_to_tgba_fm(formula::Not(f), aut->get_dict()); + aut_neg = scc_filter(aut_neg, true); + } + + if (is_terminal_automaton(aut_neg)) + return true; + + return product(min_aut, aut_neg)->is_empty(); + } + + twa_graph_ptr minimize_obligation(const const_twa_graph_ptr& aut_f, formula f, @@ -591,6 +640,9 @@ namespace spot throw std::runtime_error ("minimize_obligation() does not support alternation"); + // FIXME: We should build scc_info once, pass it to minimize_wdba + // and reuse it for is_terminal_automaton(), and + // is_weak_automaton(). auto min_aut_f = minimize_wdba(aut_f); if (reject_bigger) @@ -601,16 +653,16 @@ namespace spot return std::const_pointer_cast(aut_f); } - // If the input automaton was already weak and deterministic, the - // output is necessary correct. - if (aut_f->prop_weak() && is_deterministic(aut_f)) - return min_aut_f; - // if f is a syntactic obligation formula, the WDBA minimization // must be correct. if (f && f.is_syntactic_obligation()) return min_aut_f; + // If the input automaton was already weak and deterministic, the + // output is necessary correct. + if (aut_f->prop_weak() && is_deterministic(aut_f)) + return min_aut_f; + // If aut_f is a guarantee automaton, the WDBA minimization must be // correct. if (is_terminal_automaton(aut_f)) diff --git a/tests/core/obligation.test b/tests/core/obligation.test index 410e8b91a..1e3c9f30a 100755 --- a/tests/core/obligation.test +++ b/tests/core/obligation.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2014, 2015 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2010, 2011, 2014, 2015, 2017 Laboratoire de Recherche +# et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -117,4 +117,23 @@ while read exp f; do esac done < formulas.txt +set -x + +cut -c 4- formulas.txt | ltlfilt --obligation > o0 +for i in 1 2 3; do + cut -c 4- formulas.txt | SPOT_O_CHECK=$i ltlfilt --obligation > o$i +done +# make sure SPOT_O_CHECK is actually read +cut -c 4- formulas.txt | SPOT_O_CHECK=x ltlfilt --obligation 2>err && exit 1 +cut -c 4- formulas.txt | SPOT_O_CHECK=9 ltlfilt --obligation 2>err && exit 1 +grep SPOT_O_CHECK err +diff o0 o2 +diff o1 o2 +diff o2 o3 +cut -c 4- formulas.txt | ltlfilt -o %h.ltl +cat O.ltl G.ltl S.ltl B.ltl | sort > ogsb.ltl +sort o3 > o4 +diff o4 ogsb.ltl + + exit 0