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

dra2ba: Use tgba_digraph.

Browse source 
* src/dstarparse/dra2ba.cc: Use tgba_digraph instead of
tgba_explicit_number.
* src/tgbatest/dstar.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2014-08-05 16:33:37 +02:00
parent 9923cbaae0
commit f9d85d7d2e
2 changed files with 21 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/dstarparse/dra2ba.cc
View file

@ -19,7 +19,6 @@
#include "public.hh" #include "public.hh"
#include "tgba/tgbamask.hh" #include "tgba/tgbamask.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/scc.hh" #include "tgbaalgos/scc.hh"
#include "tgbaalgos/reachiter.hh" #include "tgbaalgos/reachiter.hh"
#include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/gtec/gtec.hh"
@ -231,7 +230,7 @@ namespace spot
const std::vector<bool>& realizable): const std::vector<bool>& realizable):
tgba_reachable_iterator_depth_first(a->aut), tgba_reachable_iterator_depth_first(a->aut),
in_(a), in_(a),
out_(new tgba_explicit_number(a->aut->get_dict())), out_(new tgba_digraph(a->aut->get_dict())),
final_(final), final_(final),
num_states_(a->aut->num_states()), num_states_(a->aut->num_states()),
sm_(sm), sm_(sm),
@ -246,9 +245,11 @@ namespace spot
out_); out_);
acc_ = bdd_ithvar(accvar); acc_ = bdd_ithvar(accvar);
out_->set_acceptance_conditions(acc_); out_->set_acceptance_conditions(acc_);
out_->new_states(num_states_ * (a->accpair_count + 1));
out_->set_init_state(a->aut->get_init_state_number());
} }
tgba_explicit_number* tgba_digraph*
result() result()
{ {
return out_; return out_;
@ -263,14 +264,13 @@ namespace spot
int out = in_->aut->state_number(sout); int out = in_->aut->state_number(sout);
unsigned in_scc = sm_.scc_of_state(sin); unsigned in_scc = sm_.scc_of_state(sin);
typedef state_explicit_number::transition trans; bdd cond = si->current_condition();
trans* t = out_->create_transition(in, out); unsigned t = out_->new_transition(in, out, cond);
bdd cond = t->condition = si->current_condition();
if (realizable_[in_scc]) if (realizable_[in_scc])
{ {
if (final_.find(sin) != final_.end()) if (final_.find(sin) != final_.end())
t->acceptance_conditions = acc_; out_->trans_data(t).acc = acc_;
} }
else if (sm_.scc_of_state(sout) == in_scc) else if (sm_.scc_of_state(sout) == in_scc)
{ {
@ -296,15 +296,12 @@ namespace spot
// implementation create more transitions than needed: // implementation create more transitions than needed:
// we do not need more than one transition per // we do not need more than one transition per
// accepting cycle. // accepting cycle.
trans* t1 = out_->create_transition(in, out + shift); out_->new_transition(in, out + shift, cond);
t1->condition = cond;
trans* t2 = out_->create_transition(in + shift, bdd acc = bddfalse;
out + shift); if (l.get(i)) // In the Li set. (Löding's Fi set.)
t2->condition = cond; acc = acc_;
// In the Li set. (Löding's Fi set.) out_->new_transition(in + shift, out + shift, cond, acc);
if (l.get(i))
t2->acceptance_conditions = acc_;
} }
} }
} }
@ -312,7 +309,7 @@ namespace spot
protected: protected:
const dstar_aut* in_; const dstar_aut* in_;
tgba_explicit_number* out_; tgba_digraph* out_;
const state_set& final_; const state_set& final_;
size_t num_states_; size_t num_states_;
bdd acc_; bdd acc_;
@ -368,8 +365,8 @@ namespace spot
state_set fs(final.begin(), final.end()); state_set fs(final.begin(), final.end());
dra_to_ba_worker w(dra, fs, sm, realizable); dra_to_ba_worker w(dra, fs, sm, realizable);
w.run(); w.run();
tgba_explicit_number* res1 = w.result(); auto res1 = w.result();
tgba* res2 = scc_filter_states(res1); auto res2 = scc_filter_states(res1);
delete res1; delete res1;
return res2; return res2;
} }

12
src/tgbatest/dstar.test
View file

@ -82,10 +82,10 @@ cat >expected <<EOF
digraph G { digraph G {
0 [label="", style=invis, height=0] 0 [label="", style=invis, height=0]
0 -> 1 0 -> 1
1 [label="1"] 1 [label="0"]
1 -> 1 [label="a & !b\n"] 1 -> 1 [label="a & !b\n"]
1 -> 2 [label="b\n"] 1 -> 2 [label="b\n"]
2 [label="2", peripheries=2] 2 [label="1", peripheries=2]
2 -> 2 [label="1\n{Acc[1]}"] 2 -> 2 [label="1\n{Acc[1]}"]
} }
EOF EOF
@ -213,22 +213,22 @@ cat >expected <<EOF
digraph G { digraph G {
0 [label="", style=invis, height=0] 0 [label="", style=invis, height=0]
0 -> 1 0 -> 1
1 [label="1"] 1 [label="0"]
1 -> 2 [label="!a & !b\n"] 1 -> 2 [label="!a & !b\n"]
1 -> 3 [label="a & !b\n"] 1 -> 3 [label="a & !b\n"]
1 -> 4 [label="!a & b\n"] 1 -> 4 [label="!a & b\n"]
1 -> 5 [label="a & b\n"] 1 -> 5 [label="a & b\n"]
2 [label="2"] 2 [label="1"]
2 -> 2 [label="!b\n"] 2 -> 2 [label="!b\n"]
2 -> 4 [label="b\n"] 2 -> 4 [label="b\n"]
3 [label="4", peripheries=2] 3 [label="2", peripheries=2]
3 -> 2 [label="!a & !b\n{Acc[1]}"] 3 -> 2 [label="!a & !b\n{Acc[1]}"]
3 -> 3 [label="a & !b\n{Acc[1]}"] 3 -> 3 [label="a & !b\n{Acc[1]}"]
3 -> 4 [label="!a & b\n{Acc[1]}"] 3 -> 4 [label="!a & b\n{Acc[1]}"]
3 -> 5 [label="a & b\n{Acc[1]}"] 3 -> 5 [label="a & b\n{Acc[1]}"]
4 [label="3", peripheries=2] 4 [label="3", peripheries=2]
4 -> 4 [label="1\n{Acc[1]}"] 4 -> 4 [label="1\n{Acc[1]}"]
5 [label="5", peripheries=2] 5 [label="4", peripheries=2]
5 -> 4 [label="!a\n{Acc[1]}"] 5 -> 4 [label="!a\n{Acc[1]}"]
5 -> 5 [label="a\n{Acc[1]}"] 5 -> 5 [label="a\n{Acc[1]}"]
} }