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

tgba: remove the global_state and global_automaton argument of succ_iter

Browse source 
* iface/dve2/dve2.cc, src/kripke/kripkeexplicit.cc,
src/kripke/kripkeexplicit.hh, src/ta/tgtaexplicit.cc,
src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh,
src/tgba/taatgba.cc, src/tgba/taatgba.hh, 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/tgbamask.cc,
src/tgba/tgbamask.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:
Here.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2014-02-17 19:43:03 +01:00
parent 0fba428cd9
commit bd870f9ab8
33 changed files with 63 additions and 179 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -60,6 +60,9 @@ New in spot 1.2.3a (not yet released)
methods have been removed from the TGBA interface and all
subclasses.
- tgba::succ_iter() now takes only one argument. The optional
global_state and global_automaton arguments have been removed.
- 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

9
iface/dve2/dve2.cc
View file

@ -848,11 +848,10 @@ namespace spot
virtual
dve2_succ_iterator*
succ_iter(const state* local_state,
const state*, const tgba*) const
succ_iter(const state* st) const
{
// This may also compute successors in state_condition_last_cc
bdd scond = compute_state_condition(local_state);
bdd scond = compute_state_condition(st);
callback_context* cc;
if (state_condition_last_cc_)
@ -863,11 +862,11 @@ namespace spot
else
{
int t;
cc = build_cc(get_vars(local_state), t);
cc = build_cc(get_vars(st), t);
// Add a self-loop to dead-states if we care about these.
if (t == 0 && scond != bddfalse)
cc->transitions.push_back(local_state->clone());
cc->transitions.push_back(st->clone());
}
if (iter_cache_)

10
src/kripke/kripkeexplicit.cc
View file

@ -175,16 +175,12 @@ namespace spot
return dict_;
}
// FIXME : Change the bddtrue.
// FIXME: Change the bddtrue.
kripke_explicit_succ_iterator*
kripke_explicit::succ_iter(const spot::state* local_state,
const spot::state* global_state,
const tgba* global_automaton) const
kripke_explicit::succ_iter(const spot::state* st) const
{
const state_kripke* s = down_cast<const state_kripke*>(local_state);
const state_kripke* s = down_cast<const state_kripke*>(st);
assert(s);
(void) global_state;
(void) global_automaton;
state_kripke* it = const_cast<state_kripke*>(s);
return new kripke_explicit_succ_iterator(it, bddtrue);
}

4
src/kripke/kripkeexplicit.hh
View file

@ -124,9 +124,7 @@ namespace spot
/// \brief Allow to get an iterator on the state we passed in
/// parameter.
kripke_explicit_succ_iterator*
succ_iter(const spot::state* local_state,
const spot::state* global_state = 0,
const tgba* global_automaton = 0) const;
succ_iter(const spot::state* state) const;
/// \brief Get the condition on the state
bdd state_condition(const state* s) const;

3
src/ta/tgtaexplicit.cc
View file

@ -43,8 +43,7 @@ namespace spot
}
tgba_succ_iterator*
tgta_explicit::succ_iter(const spot::state* state, const spot::state*,
const tgba*) const
tgta_explicit::succ_iter(const spot::state* state) const
{
return ta_.succ_iter(state);
}

3
src/ta/tgtaexplicit.hh
View file

@ -46,8 +46,7 @@ namespace spot
virtual spot::state* get_init_state() const;
virtual tgba_succ_iterator*
succ_iter(const spot::state* local_state, const spot::state* global_state =
0, const tgba* global_automaton = 0) const;
succ_iter(const spot::state* local_state) const;
virtual bdd_dict*
get_dict() const;

5
src/ta/tgtaproduct.cc
View file

@ -57,10 +57,9 @@ namespace spot
}
tgba_succ_iterator*
tgta_product::succ_iter(const state* local_state, const state*,
const tgba*) const
tgta_product::succ_iter(const state* state) const
{
const state_product* s = down_cast<const state_product*> (local_state);
const state_product* s = down_cast<const state_product*> (state);
assert(s);
fixed_size_pool* p = const_cast<fixed_size_pool*> (&pool_);

3
src/ta/tgtaproduct.hh
View file

@ -39,8 +39,7 @@ namespace spot
get_init_state() const;
virtual tgba_succ_iterator*
succ_iter(const state* local_state, const state* global_state = 0,
const tgba* global_automaton = 0) const;
succ_iter(const state* local_state) const;
};
/// \brief Iterate over the successors of a product computed on the fly.

6
src/tgba/taatgba.cc
View file

