diff --git a/NEWS b/NEWS index 06a665c97..ba229d81c 100644 --- a/NEWS +++ b/NEWS @@ -51,6 +51,9 @@ 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. + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc index 4ed8e4506..a73ce59ff 100644 --- a/spot/tl/hierarchy.cc +++ b/spot/tl/hierarchy.cc @@ -30,31 +30,30 @@ namespace spot { - namespace + bool + is_recurrence(formula f, const twa_graph_ptr& aut) { - static bool is_recurrence(formula f, const twa_graph_ptr& aut) - { - if (f.is_syntactic_recurrence() || is_universal(aut)) + 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()) + { 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()) - { - return true; - } - else - { - auto ba = rabin_to_buchi_maybe(to_generalized_rabin(dra)); - assert(ba); - return is_deterministic(ba); - } - } + } + else + { + auto ba = rabin_to_buchi_maybe(to_generalized_rabin(dra)); + assert(ba); + return is_deterministic(ba); + } } char mp_class(formula f) diff --git a/spot/tl/hierarchy.hh b/spot/tl/hierarchy.hh index 88def1831..ea9b4b672 100644 --- a/spot/tl/hierarchy.hh +++ b/spot/tl/hierarchy.hh @@ -20,9 +20,14 @@ #pragma once #include +#include namespace spot { + /// \brief Return true if the formula has the recurrence property. + SPOT_API + bool is_recurrence(formula f, const twa_graph_ptr& aut); + /// \brief Return the class of \a f in the temporal hierarchy of Manna /// and Pnueli (PODC'90). ///