magic.cc 13.6 KB
Newer Older
1
// Copyright (C) 2003, 2004  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
#include <cassert>
23
#include <list>
24
#include <iterator>
25
26
27
#include "misc/hash.hh"
#include "tgba/tgba.hh"
#include "emptiness.hh"
28
29
30
31
#include "magic.hh"

namespace spot
{
32
  namespace
33
  {
34
    enum color {WHITE, BLUE, RED};
35

36
37
38
39
40
41
42
43
44
45
    /// \brief Emptiness checker on spot::tgba automata having at most one
    /// accepting condition (i.e. a TBA).
    template <typename heap>
    class magic_search : public emptiness_check
    {
    public:
      /// \brief Initialize the Magic Search algorithm on the automaton \a a
      ///
      /// \pre The automaton \a a must have at most one accepting
      /// condition (i.e. it is a TBA).
46
47
      magic_search(const tgba *a, size_t size)
        : h(size), a(a), all_cond(a->all_acceptance_conditions())
48
49
50
      {
        assert(a->number_of_acceptance_conditions() <= 1);
      }
51

52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
      virtual ~magic_search()
      {
        // Release all iterators on the stacks.
        while (!st_blue.empty())
          {
            h.pop_notify(st_blue.front().s);
            delete st_blue.front().it;
            st_blue.pop_front();
          }
        while (!st_red.empty())
          {
            h.pop_notify(st_red.front().s);
            delete st_red.front().it;
            st_red.pop_front();
          }
      }
68

69
70
      /// \brief Perform a Magic Search.
      ///
71
      /// \return non null pointer iff the algorithm has found a
72
73
74
75
76
77
      /// new accepting path.
      ///
      /// check() can be called several times (until it returns a null
      /// pointer) to enumerate all the visited accepting paths. The method
      /// visits only a finite set of accepting paths.
      virtual emptiness_check_result* check()
78
      {
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
        nbn = nbt = 0;
        sts = mdp = st_blue.size() + st_red.size();
        if (st_red.empty())
          {
            assert(st_blue.empty());
            const state* s0 = a->get_init_state();
            ++nbn;
            h.add_new_state(s0, BLUE);
            push(st_blue, s0, bddfalse, bddfalse);
            if (dfs_blue())
              return new result(*this);
          }
        else
          {
            h.pop_notify(st_red.front().s);
            delete st_red.front().it;
            st_red.pop_front();
            if (!st_red.empty() && dfs_red())
              return new result(*this);
            else
              if (dfs_blue())
                return new result(*this);
          }
        return 0;
      }
104

105
106
107
108
109
110
111
112
113
114
115
116
      virtual std::ostream& print_stats(std::ostream &os) const
      {
        os << nbn << " distinct nodes visited" << std::endl;
        os << nbt << " transitions explored" << std::endl;
        os << mdp << " nodes for the maximal stack depth" << std::endl;
        if (!st_red.empty())
          {
            assert(!st_blue.empty());
            os << st_blue.size() + st_red.size() - 1
               << " nodes for the counter example" << std::endl;
          }
        return os;
117
118
      }

119
120
121
122
    private:
      /// \brief counters for statistics (number of distinct nodes, of
      /// transitions and maximal stacks size.
      int nbn, nbt, mdp, sts;
123

124
125
126
127
128
129
130
131
      struct stack_item
      {
        stack_item(const state* n, tgba_succ_iterator* i, bdd l, bdd a)
          : s(n), it(i), label(l), acc(a) {};
        /// The visited state.
        const state* s;
        /// Design the next successor of \a s which has to be visited.
        tgba_succ_iterator* it;
132
        /// The label of the transition traversed to reach \a s
133
134
        /// (false for the first one).
        bdd label;
135
        /// The acceptance set of the transition traversed to reach \a s
136
137
138
        /// (false for the first one).
        bdd acc;
      };
139

140
      typedef std::list<stack_item> stack_type;
141

142
143
      void push(stack_type& st, const state* s,
                        const bdd& label, const bdd& acc)
144
      {
145
146
147
148
149
150
        ++sts;
        if (sts>mdp)
          mdp = sts;
        tgba_succ_iterator* i = a->succ_iter(s);
        i->first();
        st.push_front(stack_item(s, i, label, acc));
151
      }
152

153
154
155
156
157
      /// \brief Stack of the blue dfs.
      stack_type st_blue;

      /// \brief Stack of the red dfs.
      stack_type st_red;
158

159
160
161
162
163
164
165
166
167
168
      /// \brief Map where each visited state is colored
      /// by the last dfs visiting it.
      heap h;

      /// State targeted by the red dfs.
      const state* target;

      /// The automata to check.
      const tgba* a;

169
      /// The unique accepting condition of the automaton \a a.
170
171
172
      bdd all_cond;

      bool dfs_blue()
173
      {
174
175
176
177
178
179
180
181
182
183
184
        while (!st_blue.empty())
          {
            stack_item& f = st_blue.front();
            if (!f.it->done())
              {
                ++nbt;
                const state *s_prime = f.it->current_state();
                bdd label = f.it->current_condition();
                bdd acc = f.it->current_acceptance_conditions();
                f.it->next();
                typename heap::color_ref c = h.get_color_ref(s_prime);
185
                if (c.is_white())
186
187
188
189
190
191
192
193
                // Go down the edge (f.s, <label, acc>, s_prime)
                  {
                    ++nbn;
                    h.add_new_state(s_prime, BLUE);
                    push(st_blue, s_prime, label, acc);
                  }
                else // Backtrack the edge (f.s, <label, acc>, s_prime)
                  {
194
195
                    if (c.get() != RED && acc == all_cond)
                    // the test 'c.get() != RED' is added to limit
196
197
198
199
200
201
202
203
204
205
                    // the number of runs reported by successive
                    // calls to the check method. Without this
                    // functionnality, the test can be ommited.
                      {
                        target = f.s;
                        c.set(RED);
                        push(st_red, s_prime, label, acc);
                        if (dfs_red())
                          return true;
                      }
206
207
                    else
                      h.pop_notify(s_prime);
208
209
210
211
212
213
214
215
216
217
218
                  }
              }
            else
            // Backtrack the edge
            //        (predecessor of f.s in st_blue, <f.label, f.acc>, f.s)
              {
                --sts;
                stack_item f_dest(f);
                delete f.it;
                st_blue.pop_front();
                typename heap::color_ref c = h.get_color_ref(f_dest.s);
219
                assert(!c.is_white());
220
                if (c.get() != RED && f_dest.acc == all_cond
221
                                    && !st_blue.empty())
222
                // the test 'c.get() != RED' is added to limit
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
                // the number of runs reported by successive
                // calls to the check method. Without this
                // functionnality, the test can be ommited.
                  {
                    target = st_blue.front().s;
                    c.set(RED);
                    push(st_red, f_dest.s, f_dest.label, f_dest.acc);
                    if (dfs_red())
                      return true;
                  }
                else
                  h.pop_notify(f_dest.s);
              }
          }
        return false;
238
      }
239
240

      bool dfs_red()
241
      {
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
        assert(!st_red.empty());
        if (target->compare(st_red.front().s) == 0)
          return true;

        while (!st_red.empty())
          {
            stack_item& f = st_red.front();
            if (!f.it->done()) // Go down
              {
                ++nbt;
                const state *s_prime = f.it->current_state();
                bdd label = f.it->current_condition();
                bdd acc = f.it->current_acceptance_conditions();
                f.it->next();
                typename heap::color_ref c = h.get_color_ref(s_prime);
257
                if (c.is_white())
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
                // Go down the edge (f.s, <label, acc>, s_prime)
                  {
                    ++nbn;
                    h.add_new_state(s_prime, RED);
                    push(st_red, s_prime, label, acc);
                  }
                else // Go down the edge (f.s, <label, acc>, s_prime)
                  {
                    if (c.get() != RED)
                      {
                        c.set(RED);
                        push(st_red, s_prime, label, acc);
                        if (target->compare(s_prime) == 0)
                          return true;
                      }
273
274
                    else
                      h.pop_notify(s_prime);
275
276
277
278
279
280
281
282
283
284
285
                  }
              }
            else // Backtrack
              {
                --sts;
                h.pop_notify(f.s);
                delete f.it;
                st_red.pop_front();
              }
          }
        return false;
286
287
      }

288
289
290
291
292
293
294
295
296
297
298
      class result: public emptiness_check_result
      {
      public:
        result(magic_search& ms)
          : ms_(ms)
        {
        }
        virtual tgba_run* accepting_run()
        {
          assert(!ms_.st_blue.empty());
          assert(!ms_.st_red.empty());
299

300
          tgba_run* run = new tgba_run;
301

302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
          typename stack_type::const_reverse_iterator i, j, end;
          tgba_run::steps* l;

          l = &run->prefix;

          i = ms_.st_blue.rbegin();
          end = ms_.st_blue.rend(); --end;
          j = i; ++j;
          for (; i != end; ++i, ++j)
            {
              tgba_run::step s = { i->s->clone(), j->label, j->acc };
              l->push_back(s);
            }

          l = &run->cycle;

          j = ms_.st_red.rbegin();
          tgba_run::step s = { i->s->clone(), j->label, j->acc };
          l->push_back(s);

          i = j; ++j;
          end = ms_.st_red.rend(); --end;
          for (; i != end; ++i, ++j)
            {
              tgba_run::step s = { i->s->clone(), j->label, j->acc };
              l->push_back(s);
            }
329

330
331
332
333
334
          return run;
        }
      private:
        magic_search& ms_;
      };
335

336
337
338
339
340
341
    };

    class explicit_magic_search_heap
    {
    public:
      class color_ref
342
      {
343
344
345
346
      public:
        color_ref(color* c) :p(c)
          {
          }
347
        color get() const
348
349
350
351
352
          {
            return *p;
          }
        void set(color c)
          {
353
            assert(!is_white());
354
355
            *p=c;
          }
356
        bool is_white() const
357
358
359
360
361
362
363
          {
            return p==0;
          }
      private:
        color *p;
      };

364
      explicit_magic_search_heap(size_t)
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
        {
        }

      ~explicit_magic_search_heap()
        {
          hash_type::const_iterator s = h.begin();
          while (s != h.end())
            {
              // Advance the iterator before deleting the "key" pointer.
              const state* ptr = s->first;
              ++s;
              delete ptr;
            }
        }

      color_ref get_color_ref(const state*& s)
        {
          hash_type::iterator it = h.find(s);
          if (it==h.end())
            return color_ref(0);
          if (s!=it->first)
            {
              delete s;
              s = it->first;
            }
          return color_ref(&(it->second));
        }

      void add_new_state(const state* s, color c)
        {
          assert(h.find(s)==h.end());
          h.insert(std::make_pair(s, c));
        }
398

399
400
401
402
403
404
405
406
407
408
409
      void pop_notify(const state*)
        {
        }

    private:

      typedef Sgi::hash_map<const state*, color,
                state_ptr_hash, state_ptr_equal> hash_type;
      hash_type h;
    };

410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
    class bsh_magic_search_heap
    {
    public:
      class color_ref
      {
      public:
        color_ref(unsigned char *b, unsigned char o): base(b), offset(o*2)
          {
          }
        color get() const
          {
            return color(((*base) >> offset) & 3U);
          }
        void set(color c)
          {
            *base =  (*base & ~(3U << offset)) | (c << offset);
          }
        bool is_white() const
          {
            return get()==WHITE;
          }
      private:
        unsigned char *base;
        unsigned char offset;
      };

      bsh_magic_search_heap(size_t s)
        {
          size = s;
          h = new unsigned char[size];
          memset(h, WHITE, size);
        }

      ~bsh_magic_search_heap()
        {
          delete[] h;
        }

      color_ref get_color_ref(const state*& s)
        {
          size_t ha = s->hash();
          return color_ref(&(h[ha%size]), ha%4);
        }

      void add_new_state(const state* s, color c)
        {
          color_ref cr(get_color_ref(s));
          assert(cr.is_white());
          cr.set(c);
        }

      void pop_notify(const state* s)
        {
          delete s;
        }

    private:
      size_t size;
      unsigned char* h;
    };

471
472
473
474
  } // anonymous

  emptiness_check* explicit_magic_search(const tgba *a)
  {
475
476
477
478
479
480
481
    return new magic_search<explicit_magic_search_heap>(a, 0);
  }

  emptiness_check* bit_state_hashing_magic_search(
                            const tgba *a, size_t size)
  {
    return new magic_search<bsh_magic_search_heap>(a, size);
482
483
484
  }

}