Commit e59274b6 authored by Alexandre GBAGUIDI AISSE's avatar Alexandre GBAGUIDI AISSE
Browse files

hierarchy: Make is_recurrence() public

* NEWS: Declare it.
* spot/tl/hierarchy.cc: Remove static keyword and anonymous namespace.
* spot/tl/hierarchy.hh: Declare function.
parent 8cf54264
......@@ -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.)
......
......@@ -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)
......
......@@ -20,9 +20,14 @@
#pragma once
#include <spot/tl/formula.hh>
#include <spot/twa/fwd.hh>
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).
///
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment