Awali
Another Weighted Automata library
synchronizing_word.hh
Go to the documentation of this file.
1 // This file is part of Awali.
2 // Copyright 2016-2022 Sylvain Lombardy, Victor Marsault, Jacques Sakarovitch
3 //
4 // Awali is a free software: you can redistribute it and/or modify
5 // it under the terms of the GNU General Public License as published by
6 // the Free Software Foundation, either version 3 of the License, or
7 // (at your option) any later version.
8 //
9 // This program is distributed in the hope that it will be useful,
10 // but WITHOUT ANY WARRANTY; without even the implied warranty of
11 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 // GNU General Public License for more details.
13 //
14 // You should have received a copy of the GNU General Public License
15 // along with this program. If not, see <http://www.gnu.org/licenses/>.
16 
17 #ifndef AWALI_ALGOS_SYNCHRONIZING_WORD_HH
18 # define AWALI_ALGOS_SYNCHRONIZING_WORD_HH
19 
20 # include <algorithm>
21 # include <iostream>
22 # include <limits>
23 # include <map>
24 # include <queue>
25 # include <set>
26 # include <unordered_set>
27 # include <utility>
28 # include <vector>
29 
34 #include <awali/sttc/ctx/traits.hh>
35 #include <awali/sttc/misc/map.hh>
36 #include <awali/sttc/misc/pair.hh>
37 #include <awali/sttc/misc/raise.hh>
39 
40 namespace awali {
41  namespace sttc {
42 
43 
44  /*--------------------------------------.
45  | is_synchronized_by(automaton, word). |
46  `--------------------------------------*/
47 
48  template <typename Aut>
49  bool
50  is_synchronized_by(const Aut& aut,
51  const typename labelset_t_of<Aut>::word_t& w)
52  {
53  // using automaton_t = Aut;
54  std::unordered_set<state_t> todo;
55 
56  for (auto s : aut->states())
57  todo.insert(s);
58 
59  for (auto l : aut->labelset()->letters_of(w))
60  {
61  std::unordered_set<state_t> new_todo;
62  for (auto s : todo)
63  {
64  auto ntf = aut->out(s, l);
65  auto size = ntf.size();
66  require(0 < size, "automaton must be complete");
67  require(size < 2, "automaton must be deterministic");
68  new_todo.insert(aut->dst_of(*ntf.begin()));
69  }
70  todo = std::move(new_todo);
71  }
72 
73  return todo.size() == 1;
74  }
75 
76  /*-----------------.
77  | pair_automaton. |
78  `-----------------*/
79 
80  namespace internal
81  {
82  template <typename Aut>
84  : public automaton_decorator<mutable_automaton<context_t_of<Aut>>>
85  //: public automaton_decorator<typename Aut::element_type::automaton_nocv_t>
86  {
87  public:
88  using automaton_t = Aut;
90  // typename automaton_t::element_type::automaton_nocv_t;
93  using weight_t = typename weightset_t::value_t;
95 
96  private:
99  using pair_t = std::pair<state_t, state_t>;
100  using origins_t = std::map<state_t, pair_t>;
101 
102  public:
103  pair_automaton_impl(const automaton_t& aut, bool keep_initials = false)
104  : super_t(aut->context())
105  , input_(aut)
106  , transition_map_(aut)
107  , keep_initials_(keep_initials)
108  {
109  auto ctx = input_->context();
110  auto ws = ctx.weightset();
111 
112  if (!keep_initials_)
113  {
114  q0_ = this->add_state(); // q0 special state
115  for (auto l : input_->labelset()->genset())
116  this->add_transition(q0_, q0_, l, ws->one());
117  }
118  else
119  for (auto s : input_->states())
120  pair_states_.emplace(std::make_pair(s, s), this->add_state());
121 
122  // States are "ordered": (s1, s2) is defined only for s1 < s2.
123  {
124  auto states = input_->states();
125  auto end = std::end(states);
126  for (auto i1 = std::begin(states); i1 != end; ++i1)
127  {
128  // FIXME: cannot use i2 = std::next(i1) with clang 3.5
129  // and Boost 1.55.
130  // https://svn.boost.org/trac/boost/ticket/9984
131  auto i2 = i1;
132  for (++i2; i2 != end; ++i2)
133  // s1 < s2, no need for make_ordered_pair.
134  pair_states_.emplace(std::make_pair(*i1, *i2),
135  this->add_state());
136  }
137  }
138 
139  for (auto ps : pair_states_)
140  {
141  auto pstates = ps.first; // pair of states
142  auto cstate = ps.second; // current state
143 
144  for (const auto& p : internal::zip_maps(transition_map_[pstates.first],
145  transition_map_[pstates.second]))
146  this->add_transition(cstate,
147  state_(std::get<0>(p.second).dst,
148  std::get<1>(p.second).dst),
149  p.first, ws->one());
150  }
151 
152  for (const auto& p: pair_states_)
153  origins_.emplace(p.second, p.first);
154 
155  if (keep_initials_)
156  for (auto s : input_->states())
157  singletons_.push_back(state_(s, s));
158  else
159  singletons_.push_back(q0_);
160  }
161 
162  state_t get_q0() const
163  {
164  require(!keep_initials_, "can't get_q0() on a pairer that "
165  "keeps origins");
166  return q0_;
167  }
168 
169  bool is_singleton(state_t s) const
170  {
171  if (keep_initials_)
172  {
173  pair_t p = get_origin(s);
174  return p.first == p.second;
175  }
176  else
177  return s == q0_;
178  }
179 
180  const std::vector<state_t>& singletons()
181  {
182  return singletons_;
183  }
184 
185  static std::string sname()
186  {
187  return "pair_automaton<" + automaton_t::element_type::sname() + ">";
188  }
189 
190  std::string vname(bool full = true) const
191  {
192  return "pair_automaton<" + input_->vname(full) + ">";
193  }
194 
195  const std::unordered_map<pair_t, state_t>& get_map_pair() const
196  {
197  return pair_states_;
198  }
199 
201  const origins_t& origins() const
202  {
203  return origins_;
204  }
205 
206  const pair_t get_origin(state_t s) const
207  {
208  auto i = origins().find(s);
209  require(i != std::end(origins()), "state not found in origins");
210  return i->second;
211  }
212 
213  std::ostream&
214  print_state_name(state_t ss, std::ostream& o,
215  const std::string& fmt = "text") const
216  {
217  auto i = origins().find(ss);
218  if (i == std::end(origins()))
219  this->print_state(ss, o);
220  else
221  {
222  input_->print_state_name(i->second.first, o, fmt);
223  o << ", ";
224  input_->print_state_name(i->second.second, o, fmt);
225  }
226  return o;
227  }
228 
229  private:
232  state_t state_(state_t s1, state_t s2)
233  {
234  // Benches show it is slightly faster to handle this case
235  // especially rather that mapping these "diagonal states" to
236  // q0_ in pair_states_.
237  if (s1 == s2 && !keep_initials_)
238  return q0_;
239  else
240  return pair_states_[make_ordered_pair(s1, s2)];
241  }
242 
244  automaton_t input_;
246  using transition_map_t
247  = transition_map<automaton_t, weightset_t_of<automaton_t>, true>;
248  transition_map_t transition_map_;
249  std::unordered_map<pair_t, state_t> pair_states_;
250  origins_t origins_;
251  std::vector<state_t> singletons_;
252  state_t q0_;
253  bool keep_initials_ = false;
254  };
255  }
256 
257  template <typename Aut>
259  = std::shared_ptr<internal::pair_automaton_impl<Aut>>;
260 
261  /*------------------.
262  | pair(automaton). |
263  `------------------*/
264 
265  template <typename Aut>
266  pair_automaton<Aut> pair(const Aut& aut, bool keep_initials = false)
267  {
268  auto res = make_shared_ptr<pair_automaton<Aut>>(aut, keep_initials);
269  return res;
270  }
271 
272  namespace internal
273  {
274  template <typename Aut>
275  class synchronizer
276  {
277  public:
278  using automaton_t = Aut;
281 
282  private:
283  using pair_t = std::pair<state_t, state_t>;
284  using dist_transition_t = std::pair<unsigned, transition_t>;
285 
286  automaton_t aut_;
287  pair_automaton<Aut> pair_;
288  std::unordered_map<state_t, dist_transition_t> paths_;
289  std::unordered_set<state_t> todo_;
290  word_t res_;
291 
292  public:
294  : aut_(aut)
295  {}
296 
297  private:
298  void init_pair(bool keep_initials = false)
299  {
300  pair_ = pair(aut_, keep_initials);
301  paths_ = paths_ibfs(pair_, pair_->singletons());
302 
303  if (keep_initials)
304  for (auto it = paths_.begin(); it != paths_.end(); /* nothing */)
305  {
306  if (pair_->is_singleton(it->first))
307  paths_.erase(it++);
308  else
309  ++it;
310  }
311  }
312 
313  void init_synchro(bool keep_initials = false)
314  {
315  init_pair(keep_initials);
316  require(pair_->states().size() == paths_.size() +
317  pair_->singletons().size(), "automaton is not synchronizing");
318 
319  for (auto s : pair_->states())
320  if (!pair_->is_singleton(s))
321  todo_.insert(s);
322  }
323 
324  std::vector<transition_t> recompose_path(state_t from)
325  {
326  std::vector<transition_t> res;
327  state_t bt_curr = from;
328  while (!pair_->is_singleton(bt_curr))
329  {
330  transition_t t = paths_.find(bt_curr)->second.second;
331  res.push_back(t);
332  bt_curr = pair_->dst_of(t);
333  }
334  return res;
335  }
336 
337  int dist(state_t s)
338  {
339  if (pair_->is_singleton(s))
340  return 0;
341  return paths_.find(s)->second.first;
342  }
343 
344  state_t dest_state(state_t s, const label_t& l)
345  {
346  auto ntf = pair_->out(s, l);
347  auto size = ntf.size();
348  require(0 < size, "automaton must be complete");
349  require(size < 2, "automaton must be deterministic");
350  return pair_->dst_of(*ntf.begin());
351  }
352 
353  void apply_label(const label_t& label)
354  {
355  res_ = aut_->labelset()->concat(res_, label);
356  std::unordered_set<state_t> new_todo;
357  for (auto s : todo_)
358  {
359  auto add_state = dest_state(s, label);
360  if (!pair_->is_singleton(add_state))
361  new_todo.insert(add_state);
362  }
363  todo_ = std::move(new_todo);
364  }
365 
366  // "Apply" a word to the set of active states (for each state, for each
367  // label, perform s = d(s))
368  void apply_path(const std::vector<transition_t>& path)
369  {
370  for (auto t : path)
371  apply_label(pair_->label_of(t));
372  }
373 
374  public:
375 
376  // We just perform an inverse BFS from q0 and put all the accessible
377  // states in 'paths'. If the size of paths is the same than the number
378  // of states of pa (minus q0), then for each pair of states (p, q),
379  // there is a word w such that d(p, w) = d(q, w), thus the automaton is
380  // synchronizing.
382  {
383  init_pair();
384  return paths_.size() == pair_->states().size() - 1;
385  }
386 
388  {
389  return synchro(&synchronizer::dist);
390  }
391 
393  {
394  return cycle_();
395  }
396 
398  {
399  return synchro(&synchronizer::phi_1);
400  }
401 
403  {
404  return synchro(&synchronizer::phi_2);
405  }
406 
408  {
409  return fastsynchro_();
410  }
411 
412  private:
413  using heuristic_t = auto (synchronizer::*)(state_t) -> int;
414 
415  word_t synchro(heuristic_t heuristic)
416  {
417  init_synchro();
418  while (!todo_.empty())
419  {
421  state_t s_min = 0;
422  for (auto s : todo_)
423  {
424  int d = (this->*(heuristic))(s);
425  if (d < min)
426  {
427  min = d;
428  s_min = s;
429  }
430  }
431 
432  apply_path(recompose_path(s_min));
433  }
434  return res_;
435  }
436 
437  word_t cycle_()
438  {
439  init_synchro(true);
440  bool first = true;
441  state_t previous = 0;
442  while (!todo_.empty())
443  {
445  state_t s_min = 0;
446  for (auto s : todo_)
447  {
448  pair_t o = pair_->get_origin(s);
449  if (!first && o.first != previous && o.second != previous)
450  continue;
451  int d = dist(s);
452  if (d < min)
453  {
454  min = d;
455  s_min = s;
456  }
457  }
458 
459  const auto& path = recompose_path(s_min);
460  pair_t pair_end = pair_->get_origin(
461  pair_->dst_of(path[path.size() - 1]));
462  assert(pair_end.first == pair_end.second);
463  previous = pair_end.first;
464  first = false;
465  apply_path(path);
466  }
467  return res_;
468  }
469 
470  word_t fastsynchro_()
471  {
472  init_synchro();
473 
474  // The drawback of this algorithm is that it does not guarantee us to
475  // converge, so we this to counter prevent potential infinite loops.
476  unsigned count = 0;
477  while (!todo_.empty())
478  {
479  // compute lmin = arg min { phi_3(l) } forall l in labelset
480  label_t lmin;
482  for (const auto& l : pair_->labelset()->genset())
483  {
484  int cur_min = phi_3(l);
485  if (cur_min < min)
486  {
487  min = cur_min;
488  lmin = l;
489  }
490  }
491 
492  unsigned sq_bound = aut_->states().size();
493  if (min < 0 && count++ < (sq_bound * sq_bound))
494  apply_label(lmin);
495  else
496  {
497  // fallback on the phi_2 heuristic, with a size restriction.
498  int count = 0;
499  size_t t = todo_.size();
500  int bound = std::min(aut_->states().size(), (t * t - t / 2));
502  state_t s_min = 0;
503  for (auto s : todo_)
504  {
505  if (count++ >= bound)
506  break;
507  int d = phi_2(s);
508  if (d < min)
509  {
510  min = d;
511  s_min = s;
512  }
513  }
514  apply_path(recompose_path(s_min));
515  }
516  }
517  return res_;
518  }
519 
521  int delta(state_t p, const std::vector<transition_t>& w)
522  {
523  state_t np = p;
524  for (auto t : w)
525  np = dest_state(np, pair_->label_of(t));
526  return dist(np) - dist(p);
527  }
528 
532  int phi_1(state_t p)
533  {
534  int res = 0;
535  auto w = recompose_path(p);
536  for (auto s: todo_)
537  if (s != p)
538  res += delta(s, w);
539  return res;
540  }
541 
544  int phi_2(state_t p)
545  {
546  return phi_1(p) + dist(p);
547  }
548 
551  int phi_3(const label_t& l)
552  {
553  int res = 0;
554  for (auto s: todo_)
555  res += dist(dest_state(s, l)) - dist(s);
556  return res;
557  }
558  };
559  }
560 
561 
562  /*-----------------------------.
563  | is_synchronizing(automaton). |
564  `-----------------------------*/
565 
566  template <typename Aut>
567  bool is_synchronizing(const Aut& aut)
568  {
570  return sync.is_synchronizing();
571  }
572 
573  /*-------------------------------.
574  | synchronizing_word(automaton). |
575  `-------------------------------*/
576 
577  template <typename Aut>
579  synchronizing_word(const Aut& aut, const std::string& algo = "greedy")
580  {
582  if (algo == "greedy" || algo == "eppstein")
583  return sync.greedy();
584  else if (algo == "cycle")
585  return sync.cycle();
586  else if (algo == "synchrop")
587  return sync.synchroP();
588  else if (algo == "synchropl")
589  return sync.synchroPL();
590  else if (algo == "fastsynchro")
591  return sync.fastsynchro();
592  else
593  raise("synchronizing_word: invalid algorithm: ", str_escape(algo));
594  }
595 
596  /*--------.
597  | cerny. |
598  `--------*/
599 
608 
609  template <typename Ctx>
610  mutable_automaton<Ctx>
611  cerny(const Ctx& ctx, unsigned num_states)
612  {
613  require(0 < num_states, "num_states must be > 0");
614 
615  using automaton_t = mutable_automaton<Ctx>;
616  automaton_t res = make_shared_ptr<automaton_t>(ctx);
617 
618  std::vector<state_t> states;
619  states.reserve(num_states);
620 
621  for (unsigned i = 0; i < num_states; ++i)
622  states.push_back(res->add_state());
623 
624  for (unsigned i = 0; i < num_states; ++i)
625  {
626  bool la = true;
627  for (auto l : ctx.labelset()->genset())
628  {
629  auto dest = (la || i == num_states - 1) ? (i + 1) % num_states : i;
630  res->add_transition(states[i], states[dest], l,
631  ctx.weightset()->one());
632  la = false;
633  }
634  }
635 
636  res->set_initial(states[0]);
637  res->set_final(states[0]);
638  res->set_name("cerny-"+std::to_string(num_states));
639  return res;
640  }
641  }
642 }//end of ns awali::stc
643 
644 #endif // !AWALI_ALGOS_SYNCHRONIZING_WORD_HH
carries the algebraic settings of automata
Definition: context.hh:40
Aggregate an automaton, and forward calls to it.
Definition: automaton_decorator.hh:36
auto print_state(Args &&... args) const -> decltype(aut_-> print_state(std::forward< Args >(args)...))
Definition: automaton_decorator.hh:154
auto states(Args &&... args) const -> decltype(aut_-> states(std::forward< Args >(args)...))
Definition: automaton_decorator.hh:157
auto add_state(Args &&... args) -> decltype(aut_-> add_state(std::forward< Args >(args)...))
Definition: automaton_decorator.hh:187
auto add_transition(Args &&... args) -> decltype(aut_-> add_transition(std::forward< Args >(args)...))
Definition: automaton_decorator.hh:181
Definition: synchronizing_word.hh:86
typename weightset_t::value_t weight_t
Definition: synchronizing_word.hh:93
mutable_automaton< context_t_of< Aut > > automaton_nocv_t
Definition: synchronizing_word.hh:89
state_t get_q0() const
Definition: synchronizing_word.hh:162
static std::string sname()
Definition: synchronizing_word.hh:185
const std::unordered_map< pair_t, state_t > & get_map_pair() const
Definition: synchronizing_word.hh:195
Aut automaton_t
Definition: synchronizing_word.hh:88
bool is_singleton(state_t s) const
Definition: synchronizing_word.hh:169
pair_automaton_impl(const automaton_t &aut, bool keep_initials=false)
Definition: synchronizing_word.hh:103
weightset_t_of< automaton_t > weightset_t
Definition: synchronizing_word.hh:92
const std::vector< state_t > & singletons()
Definition: synchronizing_word.hh:180
std::ostream & print_state_name(state_t ss, std::ostream &o, const std::string &fmt="text") const
Definition: synchronizing_word.hh:214
const origins_t & origins() const
A map from result state to tuple of original states.
Definition: synchronizing_word.hh:201
const pair_t get_origin(state_t s) const
Definition: synchronizing_word.hh:206
std::string vname(bool full=true) const
Definition: synchronizing_word.hh:190
context_t_of< automaton_t > context_t
Definition: synchronizing_word.hh:91
std::vector< state_t > states(abstract_automaton_t const *aut, bool all)
any_t word_t
Type for words; it is an alias to any_t since the precise type depends on the context (most of the ti...
Definition: typedefs.hh:67
json_ast_t from(std::istream &i)
Builds a json_ast_t from an input stream.
zipped_maps< Dereference, Maps... > zip_maps(Maps &&... maps)
Definition: zip_maps.hh:274
std::string to_string(identities i)
std::pair< T, T > make_ordered_pair(T e1, T e2)
Definition: pair.hh:52
typename internal::label_t_of_impl< internal::base_t< ValueSet > >::type label_t_of
Helper to retrieve the type of the labels of a value set.
Definition: traits.hh:71
std::shared_ptr< internal::pair_automaton_impl< Aut > > pair_automaton
Definition: synchronizing_word.hh:259
bool is_synchronizing(const Aut &aut)
Definition: synchronizing_word.hh:567
std::ostream & str_escape(std::ostream &os, const int c)
Definition: escape.hh:30
typename internal::context_t_of_impl< internal::base_t< ValueSet > >::type context_t_of
Helper to retrieve the type of the context of a value set.
Definition: traits.hh:66
mutable_automaton< Ctx > cerny(const Ctx &ctx, unsigned num_states)
Cerny automata are automata whose synchronizing word length is always (n - 1)^2, the upper bound of t...
Definition: synchronizing_word.hh:611
typename internal::labelset_t_of_impl< internal::base_t< ValueSet > >::type labelset_t_of
Helper to retrieve the type of the labelset of a value set.
Definition: traits.hh:76
std::unordered_map< state_t, std::pair< unsigned, transition_t > > paths_ibfs(const Aut &aut, std::vector< state_t > start)
Definition: distance.hh:40
std::shared_ptr< internal::mutable_automaton_impl< Context > > mutable_automaton
Definition: mutable_automaton.hh:45
void require(bool b, Args &&... args)
If b is not verified, raise an error with args as message.
Definition: raise.hh:55
pair_automaton< Aut > pair(const Aut &aut, bool keep_initials=false)
Definition: synchronizing_word.hh:266
labelset_t_of< Aut >::word_t synchronizing_word(const Aut &aut, const std::string &algo="greedy")
Definition: synchronizing_word.hh:579
typename internal::weightset_t_of_impl< internal::base_t< ValueSet > >::type weightset_t_of
Helper to retrieve the type of the weightset of a value set.
Definition: traits.hh:86
bool is_synchronized_by(const Aut &aut, const typename labelset_t_of< Aut >::word_t &w)
Definition: synchronizing_word.hh:50
ATTRIBUTE_CONST int max(int a, int b)
Definition: arith.hh:54
ATTRIBUTE_CONST int min(int a, int b)
Definition: arith.hh:48
static const std::string full
Completely version of Awali as a std::string.
Definition: version.hh:42
Main namespace of Awali.
Definition: ato.hh:22
unsigned state_t
Definition: types.hh:21
unsigned transition_t
Definition: types.hh:22
Definition: synchronize.hh:47
word_t cycle()
Definition: synchronizing_word.hh:392
word_t greedy()
Definition: synchronizing_word.hh:387
word_t synchroP()
Definition: synchronizing_word.hh:397
synchronizer(const automaton_t &aut)
Definition: synchronizing_word.hh:293
word_t synchroPL()
Definition: synchronizing_word.hh:402
Aut automaton_t
Definition: synchronizing_word.hh:278
typename labelset_t_of< automaton_t >::word_t word_t
Definition: synchronizing_word.hh:279
bool is_synchronizing()
Definition: synchronizing_word.hh:381
label_t_of< automaton_t > label_t
Definition: synchronizing_word.hh:280
word_t fastsynchro()
Definition: synchronizing_word.hh:407