twa: make acc_ private
* spot/twa/twa.hh: Here. * spot/ta/ta.hh, spot/twa/taatgba.cc, spot/twa/taatgba.hh, spot/twa/twagraph.hh, spot/twa/twasafracomplement.cc, spot/twaalgos/stutter.cc: Adjust.
This commit is contained in:
parent
681bb82b8e
commit
aebe6593f9
7 changed files with 15 additions and 16 deletions
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2010, 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
// Copyright (C) 2010, 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
|
||||||
// Developpement de l Epita (LRDE).
|
// Developpement de l Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -36,7 +36,7 @@ namespace spot
|
||||||
/// This type and its cousins are listed \ref ta_essentials "here".
|
/// This type and its cousins are listed \ref ta_essentials "here".
|
||||||
/// This is an abstract interface. Its implementations are \ref
|
/// This is an abstract interface. Its implementations are \ref
|
||||||
/// ta_representation "concrete representations". The
|
/// ta_representation "concrete representations". The
|
||||||
/// algorithms that work on spot::ta are \ref tgba_algorithms
|
/// algorithms that work on spot::ta are \ref ta_algorithms
|
||||||
/// "listed separately".
|
/// "listed separately".
|
||||||
|
|
||||||
/// \addtogroup ta_essentials Essential TA types
|
/// \addtogroup ta_essentials Essential TA types
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
|
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
|
||||||
// de Recherche et Développement de l'Epita (LRDE)
|
// Laboratoire de Recherche et Développement de l'Epita (LRDE)
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -63,7 +63,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
const spot::set_state* s = down_cast<const spot::set_state*>(state);
|
const spot::set_state* s = down_cast<const spot::set_state*>(state);
|
||||||
assert(s);
|
assert(s);
|
||||||
return new taa_succ_iterator(s->get_state(), acc_);
|
return new taa_succ_iterator(s->get_state(), acc());
|
||||||
}
|
}
|
||||||
|
|
||||||
bdd
|
bdd
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015 Laboratoire de
|
// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
|
||||||
// Recherche et Développement de l'Epita (LRDE).
|
// Recherche et Développement de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -196,7 +196,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
auto p = acc_map_.emplace(f, 0);
|
auto p = acc_map_.emplace(f, 0);
|
||||||
if (p.second)
|
if (p.second)
|
||||||
p.first->second = acc_cond::mark_t({acc_.add_set()});
|
p.first->second = acc_cond::mark_t({acc().add_set()});
|
||||||
t->acceptance_conditions |= p.first->second;
|
t->acceptance_conditions |= p.first->second;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -721,7 +721,7 @@ namespace spot
|
||||||
/// Check whether the language of the automaton is empty.
|
/// Check whether the language of the automaton is empty.
|
||||||
virtual bool is_empty() const;
|
virtual bool is_empty() const;
|
||||||
|
|
||||||
protected:
|
private:
|
||||||
acc_cond acc_;
|
acc_cond acc_;
|
||||||
|
|
||||||
void set_num_sets_(unsigned num)
|
void set_num_sets_(unsigned num)
|
||||||
|
|
|
||||||
|
|
@ -386,7 +386,7 @@ namespace spot
|
||||||
bdd cond, bool acc = true)
|
bdd cond, bool acc = true)
|
||||||
{
|
{
|
||||||
if (acc)
|
if (acc)
|
||||||
return g_.new_edge(src, dst, cond, acc_.all_sets());
|
return g_.new_edge(src, dst, cond, this->acc().all_sets());
|
||||||
else
|
else
|
||||||
return g_.new_edge(src, dst, cond);
|
return g_.new_edge(src, dst, cond);
|
||||||
}
|
}
|
||||||
|
|
@ -459,7 +459,7 @@ namespace spot
|
||||||
for (auto& t: g_.out(s))
|
for (auto& t: g_.out(s))
|
||||||
// Stop at the first edge, since the remaining should be
|
// Stop at the first edge, since the remaining should be
|
||||||
// labeled identically.
|
// labeled identically.
|
||||||
return acc_.accepting(t.acc);
|
return acc().accepting(t.acc);
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1061,18 +1061,18 @@ namespace spot
|
||||||
assert(safra_ || !"safra construction fails");
|
assert(safra_ || !"safra construction fails");
|
||||||
|
|
||||||
#if TRANSFORM_TO_TBA
|
#if TRANSFORM_TO_TBA
|
||||||
the_acceptance_cond_ = acc_.mark(acc_.add_set());
|
the_acceptance_cond_ = set_buchi();
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
#if TRANSFORM_TO_TGBA
|
#if TRANSFORM_TO_TGBA
|
||||||
unsigned nb_acc =
|
unsigned nb_acc =
|
||||||
static_cast<safra_tree_automaton*>(safra_)->get_nb_acceptance_pairs();
|
static_cast<safra_tree_automaton*>(safra_)->get_nb_acceptance_pairs();
|
||||||
|
|
||||||
|
set_generalized_buchi(nb_acc);
|
||||||
acceptance_cond_vec_.reserve(nb_acc);
|
acceptance_cond_vec_.reserve(nb_acc);
|
||||||
for (unsigned i = 0; i < nb_acc; ++i)
|
for (unsigned i = 0; i < nb_acc; ++i)
|
||||||
acceptance_cond_vec_.push_back(acc_.mark(acc_.add_set()));
|
acceptance_cond_vec_.emplace_back(acc_cond::mark_t{i});
|
||||||
#endif
|
#endif
|
||||||
acc_.set_generalized_buchi();
|
|
||||||
}
|
}
|
||||||
|
|
||||||
tgba_safra_complement::~tgba_safra_complement()
|
tgba_safra_complement::~tgba_safra_complement()
|
||||||
|
|
|
||||||
|
|
@ -210,9 +210,8 @@ namespace spot
|
||||||
: twa(a->get_dict()), a_(a), aps_(atomic_propositions)
|
: twa(a->get_dict()), a_(a), aps_(atomic_propositions)
|
||||||
{
|
{
|
||||||
get_dict()->register_all_propositions_of(&a_, this);
|
get_dict()->register_all_propositions_of(&a_, this);
|
||||||
assert(acc_.num_sets() == 0);
|
assert(num_sets() == 0);
|
||||||
acc_.add_sets(a_->num_sets());
|
set_generalized_buchi(a_->num_sets());
|
||||||
acc_.set_generalized_buchi();
|
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual const state* get_init_state() const override
|
virtual const state* get_init_state() const override
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue