bdddict.hh 9.56 KB
 Alexandre Duret-Lutz committed May 20, 2012 1 ``````// -*- coding: utf-8 -*- `````` Alexandre Duret-Lutz committed Feb 20, 2013 2 ``````// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et Développement `````` Alexandre Duret-Lutz committed May 20, 2012 3 ``````// de l'Epita (LRDE). `````` 4 ``````// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), `````` Alexandre Duret-Lutz committed May 20, 2012 5 ``````// département Systèmes Répartis Coopératifs (SRC), Université Pierre `````` 6 ``````// et Marie Curie. `````` Alexandre Duret-Lutz committed Nov 21, 2003 7 8 9 10 11 ``````// // 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 12 ``````// the Free Software Foundation; either version 3 of the License, or `````` Alexandre Duret-Lutz committed Nov 21, 2003 13 14 15 16 17 18 19 20 ``````// (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 21 ``````// along with this program. If not, see . `````` Alexandre Duret-Lutz committed Nov 21, 2003 22 `````` `````` Alexandre Duret-Lutz committed Jul 14, 2003 23 24 25 26 27 ``````#ifndef SPOT_TGBA_BDDDICT_HH # define SPOT_TGBA_BDDDICT_HH #include #include `````` Alexandre Duret-Lutz committed Dec 15, 2004 28 ``````#include `````` Alexandre Duret-Lutz committed Aug 09, 2004 29 ``````#include `````` Alexandre Duret-Lutz committed Jul 14, 2003 30 ``````#include `````` Alexandre Duret-Lutz committed May 20, 2012 31 ``````#include `````` 32 ``````#include "ltlast/formula.hh" `````` Alexandre Duret-Lutz committed Jul 14, 2003 33 34 35 `````` namespace spot { `````` Alexandre Duret-Lutz committed Jul 29, 2013 36 37 `````` /// \brief Private data for bdd_dict. class bdd_dict_priv; `````` Alexandre Duret-Lutz committed Jul 14, 2003 38 `````` `````` Alexandre Duret-Lutz committed Nov 16, 2004 39 `````` /// \ingroup tgba_essentials `````` Alexandre Duret-Lutz committed Feb 21, 2011 40 41 42 43 44 45 46 47 `````` /// \brief Map BDD variables to formulae. /// /// The BDD library uses integers to designate Boolean variables in /// its decision diagrams. This class is used to map such integers /// to objects actually used in Spot. These objects are usually /// atomic propositions, but they can also be acceptance conditions, /// or "Now/Next" variables (although the latter should be /// eventually removed). `````` Alexandre Duret-Lutz committed Feb 20, 2013 48 49 50 51 52 53 54 55 56 `````` /// /// When a BDD variable is registered using a bdd_dict, it is always /// associated to a "user" (or "owner") object. This is done by /// supplying the bdd_dict with a pointer to the intended user of /// the variable. When the user object dies, it should release the /// BDD variables it was using by calling (for instance) /// unregister_all_my_variables(), giving the same pointer. /// Variables can also by unregistered one by one using /// unregister_variable(). `````` Alexandre Duret-Lutz committed Jul 29, 2013 57 `````` class SPOT_API bdd_dict `````` Alexandre Duret-Lutz committed Jul 14, 2003 58 `````` { `````` Alexandre Duret-Lutz committed Jul 29, 2013 59 `````` bdd_dict_priv* priv_; `````` Alexandre Duret-Lutz committed Jul 14, 2003 60 61 62 `````` public: bdd_dict(); `````` Alexandre Duret-Lutz committed Feb 20, 2013 63 64 65 66 67 `````` /// \brief Destroy the BDD dict. /// /// This always calls assert_emptiness() to diagnose cases where /// variables have not been unregistered. `````` Alexandre Duret-Lutz committed Jul 14, 2003 68 69 70 `````` ~bdd_dict(); /// Formula-to-BDD-variable maps. `````` 71 `````` typedef std::map fv_map; `````` Alexandre Duret-Lutz committed Jul 14, 2003 72 `````` /// BDD-variable-to-formula maps. `````` 73 `````` typedef std::map vf_map; `````` Alexandre Duret-Lutz committed Jul 14, 2003 74 75 `````` fv_map now_map; ///< Maps formulae to "Now" BDD variables `````` Alexandre Duret-Lutz committed Aug 10, 2003 76 `````` fv_map var_map; ///< Maps atomic propositions to BDD variables `````` Alexandre Duret-Lutz committed Nov 28, 2003 77 `````` fv_map acc_map; ///< Maps acceptance conditions to BDD variables `````` Alexandre Duret-Lutz committed Jul 14, 2003 78 `````` `````` Alexandre Duret-Lutz committed May 20, 2012 79 80 81 82 83 84 85 86 87 88 89 90 91 92 `````` /// BDD-variable reference counts. typedef std::set ref_set; enum var_type { anon = 0, now, next, var, acc }; struct bdd_info { bdd_info() : type(anon) {} var_type type; const ltl::formula* f; // Used unless t==anon. ref_set refs; int clone_counts; }; typedef std::vector bdd_info_map; // Map BDD variables to their meaning. bdd_info_map bdd_map; `````` Alexandre Duret-Lutz committed Feb 25, 2008 93 `````` `````` Alexandre Duret-Lutz committed Jul 14, 2003 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 `````` /// \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. `````` 113 `````` int register_proposition(const ltl::formula* f, const void* for_me); `````` Alexandre Duret-Lutz committed Jul 14, 2003 114 `````` `````` Alexandre Duret-Lutz committed Nov 14, 2003 115 116 117 118 119 120 121 122 123 `````` /// \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 124 125 126 127 128 129 130 131 132 133 134 `````` /// \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. `````` 135 `````` int register_state(const ltl::formula* f, const void* for_me); `````` Alexandre Duret-Lutz committed Jul 14, 2003 136 137 138 139 `````` /// \brief Register an atomic proposition. /// /// Return (and maybe allocate) a BDD variable designating an `````` Alexandre Duret-Lutz committed Nov 28, 2003 140 `````` /// acceptance set associated to formula \a f. The \a for_me `````` Alexandre Duret-Lutz committed Jul 14, 2003 141 142 143 144 145 146 `````` /// 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. `````` 147 `````` int register_acceptance_variable(const ltl::formula* f, const void* for_me); `````` Alexandre Duret-Lutz committed Jul 14, 2003 148 `````` `````` Alexandre Duret-Lutz committed Feb 25, 2008 149 150 151 152 153 154 155 `````` /// \brief Clone an acceptance variable VAR for FOR_ME. /// /// This is used in products TGBAs when both operands share the /// same acceptance variables but they need to be distinguished in /// the result. int register_clone_acc(int var, const void* for_me); `````` Alexandre Duret-Lutz committed Nov 28, 2003 156 `````` /// \brief Register BDD variables as acceptance variables. `````` Alexandre Duret-Lutz committed Nov 14, 2003 157 `````` /// `````` Alexandre Duret-Lutz committed Nov 28, 2003 158 159 `````` /// 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 160 `````` /// are already known from the dictionary (i.e., they have already `````` Alexandre Duret-Lutz committed Nov 28, 2003 161 `````` /// been registered by register_acceptance_variable() for another `````` Alexandre Duret-Lutz committed Nov 14, 2003 162 `````` /// automaton). `````` Alexandre Duret-Lutz committed Nov 28, 2003 163 `````` void register_acceptance_variables(bdd f, const void* for_me); `````` Alexandre Duret-Lutz committed Nov 14, 2003 164 `````` `````` Alexandre Duret-Lutz committed May 22, 2012 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 `````` /// \brief Convert one acceptance condition into the associated /// formula. /// /// This version accepts a conjunction of Acc variables, in which /// only one must be positive. This positive variable will be /// converted back into the associated formula. /// /// The returned formula is not cloned, and is valid until the BDD /// variable used in \a oneacc are unregistered. const ltl::formula* oneacc_to_formula(bdd oneacc) const; /// \brief Convert one acceptance condition into the associated /// formula. /// /// This version takes the number of a BDD variable that must has /// been returned by a call to register_acceptance_variable(). /// /// The returned formula is not cloned, and is valid until the BDD /// variable \a var is unregistered. const ltl::formula* oneacc_to_formula(int var) const; `````` Alexandre Duret-Lutz committed Mar 23, 2004 186 187 188 189 190 191 192 193 194 `````` /// \brief Register anonymous BDD variables. /// /// Return (and maybe allocate) \a n consecutive BDD variables which /// will be used only by \a for_me. /// /// \return The variable number. Use bdd_ithvar() or bdd_nithvar() /// to convert this to a BDD. int register_anonymous_variables(int n, const void* for_me); `````` Alexandre Duret-Lutz committed Jul 14, 2003 195 196 197 198 199 200 201 202 `````` /// \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); `````` Alexandre Duret-Lutz committed Mar 25, 2004 203 `````` /// \brief Release all variables used by an object. `````` Alexandre Duret-Lutz committed Jul 14, 2003 204 205 206 `````` /// /// Usually called in the destructor if \a me. void unregister_all_my_variables(const void* me); `````` Alexandre Duret-Lutz committed May 12, 2013 207 208 209 210 `````` /// \brief Release all variables of a given type, used by an /// object. void unregister_all_typed_variables(var_type type, const void* me); `````` Alexandre Duret-Lutz committed Jul 14, 2003 211 `````` `````` Alexandre Duret-Lutz committed Mar 25, 2004 212 213 214 `````` /// \brief Release a variable used by \a me. void unregister_variable(int var, const void* me); `````` Alexandre Duret-Lutz committed Aug 15, 2003 215 `````` /// @{ `````` Alexandre Duret-Lutz committed Jul 14, 2003 216 `````` /// Check whether formula \a f has already been registered by \a by_me. `````` 217 218 219 `````` bool is_registered_proposition(const ltl::formula* f, const void* by_me); bool is_registered_state(const ltl::formula* f, const void* by_me); bool is_registered_acceptance_variable(const ltl::formula* f, `````` Alexandre Duret-Lutz committed Mar 23, 2004 220 `````` const void* by_me); `````` Alexandre Duret-Lutz committed Aug 15, 2003 221 `````` /// @} `````` Alexandre Duret-Lutz committed Jul 14, 2003 222 223 224 225 226 227 228 `````` /// \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. /// `````` Alexandre Duret-Lutz committed Feb 20, 2013 229 230 231 232 233 234 235 236 237 `````` /// This will print diagnostics if the dictionary is not empty. /// Use for debugging. This is called automatically by the /// destructor. When Spot is compiled in development mode (i.e., /// with ./configure --enable-devel), this function /// will abort if the dictionary is not empty. /// /// The errors detected by this function usually indicate missing /// calls to unregister_variable() or /// unregister_all_my_variables(). `````` Alexandre Duret-Lutz committed Jul 14, 2003 238 239 240 241 `````` void assert_emptiness() const; private: // Disallow copy. `````` Alexandre Duret-Lutz committed Feb 12, 2014 242 243 `````` bdd_dict(const bdd_dict& other) SPOT_DELETED; bdd_dict& operator=(const bdd_dict& other) SPOT_DELETED; `````` Alexandre Duret-Lutz committed Jul 14, 2003 244 245 246 247 248 249 `````` }; } #endif // SPOT_TGBA_BDDDICT_HH``````