7 #include <boost/heap/binomial_heap.hpp>
8 #include <boost/optional.hpp>
37 template <Automaton Aut>
57 using profile_t = std::tuple<state_t, word_t, weight_t>;
72 if (weightset_t::less(std::get<2>(l), std::get<2>(r)))
74 else if (weightset_t::less(std::get<2>(r), std::get<2>(l)))
76 else if (labelset_t::less(std::get<1>(l), std::get<1>(r)))
78 else if (labelset_t::less(std::get<1>(r), std::get<1>(l)))
80 else if (std::get<0>(r) == automaton_t::element_type::post())
82 else if (std::get<0>(l) == automaton_t::element_type::post())
85 return std::get<0>(l) < std::get<0>(r);
90 boost::heap::compare<profile_less>>;
104 "lightest(n > 1): requires automaton without lightening cycles");
112 queue.emplace(
aut_->pre(),
ls_.one(),
ws_.one());
116 while (!queue.empty() && num != res.size())
119 std::tie(s, l, w) = queue.top();
126 && std::get<0>(queue.top()) == s
127 &&
ls_.equal(std::get<1>(queue.top()), l))
129 while (!queue.empty()
130 && std::get<0>(queue.top()) == s
131 &&
ls_.equal(std::get<1>(queue.top()), l))
133 w =
ws_.add(w, std::get<2>(queue.top()));
136 queue.emplace(s, l, w);
140 if (s ==
aut_->post())
141 ps_.add_here(res, std::move(l), std::move(w));
145 auto dst =
aut_->dst_of(t);
146 auto nw =
ws_.mul(w,
aut_->weight_of(t));
147 if (
aut_->src_of(t) ==
aut_->pre() || dst ==
aut_->post())
148 queue.emplace(dst, l, std::move(nw));
151 auto nl =
ls_.mul(l,
aut_->label_of(t));
152 queue.emplace(dst, std::move(nl), std::move(nw));
163 const char* sep =
"";
164 for (
auto i = q.ordered_begin(), end = q.ordered_end();
169 aut_->print_state_name(std::get<0>(*i),
os) <<
":<";
170 ws_.print(std::get<2>(*i),
os);
172 ls_.print(std::get<1>(*i),
os);
189 template <Automaton Aut>
191 lightest(
const Aut& aut,
unsigned num = 1,
const std::string& algo =
"auto")
193 if (num != 1 || algo ==
"breadth-first")
213 template <Automaton Aut,
typename Num,
typename String>
217 const auto& a = aut->as<Aut>();
auto all_out(const Aut &aut, state_t_of< Aut > s)
Indexes of transitions leaving state s.
context_t_of< Aut > context_t
std::shared_ptr< const detail::polynomial_base > polynomial
boost::heap::binomial_heap< profile_t, boost::heap::compare< profile_less >> queue_t
polynomial lightest(const automaton &aut, unsigned num, const std::string &algo)
Bridge.
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)
void require(Bool b, Args &&...args)
If b is not verified, raise an error with args as message.
polynomial_t operator()(unsigned num)
The approximated behavior of the automaton.
std::ostringstream os
The output stream: the corresponding C++ snippet to compile.
word_t_of< automaton_t > word_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
weightset_t_of< automaton_t > weightset_t
Provide a variadic mul on top of a binary mul(), and one().
lightest_impl(const automaton_t &aut)
Prepare to compute an approximation of the behavior.
typename detail::weight_t_of_impl< base_t< ValueSet >>::type weight_t_of
state_t_of< automaton_t > state_t
typename detail::state_t_of_impl< base_t< ValueSet >>::type state_t_of
void show_heap_(const queue_t &q, std::ostream &os=std::cerr)
Show the heap, for debugging.
const polynomialset_t ps_
detail::word_polynomialset_t< context_t_of< Aut > >::value_t lightest(const Aut &aut, unsigned num=1, const std::string &algo="auto")
The approximated behavior of an automaton.
std::shared_ptr< detail::automaton_base > automaton
typename detail::context_t_of_impl< base_t< ValueSet >>::type context_t_of
labelset_t_of< polynomialset_t > labelset_t
Wordset.
weight_t_of< automaton_t > weight_t
auto make_word_polynomialset(const Ctx &ctx) -> word_polynomialset_t< Ctx >
The polynomialset of words of a labelset (not necessarily on words itself).
automaton_t aut_
The automaton whose behavior to approximate.
typename polynomialset_t::monomial_t monomial_t
The lightest algorithm computes the paths between pre and post with the smallest weight possible...
typename labelset_t_of< base_t< ValueSet >>::word_t word_t_of
polynomial_t lightest_(unsigned num)
std::enable_if_t< weightset_t_of< Aut >::has_lightening_weights(), bool > has_lightening_cycle(const Aut &aut)
std::vector< transition_t_of< Aut > > lightest_path(const Aut &aut, state_t_of< Aut > source, state_t_of< Aut > dest, a_star_tag)
std::tuple< state_t, word_t, weight_t > profile_t
typename polynomialset_t::value_t polynomial_t
bool operator()(const profile_t &r, const profile_t &l) const
Whether l < r (as this is a max heap).