From ddf05b5d47094fc459278c6226670c7ce2713352 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 27 May 2003 14:42:58 +0000 Subject: [PATCH] * src/tgba/bddfactory.hh, src/tgba/statebdd.hh, src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add Doxygen comments. --- ChangeLog | 5 +++ src/tgba/bddfactory.hh | 43 ++++++++++++++++++++----- src/tgba/statebdd.hh | 4 ++- src/tgba/succiterconcrete.hh | 17 +++++++--- src/tgba/tgbabddconcrete.hh | 33 ++++++++++++++++--- src/tgba/tgbabddcoredata.hh | 62 ++++++++++++++++++++++-------------- src/tgba/tgbabdddict.hh | 22 +++++++------ 7 files changed, 135 insertions(+), 51 deletions(-) diff --git a/ChangeLog b/ChangeLog index c98e0c0d4..060df3f70 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,10 @@ 2003-05-27 Alexandre Duret-Lutz + * src/tgba/bddfactory.hh, src/tgba/statebdd.hh, + src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh, + src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add + Doxygen comments. + * src/tgba/bddprint.hh (bdd_format_set): New function. * src/tgba/bddprint.cc (bdd_format_set): Likewise. * src/tgba/state.hh: Add Doxygen comments. diff --git a/src/tgba/bddfactory.hh b/src/tgba/bddfactory.hh index 29b504b08..bde475499 100644 --- a/src/tgba/bddfactory.hh +++ b/src/tgba/bddfactory.hh @@ -6,27 +6,54 @@ namespace spot { + /// \brief Help construct BDDs by reusing existing variables. + /// + /// Spot uses BuDDy as BDD library, and BuDDy needs to + /// know the number of BDD variables in use. As a rule + /// of thumb: the more BDD variables the slowere. So + /// creating new BDD variables each time we build a new + /// Automata won't do. + /// + /// To avoid variable explosion, we reuse existing variables + /// when building new automata, and only allocate new variables + /// when we ran out of existing variables. This class helps + /// reusing variables this way. + /// + /// Using the same variables in different automata is not a + /// problem until an operation is performed on both automata. + /// In this case some homogenization of BDD variable will be + /// required. Such operation is out of the scope of this class. class bdd_factory { public: bdd_factory(); + /// \brief Allocate a BDD variable. + /// + /// The returned integer can be converted to a BDD using ithvar(). int create_node(); + + /// \brief Allocate a pair BDD variable. + /// + /// The returned integer is the first variable of the pair, + /// it's successor (i.e., n + 1) is the second variable. + /// They can be converted to BDDs using ithvar(). int create_pair(); - + + /// Convert a variable number into a BDD. static bdd ithvar(int i) { return bdd_ithvar(i); } - + protected: - static void initialize(); - int create_nodes(int i); - - static bool initialized; - static int varnum; - int varused; + static void initialize(); ///< Initialize the BDD library. + int create_nodes(int i); ///< Create \a i variables. + + static bool initialized; ///< Whether the BDD library has been initialized. + static int varnum; ///< number of variable in use in the BDD library. + int varused; ///< Number of variables used for this construction. }; } diff --git a/src/tgba/statebdd.hh b/src/tgba/statebdd.hh index fdc84b0b6..2f508c374 100644 --- a/src/tgba/statebdd.hh +++ b/src/tgba/statebdd.hh @@ -6,6 +6,7 @@ namespace spot { + /// A state whose representation is a BDD. class state_bdd: public state { public: @@ -14,6 +15,7 @@ namespace spot { } + /// Return the BDD part of the state. bdd as_bdd() const { @@ -23,7 +25,7 @@ namespace spot virtual int compare(const state* other) const; protected: - bdd state_; + bdd state_; ///< BDD representation of the state. }; } diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh index 339ac5625..2e4b13f86 100644 --- a/src/tgba/succiterconcrete.hh +++ b/src/tgba/succiterconcrete.hh @@ -7,9 +7,18 @@ namespace spot { + /// A concrete iterator over successors of a TGBA state. class tgba_succ_iterator_concrete: public tgba_succ_iterator { public: + /// \brief Build a spot::tgba_succ_iterator_concrete. + /// + /// \param successors The set of successors with ingoing conditions + /// and promises, represented as a BDD. The job of this iterator + /// will be to enumerate the satisfactions of that BDD and split + /// them into destination state, conditions, and promises. + /// \param d The core data of the automata. These contains + /// sets of variables useful to split a BDD. tgba_succ_iterator_concrete(const tgba_bdd_core_data& d, bdd successors); virtual ~tgba_succ_iterator_concrete(); @@ -24,10 +33,10 @@ namespace spot bdd current_promise(); private: - const tgba_bdd_core_data& data_; - bdd succ_set_; // The set of successors. - bdd next_succ_set_; // Unexplored successors (including current_). - bdd current_; // Current successor. + const tgba_bdd_core_data& data_; ///< Core data of the automata. + bdd succ_set_; ///< The set of successors. + bdd next_succ_set_; ///< Unexplored successors (including current_). + bdd current_; ///< Current successor. }; } diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh index 312a10dae..f4e7ff34f 100644 --- a/src/tgba/tgbabddconcrete.hh +++ b/src/tgba/tgbabddconcrete.hh @@ -8,15 +8,35 @@ namespace spot { + /// \brief A concrete spot::tgba implemented using BDDs. + /// class tgba_bdd_concrete: public tgba { public: + /// \brief Construct a tgba_bdd_concrete with unknown initial state. + /// + /// set_init_state() should be called later. tgba_bdd_concrete(const tgba_bdd_factory& fact); + + /// \brief Construct a tgba_bdd_concrete with known initial state. tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init); + ~tgba_bdd_concrete(); + /// \brief Set the initial state. void set_init_state(bdd s); + state_bdd* get_init_state() const; + + /// \brief Get the initial state directly as a BDD. + /// + /// The sole point of this method is to prevent writing + /// horrors such as + /// \code + /// state_bdd* s = automata.get_init_state(); + /// some_class some_instance(s->as_bdd()); + /// delete s; + /// \endcode bdd get_init_bdd() const; tgba_succ_iterator_concrete* succ_iter(const state* state) const; @@ -24,13 +44,18 @@ namespace spot std::string format_state(const state* state) const; const tgba_bdd_dict& get_dict() const; + + /// \brief Get the core data associated to this automaton. + /// + /// These data includes the various BDD used to represent + /// the relation, encode variable sets, Next-to-Now rewrite + /// rules, etc. const tgba_bdd_core_data& get_core_data() const; protected: - tgba_bdd_core_data data_; - tgba_bdd_dict dict_; - bdd init_; - friend class tgba_tgba_succ_iterator; + tgba_bdd_core_data data_; ///< Core data associated to the automaton. + tgba_bdd_dict dict_; ///< Dictionary used by the automaton. + bdd init_; ///< Initial state. }; } diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh index 08a35ef94..aac99c2e4 100644 --- a/src/tgba/tgbabddcoredata.hh +++ b/src/tgba/tgbabddcoredata.hh @@ -5,48 +5,62 @@ namespace spot { + /// Core data for a TGBA encoded using BDDs. struct tgba_bdd_core_data { - // RELATION encodes the transition relation of the TGBA. - // It uses four kinds of variables: - // - "Now" variables, that encode the current state - // - "Next" variables, that encode the destination state - // - atomic propositions, which are things to verify before going on - // to the next state - // - promises: a U b, or F b, both implie that b should be verified - // eventually. We encode this with Prom[b], and check - // that promises are fullfilled in the emptyness check. + /// \brief encodes the transition relation of the TGBA. + /// + /// \c relation uses four kinds of variables: + /// \li "Now" variables, that encode the current state + /// \li "Next" variables, that encode the destination state + /// \li atomic propositions, which are things to verify before going on + /// to the next state + /// \li promises: \c a \c U \c b, or \c F \cb, both imply that \c b + /// should be verified eventually. We encode this with \c Prom[b], + /// and check that promises are fullfilled in the emptyness check. bdd relation; - - // The conjunction of all Now variables, in their positive form. + + /// The conjunction of all Now variables, in their positive form. bdd now_set; - // The conjunction of all Now variables, in their negated form. + /// The conjunction of all Now variables, in their negated form. bdd negnow_set; - // The (positive) conjunction of all variables which are not Now variables. + /// \brief The (positive) conjunction of all variables which are + /// not Now variables. bdd notnow_set; - // The (positive) conjunction of all variables which are not atomic - // propositions. + /// \brief The (positive) conjunction of all variables which are + /// not atomic propositions. bdd notvar_set; - // The (positive) conjunction of all variables which are not promises. + /// The (positive) conjunction of all variables which are not promises. bdd notprom_set; - - // Record pairings between Next and Now variables. + + /// Record pairings between Next and Now variables. bddPair* next_to_now; - + /// \brief Default constructor. + /// + /// Initially all variable set are empty and the \c relation is true. tgba_bdd_core_data(); + + /// Copy constructor. tgba_bdd_core_data(const tgba_bdd_core_data& copy); - - // Merge two core_data. + + /// \brief Merge two tgba_bdd_core_data. + /// + /// This is used when building a product of two automata. tgba_bdd_core_data(const tgba_bdd_core_data& left, const tgba_bdd_core_data& right); - + const tgba_bdd_core_data& operator= (const tgba_bdd_core_data& copy); - + ~tgba_bdd_core_data(); - + + /// \brief Update the variable sets to take a new pair of variables into + /// account. void declare_now_next(bdd now, bdd next); + /// \brief Update the variable sets to take a new automic proposition into + /// account. void declare_atomic_prop(bdd var); + /// Update the variable sets to take a new promise into account. void declare_promise(bdd prom); }; } diff --git a/src/tgba/tgbabdddict.hh b/src/tgba/tgbabdddict.hh index 00e39314d..20a4d4d56 100644 --- a/src/tgba/tgbabdddict.hh +++ b/src/tgba/tgbabdddict.hh @@ -7,22 +7,24 @@ namespace spot { + + /// Dictionary of BDD variables. struct tgba_bdd_dict { - // Dictionaries for BDD variables. - - // formula-to-BDD-variable maps + /// Formula-to-BDD-variable maps. typedef std::map fv_map; - // BDD-variable-to-formula maps + /// BDD-variable-to-formula maps. typedef std::map vf_map; - fv_map now_map; - vf_map now_formula_map; - fv_map var_map; - vf_map var_formula_map; - fv_map prom_map; - vf_map prom_formula_map; + fv_map now_map; ///< Maps formulae to "Now" BDD variables. + vf_map now_formula_map; ///< Maps "Now" BDD variables to formulae. + fv_map var_map; ///< Maps atomic propisitions to BDD variables + vf_map var_formula_map; ///< Maps BDD variables to atomic propisitions + fv_map prom_map; ///< Maps promises to BDD variables. + vf_map prom_formula_map; ///< Maps BDD variables to promises. + /// \brief Dump all variables for debugging. + /// \param os The output stream. std::ostream& dump(std::ostream& os) const; }; }