* src/tgba/tgba.hh, src/tgba/tgba.cc
(tgba::number_of_acceptance_conditions): New method. * src/tgbaalgos/lbtt.cc (lbtt_bfs::lbtt_bfs): Use it.
This commit is contained in:
parent
1d3100607a
commit
d60025dcd1
4 changed files with 28 additions and 11 deletions
|
|
@ -1,5 +1,9 @@
|
|||
2004-11-04 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||
|
||||
* src/tgba/tgba.hh, src/tgba/tgba.cc
|
||||
(tgba::number_of_acceptance_conditions): New method.
|
||||
* src/tgbaalgos/lbtt.cc (lbtt_bfs::lbtt_bfs): Use it.
|
||||
|
||||
* wrap/python/spot.i: Generate bindings for tgbaalgos/dottydec.hh,
|
||||
tgbaalgos/emptiness.hh, tgbaalgos/gtec/gtec.hh, and
|
||||
tgbaalgos/rundotdec.hh.
|
||||
|
|
|
|||
|
|
@ -25,7 +25,8 @@ namespace spot
|
|||
{
|
||||
tgba::tgba()
|
||||
: last_support_conditions_input_(0),
|
||||
last_support_variables_input_(0)
|
||||
last_support_variables_input_(0),
|
||||
num_acc_(-1)
|
||||
{
|
||||
}
|
||||
|
||||
|
|
@ -75,4 +76,21 @@ namespace spot
|
|||
return "";
|
||||
}
|
||||
|
||||
int
|
||||
tgba::number_of_acceptance_conditions() const
|
||||
{
|
||||
if (num_acc_ < 0)
|
||||
{
|
||||
bdd all = all_acceptance_conditions();
|
||||
int n = 0;
|
||||
while (all != bddfalse)
|
||||
{
|
||||
++n;
|
||||
all -= bdd_satone(all);
|
||||
}
|
||||
num_acc_ = n;
|
||||
}
|
||||
return num_acc_;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -173,6 +173,9 @@ namespace spot
|
|||
/// the SCC should be equal to the result of this function.
|
||||
virtual bdd all_acceptance_conditions() const = 0;
|
||||
|
||||
/// The number of acceptance conditions.
|
||||
virtual int number_of_acceptance_conditions() const;
|
||||
|
||||
/// \brief Return the conjuction of all negated acceptance
|
||||
/// variables.
|
||||
///
|
||||
|
|
@ -195,6 +198,7 @@ namespace spot
|
|||
mutable bdd last_support_conditions_output_;
|
||||
mutable const state* last_support_variables_input_;
|
||||
mutable bdd last_support_variables_output_;
|
||||
mutable int num_acc_;
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -108,18 +108,9 @@ namespace spot
|
|||
lbtt_bfs(const tgba* a, std::ostream& os)
|
||||
: tgba_reachable_iterator_breadth_first(a),
|
||||
os_(os),
|
||||
acc_count_(0),
|
||||
acc_count_(a->number_of_acceptance_conditions()),
|
||||
acs_(a->all_acceptance_conditions())
|
||||
|
||||
{
|
||||
// Count the number of acceptance_conditions.
|
||||
bdd all = a->all_acceptance_conditions();
|
||||
while (all != bddfalse)
|
||||
{
|
||||
bdd one = bdd_satone(all);
|
||||
all -= one;
|
||||
++acc_count_;
|
||||
}
|
||||
}
|
||||
|
||||
void
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue