se05.cc 20.5 KB
Newer Older
1
2
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
3
// Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
// 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.

24
25
//#define TRACE

26
#include <iostream>
27
28
29
30
#ifdef TRACE
#define trace std::cerr
#else
#define trace while (0) std::cerr
31
#endif
32
33

#include <cassert>
34
#include <list>
35
36
37
#include "misc/hash.hh"
#include "tgba/tgba.hh"
#include "emptiness.hh"
38
#include "emptiness_stats.hh"
39
#include "se05.hh"
40
#include "ndfs_result.hxx"
41
42
43
44
45
46
47
48

namespace spot
{
  namespace
  {
    enum color {WHITE, CYAN, BLUE, RED};

    /// \brief Emptiness checker on spot::tgba automata having at most one
49
    /// acceptance condition (i.e. a TBA).
50
    template <typename heap>
51
    class se05_search : public emptiness_check, public ec_statistics
52
53
54
55
    {
    public:
      /// \brief Initialize the Magic Search algorithm on the automaton \a a
      ///
56
      /// \pre The automaton \a a must have at most one acceptance
57
      /// condition (i.e. it is a TBA).
58
59
      se05_search(const tgba *a, size_t size, option_map o = option_map())
        : emptiness_check(a, o),
60
61
          h(size),
          all_cond(a->all_acceptance_conditions())
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
      {
        assert(a->number_of_acceptance_conditions() <= 1);
      }

      virtual ~se05_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();
          }
      }

      /// \brief Perform a Magic Search.
      ///
85
      /// \return non null pointer iff the algorithm has found a
86
87
88
89
90
91
92
93
94
95
      /// 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()
      {
        if (st_red.empty())
          {
            assert(st_blue.empty());
96
            const state* s0 = a_->get_init_state();
97
            inc_states();
98
            h.add_new_state(s0, CYAN);
99
100
            push(st_blue, s0, bddfalse, bddfalse);
            if (dfs_blue())
101
              return new se05_result(*this, options());
102
103
104
105
          }
        else
          {
            h.pop_notify(st_red.front().s);
106
            pop(st_red);
107
            if (!st_red.empty() && dfs_red())
108
              return new se05_result(*this, options());
109
110
            else
              if (dfs_blue())
111
                return new se05_result(*this, options());
112
113
114
115
116
117
          }
        return 0;
      }

      virtual std::ostream& print_stats(std::ostream &os) const
      {
118
119
120
        os << states() << " distinct nodes visited" << std::endl;
        os << transitions() << " transitions explored" << std::endl;
        os << max_depth() << " nodes for the maximal stack depth" << std::endl;
121
122
123
124
125
126
127
128
129
        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;
      }

130
131
132
133
134
      virtual bool safe() const
      {
	return heap::Safe;
      }

135
      const heap& get_heap() const
136
137
138
      {
	return h;
      }
139

140
      const stack_type& get_st_blue() const
141
142
143
      {
	return st_blue;
      }
144

145
      const stack_type& get_st_red() const
146
147
148
      {
	return st_red;
      }
149
    private:
150
151

      void push(stack_type& st, const state* s,
152
		const bdd& label, const bdd& acc)
153
      {
154
        inc_depth();
155
        tgba_succ_iterator* i = a_->succ_iter(s);
156
157
158
159
        i->first();
        st.push_front(stack_item(s, i, label, acc));
      }

160
161
162
163
164
165
      void pop(stack_type& st)
      {
        dec_depth();
        delete st.front().it;
        st.pop_front();
      }
166

167
168
169
      /// \brief Stack of the blue dfs.
      stack_type st_blue;

170
171
172
173
174
175
176
      /// \brief Stack of the red dfs.
      stack_type st_red;

      /// \brief Map where each visited state is colored
      /// by the last dfs visiting it.
      heap h;

177
      /// The unique acceptance condition of the automaton \a a.
178
179
180
181
182
183
184
      bdd all_cond;

