23 #include <spot/twa/fwd.hh> 60 twa_graph_ptr aut =
nullptr,
73 twa_graph_ptr aut =
nullptr,
107 twa_graph_ptr aut =
nullptr,
108 ocheck algo = ocheck::Auto);
156 SPOT_API std::string
mp_class(
char mpc,
const char* opt);
163 SPOT_API
unsigned nesting_depth(
formula f,
op oper);
166 SPOT_API
unsigned nesting_depth(
formula f,
const op* begin,
const op* end);
186 SPOT_API
unsigned nesting_depth(
formula f,
const char* opers);
Definition: automata.hh:26
prcheck
Enum used to change the behavior of is_persistence() or is_recurrence().
Definition: hierarchy.hh:45
bool is_recurrence(formula f, twa_graph_ptr aut=nullptr, prcheck algo=prcheck::Auto)
Return true if f represents a recurrence property.
bool is_persistence(formula f, twa_graph_ptr aut=nullptr, prcheck algo=prcheck::Auto)
Return true if f represents a persistence property.
op
Operator types.
Definition: formula.hh:64
std::string mp_class(char mpc, const char *opt)
Expand a class in the temporal hierarchy of Manna and Pnueli (PODC'90).
bool is_obligation(formula f, twa_graph_ptr aut=nullptr, ocheck algo=ocheck::Auto)
Return true if f has the recurrence property.