21#include <spot/twaalgos/sccinfo.hh>
48 SPOT_DEPRECATED(
"is third argument of is_terminal_automaton()"
182 SPOT_API twa_graph_ptr
192 SPOT_API twa_graph_ptr
196 SPOT_API twa_graph_ptr
197 decompose_strength(const const_twa_graph_ptr& aut, const
char* keep);
208 SPOT_API twa_graph_ptr
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:449
Definition: automata.hh:26
bool is_weak_automaton(const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
Check whether an automaton is weak.
bool is_inherently_weak_automaton(const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
Check whether an automaton is inherently weak.
twa_graph_ptr decompose_scc(const const_twa_graph_ptr &aut, const char *keep)
Extract a sub-automaton of a given strength.
bool is_very_weak_automaton(const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
Check whether an automaton is very-weak.
bool is_terminal_automaton(const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
Check whether an automaton is terminal.
bool is_safety_automaton(const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
Check whether an automaton is a safety automaton.
bool is_liveness_automaton(const const_twa_graph_ptr &aut)
Whether the automaton represents a liveness property.
void check_strength(const twa_graph_ptr &aut, scc_info *sm=nullptr)
Check whether an automaton is weak or terminal.