Vcsn  2.2
Be Rational
has-bounded-lag.hh
Go to the documentation of this file.
1 #pragma once
2 
3 #include <array>
4 #include <vector>
5 
7 #include <vcsn/ctx/context.hh>
8 #include <vcsn/dyn/automaton.hh> // dyn::make_automaton
10 #include <vcsn/misc/algorithm.hh> // detail::back
11 #include <vcsn/misc/tuple.hh> // make_index_sequence
12 
13 namespace vcsn
14 {
15 
16  namespace detail
17  {
18  template <Automaton Aut>
20  {
21  static_assert(context_t_of<Aut>::is_lat,
22  "has_bounded_lag: automaton labelset must be a tupleset");
23  // The algorithm makes no sense (and doesn't compile) if the transducer
24  // has only one tape.
25  static_assert(labelset_t_of<Aut>::size() >= 2,
26  "has_bounded_lag: transducer labelset must have at least 2 tapes");
27 
28  using automaton_t = Aut;
31  using label_t = typename labelset_t::value_t;
33 
34  static constexpr size_t number_of_tapes = labelset_t_of<Aut>::size();
35 
36  enum visit_state {
40  };
41 
42  // Keep track of what states we have visited or are visiting
43  using visited_t = std::vector<visit_state>;
44 
45  // Keep track of how we arrived in a state
46  using parent_state_t = std::vector<transition_t>;
47 
49  template <std::size_t... I>
51 
52  using delay_index_t = detail::make_index_sequence<number_of_tapes - 1>;
53 
55  using delay_t = std::array<int, number_of_tapes - 1>;
56 
57  public:
58 
59  // The vectors are indexed by the state number
61  : aut_(aut), v_(detail::back(aut_->all_states()) + 1, NOT_VISITED)
62  , p_(detail::back(aut_->all_states()) + 1, -1)
63  {}
64 
65  // Get the size (number of letters) of a label on a specific tape.
66  template <std::size_t I>
68  {
69  using tape_labelset_t = typename labelset_t::template valueset_t<I>;
70  return tape_labelset_t::size(std::get<I>(l));
71  }
72 
73  // Add the delay from the transition's label to the given delay
74  template <std::size_t... I>
76  {
77  label_t l = aut_->label_of(tr);
78  int i0 = get_size_tape<0>(l);
79  d = {(d[I] + i0 - get_size_tape<I + 1>(l))...};
80  }
81 
83  {
84  add_delay(d, tr, delay_index_t{});
85  }
86 
87  // Depth-first search
89  {
90  v_[src] = VISITING;
91  for (auto tr : all_out(aut_, src))
92  {
93  state_t dst = aut_->dst_of(tr);
94  auto visited = v_[dst];
95  if (visited == NOT_VISITED)
96  {
97  p_[dst] = tr;
98  if (!has_bounded_lag(dst))
99  return false;
100  }
101  else if (visited == VISITING)
102  {
103  // Cycle, compute the cycle's delay
104  delay_t d = {0};
105  add_delay(d, tr);
106  if (src != dst)
107  {
108  transition_t t = p_[src];
109  // Go back through the transitions we followed until we
110  // loop
111  while (aut_->src_of(t) != dst)
112  {
113  add_delay(d, t);
114  t = p_[aut_->src_of(t)];
115  }
116  add_delay(d, t);
117  }
118  if (d != delay_t{0})
119  return false;
120  }
121  }
122  v_[src] = VISITED;
123  return true;
124  }
125 
127  {
128  return has_bounded_lag(aut_->pre());
129  }
130 
131  private:
135  };
136  }
137 
138 
139  /*------------------.
140  | has_bounded_lag. |
141  `------------------*/
142 
147  template <Automaton Aut>
148  bool has_bounded_lag(const Aut& aut)
149  {
151  return blc.has_bounded_lag();
152  }
153 
154  namespace dyn
155  {
156  namespace detail
157  {
159  template <Automaton Aut>
160  bool has_bounded_lag(const automaton& aut)
161  {
162  return has_bounded_lag(aut->as<Aut>());
163  }
164  }
165  }
166 
167 }
auto all_out(const Aut &aut, state_t_of< Aut > s)
Indexes of transitions leaving state s.
Definition: automaton.hh:37
Container::value_type back(const Container &container)
The last member of this Container.
Definition: algorithm.hh:27
static constexpr size_t number_of_tapes
std::array< int, number_of_tapes-1 > delay_t
The delay associated with each state.
Definition: a-star.hh:8
std::vector< visit_state > visited_t
bool has_bounded_lag(const automaton &aut)
Bridge.
void add_delay(delay_t &d, transition_t tr)
typename detail::labelset_t_of_impl< base_t< ValueSet >>::type labelset_t_of
Definition: traits.hh:55
typename detail::state_t_of_impl< base_t< ValueSet >>::type state_t_of
Definition: traits.hh:56
std::vector< transition_t > parent_state_t
typename labelset_t::value_t label_t
bounded_lag_checker(const automaton_t &aut)
std::shared_ptr< detail::automaton_base > automaton
Definition: automaton.hh:69
typename detail::transition_t_of_impl< base_t< ValueSet >>::type transition_t_of
Definition: traits.hh:57
typename detail::context_t_of_impl< base_t< ValueSet >>::type context_t_of
Definition: traits.hh:53
labelset_t_of< automaton_t > labelset_t
bool has_bounded_lag(const Aut &aut)
Whether a transducer has a bounded lag.
void add_delay(delay_t &d, transition_t tr, seq< I... >)
state_t_of< automaton_t > state_t
size_t size(const ExpSet &rs, const typename ExpSet::value_t &r)
transition_t_of< automaton_t > transition_t