21#include <spot/twa/twagraph.hh>
33 SPOT_API twa_graph_ptr
34 sl(const_twa_graph_ptr aut);
46 SPOT_API twa_graph_ptr
49 SPOT_API twa_graph_ptr
50 sl2(const_twa_graph_ptr aut);
65 SPOT_API twa_graph_ptr
68 SPOT_API twa_graph_ptr
108 const_twa_graph_ptr aut_nf =
nullptr,
135 bool do_not_determinize =
false,
136 bool find_counterexamples =
false);
150 SPOT_API std::vector<bool>
152 const_twa_graph_ptr neg =
nullptr);
154 SPOT_API std::vector<bool>
177 formula f_pos,
unsigned color = 0);
180 const_twa_graph_ptr neg =
nullptr,
196 SPOT_API std::vector<bdd>
198 const_twa_graph_ptr neg =
nullptr);
200 SPOT_API std::vector<bdd>
221 const std::vector<bool>& sistates);
238 SPOT_API std::vector<bool>
240 (twa_graph_ptr aut,
const std::vector<bool>& sistates);
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
trival check_stutter_invariance(twa_graph_ptr aut_f, formula f=nullptr, bool do_not_determinize=false, bool find_counterexamples=false)
Check whether aut is stutter-invariant.
twa_graph_ptr closure(const_twa_graph_ptr aut)
Close the automaton by allowing duplicate letter removal.
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.
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.
std::vector< bdd > stutter_invariant_letters(const_twa_graph_ptr pos, const_twa_graph_ptr neg=nullptr)
Determinate the letters with which each state is stutter-invariant.
twa_graph_ptr sl(const_twa_graph_ptr aut)
Close the automaton by allowing letters to be duplicated.
void highlight_stutter_invariant_states(twa_graph_ptr pos, formula f_pos, unsigned color=0)
Highlight the states of pos that are stutter-invariant.
bool is_stutter_invariant(formula f, twa_graph_ptr aut_f=nullptr)
Check if a formula is stutter invariant.
twa_graph_ptr sl2(const_twa_graph_ptr aut)
Close the automaton by allowing letters to be duplicated.
std::vector< bool > stutter_invariant_states(const_twa_graph_ptr pos, const_twa_graph_ptr neg=nullptr)
Determinate the states that are stutter-invariant in pos.
twa_graph_ptr sl2_inplace(twa_graph_ptr aut)
Close the automaton by allowing letters to be duplicated.
twa_graph_ptr closure_inplace(twa_graph_ptr aut)
Close the automaton by allowing duplicate letter removal.
Definition: automata.hh:26