Commit 0fba428c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

tgba: remove the support_variable() method.

* src/kripke/fairkripke.cc, src/kripke/fairkripke.hh,
src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh, src/tgba/taatgba.cc,
src/tgba/taatgba.hh, src/tgba/tgba.cc, src/tgba/tgba.hh,
src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbaexplicit.hh, src/tgba/tgbakvcomplement.cc,
src/tgba/tgbakvcomplement.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgba/tgbascc.cc, src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc,
src/tgba/tgbasgba.hh, src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc:
Remove anything related to support_variables() and
compute_support_variables().
* NEWS: Mention it.
* src/tgbaalgos/powerset.cc: Adjust the computation of all possible
conditions.
parent 358ea9ed
......@@ -56,6 +56,10 @@ New in spot 1.2.3a (not yet released)
Where the virtual calls to done() and delete have been avoided.
- tgba::support_variables() and tgba::compute_support_variables()
methods have been removed from the TGBA interface and all
subclasses.
- The long unused interface for GreatSPN (or rather, interface to
a non-public, customized version of GreatSPN) has been removed.
As a consequence, the we could get rid of many cruft in the
......
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement
// de l'Epita
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2014 Laboratoire de Recherche et
// Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
//
......@@ -53,10 +54,4 @@ namespace spot
return state_condition(s);
}
bdd
fair_kripke::compute_support_variables(const state* s) const
{
return bdd_support(state_condition(s));
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2013 Laboratoire de Recherche et
// Copyright (C) 2009, 2010, 2013, 2014 Laboratoire de Recherche et
// Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
......@@ -101,7 +101,6 @@ namespace spot
protected:
virtual bdd compute_support_conditions(const state* s) const;
virtual bdd compute_support_variables(const state* s) const;
};
}
......
// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2014 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -56,14 +57,6 @@ namespace spot
return ta_.get_tgba()->support_conditions(s->get_tgba_state());
}
bdd
tgta_explicit::compute_support_variables(const spot::state* in) const
{
const state_ta_explicit* s = down_cast<const state_ta_explicit*>(in);
assert(s);
return ta_.get_tgba()->support_variables(s->get_tgba_state());
}
bdd_dict*
tgta_explicit::get_dict() const
{
......
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -64,7 +64,6 @@ namespace spot
succ_iter_by_changeset(const spot::state* s, bdd change_set) const;
protected:
virtual bdd compute_support_conditions(const spot::state* state) const;
virtual bdd compute_support_variables(const spot::state* state) const;
ta_explicit ta_;
};
......
......@@ -116,22 +116,6 @@ namespace spot
return res;
}
bdd
taa_tgba::compute_support_variables(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 &= bdd_support((*j)->condition);
return res;
}
/*----------.
| state_set |
`----------*/
......
......@@ -65,7 +65,6 @@ namespace spot
protected:
virtual bdd compute_support_conditions(const spot::state* state) const;
virtual bdd compute_support_variables(const spot::state* state) const;
typedef std::vector<taa_tgba::state_set*> ss_vec;
......
......@@ -27,7 +27,6 @@ namespace spot
tgba::tgba()
: iter_cache_(nullptr),
last_support_conditions_input_(0),
last_support_variables_input_(0),
num_acc_(-1)
{
}
......@@ -36,8 +35,6 @@ namespace spot
{
if (last_support_conditions_input_)
last_support_conditions_input_->destroy();
if (last_support_variables_input_)
last_support_variables_input_->destroy();
delete iter_cache_;
}
......@@ -55,20 +52,6 @@ namespace spot
return last_support_conditions_output_;
}
bdd
tgba::support_variables(const state* state) const
{
if (!last_support_variables_input_
|| last_support_variables_input_->compare(state) != 0)
{
last_support_variables_output_ = compute_support_variables(state);
if (last_support_variables_input_)
last_support_variables_input_->destroy();
last_support_variables_input_ = state->clone();
}
return last_support_variables_output_;
}
state*
tgba::project_state(const state* s, const tgba* t) const
{
......
......@@ -189,20 +189,6 @@ namespace spot
/// last return value for efficiency.
bdd support_conditions(const state* state) const;
/// \brief Get the conjunctions of variables tested by
/// the outgoing transitions of \a state.
///
/// All variables tested by outgoing transitions must be
/// returned. This is mandatory.
///
/// This is used as an hint by some \c succ_iter() to reduce the
/// number of successor to compute in a product.
///
/// Sub classes should implement compute_support_variables(),
/// this function is just a wrapper that will cache the
/// last return value for efficiency.
bdd support_variables(const state* state) const;
/// \brief Get the dictionary associated to the automaton.
///
/// Atomic propositions and acceptance conditions are represented
......@@ -280,14 +266,9 @@ namespace spot
protected:
/// Do the actual computation of tgba::support_conditions().
virtual bdd compute_support_conditions(const state* state) const = 0;
/// Do the actual computation of tgba::support_variables().
virtual bdd compute_support_variables(const state* state) const = 0;
protected:
mutable const state* last_support_conditions_input_;
mutable const state* last_support_variables_input_;
private:
mutable bdd last_support_conditions_output_;
mutable bdd last_support_variables_output_;
mutable int num_acc_;
};
......
......@@ -128,27 +128,6 @@ namespace spot
return bdd_relprod(s->as_bdd(), data_.relation, data_.notvar_set);
}
bdd
tgba_bdd_concrete::compute_support_variables(const state* st) const
{
const state_bdd* s = down_cast<const state_bdd*>(st);
assert(s);
bdd succ_set = data_.relation & s->as_bdd();
// bdd_support must be called BEFORE bdd_exist
// because bdd_exist(bdd_support((a&Next[f])|(!a&Next[g])),Next[*])
// is obviously not the same as bdd_support(a|!a).
// In other words: we cannot reuse compute_support_conditions() for
// this computation.
//
// Also we need to inject the support of acceptance conditions, because a
// "Next[f]" that looks like one transition might in fact be two
// transitions if the acceptance condition distinguish between
// letters, e.g. "Next[f] & ((a & Acc[1]) | (!a))"
return bdd_exist(bdd_support(succ_set)
& data_.acceptance_conditions_support,
data_.notvar_set);
}
std::string
tgba_bdd_concrete::format_state(const state* state) const
{
......
// Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
......@@ -85,7 +86,6 @@ namespace spot
protected:
virtual bdd compute_support_conditions(const state* state) const;
virtual bdd compute_support_variables(const state* state) const;
tgba_bdd_core_data data_; ///< Core data associated to the automaton.
bdd init_; ///< Initial state.
......
......@@ -491,10 +491,9 @@ namespace spot
}
this->dict_->unregister_all_my_variables(this);
// These have already been destroyed by subclasses.
// Thus has already been destroyed by subclasses.
// Prevent destroying by tgba::~tgba.
this->last_support_conditions_input_ = 0;
this->last_support_variables_input_ = 0;
}
virtual State* get_init_state() const
......@@ -682,21 +681,6 @@ namespace spot
return res;
}
virtual bdd compute_support_variables(const spot::state* in) const
{
const State* s = down_cast<const State*>(in);
assert(s);
const transitions_t& st = s->successors;
bdd res = bddtrue;
typename transitions_t::const_iterator i;
for (i = st.begin(); i != st.end(); ++i)
res &= bdd_support(i->condition);
return res;
}
ls_map ls_;
alias_map alias_;
sl_map sl_;
......
......@@ -685,13 +685,4 @@ namespace spot
return result;
}
bdd
tgba_kv_complement::compute_support_variables(const state* state) const
{
bdd result = bddtrue;
for (auto i: succ(state))
result &= bdd_support(i->current_condition());
return result;
}
} // end namespace spot.
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -102,7 +102,6 @@ namespace spot
virtual bdd neg_acceptance_conditions() const;
protected:
virtual bdd compute_support_conditions(const state* state) const;
virtual bdd compute_support_variables(const state* state) const;
private:
/// Retrieve all the atomic acceptance conditions of the automaton.
/// They are inserted into \a acc_list_.
......
......@@ -363,11 +363,6 @@ namespace spot
last_support_conditions_input_->destroy();
last_support_conditions_input_ = 0;
}
if (last_support_variables_input_)
{
last_support_variables_input_->destroy();
last_support_variables_input_ = 0;
}
}
state*
......@@ -430,16 +425,6 @@ namespace spot
return lsc & rsc;
}
bdd
tgba_product::compute_support_variables(const state* in) const
{
const state_product* s = down_cast<const state_product*>(in);
assert(s);
bdd lsc = left_->support_variables(s->left());
bdd rsc = right_->support_variables(s->right());
return lsc & rsc;
}
bdd_dict*
tgba_product::get_dict() const
{
......
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
......@@ -110,7 +110,6 @@ namespace spot
protected:
virtual bdd compute_support_conditions(const state* state) const;
virtual bdd compute_support_variables(const state* state) const;
protected:
bdd_dict* dict_;
......
......@@ -91,11 +91,5 @@ namespace spot
{
return original_->support_conditions(state);
}
bdd
tgba_proxy::compute_support_variables(const state* state) const
{
return original_->support_variables(state);
}
}
// Copyright (C) 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -62,8 +63,6 @@ namespace spot
protected:
virtual bdd compute_support_conditions(const state* state) const;
virtual bdd compute_support_variables(const state* state) const;
const tgba* original_;
};
}
......
......@@ -1307,24 +1307,6 @@ namespace spot
return res;
}
bdd
tgba_safra_complement::compute_support_variables(const state* state) const
{
const safra_tree_automaton* a = static_cast<safra_tree_automaton*>(safra_);
const state_complement* s = down_cast<const state_complement*>(state);
assert(s);
typedef safra_tree_automaton::automaton_t::const_iterator auto_it;
auto_it node(a->automaton.find(const_cast<safra_tree*>(s->get_safra())));
if (node == a->automaton.end())
return bddtrue;
bdd res = bddtrue;
for (auto& i: node->second)
res &= bdd_support(i.first);
return res;
}
// display_safra: debug routine.
//////////////////////////////
void display_safra(const tgba_safra_complement* a)
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2009, 2010, 2011, 2013, 2014 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -72,7 +72,6 @@ namespace spot
protected:
virtual bdd compute_support_conditions(const state* state) const;
virtual bdd compute_support_variables(const state* state) const;
private:
const tgba* automaton_;
void* safra_;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment