From c827f75c37f7991021101c0396487260161e9888 Mon Sep 17 00:00:00 2001 From: Alexandre GBAGUIDI AISSE Date: Fri, 28 Jul 2017 13:28:09 +0200 Subject: [PATCH] hierarchy: Add is_persistence() and make is_recurrence() use it * NEWS: Update. * bin/man/spot-x.x: Add environment variable. * spot/tl/hierarchy.cc: Implement them. * spot/tl/hierarchy.hh: Declare them. --- NEWS | 13 +++- bin/man/spot-x.x | 17 +++++ spot/tl/hierarchy.cc | 159 ++++++++++++++++++++++++++++++++++++------- spot/tl/hierarchy.hh | 47 ++++++++++++- 4 files changed, 208 insertions(+), 28 deletions(-) diff --git a/NEWS b/NEWS index ba229d81c..964d08c64 100644 --- a/NEWS +++ b/NEWS @@ -51,8 +51,17 @@ New in spot 2.4.0.dev (not yet released) recognize more if the original language can not be expressed with a co-Büchi acceptance condition. - - The function spot::is_recurrence() is now public. It checks if a formula - has the reccurence property. + - The new functions spot::is_recurrence() and spot::is_persistence() + check respectively if a formula f belongs to the recurrence or + persistence class. Two algorithms are available, one that + checks if a formula is cobuchi_realizable (then it belongs to the + persistence class) and the other that checks if it is + detbuchi_realizable (then it belongs to the recurrence class). + Force one method or the other by setting the environment variable + SPOT_PR_CHECK to 1 or 2. + Note that thanks to the duality of both classes, both algorithms + will work either on f or its negation. + (see https://spot.lrde.epita.fr/hierarchy.html for details). Deprecation notices: diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x index ef31b991c..c86b44376 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_PR_CHECK\fR +Select the default algorithm that must be used to check the persistence +or recurrence property of a formula f. The values it can take are 1 +or 2. Both methods work either on f or !f thanks to the duality of +persistence and recurrence classes. +See "https://spot.lrde.epita.fr/hierarchy.html" for more details. If +it is set to: +.RS +.IP 1 +It will try to check if f (or !f) is co-Büchi realizable in order to +tell if f belongs to the persistence (or the recurrence) class. +.IP 2 +It checks if f (or !f) is det-Büchi realizable to tell if f belongs +to the recurrence (or the persistence) class. +.RE + .TP \fBSPOT_SATLOG\fR If set to a filename, the SAT-based minimization routines will append diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc index a73ce59ff..72e40ba34 100644 --- a/spot/tl/hierarchy.cc +++ b/spot/tl/hierarchy.cc @@ -26,34 +26,149 @@ #include #include #include +#include namespace spot { - bool - is_recurrence(formula f, const twa_graph_ptr& aut) + namespace { - if (f.is_syntactic_recurrence() || is_universal(aut)) - return true; - // If aut is a non-deterministic TGBA, we do - // TGBA->DPA->DRA->(D?)BA. The conversion from DRA to - // BA will preserve determinism if possible. - spot::postprocessor p; - p.set_type(spot::postprocessor::Generic); - p.set_pref(spot::postprocessor::Deterministic - | spot::postprocessor::SBAcc); - p.set_level(spot::postprocessor::Low); - auto dra = p.run(aut); - if (dra->acc().is_generalized_buchi()) - { + static bool + cobuchi_realizable(spot::formula f, + const const_twa_graph_ptr& aut) + { + twa_graph_ptr cobuchi = nullptr; + std::vector pairs; + if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity()) + cobuchi = nsa_to_dca(aut, false); + else if (aut->get_acceptance().is_dnf()) + cobuchi = dnf_to_dca(aut, false); + else + throw std::runtime_error("cobuchi_realizable() only works with " + "Streett-like, Parity or any " + "acceptance condition in DNF"); + + return !cobuchi->intersects(ltl_to_tgba_fm(formula::Not(f), + cobuchi->get_dict(), + true)); + } + + static bool + detbuchi_realizable(const twa_graph_ptr& aut) + { + if (is_universal(aut)) return true; + + // if aut is a non-deterministic TGBA, we do + // TGBA->DPA->DRA->(D?)BA. The conversion from DRA to + // BA will preserve determinism if possible. + spot::postprocessor p; + p.set_type(spot::postprocessor::Generic); + p.set_pref(spot::postprocessor::Deterministic); + p.set_level(spot::postprocessor::Low); + auto dra = p.run(aut); + if (dra->acc().is_generalized_buchi()) + { + assert(is_deterministic(dra)); + return true; + } + else + { + auto ba = rabin_to_buchi_maybe(to_generalized_rabin(dra)); + assert(ba); + return is_deterministic(ba); + } + } + } + + static prcheck + algo_to_perform(bool is_persistence, bool aut_given, prcheck algo) + { + if (algo == prcheck::PR_Auto) + { + // Check environment variable. + static int val_s = []() + { + try + { + auto s = getenv("SPOT_PR_CHECK"); + return s ? std::stoi(s) : 0; + } + catch (const std::exception& e) + { + throw std::runtime_error("invalid value for SPOT_PR_CHECK " + "(should be 1 or 2)"); + } + }(); + + if (val_s == 1) + { + return prcheck::PR_via_CoBuchi; + } + else if (val_s == 2) + { + return prcheck::PR_via_Rabin; + } + else if (!val_s) + { + if (aut_given && !is_persistence) + return prcheck::PR_via_Rabin; + else if ((aut_given && is_persistence) || !aut_given) + return prcheck::PR_via_CoBuchi; + else + SPOT_UNREACHABLE(); + } + else + SPOT_UNREACHABLE(); } else - { - auto ba = rabin_to_buchi_maybe(to_generalized_rabin(dra)); - assert(ba); - return is_deterministic(ba); - } + return algo; + } + + bool + is_persistence(formula f, twa_graph_ptr aut, prcheck algo) + { + if (f.is_syntactic_persistence()) + 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)); + + case prcheck::PR_via_Rabin: + return detbuchi_realizable( + ltl_to_tgba_fm(formula::Not(f), make_bdd_dict(), true)); + + case prcheck::PR_Auto: + SPOT_UNREACHABLE(); + } + + SPOT_UNREACHABLE(); + } + + bool + is_recurrence(formula f, twa_graph_ptr aut, prcheck algo) + { + if (f.is_syntactic_recurrence()) + 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)); + + case prcheck::PR_via_Rabin: + return detbuchi_realizable( + aut ? aut : ltl_to_tgba_fm(f, make_bdd_dict(), true)); + + case prcheck::PR_Auto: + SPOT_UNREACHABLE(); + } + + SPOT_UNREACHABLE(); } char mp_class(formula f) @@ -78,9 +193,7 @@ namespace spot // Not an obligation. Could by 'P', 'R', or 'T'. if (is_recurrence(f, aut)) return 'R'; - f = formula::Not(f); - aut = ltl_to_tgba_fm(f, dict, true); - if (is_recurrence(f, aut)) + if (is_persistence(f, aut)) return 'P'; return 'T'; } diff --git a/spot/tl/hierarchy.hh b/spot/tl/hierarchy.hh index ea9b4b672..c0dd15a75 100644 --- a/spot/tl/hierarchy.hh +++ b/spot/tl/hierarchy.hh @@ -24,9 +24,50 @@ namespace spot { - /// \brief Return true if the formula has the recurrence property. - SPOT_API - bool is_recurrence(formula f, const twa_graph_ptr& aut); + /// Enum used to change the behaviour of is_persistence() or is_recurrence(). + /// + /// If PR_Auto, both methodes 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. + /// + /// If PR_via_Rabin, they will check if the formula is detbuchi_realizable + /// going through a rabin automaton: TGBA->DPA->DRA->(D?)BA. + /// + /// If PR_via_CoBuchi, they will check if the formula is cobuchi_realizable. + /// + /// Note that is_persistence() and is_recurrence() will work on a formula f + /// or its negation because of the duality of both classes + /// (see https://spot.lrde.epita.fr/hierarchy.html for details). + /// For instance if is_recurrence() wants to use PR_via_CoBuchi it will check + /// if !f is cobuchi_realizable. + enum class prcheck + { + PR_Auto, + PR_via_CoBuchi, + PR_via_Rabin + }; + + /// \brief Return true if \a f has the persistence property. + /// + /// \param f the formula to check. + /// \param aut the corresponding automaton (not required). + /// \param algo the algorithm to use (see enum class prcheck). + SPOT_API bool + is_persistence(formula f, + twa_graph_ptr aut = nullptr, + prcheck algo = prcheck::PR_Auto); + + /// \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 (see enum class prcheck). + SPOT_API bool + is_recurrence(formula f, + twa_graph_ptr aut = nullptr, + prcheck algo = prcheck::PR_Auto); /// \brief Return the class of \a f in the temporal hierarchy of Manna /// and Pnueli (PODC'90).