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

remove twa::compute_support_conditions

Browse source 
Fixes #148.

* spot/twa/twa.hh, spot/twa/twa.cc, spot/kripke/fairkripke.hh,
spot/kripke/fairkripke.cc, spot/ta/tgtaexplicit.hh,
spot/ta/tgtaexplicit.cc, spot/twa/twagraph.hh, spot/twa/twaproduct.hh,
spot/twa/twaproduct.cc, spot/twaalgos/stutter.cc, spot/twa/taatgba.hh,
spot/twa/taatgba.cc: Remove the method.
* spot/taalgos/tgba2ta.cc: Emulate it with a simple loop.
* NEWS: Mention the removal.
This commit is contained in:
Alexandre Duret-Lutz 2016-02-15 10:45:05 +01:00
parent 39b95474f8
commit a3e0c8624e
14 changed files with 15 additions and 120 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -82,7 +82,8 @@ New in spot 1.99.7a (not yet released)
* The twa_safra_complement class has been removed. Use
tgba_determinize() and dtwa_complement() instead.
* The twa::transition_annotation() method has been removed.
* The twa::transition_annotation() and
twa::compute_support_conditions() methods have been removed.
Python:

9
spot/kripke/fairkripke.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2014 Laboratoire de Recherche et
// Copyright (C) 2009, 2010, 2014, 2016 Laboratoire de Recherche et
// Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
@ -47,11 +47,4 @@ namespace spot
// this function on a state without successor.
return acc_cond_;
}
bdd
fair_kripke::compute_support_conditions(const state* s) const
{
return state_condition(s);
}
}

3
spot/kripke/fairkripke.hh
View file

@ -100,8 +100,5 @@ namespace spot
/// \brief The set of acceptance conditions that label the state \a s.
virtual acc_cond::mark_t
state_acceptance_conditions(const state* s) const = 0;
protected:
virtual bdd compute_support_conditions(const state* s) const;
};
}

12
spot/ta/tgtaexplicit.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2014, 2015 Laboratoire de Recherche
// et Developpement de l'Epita (LRDE).
// Copyright (C) 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire de
// Recherche et Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -44,14 +44,6 @@ namespace spot
return ta_->succ_iter(state);
}
bdd
tgta_explicit::compute_support_conditions(const spot::state* in) const
{
const state_ta_explicit* s = down_cast<const state_ta_explicit*>(in);
assert(s);
return ta_->get_tgba()->support_conditions(s->get_tgba_state());
}
bdd_dict_ptr
tgta_explicit::get_dict() const
{

6
spot/ta/tgtaexplicit.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
// de Recherche et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -58,8 +58,6 @@ namespace spot
virtual twa_succ_iterator*
succ_iter_by_changeset(const spot::state* s, bdd change_set) const;
protected:
virtual bdd compute_support_conditions(const spot::state* state) const;
ta_explicit_ptr ta_;
};

8
spot/taalgos/tgba2ta.cc
View file

@ -413,7 +413,13 @@ namespace spot
// build Initial states set:
auto tgba_init_state = tgba_->get_init_state();
bdd tgba_condition = tgba_->support_conditions(tgba_init_state);
bdd tgba_condition = [&]()
{
bdd cond = bddfalse;
for (auto i: tgba_->succ(tgba_init_state))
cond |= i->cond();
return cond;
}();
bool is_acc = false;
if (degeneralized)

16
spot/twa/taatgba.cc
View file

@ -66,22 +66,6 @@ namespace spot
return new taa_succ_iterator(s->get_state(), acc());
}
bdd
taa_tgba::compute_support_conditions(const spot::state* s) const
{
const spot::set_state* se = down_cast<const spot::set_state*>(s);
assert(se);
const state_set* ss = se->get_state();
bdd res = bddtrue;
taa_tgba::state_set::const_iterator i;
taa_tgba::state::const_iterator j;
for (i = ss->begin(); i != ss->end(); ++i)
for (j = (*i)->begin(); j != (*i)->end(); ++j)
res |= (*j)->condition;
return res;
}
/*----------.
| state_set |
`----------*/

2
spot/twa/taatgba.hh
View file

@ -58,8 +58,6 @@ namespace spot
virtual std::string format_state(const spot::state* state) const = 0;
protected:
virtual bdd compute_support_conditions(const spot::state* state)
const final;
typedef std::vector<taa_tgba::state_set*> ss_vec;

