bdddict.cc 9.52 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2009, 2012, 2013, 2014, 2015, 2016 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
5
6
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
12
// the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22

23
#include <ostream>
24
#include <sstream>
25
#include <cassert>
26
27
28
29
30
#include <spot/tl/print.hh>
#include <spot/tl/formula.hh>
#include <spot/tl/defaultenv.hh>
#include "spot/priv/bddalloc.hh"
#include <spot/twa/bdddict.hh>
31
32
33

namespace spot
{
34
35
36
37
38
39
40
41

  // Empty anonymous namespace so that the style checker does no
  // complain about bdd_dict_priv (which should not be in an anonymous
  // namespace).
  namespace
  {
  }

42
  class bdd_dict_priv final: public bdd_allocator
43
44
45
46
47
48
49
50
51
  {
  public:

    class anon_free_list : public spot::free_list
    {
    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 p==0.
52
      anon_free_list(bdd_dict_priv* p = nullptr)
53
        : priv_(p)
54
55
56
57
      {
      }

      virtual int
58
      extend(int n) override
59
      {
60
61
62
63
64
65
66
67
        assert(priv_);
        int b = priv_->allocate_variables(n);
        free_anonymous_list_of_type::iterator i;
        for (i = priv_->free_anonymous_list_of.begin();
             i != priv_->free_anonymous_list_of.end(); ++i)
          if (&i->second != this)
            i->second.insert(b, n);
        return b;
68
69
70
71
72
73
74
75
      }

    private:
      bdd_dict_priv* priv_;
    };

    bdd_dict_priv()
    {
76
      free_anonymous_list_of[nullptr] = anon_free_list(this);
77
78
79
80
81
82
83
    }

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

84
  bdd_dict::bdd_dict()
85
86
    // Initialize priv_ first, because it also initializes BuDDy
    : priv_(new bdd_dict_priv()),
87
      bdd_map(bdd_varnum())
88
89
90
91
92
93
  {
  }

  bdd_dict::~bdd_dict()
  {
    assert_emptiness();
94
    delete priv_;
95
96
97
  }

  int
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
98
  bdd_dict::register_proposition(formula f, const void* for_me)
99
100
101
102
103
104
  {
    int num;
    // Do not build a variable that already exists.
    fv_map::iterator sii = var_map.find(f);
    if (sii != var_map.end())
      {
105
        num = sii->second;
106
107
108
      }
    else
      {
109
110
111
112
113
        num = priv_->allocate_variables(1);
        var_map[f] = num;
        bdd_map.resize(bdd_varnum());
        bdd_map[num].type = var;
        bdd_map[num].f = f;
114
      }
115
    bdd_map[num].refs.insert(for_me);
116
117
118
    return num;
  }

119
  int
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
120
  bdd_dict::has_registered_proposition(formula f,
121
                                       const void* me)
122
123
124
125
126
127
128
129
130
131
132
  {
    auto ssi = var_map.find(f);
    if (ssi == var_map.end())
      return -1;
    int num = ssi->second;
    auto& r = bdd_map[num].refs;
    if (r.find(me) == r.end())
      return -1;
    return num;
  }

133
  int
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
134
  bdd_dict::register_acceptance_variable(formula f,
135
                                         const void* for_me)
136
137
  {
    int num;
138
    // Do not build an acceptance variable that already exists.
139
140
141
    fv_map::iterator sii = acc_map.find(f);
    if (sii != acc_map.end())
      {
142
        num = sii->second;
143
144
145
      }
    else
      {
146
147
148
149
150
151
        num = priv_->allocate_variables(1);
        acc_map[f] = num;
        bdd_map.resize(bdd_varnum());
        bdd_info& i = bdd_map[num];
        i.type = acc;
        i.f = f;
152
      }
153
    bdd_map[num].refs.insert(for_me);
154
155
156
    return num;
  }

157
158
159
  int
  bdd_dict::register_anonymous_variables(int n, const void* for_me)
  {
160
161
    typedef bdd_dict_priv::free_anonymous_list_of_type fal;
    fal::iterator i = priv_->free_anonymous_list_of.find(for_me);
162

163
    if (i == priv_->free_anonymous_list_of.end())
164
      {
165
166
167
        i = (priv_->free_anonymous_list_of.insert
             (fal::value_type(for_me,
                              priv_->free_anonymous_list_of[nullptr]))).first;
168
169
      }
    int res = i->second.register_n(n);
170

171
172
    bdd_map.resize(bdd_varnum());

173
    while (n--)
174
      {
175
176
        bdd_map[res + n].type = anon;
        bdd_map[res + n].refs.insert(for_me);
177
      }
178

179
180
181
182
    return res;
  }


183
184
  void
  bdd_dict::register_all_variables_of(const void* from_other,
185
                                      const void* for_me)
186
  {
187
188
189
190
191
    auto j = priv_->free_anonymous_list_of.find(from_other);
    if (j != priv_->free_anonymous_list_of.end())
      priv_->free_anonymous_list_of[for_me] = j->second;

    for (auto& i: bdd_map)
192
      {
193
194
195
        ref_set& s = i.refs;
        if (s.find(from_other) != s.end())
          s.insert(for_me);
196
      }
197

198
199
200
201
  }

  void
  bdd_dict::register_all_propositions_of(const void* from_other,
202
                                         const void* for_me)
203
204
205
  {
    for (auto& i: bdd_map)
      {
206
207
208
209
210
        if (i.type != var_type::var)
          continue;
        ref_set& s = i.refs;
        if (s.find(from_other) != s.end())
          s.insert(for_me);
211
      }
212
213
214
  }

  void
215
  bdd_dict::unregister_variable(int v, const void* me)
216
  {
217
    assert(unsigned(v) < bdd_map.size());
218

219
    ref_set& s = bdd_map[v].refs;
220
    // If the variable is not owned by me, ignore it.
221
222
223
    ref_set::iterator si = s.find(me);
    if (si == s.end())
      return;
224

225
    s.erase(si);
226
227
228

    // If var is anonymous, we should reinsert it into the free list
    // of ME's anonymous variables.
229
    if (bdd_map[v].type == anon)
230
      priv_->free_anonymous_list_of[me].release_n(v, 1);
231

232
    if (!s.empty())
233
234
235
236
      return;

    // ME was the last user of this variable.
    // Let's free it.  First, we need to find
237
    // if this is a Var or an Acc variable.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
238
    formula f = nullptr;
239
    switch (bdd_map[v].type)
240
      {
241
      case var:
242
243
244
        f = bdd_map[v].f;
        var_map.erase(f);
        break;
245
      case acc:
246
247
248
        f = bdd_map[v].f;
        acc_map.erase(f);
        break;
249
      case anon:
250
251
252
253
        {
          // Nobody use this variable as an anonymous variable
          // anymore, so remove it entirely from the anonymous
          // free list so it can be used for something else.
254
255
          for (auto& fal: priv_->free_anonymous_list_of)
            fal.second.remove(v, 1);
256
257
          break;
        }
258
259
260
      }
    // Actually release the associated BDD variables, and the
    // formula itself.
261
262
263
    priv_->release_variables(v, 1);
    bdd_map[v].type = anon;
    bdd_map[v].f = nullptr;
264
265
266
267
268
  }

  void
  bdd_dict::unregister_all_my_variables(const void* me)
  {
269
270
271
    unsigned s = bdd_map.size();
    for (unsigned i = 0; i < s; ++i)
      unregister_variable(i, me);
272
    priv_->free_anonymous_list_of.erase(me);
273
274
275
276
277
  }

  std::ostream&
  bdd_dict::dump(std::ostream& os) const
  {
278
279
280
    os << "Variable Map:\n";
    unsigned s = bdd_map.size();
    for (unsigned i = 0; i < s; ++i)
281
      {
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
        os << ' ' << i << ' ';
        const bdd_info& r = bdd_map[i];
        switch (r.type)
          {
          case anon:
            os << (r.refs.empty() ? "Free" : "Anon");
            break;
          case acc:
            os << "Acc[";
            print_psl(os, r.f) << ']';
            break;
          case var:
            os << "Var[";
            print_psl(os, r.f) << ']';
            break;
          }
        if (!r.refs.empty())
          {
            os << " x" << r.refs.size() << " {";
            for (ref_set::const_iterator si = r.refs.begin();
                 si != r.refs.end(); ++si)
              os << ' ' << *si;
            os << " }";
          }
        os << '\n';
307
      }
308
    os << "Anonymous lists:\n";
309
310
    bdd_dict_priv::free_anonymous_list_of_type::const_iterator ai;
    for (ai = priv_->free_anonymous_list_of.begin();
311
         ai != priv_->free_anonymous_list_of.end(); ++ai)
312
      {
313
314
        os << "  [" << ai->first << "] ";
        ai->second.dump_free_list(os) << std::endl;
315
      }
316
    os << "Free list:\n";
317
    priv_->dump_free_list(os);
318
    os << '\n';
319
320
321
322
323
324
325
    return os;
  }

  void
  bdd_dict::assert_emptiness() const
  {
    bool fail = false;
326
327
328
329
330
331
    bool var_seen = false;
    bool acc_seen = false;
    bool refs_seen = false;
    unsigned s = bdd_map.size();
    for (unsigned i = 0; i < s; ++i)
      {
332
333
334
335
336
337
338
339
340
341
342
343
        switch (bdd_map[i].type)
          {
          case var:
            var_seen = true;
            break;
          case acc:
            acc_seen = true;
            break;
          case anon:
            break;
          }
        refs_seen |= !bdd_map[i].refs.empty();
344
      }
345
    if (var_map.empty() && acc_map.empty())
346
      {
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
        if (var_seen)
          {
            std::cerr << "var_map is empty but Var in map" << std::endl;
            fail = true;
          }
        if (acc_seen)
          {
            std::cerr << "acc_map is empty but Acc in map" << std::endl;
            fail = true;
          }
        if (refs_seen)
          {
            std::cerr << "maps are empty but var_refs is not" << std::endl;
            fail = true;
          }
        if (!fail)
          return;
364
365
366
      }
    else
      {
367
        std::cerr << "some maps are not empty" << std::endl;
368
369
      }
    dump(std::cerr);
370
    abort();
371
  }
372
373
374



375
}