      bool dfs_blue()
      {
        while (!st_blue.empty())
          {
            stack_item& f = st_blue.front();
185
            trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl;
186
187
188
            if (!f.it->done())
              {
                const state *s_prime = f.it->current_state();
189
190
                trace << "  Visit the successor: "
                      << a_->format_state(s_prime) << std::endl;
191
192
193
                bdd label = f.it->current_condition();
                bdd acc = f.it->current_acceptance_conditions();
                // Go down the edge (f.s, <label, acc>, s_prime)
194
                f.it->next();
195
                inc_transitions();
196
                typename heap::color_ref c = h.get_color_ref(s_prime);
197
                if (c.is_white())
198
                  {
199
                    trace << "  It is white, go down" << std::endl;
200
                    inc_states();
201
                    h.add_new_state(s_prime, CYAN);
202
203
                    push(st_blue, s_prime, label, acc);
                  }
204
                else if (c.get_color() == CYAN && (acc == all_cond ||
205
                             (f.s->compare(s_prime) != 0 && f.acc == all_cond)))
206
                  {
207
208
                    trace << "  It is cyan and acceptance condition "
                          << "is reached, report cycle" << std::endl;
209
210
211
212
213
214
215
216
217
218
                    c.set_color(RED);
                    push(st_red, s_prime, label, acc);
                    return true;
                  }
                else if (acc == all_cond && c.get_color() != RED)
                  {
                    // the test 'c.get_color() != RED' is added to limit
                    // the number of runs reported by successive
                    // calls to the check method. Without this
                    // functionnality, the test can be ommited.
219
220
                    trace << "  It is cyan or blue and the arc is "
                          << "accepting, start a red dfs" << std::endl;
221
222
223
224
225
226
227
                    c.set_color(RED);
                    push(st_red, s_prime, label, acc);
                    if (dfs_red())
                      return true;
                  }
                else
                  {
228
                    trace << "  It is cyan, blue or red, pop it" << std::endl;
229
                    h.pop_notify(s_prime);
230
231
232
233
234
235
                  }
              }
            else
            // Backtrack the edge
            //        (predecessor of f.s in st_blue, <f.label, f.acc>, f.s)
              {
236
                trace << "  All the successors have been visited" << std::endl;
237
                stack_item f_dest(f);
238
                pop(st_blue);
239
                typename heap::color_ref c = h.get_color_ref(f_dest.s);
240
                assert(!c.is_white());
241
242
                if (!st_blue.empty() &&
                          f_dest.acc == all_cond && c.get_color() != RED)
243
                  {
244
245
246
247
                    // the test 'c.get_color() != RED' is added to limit
                    // the number of runs reported by successive
                    // calls to the check method. Without this
                    // functionnality, the test can be ommited.
248
249
250
251
                    trace << "  The arc from "
                          << a_->format_state(st_blue.front().s)
                          << " to the current state is accepting, start a "
                          << "red dfs" << std::endl;
252
                    c.set_color(RED);
253
254
255
256
257
258
                    push(st_red, f_dest.s, f_dest.label, f_dest.acc);
                    if (dfs_red())
                      return true;
                  }
                else
                  {
259
                    trace << "  Pop it" << std::endl;
260
                    c.set_color(BLUE);
261
262
263
264
265
266
267
268
269
270
271
272
273
274
                    h.pop_notify(f_dest.s);
                  }
              }
          }
        return false;
      }

      bool dfs_red()
      {
        assert(!st_red.empty());

        while (!st_red.empty())
          {
            stack_item& f = st_red.front();
275
            trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl;
276
277
278
            if (!f.it->done())
              {
                const state *s_prime = f.it->current_state();
279
280
                trace << "  Visit the successor: "
                      << a_->format_state(s_prime) << std::endl;
281
282
283
                bdd label = f.it->current_condition();
                bdd acc = f.it->current_acceptance_conditions();
                // Go down the edge (f.s, <label, acc>, s_prime)
284
                f.it->next();
285
                inc_transitions();
286
                typename heap::color_ref c = h.get_color_ref(s_prime);
287
                if (c.is_white())
288
                  {
289
290
291
292
293
294
                    // For an explicit search, we can pose assert(!c.is_white())
                    // because to reach a white state, the red dfs must
                    // have crossed a cyan one (a state in the blue stack)
                    // implying the report of a cycle.
                    // However, with a bit-state hashing search and due to
                    // collision, this property does not hold.
295
296
                    trace << "  It is white (due to collision), pop it"
                          << std::endl;
297
                    s_prime->destroy();
298
299
300
                  }
                else if (c.get_color() == RED)
                  {
301
                    trace << "  It is red, pop it" << std::endl;
302
303
304
305
                    h.pop_notify(s_prime);
                  }
                else if (c.get_color() == CYAN)
                  {
306
                    trace << "  It is cyan, report a cycle" << std::endl;
307
                    c.set_color(RED);
308
                    push(st_red, s_prime, label, acc);
309
                    return true;
310
                  }
311
                else
312
                  {
313
                    trace << "  It is blue, go down" << std::endl;
314
315
                    c.set_color(RED);
                    push(st_red, s_prime, label, acc);
316
317
318
319
                  }
              }
            else // Backtrack
              {
320
321
                trace << "  All the successors have been visited, pop it"
                      << std::endl;
322
                h.pop_notify(f.s);
323
                pop(st_red);
324
325
326
327
328
              }
          }
        return false;
      }

329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
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
398
399
400
401
402
403
404
405
406
407
408
409
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
      class result_from_stack: public emptiness_check_result,
        public acss_statistics
      {
      public:
        result_from_stack(se05_search& ms)
          : emptiness_check_result(ms.automaton()), ms_(ms)
        {
        }

        virtual tgba_run* accepting_run()
        {
          assert(!ms_.st_blue.empty());
          assert(!ms_.st_red.empty());

          tgba_run* run = new tgba_run;

          typename stack_type::const_reverse_iterator i, j, end;
          tgba_run::steps* l;

          const state* target = ms_.st_red.front().s;

          l = &run->prefix;

          i = ms_.st_blue.rbegin();
          end = ms_.st_blue.rend(); --end;
          j = i; ++j;
          for (; i != end; ++i, ++j)
            {
              if (l == &run->prefix && i->s->compare(target) == 0)
                l = &run->cycle;
              tgba_run::step s = { i->s->clone(), j->label, j->acc };
              l->push_back(s);
            }

          if (l == &run->prefix && i->s->compare(target) == 0)
            l = &run->cycle;
          assert(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);
            }

          return run;
        }

