6 #include <unordered_map>
7 #include <unordered_set>
11 #include <boost/algorithm/string.hpp>
34 template <Automaton Aut>
38 using automaton_t = Aut;
41 std::unordered_set<state_t> todo;
43 for (
auto s : aut->states())
46 for (
auto l : aut->labelset()->letters_of(w))
48 std::unordered_set<state_t> new_todo;
51 auto ntf =
out(aut, s, l);
52 auto size = ntf.size();
54 "is_synchronized_by: automaton must be complete");
56 "is_synchronized_by: automaton must be deterministic");
57 new_todo.insert(aut->dst_of(*ntf.begin()));
59 todo = std::move(new_todo);
62 return todo.size() == 1;
70 template <Automaton Aut,
typename LabelSet>
74 const auto& a = aut->
as<Aut>();
75 const auto& w = word->
as<LabelSet>();
88 template <Automaton Aut>
104 = std::pair<unsigned, transition_t_of<pair_automaton_t>>;
107 using path_t =
typename paths_t::value_type;
125 pair_ =
pair(aut_, keep_initials);
126 paths_ =
paths_ibfs(pair_, pair_->singletons());
132 return pair_->is_singleton(p.first);
140 == paths_.size() + pair_->singletons().size(),
141 "automaton is not synchronizing");
143 for (
auto s : pair_->states())
144 if (!pair_->is_singleton(s))
150 std::vector<transition_t>
res;
152 while (!pair_->is_singleton(bt_curr))
156 bt_curr = pair_->dst_of(t);
163 return pair_->is_singleton(s) ? 0 : paths_.find(s)->second.first;
168 auto ntf =
out(pair_, s, l);
169 auto size = ntf.size();
171 require(
size < 2,
"automaton must be deterministic");
172 return pair_->dst_of(*ntf.begin());
177 res_ = aut_->labelset()->mul(res_, label);
178 std::unordered_set<state_t> new_todo;
182 if (!pair_->is_singleton(new_state))
183 new_todo.insert(new_state);
185 todo_ = std::move(new_todo);
206 return paths_.size() == pair_->states().size() - 1;
240 while (!todo_.empty())
242 int min = std::numeric_limits<int>::max();
246 int d = (this->*(heuristic))(s);
264 while (!todo_.empty())
266 int min = std::numeric_limits<int>::max();
271 if (!first && o.first != previous && o.second != previous)
283 = pair_->get_origin(pair_->dst_of(
path[
path.size() - 1]));
284 assert(pair_end.first == pair_end.second);
285 previous = pair_end.first;
299 while (!todo_.empty())
303 int min = std::numeric_limits<int>::max();
304 for (
const auto& l : pair_->labelset()->generators())
306 int cur_min =
phi_3(l);
314 unsigned sq_bound = aut_->states().size();
315 if (min < 0 && count++ < (sq_bound * sq_bound))
321 size_t t = todo_.size();
322 int bound =
std::min(aut_->states().size(), (t * t - t / 2));
323 int min = std::numeric_limits<int>::max();
327 if (count++ >= bound)
389 template <Automaton Aut>
401 template <Automaton Aut>
404 const auto& a = aut->
as<Aut>();
416 template <Automaton Aut>
421 if (boost::iequals(algo,
"greedy") || boost::iequals(algo,
"eppstein"))
423 else if (boost::iequals(algo,
"cycle"))
425 else if (boost::iequals(algo,
"synchrop"))
427 else if (boost::iequals(algo,
"synchropl"))
429 else if (boost::iequals(algo,
"fastsynchro"))
432 raise(
"synchronizing_word: invalid algorithm: ",
str_escape(algo));
440 template <Automaton Aut,
typename String>
444 const auto& a = aut->
as<Aut>();
bool is_synchronizing(const Aut &aut)
Whether this automaton is synchronizing, i.e., has synchronizing words.
int phi_2(state_t p) const
Heuristic used for SynchroPL.
std::unordered_map< state_t_of< Aut >, std::pair< unsigned, transition_t_of< Aut > > > paths_ibfs(const Aut &aut, const std::vector< state_t_of< Aut >> &start)
Find the shortest paths from some states to all the states.
word_t synchro(heuristic_t heuristic)
void erase_if(Container &c, const Predicate &p)
std::shared_ptr< detail::pair_automaton_impl< Aut >> pair_automaton
word_synchronizer(const automaton_t &aut)
auto(word_synchronizer::*)(state_t) const -> int heuristic_t
pair_automaton< automaton_t > pair_automaton_t
void init_synchro(bool keep_initials=false)
label_t_of< automaton_t > label_t
bool is_synchronized_by(const automaton &aut, const label &word)
Bridge.
std::pair< state_t, state_t > state_name_t
bool is_synchronized_by(const Aut &aut, const word_t_of< Aut > &w)
Whether w synchronizes automaton aut.
int dist(state_t s) const
bool is_synchronizing(const automaton &aut)
Bridge.
void require(Bool b, Args &&...args)
If b is not verified, raise an error with args as message.
typename detail::label_t_of_impl< base_t< ValueSet >>::type label_t_of
state_t_of< automaton_t > state_t
int phi_3(const label_t &l) const
Heuristic used for FastSynchro.
typename paths_t::value_type path_t
word_t_of< Aut > synchronizing_word(const Aut &aut, const std::string &algo="greedy")
Return a synchronizing word for aut using algo algo.
std::unordered_map< state_t_of< pair_automaton_t >, dist_transition_t > paths_t
int delta(state_t p, const std::vector< transition_t > &w) const
Compute dist(d(s, w)) - dist(s).
auto out(const Aut &aut, state_t_of< Aut > s)
Indexes of visible transitions leaving state s.
size_t size(const ExpSet &rs, const typename ExpSet::value_t &r)
std::vector< transition_t > recompose_path(state_t from) const
automaton_t aut_
Input automaton.
pair_automaton< Aut > pair(const Aut &aut, bool keep_initials=false)
std::pair< unsigned, transition_t_of< pair_automaton_t >> dist_transition_t
typename detail::state_t_of_impl< base_t< ValueSet >>::type state_t_of
typename labelset_t_of< base_t< ValueSet >>::word_t word_t_of
label synchronizing_word(const automaton &aut, const std::string &algo)
Bridge.
pair_automaton_t pair_
Corresponding pair automaton.
std::ostream & str_escape(std::ostream &os, const std::string &str, const char *special=nullptr)
Output a string, escaping special characters.
void apply_label(const label_t &label)
typename detail::transition_t_of_impl< base_t< ValueSet >>::type transition_t_of
auto & as()
Extract wrapped typed value.
value_impl< detail::label_tag > label
int phi_1(state_t p) const
Heuristic used for SynchroP.
void apply_path(const std::vector< transition_t > &path)
"Apply" a word to the set of active states (for each state, for each label, perform s = d(s)) ...
transition_t_of< automaton_t > transition_t
word_t_of< automaton_t > word_t
auto & as()
Extract wrapped typed automaton.
std::unordered_set< state_t > todo_
void init_pair(bool keep_initials=false)
state_t dest_state(state_t s, const label_t &l) const
law_t< LabelSet > make_wordset(const LabelSet &ls)
The wordset of a labelset.
Paths in filesystems, i.e., file names.