Awali
Another Weighted Automata library
has_twins_property.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_HAS_TWINS_PROPERTY_HH
18 # define AWALI_ALGOS_HAS_TWINS_PROPERTY_HH
19 
20 # include <stack>
21 # include <vector>
22 # include <unordered_set>
23 # include <unordered_map>
24 
30 
31 namespace awali { namespace sttc {
32 
33  /*----------.
34  | reverse |
35  `----------*/
36 
38  template <typename Aut>
39  Aut&
40  inverse_here(Aut& aut)
41  {
42  const auto& ws = *aut->weightset();
43  for (auto t : aut->all_transitions())
44  aut->set_weight(t, ws.rdiv(ws.one(), aut->weight_of(t)));
45  return aut;
46  }
47 
48  template <typename Aut>
49  auto
50  inverse(const Aut& aut)
51  -> decltype(::sttc::copy(aut))
52  {
53  auto res = copy(aut);
54  return inverse_here(res);
55  }
56 
57 
58  /*--------------------.
59  | reverse_postorder. |
60  `--------------------*/
61 
62  namespace internal
63  {
66  template <typename Aut>
68  {
69  public:
70 
71  reverse_postorder_impl(const Aut& aut)
72  {
73  for (auto s : aut->all_states())
74  if (!has(marked_, s))
75  dfs(s, aut);
76  }
77 
78  std::stack<state_t>& reverse_post()
79  {
80  return rvp_;
81  }
82 
83  private:
84  void dfs(state_t s, const Aut& aut)
85  {
86  marked_.emplace(s);
87  for (auto t : aut->out(s))
88  {
89  auto dst = aut->dst_of(t);
90  if (!has(marked_, dst))
91  dfs(dst, aut);
92  }
93  rvp_.push(s);
94  }
95  std::stack<state_t> rvp_;
96  std::unordered_set<state_t> marked_;
97  std::stack<state_t> todo_;
98  };
99 
100  }
101 
103  template <typename Aut>
104  std::stack<state_t>
105  reverse_postorder(const Aut& aut)
106  {
108  return dv.reverse_post();
109  }
110 
111  /*---------------.
112  | scc_kosaraju. |
113  `---------------*/
114 
115  namespace internal
116  {
119  template <typename Aut>
121  {
122  public:
123  using component_t = std::unordered_set<state_t>;
124  using components_t = std::vector<component_t>;
125 
126  scc_kosaraju(const Aut& aut)
127  {
128  auto trans = sttc::transpose(aut);
129  auto todo = reverse_postorder(trans);
130  while (!todo.empty())
131  {
132  auto s = todo.top();
133  todo.pop();
134  if (!has(marked_, s))
135  {
136  dfs(s, aut);
137  ++num_;
138  }
139  }
140  }
141 
143  {
144  return components_;
145  }
146 
147  private:
148  void dfs(state_t s, const Aut& aut)
149  {
150  marked_.emplace(s);
151  if (num_ == components_.size())
152  components_.emplace_back(component_t{s});
153  else
154  components_[num_].emplace(s);
155 
156  for (auto t : aut->out(s))
157  {
158  auto dst = aut->dst_of(t);
159  if (!has(marked_, dst))
160  dfs(dst, aut);
161  }
162  }
163 
165  int num_ = 0;
166  components_t components_;
167  std::unordered_set<state_t> marked_;
168  };
169 
170  }
171 
173  template <typename Aut>
174  const std::vector<std::unordered_set<state_t>>
175  components(const Aut& aut)
176  {
178  return scc.components();
179  }
180 
181 
182  /*-----------------.
183  | cycle_identity. |
184  `-----------------*/
185 
186  namespace internal
187  {
190  template <typename Aut>
192  {
193  public:
195  using component_t = std::unordered_set<state_t> ;
196 
198 
199  // Calcule the weight with depth first search by weight
200  // and compare the weight of two state is unique.
201  bool check(const component_t& component, const Aut& aut)
202  {
203  std::unordered_map<state_t, weight_t> wm;
204  const auto& ws = *aut->weightset();
205  auto s0 = *component.begin();
206  wm[s0] = ws.one();
207 
208  for (auto t : transitions_by_dfs_(component, aut))
209  {
210  auto src = aut->src_of(t);
211  auto dst = aut->dst_of(t);
212  if (!has(wm, dst))
213  wm.emplace(dst, ws.mul(wm[src], aut->weight_of(t)));
214  if (!ws.equals(wm[dst], ws.mul(wm[src], aut->weight_of(t))))
215  return false;
216  }
217  return true;
218  }
219 
220  private:
221  using transitions_t = std::vector<transition_t>;
223  transitions_t
224  transitions_by_dfs_(const component_t& component,
225  const Aut& aut)
226  {
227  transitions_t res;
228  std::set<transition_t> marked;
229  std::stack<transition_t> todo;
230 
231  auto s0 = *component.begin();
232  for (auto t : aut->out(s0))
233  {
234  if (has(component, aut->dst_of(t)))
235  {
236  todo.push(t);
237  marked.emplace(t);
238  }
239  }
240 
241  while (!todo.empty())
242  {
243  auto e = todo.top();
244  todo.pop();
245  res.emplace_back(e);
246 
247  for (auto f : aut->out(aut->dst_of(e)))
248  if (has(component, aut->dst_of(f))
249  && !has(marked, f))
250  {
251  todo.push(f);
252  marked.emplace(f);
253  }
254  }
255  return res;
256  }
257  };
258  }
259 
261  template <typename Aut>
262  bool cycle_identity(const std::unordered_set<state_t>& c,
263  const Aut& aut)
264  {
266  return ci.check(c, aut);
267  }
268 
269 
270  /*---------------------.
271  | has_twins_property. |
272  `---------------------*/
273 
275  template <typename Aut>
276  bool has_twins_property(const Aut& aut)
277  {
278  // TODO: Check cycle-unambiguous.
279  auto trim = sttc::trim(aut);
280  auto inv = inverse(trim);
281  auto a = sttc::product(inv, trim);
282 
283  // Find all components of automate a.
284  auto cs = components(a);
285 
286  // Check unique weight of two states on each component.
287  for (auto c : cs)
288  if (!cycle_identity(c, a))
289  return false;
290 
291  return true;
292  }
293 
294 }}//end of ns awali::stc
295 #endif // !AWALI_ALGOS_HAS_TWINS_PROPERTY_HH
The semiring of complex numbers.
Definition: c.hh:44
Whether the weight of beetween two states on component, it is always unique.
Definition: has_twins_property.hh:192
bool check(const component_t &component, const Aut &aut)
Definition: has_twins_property.hh:201
weight_t_of< Aut > weight_t
Definition: has_twins_property.hh:194
std::unordered_set< state_t > component_t
Definition: has_twins_property.hh:195
cycle_identity_impl()
Definition: has_twins_property.hh:197
Get all vertexs in reverse postorder by using depth first search.
Definition: has_twins_property.hh:68
std::stack< state_t > & reverse_post()
Definition: has_twins_property.hh:78
reverse_postorder_impl(const Aut &aut)
Definition: has_twins_property.hh:71
Use Kosajaju algorithm for finding all of strongly connected components.
Definition: has_twins_property.hh:121
scc_kosaraju(const Aut &aut)
Definition: has_twins_property.hh:126
const components_t components()
Definition: has_twins_property.hh:142
std::vector< component_t > components_t
Definition: has_twins_property.hh:124
std::unordered_set< state_t > component_t
Definition: has_twins_property.hh:123
bool has(const std::map< Key, Value, Compare, Alloc > &s, const Key &e)
Definition: map.hh:53
const std::vector< std::unordered_set< state_t > > components(const Aut &aut)
Find all strongly connected components of aut.
Definition: has_twins_property.hh:175
auto inverse(const Aut &aut) -> decltype(::sttc::copy(aut))
Definition: has_twins_property.hh:50
auto product(const Lhs &lhs, const Rhs &rhs, bool keep_history=true) -> decltype(join_automata(lhs, rhs))
Definition: product.hh:394
typename internal::weight_t_of_impl< internal::base_t< ValueSet > >::type weight_t_of
Helper to retrieve the type of the weights of a value set.
Definition: traits.hh:81
Aut::element_type::automaton_nocv_t trim(const Aut &aut, bool keep_history=true)
Trim subautomaton.
Definition: accessible.hh:278
AutOut transpose(Aut &aut, bool keep_history=true)
Definition: transpose.hh:79
AutOut copy(const AutIn &input, Pred keep_state, bool keep_history=true, bool transpose=false)
A copy of input keeping only its states that are accepted by keep_state.
Definition: copy.hh:189
bool cycle_identity(const std::unordered_set< state_t > &c, const Aut &aut)
Check the weight of two states on this component is unique.
Definition: has_twins_property.hh:262
bool has_twins_property(const Aut &aut)
Whether aut has the twins property.
Definition: has_twins_property.hh:276
Aut & inverse_here(Aut &aut)
Inverse the weight of all edges of aut.
Definition: has_twins_property.hh:40
std::stack< state_t > reverse_postorder(const Aut &aut)
Get all vertices in reverse postorder.
Definition: has_twins_property.hh:105
Main namespace of Awali.
Definition: ato.hh:22
unsigned state_t
Definition: types.hh:21