7 #include <boost/heap/binomial_heap.hpp>
8 #include <boost/optional.hpp>
28 template <Automaton Aut>
48 using profile_t = std::tuple<state_t, word_t, weight_t>;
54 if (labelset_t::less(std::get<1>(l), std::get<1>(r)))
56 else if (labelset_t::less(std::get<1>(r), std::get<1>(l)))
59 return std::get<0>(l) < std::get<0>(r);
74 boost::optional<unsigned> len)
77 num = !len ? 1 : std::numeric_limits<unsigned>::max();
79 len = std::numeric_limits<unsigned>::max();
83 if (*num == 1 && *len == std::numeric_limits<unsigned>::max())
87 auto rhs =
aut_->label_of(t);
88 return (
aut_->labelset()->is_special(rhs))
110 template <
typename LabelSet = labelset_t_of<context_t>>
112 -> std::enable_if_t<LabelSet::is_free(), polynomial_t>
116 if (len != std::numeric_limits<unsigned>::max())
119 using queue_t = std::deque<profile_t>;
125 !queue.empty() && i < len && output.size() < num;
129 for (
const auto& sm: queue)
132 std::tie(s, l, w) = sm;
135 auto dst =
aut_->dst_of(t);
136 auto nw =
ws_.mul(w,
aut_->weight_of(t));
138 q2.emplace_back(dst, l, std::move(nw));
139 else if (dst ==
aut_->post())
140 ps_.add_here(output, l, std::move(nw));
151 for (
const auto& m: output)
153 ps_.add_here(res, m);
164 template <
typename LabelSet = labelset_t_of<context_t>>
166 -> std::enable_if_t<!LabelSet::is_free(), polynomial_t>
172 boost::heap::compare<profile_less>>;
174 auto queue = queue_t{};
175 queue.emplace(
aut_->pre(),
ls_.one(),
ws_.one());
179 while (!queue.empty())
182 std::tie(s, l, w) = queue.top();
194 while (!queue.empty()
195 && std::get<0>(queue.top()) == s
196 &&
ls_.equal(std::get<1>(queue.top()), l))
198 w =
ws_.add(w, std::get<2>(queue.top()));
204 auto dst =
aut_->dst_of(t);
205 auto nw =
ws_.mul(w,
aut_->weight_of(t));
207 queue.emplace(dst, l, std::move(nw));
208 else if (dst ==
aut_->post())
209 ps_.add_here(res, l, std::move(nw));
212 auto nl =
ls_.mul(l,
aut_->label_of(t));
214 if (
ls_.size(nl) <= len)
215 queue.emplace(dst, std::move(nl), std::move(nw));
223 || (num == res.size()
224 && !
ls_.equal(std::get<1>(queue.top()), l)))
233 template <
typename Queue>
236 const char* sep =
"";
237 for (
auto i = q.ordered_begin(), end = q.ordered_end();
242 aut_->print_state_name(std::get<0>(*i),
os) <<
":<";
243 ws_.print(std::get<2>(*i),
os) <<
'>';
244 ls_.print(std::get<1>(*i),
os);
265 template <Automaton Aut>
268 boost::optional<unsigned> num = {},
269 boost::optional<unsigned> len = {})
271 auto enumerater = detail::enumerater<Aut>{aut};
272 return enumerater(num, len);
280 template <Automaton Aut>
281 typename detail::enumerater<Aut>::polynomial_t
284 return shortest(aut, boost::none, len);
293 template <Automaton Aut,
typename Num,
typename Len>
296 boost::optional<unsigned> num,
297 boost::optional<unsigned> len)
299 const auto& a = aut->as<Aut>();
auto all_out(const Aut &aut, state_t_of< Aut > s)
Indexes of transitions leaving state s.
detail::enumerater< Aut >::polynomial_t shortest(const Aut &aut, boost::optional< unsigned > num={}, boost::optional< unsigned > len={})
The approximated behavior of an automaton.
std::shared_ptr< const detail::polynomial_base > polynomial
typename detail::weightset_t_of_impl< base_t< ValueSet >>::type weightset_t_of
polynomial make_polynomial(const PolynomialSet &ps, const typename PolynomialSet::value_t &p)
const polynomialset_t ps_
Shorthand to the polynomialset of words.
typename polynomialset_t::value_t polynomial_t
std::ostringstream os
The output stream: the corresponding C++ snippet to compile.
state_t_of< automaton_t > state_t
auto path_monomial(const Aut &aut, const std::vector< transition_t_of< Aut >> &path, state_t_of< Aut > src=Aut::element_type::pre(), state_t_of< Aut > dst=Aut::element_type::post()) -> boost::optional< typename detail::word_polynomialset_t< context_t_of< Aut >>::monomial_t >
Given a path (typically computed by lightest_path), the corresponding monomial (label, weight).
typename detail::labelset_t_of_impl< base_t< ValueSet >>::type labelset_t_of
void show_heap_(const Queue &q, std::ostream &os=std::cerr) const
Show the heap, for debugging.
Provide a variadic mul on top of a binary mul(), and one().
typename detail::weight_t_of_impl< base_t< ValueSet >>::type weight_t_of
detail::enumerater< Aut >::polynomial_t enumerate(const Aut &aut, unsigned len)
The approximated behavior of an automaton.
typename detail::state_t_of_impl< base_t< ValueSet >>::type state_t_of
const weightset_t & ws_
Shorthand to the weightset.
const labelset_t & ls_
Shorthand to the (word) labelset.
enumerater(const automaton_t &aut)
Prepare to compute an approximation of the behavior.
bool operator()(const profile_t &r, const profile_t &l) const
Whether l < r (as this is a max heap).
std::shared_ptr< detail::automaton_base > automaton
typename detail::transition_t_of_impl< base_t< ValueSet >>::type transition_t_of
auto make_dijkstra_impl(const Aut &aut, const ValueSet &vs, Mul mul)
context_t_of< Aut > context_t
typename detail::context_t_of_impl< base_t< ValueSet >>::type context_t_of
auto make_word_polynomialset(const Ctx &ctx) -> word_polynomialset_t< Ctx >
The polynomialset of words of a labelset (not necessarily on words itself).
auto shortest_(unsigned num, unsigned len) -> std::enable_if_t<!LabelSet::is_free(), polynomial_t >
Case of non free labelsets (e.g., law, lan x lan).
Compute the shortest words accepted by an automaton.
polynomial_t operator()(boost::optional< unsigned > num, boost::optional< unsigned > len)
The approximated behavior of the automaton.
labelset_t_of< polynomialset_t > labelset_t
Wordset.
auto shortest_(unsigned num, unsigned len) -> std::enable_if_t< LabelSet::is_free(), polynomial_t >
Case of free labelsets (e.g., lal or lal x lal).
word_t_of< automaton_t > word_t
typename labelset_t_of< base_t< ValueSet >>::word_t word_t_of
automaton_t aut_
The automaton whose behavior to approximate.
polynomial shortest(const automaton &aut, boost::optional< unsigned > num, boost::optional< unsigned > len)
Bridge.
value_t mul(const Ts &...ts) const
A variadic multiplication.
std::tuple< state_t, word_t, weight_t > profile_t
Used in the case of non-free labelsets.
weight_t_of< automaton_t > weight_t
weightset_t_of< automaton_t > weightset_t