Vcsn  2.3
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 }
filter_automaton< Aut > trim(const Aut &a)
Useful part of an automaton.
Definition: accessible.hh:150
std::unordered_set< state_t_of< Aut >> component_t
A strongly-connected component: set of states.
Definition: scc.hh:41
typename detail::weight_t_of_impl< base_t< ValueSet >>::type weight_t_of
Definition: traits.hh:66
Ctx make_context(const std::string &name)
Build a context from its name.
Definition: make-context.hh:22
typename detail::transition_t_of_impl< base_t< ValueSet >>::type transition_t_of
Definition: traits.hh:65
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}).
void require(Bool b, Args &&...args)
If b is not verified, raise an error with args as message.
Definition: raise.hh:91
auto all_transitions(const Aut &aut)
All the transition indexes between all states (including pre and post).
Definition: automaton.hh:192
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
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
typename detail::state_t_of_impl< base_t< ValueSet >>::type state_t_of
Definition: traits.hh:64
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...
Definition: a-star.hh:8
A dyn automaton.
Definition: automaton.hh:17
bool has_twins_property(const automaton &aut)
Bridge.
const detail::components_t< Aut > strong_components(const Aut &aut, Tag={})
Find all strongly connected components of aut.
Definition: scc.hh:540
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.
auto conjunction(const Aut &aut, to exp) -> fresh_automaton_t_of< Aut >
Repeated conjunction of a automaton.
Definition: conjunction.hh:947
bool is_cycle_ambiguous(const Aut &aut)
Whether aut is cycle-ambiguous.
auto & as()
Extract wrapped typed automaton.
Definition: automaton.hh:37
detail::component_t< Aut > component_t
Provide a variadic mul on top of a binary mul(), and one().
Definition: fwd.hh:46
auto all_out(const Aut &aut, state_t_of< Aut > s)
Indexes of transitions leaving state s.
Definition: automaton.hh:45
bool has_twins_property(const Aut &aut)
Whether aut has the twins property.
mutable_automaton< Context > make_mutable_automaton(const Context &ctx)