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>();
Ctx make_context(const std::string &name)
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...
state_t_of< Aut > state_t
const detail::components_t< Aut > strong_components(const Aut &aut, Tag={})
Find all strongly connected components of aut.
void require(Bool b, Args &&...args)
If b is not verified, raise an error with args as message.
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}).
auto conjunction(const Auts &...as) -> tuple_automaton< decltype(meet_automata(as...)), Auts...>
Build the (accessible part of the) conjunction.
detail::component_t< Aut > component_t
bool cycle_identity(const detail::component_t< Aut > &c, const Aut &aut)
Check the weight of two states on this component is unique.
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.
filter_automaton< Aut > trim(const Aut &a)
Useful part of an automaton.
transition_t_of< Aut > transition_t
std::unordered_set< state_t_of< Aut >> component_t
A strongly-connected component: set of states.
mutable_automaton< Context > make_mutable_automaton(const Context &ctx)
bool has_twins_property(const automaton &aut)
Bridge.
typename detail::transition_t_of_impl< base_t< ValueSet >>::type transition_t_of
auto all_transitions(const Aut &aut)
All the transition indexes between all states (including pre and post).
Provide a variadic mul on top of a binary mul(), and one().
ATTRIBUTE_PURE bool has(const boost::container::flat_set< Key, Compare, Allocator > &s, const Key &e)
Whether e is member of s.
bool is_cycle_ambiguous(const Aut &aut)
Whether aut is cycle-ambiguous.
typename detail::state_t_of_impl< base_t< ValueSet >>::type state_t_of
filter_automaton< scc_automaton< Aut > > component(const scc_automaton< Aut > &aut, unsigned num)
An SCC as a subautomaton.
weight_t_of< Aut > weight_t
typename detail::weight_t_of_impl< base_t< ValueSet >>::type weight_t_of
auto all_out(const Aut &aut, state_t_of< Aut > s)
Indexes of transitions leaving state s.
std::shared_ptr< detail::automaton_base > automaton