22 #include <spot/twa/twagraph.hh> 34 SPOT_API twa_graph_ptr
35 sl(const_twa_graph_ptr aut);
47 SPOT_API twa_graph_ptr
50 SPOT_API twa_graph_ptr
51 sl2(const_twa_graph_ptr aut);
66 SPOT_API twa_graph_ptr
69 SPOT_API twa_graph_ptr
70 closure(const_twa_graph_ptr aut);
109 const_twa_graph_ptr aut_nf =
nullptr,
130 bool do_not_determinize =
false);
144 SPOT_API std::vector<bool>
146 const_twa_graph_ptr neg =
nullptr);
148 SPOT_API std::vector<bool>
171 formula f_pos,
unsigned color = 0);
174 const_twa_graph_ptr neg =
nullptr,
190 SPOT_API std::vector<bdd>
192 const_twa_graph_ptr neg =
nullptr);
194 SPOT_API std::vector<bdd>
215 const std::vector<bool>& sistates);
232 SPOT_API std::vector<bool>
234 (twa_graph_ptr aut,
const std::vector<bool>& sistates);
Definition: automata.hh:26
std::vector< bool > stutter_invariant_states(const_twa_graph_ptr pos, formula f_pos)
Determinate the states that are stutter-invariant in pos.
std::vector< bool > make_stutter_invariant_forward_closed_inplace(twa_graph_ptr aut, const std::vector< bool > &sistates)
Change the automaton so its set of stutter-invariant state is forward-closed.
trival check_stutter_invariance(twa_graph_ptr aut_f, formula f=nullptr, bool do_not_determinize=false)
Check whether aut is stutter-invariant.
twa_graph_ptr sl2_inplace(twa_graph_ptr aut)
Close the automaton by allowing letters to be duplicated.
void highlight_stutter_invariant_states(twa_graph_ptr pos, const_twa_graph_ptr neg=nullptr, unsigned color=0)
Highlight the states of pos that are stutter-invariant.
twa_graph_ptr sl(const_twa_graph_ptr aut)
Close the automaton by allowing letters to be duplicated.
int is_stutter_invariant_forward_closed(twa_graph_ptr aut, const std::vector< bool > &sistates)
Test if the set of stutter-invariant states is forward-closed.
twa_graph_ptr closure_inplace(twa_graph_ptr aut)
Close the automaton by allowing duplicate letter removal.
twa_graph_ptr sl2(const_twa_graph_ptr aut)
Close the automaton by allowing letters to be duplicated.
twa_graph_ptr closure(const_twa_graph_ptr aut)
Close the automaton by allowing duplicate letter removal.
bool is_stutter_invariant(twa_graph_ptr aut_f, const_twa_graph_ptr aut_nf=nullptr, int algo=0)
Check if an automaton has the stutter invariance property.
std::vector< bdd > stutter_invariant_letters(const_twa_graph_ptr pos, formula f_pos)
Determinate the letters with which each state is stutter-invariant.