@ -65,14 +65,10 @@ namespace spot
}
tgba_succ_iterator*
taa_tgba::succ_iter(const spot::state* state,
const spot::state* global_state,
const tgba* global_automaton) const
taa_tgba::succ_iter(const spot::state* state) const
{
const spot::set_state* s = down_cast<const spot::set_state*>(state);
assert(s);
(void) global_state;
(void) global_automaton;
return new taa_succ_iterator(s->get_state(), all_acceptance_conditions());
}

5
src/tgba/taatgba.hh
View file

@ -54,10 +54,7 @@ namespace spot
/// TGBA interface.
virtual ~taa_tgba();
virtual spot::state* get_init_state() const;
virtual tgba_succ_iterator*
succ_iter(const spot::state* local_state,
const spot::state* global_state = 0,
const tgba* global_automaton = 0) const;
virtual tgba_succ_iterator* succ_iter(const spot::state* state) const;
virtual bdd_dict* get_dict() const;
virtual std::string format_state(const spot::state* state) const = 0;
virtual bdd all_acceptance_conditions() const;

23
src/tgba/tgba.hh
View file

@ -126,29 +126,8 @@ namespace spot
/// The iterator has been allocated with \c new. It is the
/// responsability of the caller to \c delete it when no
/// longer needed.
///
/// During synchornized products, additional informations are
/// passed about the entire product and its state. Recall that
/// products can be nested, forming a tree of spot::tgba where
/// most values are computed on demand. \a global_automaton
/// designate the root spot::tgba, and \a global_state its
/// state. This two objects can be used by succ_iter() to
/// restrict the set of successors to compute.
///
/// \param local_state The state whose successors are to be explored.
/// This pointer is not adopted in any way by \c succ_iter, and
/// it is still the caller's responsability to destroy it when
/// appropriate (this can be done during the lifetime of
/// the iterator).
/// \param global_state In a product, the state of the global
/// product automaton. Otherwise, 0. Like \a locale_state,
/// \a global_state is not adopted by \c succ_iter.
/// \param global_automaton In a product, the global
/// product automaton. Otherwise, 0.
virtual tgba_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = nullptr,
const tgba* global_automaton = nullptr) const = 0;
succ_iter(const state* local_state) const = 0;
#ifndef SWIG
/// \brief Build an iterable over the successors of \a s.

14
src/tgba/tgbabddconcrete.cc
View file

