22#include <spot/twa/fwd.hh>
63 twa_graph_ptr aut =
nullptr,
76 twa_graph_ptr aut =
nullptr,
110 twa_graph_ptr aut =
nullptr,
111 ocheck algo = ocheck::Auto);
159 SPOT_API std::string
mp_class(
char mpc,
const char* opt);
op
Operator types.
Definition: formula.hh:78
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:48
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:26
ocheck
Enum used to change the behavior of is_obligation().
Definition: hierarchy.hh:81
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.