se05.cc 20.3 KB
Newer Older
1
// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
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
//#define TRACE

#ifdef TRACE
25
#include <iostream>
26
#endif
27
28

#include <cassert>
29
#include <list>
30
31
32
#include "misc/hash.hh"
#include "tgba/tgba.hh"
#include "emptiness.hh"
33
#include "emptiness_stats.hh"
34
#include "se05.hh"
35

36
37
/// FIXME: make compiling depedent the taking into account of weights.

38
39
40
41
42
43
44
45
46
namespace spot
{
  namespace
  {
    enum color {WHITE, CYAN, BLUE, RED};

    /// \brief Emptiness checker on spot::tgba automata having at most one
    /// accepting condition (i.e. a TBA).
    template <typename heap>
47
    class se05_search : public emptiness_check, public ec_statistics
48
49
50
51
52
53
    {
    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).
54
      se05_search(const tgba *a, size_t size)
55
56
57
58
59
        : ec_statistics(),
          current_weight(0),
          h(size),
          a(a),
          all_cond(a->all_acceptance_conditions())
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
      {
        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.
      ///
83
      /// \return non null pointer iff the algorithm has found a
84
85
86
87
88
89
90
91
92
93
94
      /// 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());
            const state* s0 = a->get_init_state();
95
            inc_states();
96
            h.add_new_state(s0, CYAN, current_weight);
97
98
99
100
101
102
103
            push(st_blue, s0, bddfalse, bddfalse);
            if (dfs_blue())
              return new result(*this);
          }
        else
          {
            h.pop_notify(st_red.front().s);
104
            pop(st_red);
105
106
107
108
109
110
111
112
113
114
115
            if (!st_red.empty() && dfs_red())
              return new result(*this);
            else
              if (dfs_blue())
                return new result(*this);
          }
        return 0;
      }

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

    private:

      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;
138
        /// The label of the transition traversed to reach \a s
139
140
        /// (false for the first one).
        bdd label;
141
        /// The acceptance set of the transition traversed to reach \a s
142
143
144
145
146
147
148
149
150
        /// (false for the first one).
        bdd acc;
      };

      typedef std::list<stack_item> stack_type;

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

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

      /// \brief number of visited accepting arcs
165
      /// in the blue stack.
166
167
      int current_weight;

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

171
172
173
174
175
176
177
178
179
180
      /// \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;

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

181
      /// The unique accepting condition of the automaton \a a.
