saba.hh 4.2 KB
 Alexandre Duret-Lutz committed Jul 29, 2013 1 // -*- coding: utf-8 -*-  Alexandre Duret-Lutz committed Aug 15, 2014 2 // Copyright (C) 2009, 2010, 2013, 2014 Laboratoire de Recherche et  Alexandre Duret-Lutz committed Jul 29, 2013 3 // Développement de l'Epita (LRDE).  Guillaume Sadegh committed Nov 30, 2009 4 5 6 7 8 // // 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  Alexandre Duret-Lutz committed Oct 12, 2012 9 // the Free Software Foundation; either version 3 of the License, or  Guillaume Sadegh committed Nov 30, 2009 10 11 12 13 14 15 16 17 // (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  Alexandre Duret-Lutz committed Oct 12, 2012 18 // along with this program. If not, see .  Guillaume Sadegh committed Nov 30, 2009 19 20 21 22 23 24 25 26 27 28  #ifndef SPOT_SABA_SABA_HH # define SPOT_SABA_SABA_HH #include "sabastate.hh" #include "sabasucciter.hh" #include namespace spot {  Alexandre Duret-Lutz committed Jul 29, 2013 29  /// \defgroup saba SABA (State-based Alternating Büchi Automata)  Guillaume Sadegh committed Nov 30, 2009 30 31 32 33 34 35 36 37 38 39 40  /// /// Spot was centered around non-deterministic \ref tgba. /// Alternating automata are an extension to non-deterministic /// automata, and are presented with spot::saba. /// This type and its cousins are listed \ref saba_essentials "here". /// This is an abstract interface. /// \addtogroup saba_essentials Essential SABA types /// \ingroup saba /// \ingroup saba_essentials  Alexandre Duret-Lutz committed Jul 29, 2013 41  /// \brief A State-based Alternating (Generalized) Büchi Automaton.  Guillaume Sadegh committed Nov 30, 2009 42 43 44 45 46 47 48 49 50 51  /// /// Browsing such automaton can be achieved using two functions: /// \c get_init_state, and \c succ_iter. The former returns /// the initial state while the latter lists the /// successor states of any state. /// /// Note that although this is a transition-based automata, /// we never represent transitions! Transition informations are /// obtained by querying the iterator over the successors of /// a state.  Alexandre Duret-Lutz committed Jul 29, 2013 52  class SPOT_API saba  Guillaume Sadegh committed Nov 30, 2009 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87  { protected: saba(); public: virtual ~saba(); /// \brief Get the initial state of the automaton. /// /// The state has been allocated with \c new. It is the /// responsability of the caller to \c delete it when no /// longer needed. virtual saba_state* get_init_state() const = 0; /// \brief Get an iterator over the successors of \a local_state. /// /// The iterator has been allocated with \c new. It is the /// responsability of the caller to \c delete it when no /// longer needed. /// /// \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 delete it when /// appropriate (this can be done during the lifetime of /// the iterator). virtual saba_succ_iterator* succ_iter(const saba_state* local_state) const = 0; /// \brief Get the dictionary associated to the automaton. /// /// State are represented as BDDs. The dictionary allows /// to map BDD variables back to formulae, and vice versa. /// This is useful when dealing with several automata (which /// may use the same BDD variable for different formula), /// or simply when printing.  Alexandre Duret-Lutz committed Aug 13, 2014 88  virtual bdd_dict_ptr get_dict() const = 0;  Guillaume Sadegh committed Nov 30, 2009 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111  /// \brief Format the state as a string for printing. /// /// This formating is the responsability of the automata /// that owns the state. virtual std::string format_state(const saba_state* state) const = 0; /// \brief Return the set of all acceptance conditions used /// by this automaton. /// /// The goal of the emptiness check is to ensure that /// a strongly connected component walks through each /// of these acceptiong conditions. I.e., the union /// of the acceptiong conditions of all transition in /// the SCC should be equal to the result of this function. virtual bdd all_acceptance_conditions() const = 0; /// The number of acceptance conditions. virtual unsigned int number_of_acceptance_conditions() const; private: mutable int num_acc_; };  Alexandre Duret-Lutz committed Aug 15, 2014 112 113 114  typedef std::shared_ptr saba_ptr; typedef std::shared_ptr const_saba_ptr;  Guillaume Sadegh committed Nov 30, 2009 115 116 117 118 } // end namespace spot. #endif // SPOT_SABA_SABA_HH