23 #include <spot/twa/fwd.hh>
64 twa_graph_ptr aut =
nullptr,
77 twa_graph_ptr aut =
nullptr,
111 twa_graph_ptr aut =
nullptr,
112 ocheck algo = ocheck::Auto);
160 SPOT_API std::string
mp_class(
char mpc,
const char* opt);
op
Operator types.
Definition: formula.hh:79
bool is_obligation(formula f, twa_graph_ptr aut=nullptr, ocheck algo=ocheck::Auto)
Return true if f has the recurrence property.
bool is_recurrence(formula f, twa_graph_ptr aut=nullptr, prcheck algo=prcheck::Auto)
Return true if f represents a recurrence property.
prcheck
Enum used to change the behavior of is_persistence() or is_recurrence().
Definition: hierarchy.hh:49
bool is_persistence(formula f, twa_graph_ptr aut=nullptr, prcheck algo=prcheck::Auto)
Return true if f represents a persistence property.
char mp_class(formula f)
Return the class of f in the temporal hierarchy of Manna and Pnueli (PODC'90).
Definition: automata.hh:27
ocheck
Enum used to change the behavior of is_obligation().
Definition: hierarchy.hh:82
bool is_liveness(formula f)
Check whether a formula represents a liveness property.
unsigned nesting_depth(formula f, op oper)
Compute the nesting depth of an operator.