22 #include <spot/twaalgos/sccinfo.hh>
48 bool ignore_trivial_scc =
false);
166 SPOT_API twa_graph_ptr
176 SPOT_API twa_graph_ptr
180 SPOT_API twa_graph_ptr
181 decompose_strength(const const_twa_graph_ptr& aut, const
char* keep);
192 SPOT_API twa_graph_ptr
Compute an SCC map and gather assorted information.
Definition: sccinfo.hh:443
Definition: automata.hh:27
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_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.
bool is_terminal_automaton(const const_twa_graph_ptr &aut, scc_info *sm=nullptr, bool ignore_trivial_scc=false)
Check whether an automaton is terminal.