alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

nsa2tgba: Construct a tgba_digraph.

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2014-08-05 11:57:33 +02:00
parent ed94a35bea
commit 7c0ce376c5
2 changed files with 57 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

72
src/dstarparse/nsa2tgba.cc
View file

@ -22,7 +22,7 @@
#include "public.hh" #include "public.hh"
#include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/sccfilter.hh"
#include "ltlenv/defaultenv.hh" #include "ltlenv/defaultenv.hh"
#include "tgba/tgbaexplicit.hh" #include "priv/accmap.hh"
namespace spot namespace spot
{ {
@ -61,8 +61,6 @@ namespace spot
} }
}; };
typedef std::pair<const state*, build_state> degen_state;
struct build_state_hash struct build_state_hash
{ {
size_t 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 SPOT_API
tgba* nsa_to_tgba(const dstar_aut* nsa) tgba* nsa_to_tgba(const dstar_aut* nsa)
{ {
@ -114,29 +105,12 @@ namespace spot
tgba_digraph* a = nsa->aut; tgba_digraph* a = nsa->aut;
bdd_dict* dict = a->get_dict(); 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); dict->register_all_variables_of(a, res);
// Create accpair_count acceptance sets for tge TGBA. // Create accpair_count acceptance sets for the output.
size_t npairs = nsa->accpair_count; unsigned npairs = nsa->accpair_count;
std::vector<bdd> acc_b(npairs); acc_mapper_consecutive_int acc_b(res, npairs);
{
ltl::environment& envacc = ltl::default_environment::instance();
std::vector<const ltl::formula*> 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);
}
}
// These maps make it possible to convert build_state to number // These maps make it possible to convert build_state to number
// and vice-versa. // and vice-versa.
@ -144,9 +118,8 @@ namespace spot
queue_t todo; queue_t todo;
build_state s(label(a, a->get_init_state())); build_state s(a->get_init_state_number());
bs2num[s] = res->new_state();
bs2num[s] = 0;
todo.push_back(s); todo.push_back(s);
while (!todo.empty()) while (!todo.empty())
@ -155,25 +128,23 @@ namespace spot
todo.pop_front(); todo.pop_front();
int src = bs2num[s]; 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; bitvect* pend = 0;
bdd acc = bddfalse; bdd acc = bddfalse;
if (s.pend) if (s.pend)
{ {
pend = s.pend->clone(); pend = s.pend->clone();
*pend |= nsa->accsets->at(2 * dlabel); // L *pend |= nsa->accsets->at(2 * t.dst); // L
*pend -= nsa->accsets->at(2 * dlabel + 1); // U *pend -= nsa->accsets->at(2 * t.dst + 1); // U
for (size_t i = 0; i < npairs; ++i) for (size_t i = 0; i < npairs; ++i)
if (!pend->get(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? // Have we already seen this destination?
int dest; int dest;
auto dres = bs2num.emplace(d, 0); auto dres = bs2num.emplace(d, 0);
@ -182,21 +153,18 @@ namespace spot
dest = dres.first->second; dest = dres.first->second;
delete d.pend; 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); todo.push_back(d);
} }
state_explicit_number::transition* t = res->new_transition(src, dest, t.cond, acc);
res->create_transition(src, dest);
t->condition = i->current_condition();
t->acceptance_conditions = acc;
// Jump to level ∅ // Jump to level ∅
if (s.pend == 0) if (s.pend == 0)
{ {
bitvect* pend = make_bitvect(npairs); 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? // Have we already seen this destination?
int dest; int dest;
auto dres = bs2num.emplace(d, 0); auto dres = bs2num.emplace(d, 0);
@ -205,14 +173,12 @@ namespace spot
dest = dres.first->second; dest = dres.first->second;
delete d.pend; 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); todo.push_back(d);
} }
state_explicit_number::transition* t = res->new_transition(src, dest, t.cond);
res->create_transition(src, dest);
t->condition = i->current_condition();
} }
} }
} }

51
src/priv/accmap.hh
View file

@ -93,19 +93,20 @@ namespace spot
} }
}; };
// The acceptance sets are named using count integers, but we do not
// assume the numbers are necessarily consecutive. // The acceptance sets are named using count consecutive integers.
class acc_mapper_int: public acc_mapper_common class acc_mapper_consecutive_int: public acc_mapper_common
{ {
std::vector<bdd> usable_; protected:
unsigned used_; std::vector<bdd> vec_;
std::map<int, bdd> map_; std::map<int, bdd> map_;
public: public:
acc_mapper_int(tgba_digraph *aut, acc_mapper_consecutive_int(tgba_digraph *aut,
unsigned count, unsigned count,
ltl::environment& env = ltl::default_environment::instance()) ltl::environment& env =
: acc_mapper_common(aut, env), usable_(count), used_(0) ltl::default_environment::instance())
: acc_mapper_common(aut, env), vec_(count)
{ {
std::vector<int> vmap(count); std::vector<int> vmap(count);
for (unsigned n = 0; n < count; ++n) for (unsigned n = 0; n < count; ++n)
@ -121,26 +122,50 @@ namespace spot
for (unsigned n = 0; n < count; ++n) for (unsigned n = 0; n < count; ++n)
{ {
int v = vmap[n]; int v = vmap[n];
usable_[n] = bdd_compose(neg_, bdd_nithvar(v), v); vec_[n] = bdd_compose(neg_, bdd_nithvar(v), v);
} }
commit(); commit();
} }
std::pair<bool, bdd> 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<int, bdd> 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<bool, bdd> lookup(unsigned n) std::pair<bool, bdd> lookup(unsigned n)
{ {
auto p = map_.find(n); auto p = map_.find(n);
if (p != map_.end()) if (p != map_.end())
return std::make_pair(true, p->second); 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; map_[n] = res;
return std::make_pair(true, res); return std::make_pair(true, res);
} }
return std::make_pair(false, bddfalse); return std::make_pair(false, bddfalse);
} }
}; };
} }
#endif // SPOT_PRIV_ACCCONV_HH #endif // SPOT_PRIV_ACCCONV_HH