From 7c0ce376c5bbf973c375463ae70f9be3f99458f4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 5 Aug 2014 11:57:33 +0200 Subject: [PATCH] nsa2tgba: Construct a tgba_digraph. * src/priv/accmap.hh (acc_mapper_consecutive_int): New class. * src/dstarparse/nsa2tgba.cc: Build a tgba_digraph, and simplify using acc_mapper_consecutive_int. --- src/dstarparse/nsa2tgba.cc | 72 ++++++++++---------------------------- src/priv/accmap.hh | 51 ++++++++++++++++++++------- 2 files changed, 57 insertions(+), 66 deletions(-) diff --git a/src/dstarparse/nsa2tgba.cc b/src/dstarparse/nsa2tgba.cc index 80ebdd678..03df2a1f8 100644 --- a/src/dstarparse/nsa2tgba.cc +++ b/src/dstarparse/nsa2tgba.cc @@ -22,7 +22,7 @@ #include "public.hh" #include "tgbaalgos/sccfilter.hh" #include "ltlenv/defaultenv.hh" -#include "tgba/tgbaexplicit.hh" +#include "priv/accmap.hh" namespace spot { @@ -61,8 +61,6 @@ namespace spot } }; - typedef std::pair degen_state; - struct build_state_hash { size_t @@ -100,13 +98,6 @@ namespace spot } - int label(const tgba_digraph* aut, state* s) - { - int label = aut->state_number(s); - s->destroy(); - return label; - } - SPOT_API tgba* nsa_to_tgba(const dstar_aut* nsa) { @@ -114,29 +105,12 @@ namespace spot tgba_digraph* a = nsa->aut; bdd_dict* dict = a->get_dict(); - tgba_explicit_number* res = new tgba_explicit_number(dict); + tgba_digraph* res = new tgba_digraph(dict); dict->register_all_variables_of(a, res); - // Create accpair_count acceptance sets for tge TGBA. - size_t npairs = nsa->accpair_count; - std::vector acc_b(npairs); - { - ltl::environment& envacc = ltl::default_environment::instance(); - std::vector acc_f(npairs); - for (unsigned n = 0; n < npairs; ++n) - { - std::ostringstream s; - s << n; - const ltl::formula* af = acc_f[n] = envacc.require(s.str()); - res->declare_acceptance_condition(af->clone()); - } - bdd allacc = bddfalse; - for (unsigned n = 0; n < npairs; ++n) - { - const ltl::formula* af = acc_f[n]; - allacc |= acc_b[n] = res->get_acceptance_condition(af); - } - } + // Create accpair_count acceptance sets for the output. + unsigned npairs = nsa->accpair_count; + acc_mapper_consecutive_int acc_b(res, npairs); // These maps make it possible to convert build_state to number // and vice-versa. @@ -144,9 +118,8 @@ namespace spot queue_t todo; - build_state s(label(a, a->get_init_state())); - - bs2num[s] = 0; + build_state s(a->get_init_state_number()); + bs2num[s] = res->new_state(); todo.push_back(s); while (!todo.empty()) @@ -155,25 +128,23 @@ namespace spot todo.pop_front(); int src = bs2num[s]; - for (auto i: a->succ(a->state_from_number(s.s))) + for (auto& t: a->out(s.s)) { - int dlabel = label(a, i->current_state()); - bitvect* pend = 0; bdd acc = bddfalse; if (s.pend) { pend = s.pend->clone(); - *pend |= nsa->accsets->at(2 * dlabel); // L - *pend -= nsa->accsets->at(2 * dlabel + 1); // U + *pend |= nsa->accsets->at(2 * t.dst); // L + *pend -= nsa->accsets->at(2 * t.dst + 1); // U for (size_t i = 0; i < npairs; ++i) if (!pend->get(i)) - acc |= acc_b[i]; + acc |= acc_b.lookup(i).second; } - build_state d(dlabel, pend); + build_state d(t.dst, pend); // Have we already seen this destination? int dest; auto dres = bs2num.emplace(d, 0); @@ -182,21 +153,18 @@ namespace spot dest = dres.first->second; delete d.pend; } - else + else // No, this is a new state { - dest = dres.first->second = bs2num.size() - 1; + dest = dres.first->second = res->new_state(); todo.push_back(d); } - state_explicit_number::transition* t = - res->create_transition(src, dest); - t->condition = i->current_condition(); - t->acceptance_conditions = acc; + res->new_transition(src, dest, t.cond, acc); // Jump to level ∅ if (s.pend == 0) { bitvect* pend = make_bitvect(npairs); - build_state d(label(a, i->current_state()), pend); + build_state d(t.dst, pend); // Have we already seen this destination? int dest; auto dres = bs2num.emplace(d, 0); @@ -205,14 +173,12 @@ namespace spot dest = dres.first->second; delete d.pend; } - else + else // No, this is a new state { - dest = dres.first->second = bs2num.size() - 1; + dest = dres.first->second = res->new_state(); todo.push_back(d); } - state_explicit_number::transition* t = - res->create_transition(src, dest); - t->condition = i->current_condition(); + res->new_transition(src, dest, t.cond); } } } diff --git a/src/priv/accmap.hh b/src/priv/accmap.hh index a8212f9ca..4e2a30f1f 100644 --- a/src/priv/accmap.hh +++ b/src/priv/accmap.hh @@ -93,19 +93,20 @@ namespace spot } }; - // The acceptance sets are named using count integers, but we do not - // assume the numbers are necessarily consecutive. - class acc_mapper_int: public acc_mapper_common + + // The acceptance sets are named using count consecutive integers. + class acc_mapper_consecutive_int: public acc_mapper_common { - std::vector usable_; - unsigned used_; + protected: + std::vector vec_; std::map map_; public: - acc_mapper_int(tgba_digraph *aut, - unsigned count, - ltl::environment& env = ltl::default_environment::instance()) - : acc_mapper_common(aut, env), usable_(count), used_(0) + acc_mapper_consecutive_int(tgba_digraph *aut, + unsigned count, + ltl::environment& env = + ltl::default_environment::instance()) + : acc_mapper_common(aut, env), vec_(count) { std::vector vmap(count); for (unsigned n = 0; n < count; ++n) @@ -121,26 +122,50 @@ namespace spot for (unsigned n = 0; n < count; ++n) { int v = vmap[n]; - usable_[n] = bdd_compose(neg_, bdd_nithvar(v), v); + vec_[n] = bdd_compose(neg_, bdd_nithvar(v), v); } commit(); } + std::pair lookup(unsigned n) + { + if (n < vec_.size()) + return std::make_pair(true, vec_[n]); + else + return std::make_pair(false, bddfalse); + } + }; + + // The acceptance sets are named using count integers, but we do not + // assume the numbers are necessarily consecutive. + class acc_mapper_int: public acc_mapper_consecutive_int + { + unsigned used_; + std::map map_; + + public: + acc_mapper_int(tgba_digraph *aut, + unsigned count, + ltl::environment& env = + ltl::default_environment::instance()) + : acc_mapper_consecutive_int(aut, count, env), used_(0) + { + } + std::pair lookup(unsigned n) { auto p = map_.find(n); if (p != map_.end()) return std::make_pair(true, p->second); - if (used_ < usable_.size()) + if (used_ < vec_.size()) { - bdd res = usable_[used_++]; + bdd res = vec_[used_++]; map_[n] = res; return std::make_pair(true, res); } return std::make_pair(false, bddfalse); } }; - } #endif // SPOT_PRIV_ACCCONV_HH