From 37a6b601c1c5e06a52d47b32f80d874b417326e4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 12 Apr 2012 17:22:08 +0200 Subject: [PATCH] Declare the sba class in its own header. * src/tgba/sba.hh: New file, extrated from... * src/tgba/tgbaexplicit.hh: ... here. Also rename sba_explicit::is_accepting as sba_explicit::state_is_accepting for consistency with tgba_sba_proxy. * src/tgbatest/explicit2.cc: Adjust to the renaming. * src/tgba/Makefile.am: Add sba.hh. --- src/tgba/Makefile.am | 5 +++-- src/tgba/sba.hh | 45 +++++++++++++++++++++++++++++++++++++++ src/tgba/tgbaexplicit.hh | 23 +++++++------------- src/tgbatest/explicit2.cc | 16 +++++++------- 4 files changed, 64 insertions(+), 25 deletions(-) create mode 100644 src/tgba/sba.hh diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 484194e5b..1d762a429 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -1,5 +1,5 @@ -## Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -## de l'Epita (LRDE). +## Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +## Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. @@ -32,6 +32,7 @@ tgba_HEADERS = \ formula2bdd.hh \ futurecondcol.hh \ public.hh \ + sba.hh \ state.hh \ statebdd.hh \ succiter.hh \ diff --git a/src/tgba/sba.hh b/src/tgba/sba.hh new file mode 100644 index 000000000..31f72ce65 --- /dev/null +++ b/src/tgba/sba.hh @@ -0,0 +1,45 @@ +// Copyright (C) 2012 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBA_SBA_HH +# define SPOT_TGBA_SBA_HH + +#include "tgba.hh" + +namespace spot +{ + /// \brief A State-based Generalized Büchi Automaton. + /// \ingroup tgba_essentials + /// + /// An SBA is a TGBA in which the outgoing transitions of + /// a state are either all accepting (in which case the + /// source state is said "accepting"(, or all non-accepting. + class sba: public tgba + { + public: + /// \brief is \a s an accepting state? + /// + /// If a state is accepting all its outgoing transitions are + /// accepting. + virtual bool state_is_accepting(const spot::state* s) const = 0; + }; +} + +#endif // SPOT_TGBA_SBA_HH diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 420d8f446..bffb5c718 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -29,6 +29,7 @@ #include #include "tgba.hh" +#include "sba.hh" #include "tgba/formula2bdd.hh" #include "misc/hash.hh" #include "misc/bddop.hh" @@ -37,7 +38,7 @@ namespace spot { - ///misc + // How to destroy the label of a state. template struct destroy_key { @@ -56,14 +57,6 @@ namespace spot } }; - class sba: public tgba - { - public: - /// A State in an SBA (State-based Buchi Automaton) is accepting - /// iff all outgoing transitions are accepting. - virtual bool is_accepting(const spot::state* s) const = 0; - }; - /// States used by spot::explicit_graph implementation /// \ingroup tgba_representation template @@ -140,7 +133,7 @@ namespace spot Label label_; }; - ///states labeled by an int + /// States labeled by an int /// \ingroup tgba_representation class state_explicit_number: public state_explicit > @@ -721,10 +714,10 @@ namespace spot { } - /// Assume that an accepting state has only accepting output transitions - /// So we need only to check one to decide - virtual bool is_accepting(const spot::state* s) const + virtual bool state_is_accepting(const spot::state* s) const { + // Assume that an accepting state has only accepting output transitions + // So we need only to check one to decide tgba_explicit_succ_iterator* it = this->succ_iter(s); it->first(); @@ -748,12 +741,12 @@ namespace spot }; - /// Typedefs for tgba + // Typedefs for tgba typedef tgba_explicit tgba_explicit_string; typedef tgba_explicit tgba_explicit_formula; typedef tgba_explicit tgba_explicit_number; - /// Typedefs for sba + // Typedefs for sba typedef sba_explicit sba_explicit_string; typedef sba_explicit sba_explicit_formula; typedef sba_explicit sba_explicit_number; diff --git a/src/tgbatest/explicit2.cc b/src/tgbatest/explicit2.cc index 87fa19d7a..68668a9fd 100644 --- a/src/tgbatest/explicit2.cc +++ b/src/tgbatest/explicit2.cc @@ -121,9 +121,9 @@ void create_sba_explicit_string(bdd_dict* d) t = sba->create_transition(s1, s3); sba->add_acceptance_conditions(t, bdd_ithvar(v)); - std::cout << "S1 ACCEPTING? " << sba->is_accepting (s1) << std::endl; - std::cout << "S2 ACCEPTING? " << sba->is_accepting (s2) << std::endl; - std::cout << "S3 ACCEPTING? " << sba->is_accepting (s3) << std::endl; + std::cout << "S1 ACCEPTING? " << sba->state_is_accepting(s1) << std::endl; + std::cout << "S2 ACCEPTING? " << sba->state_is_accepting(s2) << std::endl; + std::cout << "S3 ACCEPTING? " << sba->state_is_accepting(s3) << std::endl; delete sba; } @@ -143,8 +143,8 @@ void create_sba_explicit_number(bdd_dict* d) sba->create_transition(s1, s2); sba->add_acceptance_conditions(t, bdd_ithvar(v)); - std::cout << "S1 ACCEPTING? " << sba->is_accepting (s1) << std::endl; - std::cout << "S2 ACCEPTING? " << sba->is_accepting (s2) << std::endl; + std::cout << "S1 ACCEPTING? " << sba->state_is_accepting(s1) << std::endl; + std::cout << "S2 ACCEPTING? " << sba->state_is_accepting(s2) << std::endl; delete sba; } @@ -169,9 +169,9 @@ create_sba_explicit_formula(bdd_dict* d, spot::ltl::default_environment& e) t = sba->create_transition(s1, s3); sba->add_acceptance_conditions(t, bdd_ithvar(v)); - std::cout << "S1 ACCEPTING? " << sba->is_accepting (s1) << std::endl; - std::cout << "S2 ACCEPTING? " << sba->is_accepting (s2) << std::endl; - std::cout << "S3 ACCEPTING? " << sba->is_accepting (s3) << std::endl; + std::cout << "S1 ACCEPTING? " << sba->state_is_accepting(s1) << std::endl; + std::cout << "S2 ACCEPTING? " << sba->state_is_accepting(s2) << std::endl; + std::cout << "S3 ACCEPTING? " << sba->state_is_accepting(s3) << std::endl; delete sba; }