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

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.
parent e59274b6
......@@ -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:
......
......@@ -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
......
......@@ -26,34 +26,149 @@
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/strength.hh>
#include <spot/twaalgos/totgba.hh>
#include <spot/twaalgos/cobuchi.hh>
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<acc_cond::rs_pair> 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;
}
else
// 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)
{
auto ba = rabin_to_buchi_maybe(to_generalized_rabin(dra));
assert(ba);
return is_deterministic(ba);
// 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
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';
}
......
......@@ -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
/// <code>SPOT_PR_CHECK</code> 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).
......
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