21#include <spot/twaalgos/emptiness.hh>
35 twa_word(
const bdd_dict_ptr& dict)
noexcept;
36 twa_word(
const twa_run_ptr& run)
noexcept;
39 dict_->unregister_all_my_variables(
this);
71 typedef std::list<bdd> seq_t;
75 bdd_dict_ptr get_dict()
const
95 return as_automaton()->intersects(aut);
121 return std::make_shared<twa_word>(dict);
127 return std::make_shared<twa_word>(run);
142 twa_word_ptr
parse_word(
const std::string& word,
const bdd_dict_ptr& dict);
Definition: automata.hh:26
twa_word_ptr parse_word(const std::string &word, const bdd_dict_ptr &dict)
Parse a twa_word.
twa_word_ptr make_twa_word(const bdd_dict_ptr &dict)
Create an empty twa_word.
Definition: word.hh:119
An infinite word stored as a lasso.
Definition: word.hh:34
twa_graph_ptr as_automaton() const
Convert the twa_word as an automaton.
friend std::ostream & operator<<(std::ostream &os, const twa_word &w)
Print a twa_word.
bool intersects(const_twa_ptr aut) const
Check if a the twa_word intersect another automaton.
Definition: word.hh:93
void use_all_aps(bdd aps, bool positive=false)
Use all atomic proposition.
void simplify()
Simplify a lasso-shaped word.