182
183
184
185
186
187
188
      bdd all_cond;

      bool dfs_blue()
      {
        while (!st_blue.empty())
          {
            stack_item& f = st_blue.front();
189
#           ifdef TRACE
190
            std::cout << "DFS_BLUE treats: "
191
                      << a->format_state(f.s) << std::endl;
192
#           endif
193
194
195
            if (!f.it->done())
              {
                const state *s_prime = f.it->current_state();
196
#               ifdef TRACE
197
198
                std::cout << "  Visit the successor: "
                          << a->format_state(s_prime) << std::endl;
199
200
201
202
#               endif
                bdd label = f.it->current_condition();
                bdd acc = f.it->current_acceptance_conditions();
                // Go down the edge (f.s, <label, acc>, s_prime)
203
                f.it->next();
204
                inc_transitions();
205
                typename heap::color_ref c = h.get_color_ref(s_prime);
206
                if (c.is_white())
207
                  {
208
209
210
#                   ifdef TRACE
                    std::cout << "  It is white, go down" << std::endl;
#                   endif
211
212
                    if (acc == all_cond)
                      ++current_weight;
213
                    inc_states();
214
215
216
                    h.add_new_state(s_prime, CYAN, current_weight);
                    push(st_blue, s_prime, label, acc);
                  }
217
218
219
220
221
                else if (c.get_color() == CYAN && (acc == all_cond ||
             (f.s->compare(s_prime) != 0 && f.acc == all_cond) // option SE05
//                            current_weight > c.get_weight()  // option WEIGHT
                                              /**/))
// For Alexandre: combat style.test! ----------^
222
                  {
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
#                   ifdef TRACE
                    std::cout << "  It is cyan and acceptance condition "
                              << "is reached, report cycle" << std::endl;
#                   endif
                    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.
#                   ifdef TRACE
                    std::cout << "  It is cyan or blue and the arc is "
                              << "accepting, start a red dfs" << std::endl;
#                   endif
                    c.set_color(RED);
                    push(st_red, s_prime, label, acc);
                    if (dfs_red())
                      return true;
                  }
                else
                  {
#                   ifdef TRACE
                    std::cout << "  It is cyan, blue or red, pop it"
                              << std::endl;
#                   endif
                    h.pop_notify(s_prime);
253
254
255
256
257
258
                  }
              }
            else
            // Backtrack the edge
            //        (predecessor of f.s in st_blue, <f.label, f.acc>, f.s)
              {
259
#               ifdef TRACE
260
261
                std::cout << "  All the successors have been visited"
                          << std::endl;
262
#               endif
263
                stack_item f_dest(f);
264
                pop(st_blue);
265
266
267
                if (f_dest.acc == all_cond)
                  --current_weight;
                typename heap::color_ref c = h.get_color_ref(f_dest.s);
268
                assert(!c.is_white());
269
270
                if (!st_blue.empty() &&
                          f_dest.acc == all_cond && c.get_color() != RED)
271
                  {
272
273
274
275
276
                    // 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.
#                   ifdef TRACE
277
278
                    std::cout << "  The arc from "
                              << a->format_state(st_blue.front().s)
279
280
281
282
                              << " to the current state is accepting, start a "
                              << "red dfs" << std::endl;
#                   endif
                    c.set_color(RED);
283
284
285
286
287
288
                    push(st_red, f_dest.s, f_dest.label, f_dest.acc);
                    if (dfs_red())
                      return true;
                  }
                else
                  {
289
290
291
292
#                   ifdef TRACE
                    std::cout << "  Pop it" << std::endl;
#                   endif
                    c.set_color(BLUE);
293
294
295
296
297
298
299
300
301
302
303
304
305
306
                    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();
307
#           ifdef TRACE
308
            std::cout << "DFS_RED treats: "
309
                      << a->format_state(f.s) << std::endl;
310
#           endif
311
312
313
            if (!f.it->done())
              {
                const state *s_prime = f.it->current_state();
314
#               ifdef TRACE
315
316
                std::cout << "  Visit the successor: "
                          << a->format_state(s_prime) << std::endl;
317
318
319
320
#               endif
                bdd label = f.it->current_condition();
                bdd acc = f.it->current_acceptance_conditions();
                // Go down the edge (f.s, <label, acc>, s_prime)
321
                f.it->next();
322
                inc_transitions();
323
                typename heap::color_ref c = h.get_color_ref(s_prime);
324
                if (c.is_white())
325
                  {
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
                    // 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.
#                   ifdef TRACE
                    std::cout << "  It is white (due to collision), pop it"
                              << std::endl;
#                   endif
                    delete s_prime;
                  }
                else if (c.get_color() == RED)
                  {
#                   ifdef TRACE
                    std::cout << "  It is red, pop it"
                              << std::endl;
#                   endif
                    h.pop_notify(s_prime);
                  }
                else if (c.get_color() == CYAN)
                  {
#                   ifdef TRACE
                    std::cout << "  It is cyan, report a cycle"
                              << std::endl;
#                   endif
                    c.set_color(RED);
353
                    push(st_red, s_prime, label, acc);
354
                    return true;
355
                  }
356
                else
357
                  {
358
359
360
361
362
#                   ifdef TRACE
                    std::cout << "  It is blue, go down" << std::endl;
#                   endif
                    c.set_color(RED);
                    push(st_red, s_prime, label, acc);
363
364
365
366
                  }
              }
            else // Backtrack
              {
367
368
369
370
#               ifdef TRACE
                std::cout << "  All the successors have been visited, pop it"
                          << std::endl;
#               endif
371
                h.pop_notify(f.s);
372
                pop(st_red);
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
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
              }
          }
        return false;
      }

      class result: public emptiness_check_result
      {
      public:
        result(se05_search& ms)
          : 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;
        }
      private:
        se05_search& ms_;
      };

    };

    class explicit_se05_search_heap
    {
      typedef Sgi::hash_map<const state*, int,
                state_ptr_hash, state_ptr_equal> hcyan_type;
      typedef Sgi::hash_map<const state*, color,
                state_ptr_hash, state_ptr_equal> hash_type;
    public:
      class color_ref
      {
      public:
        color_ref(hash_type* h, hcyan_type* hc, const state* s, int w)
          : is_cyan(true), weight(w), ph(h), phc(hc), ps(s), pc(0)
          {
          }
        color_ref(color* c)
          : is_cyan(false), weight(0), ph(0), phc(0), ps(0), pc(c)
          {
          }
452
        color get_color() const
453
454
          {
            if (is_cyan)
455
              return CYAN;
456
457
458
459
460
461
462
            return *pc;
          }
        int get_weight() const
          {
            assert(is_cyan);
            return weight;
          }
463
        void set_color(color c)
464
          {
465
            assert(!is_white());
466
467
            if (is_cyan)
              {
468
                assert(c != CYAN);
469
470
471
                int i = phc->erase(ps);
                assert(i==1);
                (void)i;
472
473
474
475
476
477
478
                ph->insert(std::make_pair(ps, c));
              }
            else
              {
                *pc=c;
              }
          }
479
        bool is_white() const
480
481
482
483
484
485
486
487
488
489
490
491
          {
            return !is_cyan && pc==0;
          }
      private:
        bool is_cyan;
        int weight; // weight of a cyan node
        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
      };

492
      explicit_se05_search_heap(size_t)
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
        {
        }

      ~explicit_se05_search_heap()
        {
          hcyan_type::const_iterator sc = hc.begin();
          while (sc != hc.end())
            {
              const state* ptr = sc->first;
              ++sc;
              delete ptr;
            }
          hash_type::const_iterator s = h.begin();
          while (s != h.end())
            {
              const state* ptr = s->first;
              ++s;
              delete ptr;
            }
        }

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

537
      void add_new_state(const state* s, color c, int w=-1)
538
539
        {
          assert(hc.find(s)==hc.end() && h.find(s)==h.end());
540
          assert(c!=CYAN || w>=0);
541
542
543
544
545
546
547
548
549
550
551
552
          if (c == CYAN)
            hc.insert(std::make_pair(s, w));
          else
            h.insert(std::make_pair(s, c));
        }

      void pop_notify(const state*)
        {
        }

    private:

553
      hash_type h; // associate to each blue and red state its color
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
      hcyan_type hc; // associate to each cyan state its weight
    };

    class bsh_se05_search_heap
    {
    private:
      typedef Sgi::hash_map<const state*, int,
                state_ptr_hash, state_ptr_equal> hcyan_type;
    public:
      class color_ref
      {
      public:
        color_ref(hcyan_type* h, const state* st, int w,
                    unsigned char *base, unsigned char offset)
          : is_cyan(true), weight(w), phc(h), ps(st), b(base), o(offset*2)
          {
          }
        color_ref(unsigned char *base, unsigned char offset)
          : is_cyan(false), weight(0), phc(0), ps(0), b(base), o(offset*2)
          {
          }
575
        color get_color() const
576
577
578
579
580
581
582
583
584
585
          {
            if (is_cyan)
              return CYAN;
            return color(((*b) >> o) & 3U);
          }
        int get_weight() const
          {
            assert(is_cyan);
            return weight;
          }
586
        void set_color(color c)
587
588
589
590
591
592
593
594
595
596
597
          {
            if (is_cyan && c!=CYAN)
              {
                int i = phc->erase(ps);
                assert(i==1);
                (void)i;
              }
            *b =  (*b & ~(3U << o)) | (c << o);
          }
        bool is_white() const
          {
598
            return get_color()==WHITE;
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
          }
      private:
        bool is_cyan;
        int weight;
        hcyan_type* phc;
        const state* ps;
        unsigned char *b;
        unsigned char o;
      };

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

      ~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);
          if (ic!=hc.end())
            return color_ref(&hc, ic->first, ic->second, &h[ha%size], ha%4);
          return color_ref(&h[ha%size], ha%4);
        }

      void add_new_state(const state* s, color c, int w=-1)
        {
          assert(c!=CYAN || w>=0);
          assert(get_color_ref(s).is_white());
          if (c==CYAN)
            hc.insert(std::make_pair(s, w));
          else
            {
              color_ref cr(get_color_ref(s));
638
              cr.set_color(c);
639
640
641
642
643
644
645
646
647
648
649
            }
        }

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

    private:
      size_t size;
      unsigned char* h;
650
651
652
653
654
655
656
      hcyan_type hc;
    };

  } // anonymous

  emptiness_check* explicit_se05_search(const tgba *a)
  {
657
658
659
660
661
662
    return new se05_search<explicit_se05_search_heap>(a, 0);
  }

  emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size)
  {
    return new se05_search<bsh_se05_search_heap>(a, size);
663
664
665
  }

}