22 #include <spot/twa/twagraph.hh> 49 SPOT_API twa_graph_ptr
50 sl(const_twa_graph_ptr aut);
74 SPOT_API twa_graph_ptr
80 SPOT_API twa_graph_ptr
81 sl2(const_twa_graph_ptr aut);
108 SPOT_API twa_graph_ptr
115 SPOT_API twa_graph_ptr
116 closure(const_twa_graph_ptr aut);
185 const_twa_graph_ptr aut_nf =
nullptr,
206 bool do_not_determinize =
false);
220 SPOT_API std::vector<bool>
222 const_twa_graph_ptr neg =
nullptr);
224 SPOT_API std::vector<bool>
247 formula f_pos,
unsigned color = 0);
250 const_twa_graph_ptr neg =
nullptr,
266 SPOT_API std::vector<bdd>
268 const_twa_graph_ptr neg =
nullptr);
270 SPOT_API std::vector<bdd>
291 const std::vector<bool>& sistates);
308 SPOT_API std::vector<bool>
310 (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.