        unsigned acss_states() const
        {
          return 0;
        }
      private:
        se05_search& ms_;
      };

#     define FROM_STACK "ar:from_stack"

      class se05_result: public emptiness_check_result
      {
      public:
        se05_result(se05_search& m, option_map o = option_map())
          : emptiness_check_result(m.automaton(), o), ms(m)
        {
          if (options()[FROM_STACK])
            computer = new result_from_stack(ms);
          else
            computer = new ndfs_result<se05_search<heap>, heap>(ms);
        }

        virtual void options_updated(const option_map& old)
        {
          if (old[FROM_STACK] && !options()[FROM_STACK])
            {
              delete computer;
              computer = new ndfs_result<se05_search<heap>, heap>(ms);
            }
          else if (!old[FROM_STACK] && options()[FROM_STACK])
            {
              delete computer;
              computer = new result_from_stack(ms);
            }
        }

        virtual ~se05_result()
        {
          delete computer;
        }

        virtual tgba_run* accepting_run()
        {
          return computer->accepting_run();
        }

        virtual const unsigned_statistics* statistics() const
        {
          return computer->statistics();
        }

      private:
        emptiness_check_result* computer;
        se05_search& ms;
      };
437
438
439
440
    };

    class explicit_se05_search_heap
    {
441
      typedef Sgi::hash_set<const state*,
442
443
444
445
                state_ptr_hash, state_ptr_equal> hcyan_type;
      typedef Sgi::hash_map<const state*, color,
                state_ptr_hash, state_ptr_equal> hash_type;
    public:
446
447
      enum { Safe = 1 };

448
449
450
      class color_ref
      {
      public:
451
452
        color_ref(hash_type* h, hcyan_type* hc, const state* s)
          : is_cyan(true), ph(h), phc(hc), ps(s), pc(0)
453
454
455
          {
          }
        color_ref(color* c)
456
          : is_cyan(false), ph(0), phc(0), ps(0), pc(c)
457
458
          {
          }
459
        color get_color() const
460
461
          {
            if (is_cyan)
462
              return CYAN;
463
464
            return *pc;
          }
465
        void set_color(color c)
466
          {
467
            assert(!is_white());
468
469
            if (is_cyan)
              {
470
                assert(c != CYAN);
471
                int i = phc->erase(ps);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
472
                assert(i == 1);
473
                (void)i;
474
475
476
477
478
479
480
                ph->insert(std::make_pair(ps, c));
              }
            else
              {
                *pc=c;
              }
          }
481
        bool is_white() const
482
          {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
483
            return !is_cyan && pc == 0;
484
485
486
487
488
489
490
491
492
          }
      private:
        bool is_cyan;
        hash_type* ph; //point to the main hash table
        hcyan_type* phc; // point to the hash table hcyan
        const state* ps; // point to the state in hcyan
        color *pc; // point to the color of a state stored in main hash table
      };

493
      explicit_se05_search_heap(size_t)
494
495
496
497
498
499
500
501
        {
        }

      ~explicit_se05_search_heap()
        {
          hcyan_type::const_iterator sc = hc.begin();
          while (sc != hc.end())
            {
502
              const state* ptr = *sc;
503
              ++sc;
504
              ptr->destroy();
505
506
507
508
509
510
            }
          hash_type::const_iterator s = h.begin();
          while (s != h.end())
            {
              const state* ptr = s->first;
              ++s;
511
              ptr->destroy();
512
513
514
515
516
517
            }
        }

      color_ref get_color_ref(const state*& s)
        {
          hcyan_type::iterator ic = hc.find(s);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
518
          if (ic == hc.end())
519
520
            {
              hash_type::iterator it = h.find(s);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
521
              if (it == h.end())
522
                return color_ref(0); // white state
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
523
              if (s != it->first)
524
                {
525
                  s->destroy();
526
527
                  s = it->first;
                }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
528
              return color_ref(&it->second); // blue or red state
529
            }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
530
          if (s != *ic)
531
            {
532
              s->destroy();
533
              s = *ic;
534
            }
535
          return color_ref(&h, &hc, *ic); // cyan state
536
537
        }

538
      void add_new_state(const state* s, color c)
539
        {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
540
          assert(hc.find(s) == hc.end() && h.find(s) == h.end());
541
          if (c == CYAN)
542
            hc.insert(s);
543
544
545
546
          else
            h.insert(std::make_pair(s, c));
        }

547
      void pop_notify(const state*) const
548
549
550
        {
        }

551
      bool has_been_visited(const state* s) const
552
553
        {
          hcyan_type::const_iterator ic = hc.find(s);
554
          if (ic == hc.end())
555
556
            {
              hash_type::const_iterator it = h.find(s);
557
              return (it != h.end());
558
            }
559
          return true;
560
561
        }

562
      enum { Has_Size = 1 };
563
564
565
566
567
      int size() const
        {
          return h.size() + hc.size();
        }

568
569
    private:

570
      hash_type h; // associate to each blue and red state its color
571
572
573
574
575
576
      hcyan_type hc; // associate to each cyan state its weight
    };

    class bsh_se05_search_heap
    {
    private:
577
      typedef Sgi::hash_set<const state*,
578
579
                state_ptr_hash, state_ptr_equal> hcyan_type;
    public:
580
581
      enum { Safe = 0 };

582
583
584
      class color_ref
      {
      public:
585
        color_ref(hcyan_type* h, const state* st,
586
                    unsigned char *base, unsigned char offset)
587
          : is_cyan(true), phc(h), ps(st), b(base), o(offset*2)
588
589
590
          {
          }
        color_ref(unsigned char *base, unsigned char offset)
591
          : is_cyan(false), phc(0), ps(0), b(base), o(offset*2)
592
593
          {
          }
594
        color get_color() const
595
596
597
598
599
          {
            if (is_cyan)
              return CYAN;
            return color(((*b) >> o) & 3U);
          }
600
        void set_color(color c)
601
          {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
602
            if (is_cyan && c != CYAN)
603
604
              {
                int i = phc->erase(ps);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
605
                assert(i == 1);
606
607
608
609
610
611
                (void)i;
              }
            *b =  (*b & ~(3U << o)) | (c << o);
          }
        bool is_white() const
          {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
612
            return get_color() == WHITE;
613
614
615
616
617
618
619
620
621
          }
      private:
        bool is_cyan;
        hcyan_type* phc;
        const state* ps;
        unsigned char *b;
        unsigned char o;
      };

622
      bsh_se05_search_heap(size_t s) : size_(s)
623
        {
624
625
          h = new unsigned char[size_];
          memset(h, WHITE, size_);
626
627
628
629
630
631
632
633
634
635
636
        }

      ~bsh_se05_search_heap()
        {
          delete[] h;
        }

      color_ref get_color_ref(const state*& s)
        {
          size_t ha = s->hash();
          hcyan_type::iterator ic = hc.find(s);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
637
          if (ic != hc.end())
638
639
            return color_ref(&hc, *ic, &h[ha%size_], ha%4);
          return color_ref(&h[ha%size_], ha%4);
640
641
        }

642
      void add_new_state(const state* s, color c)
643
644
        {
          assert(get_color_ref(s).is_white());
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
645
          if (c == CYAN)
646
            hc.insert(s);
647
648
649
          else
            {
              color_ref cr(get_color_ref(s));
650
              cr.set_color(c);
651
652
653
            }
        }

654
      void pop_notify(const state* s) const
655
        {
656
          s->destroy();
657
658
        }

659
      bool has_been_visited(const state* s) const
660
661
        {
          hcyan_type::const_iterator ic = hc.find(s);
662
          if (ic != hc.end())
663
664
            return true;
          size_t ha = s->hash();
665
666
667
          return color((h[ha%size_] >> ((ha%4)*2)) & 3U) != WHITE;
        }

668
      enum { Has_Size = 0 };
669

670
    private:
671
      size_t size_;
672
      unsigned char* h;
673
674
675
676
677
      hcyan_type hc;
    };

  } // anonymous

678
  emptiness_check* explicit_se05_search(const tgba *a, option_map o)
679
  {
680
    return new se05_search<explicit_se05_search_heap>(a, 0, o);
681
682
  }

683
684
  emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size,
                                                option_map o)
685
  {
686
    return new se05_search<bsh_se05_search_heap>(a, size, o);
687
688
  }

689
690
691
692
693
694
695
696
697
  emptiness_check*
  se05(const tgba *a, option_map o)
  {
    size_t size = o.get("bsh");
    if (size)
      return bit_state_hashing_se05_search(a, size, o);
    return explicit_se05_search(a, o);
  }

698
}