bdddict.hh 6.3 KB
 Alexandre Duret-Lutz committed Nov 21, 2003 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 ``````// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // 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. `````` Alexandre Duret-Lutz committed Jul 14, 2003 22 23 24 ``````#ifndef SPOT_TGBA_BDDDICT_HH # define SPOT_TGBA_BDDDICT_HH `````` Alexandre Duret-Lutz committed Aug 28, 2003 25 ``````#include "misc/hash.hh" `````` Alexandre Duret-Lutz committed Jul 14, 2003 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 ``````#include #include #include #include #include "ltlast/formula.hh" #include "misc/bddalloc.hh" namespace spot { /// Map BDD variables to formulae. class bdd_dict: public bdd_allocator { public: bdd_dict(); ~bdd_dict(); /// Formula-to-BDD-variable maps. `````` Alexandre Duret-Lutz committed Aug 28, 2003 45 46 `````` typedef Sgi::hash_map > fv_map; `````` Alexandre Duret-Lutz committed Jul 14, 2003 47 `````` /// BDD-variable-to-formula maps. `````` Alexandre Duret-Lutz committed Aug 28, 2003 48 `````` typedef Sgi::hash_map vf_map; `````` Alexandre Duret-Lutz committed Jul 14, 2003 49 50 51 `````` fv_map now_map; ///< Maps formulae to "Now" BDD variables vf_map now_formula_map; ///< Maps "Now" BDD variables to formulae `````` Alexandre Duret-Lutz committed Aug 10, 2003 52 53 `````` fv_map var_map; ///< Maps atomic propositions to BDD variables vf_map var_formula_map; ///< Maps BDD variables to atomic propositions `````` Alexandre Duret-Lutz committed Nov 28, 2003 54 55 `````` fv_map acc_map; ///< Maps acceptance conditions to BDD variables vf_map acc_formula_map; ///< Maps BDD variables to acceptance conditions `````` Alexandre Duret-Lutz committed Jul 14, 2003 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 `````` /// \brief Map Next variables to Now variables. /// /// Use with BuDDy's bdd_replace() function. bddPair* next_to_now; /// \brief Map Now variables to Next variables. /// /// Use with BuDDy's bdd_replace() function. bddPair* now_to_next; /// \brief Register an atomic proposition. /// /// Return (and maybe allocate) a BDD variable designating formula /// \a f. The \a for_me argument should point to the object using /// this BDD variable, this is used for reference counting. It is /// perfectly safe to call this function several time with the same /// arguments. /// /// \return The variable number. Use bdd_ithvar() or bdd_nithvar() /// to convert this to a BDD. int register_proposition(const ltl::formula* f, const void* for_me); `````` Alexandre Duret-Lutz committed Nov 14, 2003 78 79 80 81 82 83 84 85 86 `````` /// \brief Register BDD variables as atomic propositions. /// /// Register all variables occurring in \a f as atomic propositions /// used by \a for_me. This assumes that these atomic propositions /// are already known from the dictionary (i.e., they have already /// been registered by register_proposition() for another /// automaton). void register_propositions(bdd f, const void* for_me); `````` Alexandre Duret-Lutz committed Jul 14, 2003 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 `````` /// \brief Register a couple of Now/Next variables /// /// Return (and maybe allocate) two BDD variables for a state /// associated to formula \a f. The \a for_me argument should point /// to the object using this BDD variable, this is used for /// reference counting. It is perfectly safe to call this /// function several time with the same arguments. /// /// \return The first variable number. Add one to get the second /// variable. Use bdd_ithvar() or bdd_nithvar() to convert this /// to a BDD. int register_state(const ltl::formula* f, const void* for_me); /// \brief Register an atomic proposition. /// /// Return (and maybe allocate) a BDD variable designating an `````` Alexandre Duret-Lutz committed Nov 28, 2003 103 `````` /// acceptance set associated to formula \a f. The \a for_me `````` Alexandre Duret-Lutz committed Jul 14, 2003 104 105 106 107 108 109 `````` /// argument should point to the object using this BDD variable, /// this is used for reference counting. It is perfectly safe to /// call this function several time with the same arguments. /// /// \return The variable number. Use bdd_ithvar() or bdd_nithvar() /// to convert this to a BDD. `````` Alexandre Duret-Lutz committed Nov 28, 2003 110 `````` int register_acceptance_variable(const ltl::formula* f, const void* for_me); `````` Alexandre Duret-Lutz committed Jul 14, 2003 111 `````` `````` Alexandre Duret-Lutz committed Nov 28, 2003 112 `````` /// \brief Register BDD variables as acceptance variables. `````` Alexandre Duret-Lutz committed Nov 14, 2003 113 `````` /// `````` Alexandre Duret-Lutz committed Nov 28, 2003 114 115 `````` /// Register all variables occurring in \a f as acceptance variables /// used by \a for_me. This assumes that these acceptance variables `````` Alexandre Duret-Lutz committed Nov 14, 2003 116 `````` /// are already known from the dictionary (i.e., they have already `````` Alexandre Duret-Lutz committed Nov 28, 2003 117 `````` /// been registered by register_acceptance_variable() for another `````` Alexandre Duret-Lutz committed Nov 14, 2003 118 `````` /// automaton). `````` Alexandre Duret-Lutz committed Nov 28, 2003 119 `````` void register_acceptance_variables(bdd f, const void* for_me); `````` Alexandre Duret-Lutz committed Nov 14, 2003 120 `````` `````` Alexandre Duret-Lutz committed Jul 14, 2003 121 122 123 124 125 126 127 128 129 130 131 132 133 `````` /// \brief Duplicate the variable usage of another object. /// /// This tells this dictionary that the \a for_me object /// will be using the same BDD variables as the \a from_other objects. /// This ensure that the variables won't be freed when \a from_other /// is deleted if \a from_other is still alive. void register_all_variables_of(const void* from_other, const void* for_me); /// \brief Release the variables used by object. /// /// Usually called in the destructor if \a me. void unregister_all_my_variables(const void* me); `````` Alexandre Duret-Lutz committed Aug 15, 2003 134 `````` /// @{ `````` Alexandre Duret-Lutz committed Jul 14, 2003 135 `````` /// Check whether formula \a f has already been registered by \a by_me. `````` Alexandre Duret-Lutz committed Aug 15, 2003 136 137 `````` bool is_registered_proposition(const ltl::formula* f, const void* by_me); bool is_registered_state(const ltl::formula* f, const void* by_me); `````` Alexandre Duret-Lutz committed Nov 28, 2003 138 `````` bool is_registered_acceptance_variable(const ltl::formula* f, `````` Alexandre Duret-Lutz committed Aug 15, 2003 139 140 `````` const void* by_me); /// @} `````` Alexandre Duret-Lutz committed Jul 14, 2003 141 142 143 144 145 146 147 148 149 150 151 152 153 `````` /// \brief Dump all variables for debugging. /// \param os The output stream. std::ostream& dump(std::ostream& os) const; /// \brief Make sure the dictionary is empty. /// /// This will print diagnostics and abort if the dictionary /// is not empty. Use for debugging. void assert_emptiness() const; protected: /// BDD-variable reference counts. `````` Alexandre Duret-Lutz committed Aug 28, 2003 154 155 `````` typedef Sgi::hash_set > ref_set; typedef Sgi::hash_map vr_map; `````` Alexandre Duret-Lutz committed Jul 14, 2003 156 157 158 159 160 161 162 163 164 165 166 167 `````` vr_map var_refs; private: // Disallow copy. bdd_dict(const bdd_dict& other); bdd_dict& operator=(const bdd_dict& other); }; } #endif // SPOT_TGBA_BDDDICT_HH``````