30 template <
typename Aut>
44 std::unordered_map<state_t, weight_t> wm;
46 const auto& ws = *aut->weightset();
48 auto ws1 = ws.template set<0>();
49 auto s0 = *component.begin();
50 std::stack<state_t> todo;
58 for (
auto t : aut->all_out(s))
60 auto dst = aut->dst_of(t);
61 if (
has(component, dst))
63 auto w = ws.mul(wm[s], aut->weight_of(t));
71 auto w2 = ws.mul(wm[dst], w);
73 if (!ws1.equal(std::get<0>(w2), std::get<1>(w2)))
85 template <
typename Aut>
90 return ci.
check(c, aut);
101 template <
typename InAut,
typename OutAut>
103 OutAut& naut1, OutAut& naut2)
106 std::unordered_map<state_t, state_t> ms;
108 ms[aut->pre()] = naut1->pre();
109 ms[aut->post()] = naut1->post();
110 for (
auto s : aut->states())
112 ms[s] = naut1->new_state();
116 const auto& ws = *aut->weightset();
117 for (
auto t : aut->all_transitions())
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);
131 template <
typename Aut>
135 "has_twins_property: requires a cycle-unambiguous automaton");
138 auto ws = *aut->weightset();
139 auto nt = std::make_tuple(ws, ws);
155 for (
const auto& c : cs)
167 template <
typename Aut>
170 const auto& a = aut->as<Aut>();
filter_automaton< Aut > trim(const Aut &a)
Useful part of an automaton.
bool has_twins_property(const automaton &aut)
Bridge.
typename detail::state_t_of_impl< base_t< ValueSet >>::type state_t_of
const detail::components_t< Aut > strong_components(const Aut &aut, scc_algo_t algo=scc_algo_t::tarjan_iterative)
Find all strongly connected components of aut.
bool has_twins_property(const Aut &aut)
Whether aut has the twins property.
filter_automaton< scc_automaton< Aut > > component(const scc_automaton< Aut > &aut, unsigned num)
An SCC as a subautomaton.
transition_t_of< Aut > transition_t
state_t_of< Aut > state_t
weight_t_of< Aut > weight_t
mutable_automaton< Context > make_mutable_automaton(const Context &ctx)
bool cycle_identity(const detail::component_t< Aut > &c, const Aut &aut)
Check the weight of two states on this component is unique.
Provide a variadic mul on top of a binary mul(), and one().
detail::component_t< Aut > component_t
std::shared_ptr< detail::automaton_base > automaton
auto conjunction(const Auts &...as) -> tuple_automaton< decltype(meet_automata(as...)), Auts...>
Build the (accessible part of the) conjunction.
void require(bool b, Args &&...args)
If b is not verified, raise an error with args as message.
typename detail::transition_t_of_impl< base_t< ValueSet >>::type transition_t_of
void create_states_and_trans_(const InAut &aut, OutAut &naut1, OutAut &naut2)
Create states and the transitions two new automata naut1 and naut2 with weight of transition <(w...
std::unordered_set< state_t_of< Aut >> component_t
A strongly-connected component: set of states.
Ctx make_context(const std::string &name)
bool is_cycle_ambiguous(const Aut &aut)
Whether aut is cycle-ambiguous.
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}).
ATTRIBUTE_PURE bool has(const std::deque< T, Allocator > &s, const T &e)
Whether e is member of s.
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.
typename detail::weight_t_of_impl< base_t< ValueSet >>::type weight_t_of