Vcsn  2.2
Be Rational
has-twins-property.hh
Go to the documentation of this file.
1 #pragma once
2 
3 #include <stack>
4 
5 #include <vcsn/algos/accessible.hh> // vcsn::trim
6 #include <vcsn/algos/is-ambiguous.hh> // is_cycle_ambiguous
7 #include <vcsn/algos/conjunction.hh> // conjunction
8 #include <vcsn/algos/scc.hh>
9 #include <vcsn/dyn/automaton.hh>
10 #include <vcsn/dyn/fwd.hh>
12 #include <vcsn/misc/unordered_map.hh> // vcsn::has
13 
14 namespace vcsn
15 {
16 
17  /*-----------------.
18  | cycle_identity. |
19  `-----------------*/
20 
21  namespace detail
22  {
30  template <Automaton Aut>
32  {
33  public:
38 
41  bool check(const component_t& component, const Aut& aut)
42  {
43  // FIXME: check ordered_map, or even polynomial of state.
44  std::unordered_map<state_t, weight_t> wm;
45  // Double-tape weightset.
46  const auto& ws = *aut->weightset();
47  // Single-tape weightset.
48  auto ws1 = ws.template set<0>();
49  auto s0 = *component.begin();
50  std::stack<state_t> todo;
51  todo.push(s0);
52  wm[s0] = ws.one();
53  while (!todo.empty())
54  {
55  auto s = todo.top();
56  todo.pop();
57 
58  for (auto t : all_out(aut, s))
59  {
60  auto dst = aut->dst_of(t);
61  if (has(component, dst))
62  {
63  auto w = ws.mul(wm[s], aut->weight_of(t));
64  if (!has(wm, dst))
65  {
66  todo.push(dst);
67  wm.emplace(dst, w);
68  }
69  else
70  {
71  auto w2 = ws.mul(wm[dst], w);
72  // FIXME: return the counter example?
73  if (!ws1.equal(std::get<0>(w2), std::get<1>(w2)))
74  return false;
75  }
76  }
77  }
78  }
79  return true;
80  }
81  };
82  }
83 
85  template <Automaton Aut>
87  const Aut& aut)
88  {
90  return ci.check(c, aut);
91  }
92 
93 
94  /*---------------------.
95  | has_twins_property. |
96  `---------------------*/
97 
101  template <Automaton AutIn, Automaton AutOut>
102  void create_states_and_trans_(const AutIn& aut,
103  AutOut& naut1, AutOut& naut2)
104  {
105  using state_t = state_t_of<AutIn>;
106  std::unordered_map<state_t, state_t_of<AutOut>> ms;
107 
108  ms[aut->pre()] = naut1->pre();
109  ms[aut->post()] = naut1->post();
110  for (auto s : aut->states())
111  {
112  ms[s] = naut1->new_state();
113  naut2->new_state();
114  }
115 
116  const auto& ws = *aut->weightset();
117  for (auto t : all_transitions(aut))
118  {
119  auto src = aut->src_of(t);
120  auto dst = aut->dst_of(t);
121  auto w = aut->weight_of(t);
122  auto l = aut->label_of(t);
123  auto nw1 = std::make_tuple(w, ws.one());
124  auto nw2 = std::make_tuple(ws.one(), w);
125  naut1->new_transition(ms[src], ms[dst], l, nw1);
126  naut2->new_transition(ms[src], ms[dst], l, nw2);
127  }
128  }
129 
131  template <Automaton Aut>
132  bool has_twins_property(const Aut& aut)
133  {
135  "has_twins_property: requires a cycle-unambiguous automaton");
136 
137  // Create new weightset lat<ws, ws> from weightset ws of aut.
138  auto ws = *aut->weightset();
139  auto nt = std::make_tuple(ws, ws);
141 
142  auto nctx = make_context(*aut->labelset(), nws);
143  auto naut1 = make_mutable_automaton(nctx);
144  auto naut2 = make_mutable_automaton(nctx);
145 
146  auto trim = ::vcsn::trim(aut);
147  create_states_and_trans_(trim, naut1, naut2);
148 
149  auto a = conjunction(naut1, naut2);
150 
151  // Find all components of automate a.
153 
154  // Check unique weight of two states on each component.
155  for (const auto& c : cs)
156  if (!cycle_identity(c, a))
157  return false;
158 
159  return true;
160  }
161 
162  namespace dyn
163  {
164  namespace detail
165  {
167  template <Automaton Aut>
168  bool has_twins_property(const automaton& aut)
169  {
170  const auto& a = aut->as<Aut>();
172  }
173  }
174  }
175 }
auto all_out(const Aut &aut, state_t_of< Aut > s)
Indexes of transitions leaving state s.
Definition: automaton.hh:37
filter_automaton< Aut > trim(const Aut &a)
Useful part of an automaton.
Definition: accessible.hh:150
auto conjunction(const Auts &...as) -> tuple_automaton< decltype(meet_automata(as...)), Auts... >
Build the (accessible part of the) conjunction.
Definition: conjunction.hh:448
Whether all the paths between any two states have the same weight (i.e., for all s0, s1, any two paths p0, p1 between s0 and s1 have the same weight w_{s0,s1}).
Definition: a-star.hh:8
void require(Bool b, Args &&...args)
If b is not verified, raise an error with args as message.
Definition: raise.hh:78
bool is_cycle_ambiguous(const Aut &aut)
Whether aut is cycle-ambiguous.
bool has_twins_property(const automaton &aut)
Bridge.
detail::component_t< Aut > component_t
bool check(const component_t &component, const Aut &aut)
By DFS starting in s0, check that all the states are reached with a single weight.
bool has_twins_property(const Aut &aut)
Whether aut has the twins property.
Provide a variadic mul on top of a binary mul(), and one().
Definition: fwd.hh:46
void create_states_and_trans_(const AutIn &aut, AutOut &naut1, AutOut &naut2)
Create states and the transitions two new automata naut1 and naut2 with weight of transition <(w...
typename detail::weight_t_of_impl< base_t< ValueSet >>::type weight_t_of
Definition: traits.hh:58
typename detail::state_t_of_impl< base_t< ValueSet >>::type state_t_of
Definition: traits.hh:56
bool cycle_identity(const detail::component_t< Aut > &c, const Aut &aut)
Check the weight of two states on this component is unique.
filter_automaton< scc_automaton< Aut > > component(const scc_automaton< Aut > &aut, unsigned num)
An SCC as a subautomaton.
Definition: scc.hh:753
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
ATTRIBUTE_PURE bool has(const boost::container::flat_set< Key, Compare, Allocator > &s, const Key &e)
Whether e is member of s.
Definition: setalpha.hh:25
mutable_automaton< Context > make_mutable_automaton(const Context &ctx)
std::unordered_set< state_t_of< Aut >> component_t
A strongly-connected component: set of states.
Definition: scc.hh:41
auto all_transitions(const Aut &aut)
All the transition indexes between all states (including pre and post).
Definition: automaton.hh:184
const detail::components_t< Aut > strong_components(const Aut &aut, Tag={})
Find all strongly connected components of aut.
Definition: scc.hh:540
Ctx make_context(const std::string &name)
Definition: make-context.hh:21