19
spot/twa/twa.cc
View file

@ -30,8 +30,7 @@ namespace spot
{
twa::twa(const bdd_dict_ptr& d)
: iter_cache_(nullptr),
dict_(d),
last_support_conditions_input_(nullptr)
dict_(d)
{
props = 0U;
bddaps_ = bddtrue;
@ -39,27 +38,11 @@ namespace spot
twa::~twa()
{
if (last_support_conditions_input_)
last_support_conditions_input_->destroy();
delete iter_cache_;
release_named_properties();
get_dict()->unregister_all_my_variables(this);
}
bdd
twa::support_conditions(const state* state) const
{
if (!last_support_conditions_input_
|| last_support_conditions_input_->compare(state) != 0)
{
last_support_conditions_output_ = compute_support_conditions(state);
if (last_support_conditions_input_)
last_support_conditions_input_->destroy();
last_support_conditions_input_ = state->clone();
}
return last_support_conditions_output_;
}
state*
twa::project_state(const state* s,
const const_twa_ptr& t) const

20
spot/twa/twa.hh
View file

@ -687,21 +687,6 @@ namespace spot
iter_cache_ = i;
}
/// \brief Get a formula that must hold whatever successor is taken.
///
/// \return A formula which must be verified for all successors
/// of \a state.
///
/// This can be as simple as \c bddtrue, or more precisely
/// the disjunction of the condition of all successors. This
/// is used as an hint by \c succ_iter() to reduce the number
/// of successor to compute in a product.
///
/// Sub classes should implement compute_support_conditions(),
/// this function is just a wrapper that will cache the
/// last return value for efficiency.
bdd support_conditions(const state* state) const;
/// \brief Get the dictionary associated to the automaton.
///
/// Automata are labeled by Boolean formulas over atomic
@ -901,12 +886,7 @@ namespace spot
return acc_.mark(0);
}
protected:
/// Do the actual computation of tgba::support_conditions().
virtual bdd compute_support_conditions(const state* state) const = 0;
mutable const state* last_support_conditions_input_;
private:
mutable bdd last_support_conditions_output_;
std::vector<formula> aps_;
bdd bddaps_;

11
spot/twa/twagraph.hh
View file

@ -202,9 +202,6 @@ namespace spot
virtual ~twa_graph()
{
// Prevent this state from being destroyed by ~twa(),
// as the state will be destroyed when g_ is destroyed.
last_support_conditions_input_ = nullptr;
}
#ifndef SWIG
@ -425,14 +422,6 @@ namespace spot
SPOT_RETURN(g_.is_dead_edge(t));
#endif
virtual bdd compute_support_conditions(const state* s) const
{
bdd sum = bddfalse;
for (auto& t: out(state_number(s)))
sum |= t.cond;
return sum;
}
/// Iterate over all edges, and merge those with compatible
/// extremities and acceptance.
void merge_edges();

17
spot/twa/twaproduct.cc
View file

@ -318,13 +318,6 @@ namespace spot
twa_product::~twa_product()
{
// Prevent these states from being destroyed by ~tgba(): they
// will be destroyed before when the pool is destructed.
if (last_support_conditions_input_)
{
last_support_conditions_input_->destroy();
last_support_conditions_input_ = nullptr;
}
}
const state*
@ -359,16 +352,6 @@ namespace spot
return new twa_succ_iterator_product(li, ri, this, p);
}
bdd
twa_product::compute_support_conditions(const state* in) const
{
const state_product* s = down_cast<const state_product*>(in);
assert(s);
bdd lsc = left_->support_conditions(s->left());
bdd rsc = right_->support_conditions(s->right());
return lsc & rsc;
}
const acc_cond& twa_product::left_acc() const
{
return left_->acc();

3
spot/twa/twaproduct.hh
View file

@ -102,9 +102,6 @@ namespace spot
const acc_cond& left_acc() const;
const acc_cond& right_acc() const;
protected:
virtual bdd compute_support_conditions(const state* state) const;
protected:
const_twa_ptr left_;
const_twa_ptr right_;

6
spot/twaalgos/stutter.cc
View file

@ -236,12 +236,6 @@ namespace spot
+ bdd_format_formula(a_->get_dict(), s->cond()));
}
protected:
virtual bdd compute_support_conditions(const state*) const override
{
return bddtrue;
}
private:
const_twa_ptr a_;
bdd aps_;