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

nra2nba: Produce a tgba_digraph.

Browse source 
* src/dstarparse/nra2nba.cc: Produce tgba_digraph instead
of tgba_explicit_number.
* src/tgbaalgos/sccinfo.hh (is_useful_state): Make sure
it is reachable.
This commit is contained in:
Alexandre Duret-Lutz 2014-08-05 16:08:44 +02:00
parent 7c0ce376c5
commit 9923cbaae0
2 changed files with 24 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/dstarparse/nra2nba.cc
View file

@ -21,7 +21,6 @@
#include "tgbaalgos/reachiter.hh" #include "tgbaalgos/reachiter.hh"
#include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/sccfilter.hh"
#include "ltlast/constant.hh" #include "ltlast/constant.hh"
#include "tgba/tgbaexplicit.hh"
namespace spot namespace spot
{ {
@ -42,7 +41,7 @@ namespace spot
// makes its possible to mask AUT, as needed in dra_to_ba(). // makes its possible to mask AUT, as needed in dra_to_ba().
nra_to_nba_worker(const dstar_aut* a, const tgba* aut): nra_to_nba_worker(const dstar_aut* a, const tgba* aut):
tgba_reachable_iterator_depth_first(aut), tgba_reachable_iterator_depth_first(aut),
out_(new tgba_explicit_number(aut->get_dict())), out_(new tgba_digraph(aut->get_dict())),
d_(a), d_(a),
num_states_(a->aut->num_states()) num_states_(a->aut->num_states())
{ {
@ -55,9 +54,14 @@ 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_ * (d_->accpair_count + 1));
auto i = aut->get_init_state();
out_->set_init_state(a->aut->state_number(i));
i->destroy();
} }
tgba_explicit_number* tgba_digraph*
result() result()
{ {
return out_; return out_;
@ -71,9 +75,8 @@ namespace spot
int in = d_->aut->state_number(sin); int in = d_->aut->state_number(sin);
int out = d_->aut->state_number(sout); int out = d_->aut->state_number(sout);
typedef state_explicit_number::transition trans; bdd cond = si->current_condition();
trans* t = out_->create_transition(in, out); out_->new_transition(in, out, cond);
bdd cond = t->condition = si->current_condition();
// Create one clone of the automaton per accepting pair, // Create one clone of the automaton per accepting pair,
// removing states from the Ui part of the (Li, Ui) pairs. // removing states from the Ui part of the (Li, Ui) pairs.
@ -97,20 +100,18 @@ 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, out + shift); bdd acc = bddfalse;
t2->condition = cond; if (l.get(i)) // In the Li set. (Löding's Fi set.)
// In the Li set. (Löding's Fi set.) acc = acc_;
if (l.get(i)) out_->new_transition(in + shift, out + shift, cond, acc);
t2->acceptance_conditions = acc_;
} }
} }
} }
protected: protected:
tgba_explicit_number* out_; tgba_digraph* out_;
const dstar_aut* d_; const dstar_aut* d_;
size_t num_states_; size_t num_states_;
bdd acc_; bdd acc_;
@ -126,8 +127,8 @@ namespace spot
assert(nra->type == Rabin); assert(nra->type == Rabin);
nra_to_nba_worker w(nra, aut); nra_to_nba_worker w(nra, aut);
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;
} }

8
src/tgbaalgos/sccinfo.hh
View file

@ -68,6 +68,7 @@ namespace spot
std::vector<scc_node> node_; std::vector<scc_node> node_;
const tgba_digraph* aut_; const tgba_digraph* aut_;
const scc_node& node(unsigned scc) const const scc_node& node(unsigned scc) const
{ {
assert(scc < node_.size()); assert(scc < node_.size());
@ -87,6 +88,11 @@ namespace spot
return node_.size(); return node_.size();
} }
bool reachable_state(unsigned st) const
{
return scc_of(st) != -1U;
}
unsigned scc_of(unsigned st) const unsigned scc_of(unsigned st) const
{ {
assert(st < sccof_.size()); assert(st < sccof_.size());
@ -125,7 +131,7 @@ namespace spot
bool is_useful_state(unsigned st) const bool is_useful_state(unsigned st) const
{ {
return node(scc_of(st)).useful; return reachable_state(st) && node(scc_of(st)).useful;
} }
/// \brief Return the set of all used acceptance combinations, for /// \brief Return the set of all used acceptance combinations, for