From aebe6593f9e7a687bf21d84d5ac2f0026e888077 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 2 Feb 2016 16:55:51 +0100 Subject: [PATCH] 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. --- spot/ta/ta.hh | 4 ++-- spot/twa/taatgba.cc | 6 +++--- spot/twa/taatgba.hh | 4 ++-- spot/twa/twa.hh | 2 +- spot/twa/twagraph.hh | 4 ++-- spot/twa/twasafracomplement.cc | 6 +++--- spot/twaalgos/stutter.cc | 5 ++--- 7 files changed, 15 insertions(+), 16 deletions(-) diff --git a/spot/ta/ta.hh b/spot/ta/ta.hh index 443b3bc10..a7d503c8a 100644 --- a/spot/ta/ta.hh +++ b/spot/ta/ta.hh @@ -1,5 +1,5 @@ // -*- 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). // // 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 is an abstract interface. Its implementations are \ref /// 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". /// \addtogroup ta_essentials Essential TA types diff --git a/spot/twa/taatgba.cc b/spot/twa/taatgba.cc index a133d753a..3cfd38c29 100644 --- a/spot/twa/taatgba.cc +++ b/spot/twa/taatgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire -// de Recherche et Développement de l'Epita (LRDE) +// Copyright (C) 2009, 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. // @@ -63,7 +63,7 @@ namespace spot { const spot::set_state* s = down_cast(state); assert(s); - return new taa_succ_iterator(s->get_state(), acc_); + return new taa_succ_iterator(s->get_state(), acc()); } bdd diff --git a/spot/twa/taatgba.hh b/spot/twa/taatgba.hh index a720c6aac..2139009d2 100644 --- a/spot/twa/taatgba.hh +++ b/spot/twa/taatgba.hh @@ -1,5 +1,5 @@ // -*- 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). // // This file is part of Spot, a model checking library. @@ -196,7 +196,7 @@ namespace spot { auto p = acc_map_.emplace(f, 0); 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; } diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index fd7a5cd05..488057b06 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -721,7 +721,7 @@ namespace spot /// Check whether the language of the automaton is empty. virtual bool is_empty() const; - protected: + private: acc_cond acc_; void set_num_sets_(unsigned num) diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index a4591ccf4..3df6fdfd3 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -386,7 +386,7 @@ namespace spot bdd cond, bool acc = true) { if (acc) - return g_.new_edge(src, dst, cond, acc_.all_sets()); + return g_.new_edge(src, dst, cond, this->acc().all_sets()); else return g_.new_edge(src, dst, cond); } @@ -459,7 +459,7 @@ namespace spot for (auto& t: g_.out(s)) // Stop at the first edge, since the remaining should be // labeled identically. - return acc_.accepting(t.acc); + return acc().accepting(t.acc); return false; } diff --git a/spot/twa/twasafracomplement.cc b/spot/twa/twasafracomplement.cc index 955f5fa3c..54237e483 100644 --- a/spot/twa/twasafracomplement.cc +++ b/spot/twa/twasafracomplement.cc @@ -1061,18 +1061,18 @@ namespace spot assert(safra_ || !"safra construction fails"); #if TRANSFORM_TO_TBA - the_acceptance_cond_ = acc_.mark(acc_.add_set()); + the_acceptance_cond_ = set_buchi(); #endif #if TRANSFORM_TO_TGBA unsigned nb_acc = static_cast(safra_)->get_nb_acceptance_pairs(); + set_generalized_buchi(nb_acc); acceptance_cond_vec_.reserve(nb_acc); 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 - acc_.set_generalized_buchi(); } tgba_safra_complement::~tgba_safra_complement() diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index fb77b4a45..8b03e79c4 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -210,9 +210,8 @@ namespace spot : twa(a->get_dict()), a_(a), aps_(atomic_propositions) { get_dict()->register_all_propositions_of(&a_, this); - assert(acc_.num_sets() == 0); - acc_.add_sets(a_->num_sets()); - acc_.set_generalized_buchi(); + assert(num_sets() == 0); + set_generalized_buchi(a_->num_sets()); } virtual const state* get_init_state() const override