30 template <Automaton 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;
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 <Automaton Aut>
90 return ci.
check(c, aut);
101 template <Automaton AutIn, Automaton AutOut>
103 AutOut& naut1, AutOut& naut2)
106 std::unordered_map<state_t, state_t_of<AutOut>> 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();
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 <Automaton 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 <Automaton Aut>
170 const auto& a = aut->
as<Aut>();
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().
state_t_of< Aut > state_t
bool has_twins_property(const automaton &aut)
Bridge.
typename detail::transition_t_of_impl< base_t< ValueSet >>::type transition_t_of
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}).
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.
ATTRIBUTE_PURE bool has(const boost::container::flat_set< Key, Compare, Allocator > &s, const Key &e)
Whether e is member of s.
auto all_out(const Aut &aut, state_t_of< Aut > s)
Indexes of transitions leaving state s.
mutable_automaton< Context > make_mutable_automaton(const Context &ctx)
transition_t_of< Aut > transition_t
std::unordered_set< state_t_of< Aut >> component_t
A strongly-connected component: set of states.
const detail::components_t< Aut > strong_components(const Aut &aut, Tag={})
Find all strongly connected components of aut.
auto conjunction(const Auts &...as) -> tuple_automaton< decltype(meet_automata(as...)), Auts... >
Build the (accessible part of the) conjunction.
Ctx make_context(const std::string &name)
void require(Bool b, Args &&...args)
If b is not verified, raise an error with args as message.
bool is_cycle_ambiguous(const Aut &aut)
Whether aut is cycle-ambiguous.
bool has_twins_property(const Aut &aut)
Whether aut has the twins property.
filter_automaton< Aut > trim(const Aut &a)
Useful part of an automaton.
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::state_t_of_impl< base_t< ValueSet >>::type state_t_of
weight_t_of< Aut > weight_t
auto & as()
Extract wrapped typed automaton.
filter_automaton< scc_automaton< Aut > > component(const scc_automaton< Aut > &aut, unsigned num)
An SCC as a subautomaton.
typename detail::weight_t_of_impl< base_t< ValueSet >>::type weight_t_of
auto all_transitions(const Aut &aut)
All the transition indexes between all states (including pre and post).