bdddict.hh 7.47 KB
Newer Older
1
// Copyright (C) 2003, 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// 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.

22
23
24
25
26
#ifndef SPOT_TGBA_BDDDICT_HH
# define SPOT_TGBA_BDDDICT_HH

#include <list>
#include <set>
27
#include <map>
28
#include <iosfwd>
29
30
31
32
33
34
35
36
#include <bdd.h>
#include "ltlast/formula.hh"
#include "misc/bddalloc.hh"

namespace spot
{

  /// Map BDD variables to formulae.
37
  /// \ingroup tgba_essentials
38
39
40
41
42
43
44
45
  class bdd_dict: public bdd_allocator
  {
  public:

    bdd_dict();
    ~bdd_dict();

    /// Formula-to-BDD-variable maps.
46
    typedef std::map<const ltl::formula*, int> fv_map;
47
    /// BDD-variable-to-formula maps.
48
    typedef std::map<int, const ltl::formula*> vf_map;
49
50
51

    fv_map now_map;		///< Maps formulae to "Now" BDD variables
    vf_map now_formula_map;	///< Maps "Now" BDD variables to formulae
52
53
    fv_map var_map;		///< Maps atomic propositions to BDD variables
    vf_map var_formula_map;     ///< Maps BDD variables to atomic propositions
54
55
    fv_map acc_map;		///< Maps acceptance conditions to BDD variables
    vf_map acc_formula_map;	///< Maps BDD variables to acceptance conditions
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);

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);

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
103
    /// acceptance set associated to formula \a f.  The \a for_me
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.
110
    int register_acceptance_variable(const ltl::formula* f, const void* for_me);
111

112
    /// \brief Register BDD variables as acceptance variables.
113
    ///
114
115
    /// Register all variables occurring in \a f as acceptance variables
    /// used by \a for_me.  This assumes that these acceptance variables
116
    /// are already known from the dictionary (i.e., they have already
117
    /// been registered by register_acceptance_variable() for another
118
    /// automaton).
119
    void register_acceptance_variables(bdd f, const void* for_me);
120

121
122
123
124
125
126
127
128
129
    /// \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);

130
131
132
133
134
135
136
137
    /// \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);

138
    /// \brief Release all variables used by an object.
139
140
141
142
    ///
    /// Usually called in the destructor if \a me.
    void unregister_all_my_variables(const void* me);

143
144
145
    /// \brief Release a variable used by \a me.
    void unregister_variable(int var, const void* me);

146
    /// @{
147
    /// Check whether formula \a f has already been registered by \a by_me.
148
149
    bool is_registered_proposition(const ltl::formula* f, const void* by_me);
    bool is_registered_state(const ltl::formula* f, const void* by_me);
150
    bool is_registered_acceptance_variable(const ltl::formula* f,
151
					   const void* by_me);
152
    /// @}
153
154
155
156
157
158
159
160
161
162
163
164
165

    /// \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.
166
167
    typedef std::set<const void*> ref_set;
    typedef std::map<int, ref_set> vr_map;
168
169
    vr_map var_refs;

170
    void unregister_variable(vr_map::iterator& cur, const void* me);
171

172
173
174
    // SWIG does not grok the following definition, no idea why.
    // It's not important for the Python interface anyway.
#ifndef SWIG
175
    class anon_free_list : public spot::free_list
176
177
178
179
180
    {
    public:
      // WARNING: We need a default constructor so this can be used in
      // a hash; but we should ensure that no object in the hash is
      // constructed with d==0.
181
      anon_free_list(bdd_dict* d = 0);
182
183
184
185
      virtual int extend(int n);
    private:
      bdd_dict* dict_;
    };
186
#endif
187
188

    /// List of unused anonymous variable number for each automaton.
189
190
    typedef std::map<const void*, anon_free_list> free_anonymous_list_of_type;
    free_anonymous_list_of_type free_anonymous_list_of;
191

192
193
194
195
196
197
198
199
200
201
  private:
    // Disallow copy.
    bdd_dict(const bdd_dict& other);
    bdd_dict& operator=(const bdd_dict& other);
  };


}

#endif // SPOT_TGBA_BDDDICT_HH