@ -93,21 +93,11 @@ namespace spot
}
tgba_succ_iterator_concrete*
tgba_bdd_concrete::succ_iter(const state* local_state,
const state* global_state,
const tgba* global_automaton) const
tgba_bdd_concrete::succ_iter(const state* state) const
{
const state_bdd* s = down_cast<const state_bdd*>(local_state);
const state_bdd* s = down_cast<const state_bdd*>(state);
assert(s);
bdd succ_set = data_.relation & s->as_bdd();
// If we are in a product, inject the local conditions of
// all other automata to limit the number of successors.
if (global_automaton)
{
bdd varused = bdd_support(succ_set);
bdd global_conds = global_automaton->support_conditions(global_state);
succ_set = bdd_appexcomp(succ_set, global_conds, bddop_and, varused);
}
// Do not allocate an iterator if we can reuse one.
if (iter_cache_)
{

4
src/tgba/tgbabddconcrete.hh
View file

@ -62,9 +62,7 @@ namespace spot
bdd get_init_bdd() const;
virtual tgba_succ_iterator_concrete*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const;
succ_iter(const state* local_state) const;
virtual std::string format_state(const state* state) const;

7
src/tgba/tgbaexplicit.hh
View file

@ -505,16 +505,11 @@ namespace spot
}
virtual tgba_explicit_succ_iterator<State>*
succ_iter(const spot::state* state,
const spot::state* global_state = 0,
const tgba* global_automaton = 0) const
succ_iter(const spot::state* state) const
{
const State* s = down_cast<const State*>(state);
assert(s);
(void) global_state;
(void) global_automaton;
if (this->iter_cache_)
{
tgba_explicit_succ_iterator<State>* it =

12
src/tgba/tgbakvcomplement.cc
View file

@ -616,17 +616,15 @@ namespace spot
}
tgba_succ_iterator*
tgba_kv_complement::succ_iter(const state* local_state,
const state*,
const tgba*) const
tgba_kv_complement::succ_iter(const state* state) const
{
const state_kv_complement* state =
down_cast<const state_kv_complement*>(local_state);
assert(state);
const state_kv_complement* s =
down_cast<const state_kv_complement*>(state);
assert(s);
return new tgba_kv_complement_succ_iterator(automaton_,
the_acceptance_cond_,
acc_list_, state);
acc_list_, s);
}
bdd_dict*

5
src/tgba/tgbakvcomplement.hh
View file

@ -91,10 +91,7 @@ namespace spot
// tgba interface
virtual state* get_init_state() const;
virtual tgba_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const;
virtual tgba_succ_iterator* succ_iter(const state* state) const;
virtual bdd_dict* get_dict() const;
virtual std::string format_state(const state* state) const;

8
src/tgba/tgbamask.cc
View file

@ -139,9 +139,7 @@ namespace spot
}
tgba_succ_iterator*
tgba_mask::succ_iter(const state* local_state,
const state*,
const tgba*) const
tgba_mask::succ_iter(const state* state) const
{
succ_iter_filtered* res;
if (iter_cache_)
@ -153,9 +151,9 @@ namespace spot
{
res = new succ_iter_filtered;
}
for (auto it: original_->succ(local_state))
for (auto it: original_->succ(state))
{
const state* s = it->current_state();
const spot::state* s = it->current_state();
if (!wanted(s))
{
s->destroy();

6
src/tgba/tgbamask.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Développement
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -48,9 +48,7 @@ namespace spot
virtual state* get_init_state() const;
virtual tgba_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const;
succ_iter(const state* local_state) const;
virtual bool wanted(const state* s) const = 0;

22
src/tgba/tgbaproduct.cc
View file

@ -374,26 +374,12 @@ namespace spot
}
tgba_succ_iterator*
tgba_product::succ_iter(const state* local_state,
const state* global_state,
const tgba* global_automaton) const
tgba_product::succ_iter(const state* state) const
{
const state_product* s =
down_cast<const state_product*>(local_state);
const state_product* s = down_cast<const state_product*>(state);
assert(s);
// If global_automaton is not specified, THIS is the root of a
// product tree.
if (!global_automaton)
{
global_automaton = this;
global_state = local_state;
}
tgba_succ_iterator* li = left_->succ_iter(s->left(),
global_state, global_automaton);
tgba_succ_iterator* ri = right_->succ_iter(s->right(),
global_state, global_automaton);
tgba_succ_iterator* li = left_->succ_iter(s->left());
tgba_succ_iterator* ri = right_->succ_iter(s->right());
if (iter_cache_)
{

4
src/tgba/tgbaproduct.hh
View file

@ -92,9 +92,7 @@ namespace spot
virtual state* get_init_state() const;
virtual tgba_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const;
succ_iter(const state* state) const;
virtual bdd_dict* get_dict() const;

6
src/tgba/tgbaproxy.cc
View file

@ -38,16 +38,14 @@ namespace spot
}
tgba_succ_iterator*
tgba_proxy::succ_iter(const state* local_state,
const state* global_state,
const tgba* global_automaton) const
tgba_proxy::succ_iter(const state* state) const
{
if (iter_cache_)
{
original_->release_iter(iter_cache_);
iter_cache_ = nullptr;
}
return original_->succ_iter(local_state, global_state, global_automaton);
return original_->succ_iter(state);
}
bdd_dict*

4
src/tgba/tgbaproxy.hh
View file

@ -44,9 +44,7 @@ namespace spot
virtual state* get_init_state() const;
virtual tgba_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const;
succ_iter(const state* state) const;
virtual bdd_dict* get_dict() const;

7
src/tgba/tgbasafracomplement.cc
View file

@ -1161,13 +1161,10 @@ namespace spot
/// @param local_state the state from which we want to compute the successors.
///
tgba_succ_iterator*
tgba_safra_complement::succ_iter(const state* local_state,
const state* /* = 0 */,
const tgba* /* = 0 */) const
tgba_safra_complement::succ_iter(const state* state) const
{
const safra_tree_automaton* a = static_cast<safra_tree_automaton*>(safra_);
const state_complement* s =
down_cast<const state_complement*>(local_state);
const state_complement* s = down_cast<const state_complement*>(state);
assert(s);
safra_tree_automaton::automaton_t::const_iterator tr =
a->automaton.find(const_cast<safra_tree*>(s->get_safra()));

5
src/tgba/tgbasafracomplement.hh
View file

@ -55,10 +55,7 @@ namespace spot
// tgba interface.
virtual state* get_init_state() const;
virtual tgba_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const;
virtual tgba_succ_iterator* succ_iter(const state* state) const;
virtual bdd_dict* get_dict() const;
virtual std::string format_state(const state* state) const;

6
src/tgba/tgbascc.cc
View file

@ -46,16 +46,14 @@ namespace spot
}
tgba_succ_iterator*
tgba_scc::succ_iter(const state* local_state,
const state* global_state,
const tgba* global_automaton) const
tgba_scc::succ_iter(const state* state) const
{
if (iter_cache_)
{
aut_->release_iter(iter_cache_);
iter_cache_ = nullptr;
}
return aut_->succ_iter(local_state, global_state, global_automaton);
return aut_->succ_iter(state);
}
bdd_dict*

5
src/tgba/tgbascc.hh
View file

@ -57,10 +57,7 @@ namespace spot
// tgba.
virtual state* get_init_state() const;
virtual tgba_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const;
virtual tgba_succ_iterator* succ_iter(const state* state) const;
virtual bdd_dict* get_dict() const;
virtual std::string

12
src/tgba/tgbasgba.cc
View file

@ -191,17 +191,11 @@ namespace spot
}
tgba_succ_iterator*
tgba_sgba_proxy::succ_iter(const state* local_state,
const state* global_state,
const tgba* global_automaton) const
tgba_sgba_proxy::succ_iter(const state* state) const
{
const state_sgba_proxy* s =
down_cast<const state_sgba_proxy*>(local_state);
const state_sgba_proxy* s = down_cast<const state_sgba_proxy*>(state);
assert(s);
tgba_succ_iterator* it = a_->succ_iter(s->real_state(),
global_state, global_automaton);
tgba_succ_iterator* it = a_->succ_iter(s->real_state());
return new tgba_sgba_proxy_succ_iterator(it);
}

5
src/tgba/tgbasgba.hh
View file

@ -42,10 +42,7 @@ namespace spot
virtual state* get_init_state() const;
virtual tgba_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const;
virtual tgba_succ_iterator* succ_iter(const state* state) const;
virtual bdd_dict* get_dict() const;

6
src/tgba/tgbatba.cc
View file

@ -498,11 +498,9 @@ namespace spot
}
tgba_succ_iterator*
tgba_tba_proxy::succ_iter(const state* local_state,
const state*, const tgba*) const
tgba_tba_proxy::succ_iter(const state* st) const
{
const state_tba_proxy* s =
down_cast<const state_tba_proxy*>(local_state);
const state_tba_proxy* s = down_cast<const state_tba_proxy*>(st);
assert(s);
const state* rs = s->real_state();

5
src/tgba/tgbatba.hh
View file

@ -58,10 +58,7 @@ namespace spot
virtual state* get_init_state() const;
virtual tgba_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const;
virtual tgba_succ_iterator* succ_iter(const state* state) const;
virtual bdd_dict* get_dict() const;

8
src/tgba/tgbaunion.cc
View file

@ -313,13 +313,9 @@ namespace spot
}
tgba_succ_iterator_union*
tgba_union::succ_iter(const state* local_state,
const state* global_state,
const tgba* global_automaton) const
tgba_union::succ_iter(const state* st) const
{
(void) global_state;
(void) global_automaton;
const state_union* s = down_cast<const state_union*>(local_state);
const state_union* s = down_cast<const state_union*>(st);
assert(s);
// Is it the initial state ?
tgba_succ_iterator* li;

4
src/tgba/tgbaunion.hh
View file

@ -124,9 +124,7 @@ namespace spot
virtual state* get_init_state() const;
virtual tgba_succ_iterator_union*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const;
succ_iter(const state* state) const;
virtual bdd_dict* get_dict() const;

11
src/tgba/wdbacomp.cc
View file

@ -206,18 +206,16 @@ namespace spot
}
virtual tgba_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0) const
succ_iter(const state* st) const
{
const state_wdba_comp_proxy* s =
down_cast<const state_wdba_comp_proxy*>(local_state);
down_cast<const state_wdba_comp_proxy*>(st);
assert(s);
const state* o = s->real_state();
tgba_succ_iterator* it = nullptr;
if (o)
it = a_->succ_iter(s->real_state(), global_state, global_automaton);
it = a_->succ_iter(s->real_state());
if (iter_cache_)
{
tgba_wdba_comp_proxy_succ_iterator* res =
@ -226,8 +224,7 @@ namespace spot
iter_cache_ = nullptr;
return res;
}
return new tgba_wdba_comp_proxy_succ_iterator(it,
the_acceptance_cond_);
return new tgba_wdba_comp_proxy_succ_iterator(it, the_acceptance_cond_);
}
virtual bdd_dict*