6 #include <unordered_map>
7 #include <unordered_set>
11 #include <boost/algorithm/string.hpp>
34 template <
typename 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 = aut->out(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 <
typename Aut,
typename LabelSet>
74 const auto& a = aut->as<Aut>();
75 const auto& w = word->as<LabelSet>();
88 template <
typename Aut>
99 using pair_t = std::pair<state_t, state_t>;
101 using paths_t = std::unordered_map<state_t, dist_transition_t>;
102 using path_t =
typename paths_t::value_type;
118 pair_ =
pair(aut_, keep_initials);
119 paths_ =
paths_ibfs(pair_, pair_->singletons());
125 return pair_->is_singleton(p.first);
133 == paths_.size() + pair_->singletons().size(),
134 "automaton is not synchronizing");
136 for (
auto s : pair_->states())
137 if (!pair_->is_singleton(s))
143 std::vector<transition_t> res;
145 while (!pair_->is_singleton(bt_curr))
149 bt_curr = pair_->dst_of(t);
156 return pair_->is_singleton(s) ? 0 : paths_.find(s)->second.first;
161 auto ntf = pair_->out(s, l);
162 auto size = ntf.size();
164 require(
size < 2,
"automaton must be deterministic");
165 return pair_->dst_of(*ntf.begin());
170 res_ = aut_->labelset()->mul(res_, label);
171 std::unordered_set<state_t> new_todo;
175 if (!pair_->is_singleton(new_state))
176 new_todo.insert(new_state);
178 todo_ = std::move(new_todo);
199 return paths_.size() == pair_->states().size() - 1;
233 while (!todo_.empty())
235 int min = std::numeric_limits<int>::max();
239 int d = (this->*(heuristic))(s);
257 while (!todo_.empty())
259 int min = std::numeric_limits<int>::max();
263 pair_t o = pair_->get_origin(s);
264 if (!first && o.first != previous && o.second != previous)
275 pair_t pair_end = pair_->get_origin(
276 pair_->dst_of(
path[
path.size() - 1]));
277 assert(pair_end.first == pair_end.second);
278 previous = pair_end.first;
292 while (!todo_.empty())
296 int min = std::numeric_limits<int>::max();
297 for (
const auto& l : pair_->labelset()->genset())
299 int cur_min =
phi_3(l);
307 unsigned sq_bound = aut_->states().size();
308 if (min < 0 && count++ < (sq_bound * sq_bound))
314 size_t t = todo_.size();
315 int bound = std::min(aut_->states().size(), (t * t - t / 2));
316 int min = std::numeric_limits<int>::max();
320 if (count++ >= bound)
382 template <
typename Aut>
394 template <
typename Aut>
397 const auto& a = aut->as<Aut>();
409 template <
typename Aut>
414 if (boost::iequals(algo,
"greedy") || boost::iequals(algo,
"eppstein"))
416 else if (boost::iequals(algo,
"cycle"))
418 else if (boost::iequals(algo,
"synchrop"))
420 else if (boost::iequals(algo,
"synchropl"))
422 else if (boost::iequals(algo,
"fastsynchro"))
425 raise(
"synchronizing_word: invalid algorithm: ",
str_escape(algo));
433 template <
typename Aut,
typename String>
437 const auto& a = aut->as<Aut>();
label synchronizing_word(const automaton &aut, const std::string &algo)
Bridge.
std::ostream & str_escape(std::ostream &os, const std::string &str)
Output a string, escaping special characters.
typename detail::label_t_of_impl< base_t< ValueSet >>::type label_t_of
std::shared_ptr< const detail::label_base > label
bool is_synchronizing(const automaton &aut)
Bridge.
word_t_of< automaton_t > word_t
std::unordered_map< state_t, dist_transition_t > paths_t
typename detail::state_t_of_impl< base_t< ValueSet >>::type state_t_of
label_t_of< automaton_t > label_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::shared_ptr< detail::pair_automaton_impl< Aut >> pair_automaton
std::pair< state_t, state_t > pair_t
bool is_synchronizing(const Aut &aut)
Whether this automaton is synchronizing, i.e., has synchronizing words.
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.
std::vector< transition_t > recompose_path(state_t from) const
transition_t_of< automaton_t > transition_t
typename labelset_t_of< base_t< ValueSet >>::word_t word_t_of
int phi_3(const label_t &l) const
Heuristic used for FastSynchro.
word_synchronizer(const automaton_t &aut)
void erase_if(Container &c, const Predicate &p)
void apply_label(const label_t &label)
std::shared_ptr< detail::automaton_base > automaton
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.
size_t size(const ExpSet &rs, const typename ExpSet::value_t &r)
int delta(state_t p, const std::vector< transition_t > &w) const
Compute dist(d(s, w)) - dist(s).
void require(bool b, Args &&...args)
If b is not verified, raise an error with args as message.
int dist(state_t s) const
word_t synchro(heuristic_t heuristic)
typename detail::transition_t_of_impl< base_t< ValueSet >>::type transition_t_of
auto(word_synchronizer::*)(state_t) const -> int heuristic_t
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)) ...
void init_pair(bool keep_initials=false)
pair_automaton< Aut > pair(const Aut &aut, bool keep_initials=false)
void init_synchro(bool keep_initials=false)
bool is_synchronized_by(const automaton &aut, const label &word)
Bridge.
pair_automaton< Aut > pair_
std::unordered_set< state_t > todo_
int phi_2(state_t p) const
Heuristic used for SynchroPL.
state_t_of< automaton_t > state_t
std::pair< unsigned, transition_t > dist_transition_t
Paths in filesystems, i.e., file names.
typename paths_t::value_type path_t
bool is_synchronized_by(const Aut &aut, const word_t_of< Aut > &w)
Whether w synchronizes automaton aut.
label make_label(const LabelSet &ls, const typename LabelSet::value_t &l)