magic.cc 17.3 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de recherche et
3
// développement de l'Epita (LRDE).
4
// Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
5
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
6 7 8 9 10 11
// 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
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 24 25
//#define TRACE

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

32
#include <cassert>
33
#include <list>
34
#include "misc/hash.hh"
35
#include "twa/twa.hh"
36
#include "emptiness.hh"
37
#include "emptiness_stats.hh"
38
#include "magic.hh"
39
#include "ndfs_result.hxx"
40 41 42

namespace spot
{
43
  namespace
44
  {
45
    enum color {WHITE, BLUE, RED};
46

47
    /// \brief Emptiness checker on spot::tgba automata having at most one
48
    /// acceptance condition (i.e. a TBA).
49
    template <typename heap>
50
    class magic_search_ : public emptiness_check, public ec_statistics
51 52 53 54
    {
    public:
      /// \brief Initialize the Magic Search algorithm on the automaton \a a
      ///
55
      /// \pre The automaton \a a must have at most one acceptance
56
      /// condition (i.e. it is a TBA).
57
      magic_search_(const const_twa_ptr& a, size_t size,
58
		    option_map o = option_map())
59
        : emptiness_check(a, o),
60
          h(size)
61
      {
62
        assert(a->num_sets() <= 1);
63
      }
64

65
      virtual ~magic_search_()
66 67 68 69 70
      {
        // Release all iterators on the stacks.
        while (!st_blue.empty())
          {
            h.pop_notify(st_blue.front().s);
71
            a_->release_iter(st_blue.front().it);
72 73 74 75 76
            st_blue.pop_front();
          }
        while (!st_red.empty())
          {
            h.pop_notify(st_red.front().s);
77
            a_->release_iter(st_red.front().it);
78 79 80
            st_red.pop_front();
          }
      }
81

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

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

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

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

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

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

152
      void push(stack_type& st, const state* s,
153
		const bdd& label, acc_cond::mark_t acc)
154
      {
155
        inc_depth();
156
        twa_succ_iterator* i = a_->succ_iter(s);
157
        i->first();
158
        st.emplace_front(s, i, label, acc);
159
      }
160

161 162 163
      void pop(stack_type& st)
      {
        dec_depth();
164
	a_->release_iter(st.front().it);
165 166 167
        st.pop_front();
      }

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

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

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

      bool dfs_blue()
182
      {
183 184 185
        while (!st_blue.empty())
          {
            stack_item& f = st_blue.front();
186
            trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl;
187 188 189
            if (!f.it->done())
              {
                const state *s_prime = f.it->current_state();
190 191
                trace << "  Visit the successor: "
                      << a_->format_state(s_prime) << std::endl;
192
                bdd label = f.it->current_condition();
193
                auto acc = f.it->current_acceptance_conditions();
194
                // Go down the edge (f.s, <label, acc>, s_prime)
195
                f.it->next();
196
                inc_transitions();
197
                typename heap::color_ref c = h.get_color_ref(s_prime);
198
                if (c.is_white())
199
                  {
200
                    trace << "  It is white, go down" << std::endl;
201
                    inc_states();
202 203 204
                    h.add_new_state(s_prime, BLUE);
                    push(st_blue, s_prime, label, acc);
                  }
205
                else
206
                  {
207
                    if (a_->acc().accepting(acc) && c.get_color() != RED)
208
                      {
209 210 211 212
                        // 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.
213 214
                        trace << "  It is blue and the arc is "
                              << "accepting, start a red dfs" << std::endl;
215
                        target = f.s;
216
                        c.set_color(RED);
217 218 219 220
                        push(st_red, s_prime, label, acc);
                        if (dfs_red())
                          return true;
                      }
221
                    else
222
                      {
223
                        trace << "  It is blue or red, pop it" << std::endl;
224 225
                        h.pop_notify(s_prime);
                      }
226 227 228 229 230 231
                  }
              }
            else
            // Backtrack the edge
            //        (predecessor of f.s in st_blue, <f.label, f.acc>, f.s)
              {
232
                trace << "  All the successors have been visited" << std::endl;
233
                stack_item f_dest(f);
234
                pop(st_blue);
235
                typename heap::color_ref c = h.get_color_ref(f_dest.s);
236
                assert(!c.is_white());
237
                if (!st_blue.empty() &&
238
		    a_->acc().accepting(f_dest.acc) && c.get_color() != RED)
239
                  {
240 241 242 243
                    // 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.
244 245 246 247
                    trace << "  It is blue and the arc from "
                          << a_->format_state(st_blue.front().s)
                          << " to it is accepting, start a red dfs"
                          << std::endl;
248
                    target = st_blue.front().s;
249
                    c.set_color(RED);
250 251 252 253 254
                    push(st_red, f_dest.s, f_dest.label, f_dest.acc);
                    if (dfs_red())
                      return true;
                  }
                else
255
                  {
256
                    trace << "  Pop it" << std::endl;
257 258
                    h.pop_notify(f_dest.s);
                  }
259 260 261
              }
          }
        return false;
262
      }
263 264

      bool dfs_red()
265
      {
266 267 268 269 270 271 272
        assert(!st_red.empty());
        if (target->compare(st_red.front().s) == 0)
          return true;

        while (!st_red.empty())
          {
            stack_item& f = st_red.front();
273
            trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl;
274
            if (!f.it->done())
275 276
              {
                const state *s_prime = f.it->current_state();
277 278
                trace << "  Visit the successor: "
                      << a_->format_state(s_prime) << std::endl;
279
                bdd label = f.it->current_condition();
280
                auto acc = f.it->current_acceptance_conditions();
281
                // Go down the edge (f.s, <label, acc>, s_prime)
282
                f.it->next();
283
                inc_transitions();
284
                typename heap::color_ref c = h.get_color_ref(s_prime);
285
                if (c.is_white())
286
                  {
287 288 289 290 291 292 293
                    // If the red dfs find a white here, it must have crossed
                    // the blue stack and the target must be reached soon.
                    // Notice that this property holds only for explicit search.
                    // Collisions in bit-state hashing search can also lead
                    // to the visit of white state. Anyway, it is not necessary
                    // to visit white states either if a cycle can be missed
                    // with bit-state hashing search.
294
                    trace << "  It is white, pop it" << std::endl;
295
                    s_prime->destroy();
296 297 298
                  }
                else if (c.get_color() == BLUE)
                  {
299
                    trace << "  It is blue, go down" << std::endl;
300
                    c.set_color(RED);
301
                    push(st_red, s_prime, label, acc);
302 303
                    if (target->compare(s_prime) == 0)
                      return true;
304
                  }
305
                else
306
                  {
307
                    trace << "  It is red, pop it" << std::endl;
308
                    h.pop_notify(s_prime);
309 310 311 312
                  }
              }
            else // Backtrack
              {
313 314
                trace << "  All the successors have been visited, pop it"
                      << std::endl;
315
                h.pop_notify(f.s);
316
                pop(st_red);
317 318 319
              }
          }
        return false;
320 321
      }

322 323 324 325
      class result_from_stack: public emptiness_check_result,
        public acss_statistics
      {
      public:
326 327
        result_from_stack(std::shared_ptr<magic_search_> ms)
          : emptiness_check_result(ms->automaton()), ms_(ms)
328 329 330
        {
        }

331
        virtual twa_run_ptr accepting_run()
332
        {
333 334
          assert(!ms_->st_blue.empty());
          assert(!ms_->st_red.empty());
335

336
          auto run = std::make_shared<twa_run>();
337 338

          typename stack_type::const_reverse_iterator i, j, end;
339
          twa_run::steps* l;
340 341 342

          l = &run->prefix;

343 344
          i = ms_->st_blue.rbegin();
          end = ms_->st_blue.rend(); --end;
345 346 347
          j = i; ++j;
          for (; i != end; ++i, ++j)
            {
348
              twa_run::step s = { i->s->clone(), j->label, j->acc };
349 350 351 352 353
              l->push_back(s);
            }

          l = &run->cycle;

354
          j = ms_->st_red.rbegin();
355
          twa_run::step s = { i->s->clone(), j->label, j->acc };
356 357 358
          l->push_back(s);

          i = j; ++j;
359
          end = ms_->st_red.rend(); --end;
360 361
          for (; i != end; ++i, ++j)
            {
362
              twa_run::step s = { i->s->clone(), j->label, j->acc };
363 364 365 366 367 368 369 370 371 372 373
              l->push_back(s);
            }

          return run;
        }

        unsigned acss_states() const
        {
          return 0;
        }
      private:
374
        std::shared_ptr<magic_search_> ms_;
375 376 377 378 379 380 381
      };

#     define FROM_STACK "ar:from_stack"

      class magic_search_result: public emptiness_check_result
      {
      public:
382 383 384
        magic_search_result(const std::shared_ptr<magic_search_>& m,
			    option_map o = option_map())
          : emptiness_check_result(m->automaton(), o), ms(m)
385 386 387 388
        {
          if (options()[FROM_STACK])
            computer = new result_from_stack(ms);
          else
389
            computer = new ndfs_result<magic_search_<heap>, heap>(ms);
390 391 392 393 394 395 396
        }

        virtual void options_updated(const option_map& old)
        {
          if (old[FROM_STACK] && !options()[FROM_STACK])
            {
              delete computer;
397
              computer = new ndfs_result<magic_search_<heap>, heap>(ms);
398 399 400 401 402 403 404 405 406 407 408 409 410
            }
          else if (!old[FROM_STACK] && options()[FROM_STACK])
            {
              delete computer;
              computer = new result_from_stack(ms);
            }
        }

        virtual ~magic_search_result()
        {
          delete computer;
        }

411
        virtual twa_run_ptr accepting_run()
412 413 414 415 416 417 418 419 420 421 422
        {
          return computer->accepting_run();
        }

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

      private:
        emptiness_check_result* computer;
423
	std::shared_ptr<magic_search_> ms;
424
      };
425 426 427 428 429
    };

    class explicit_magic_search_heap
    {
    public:
430 431
      enum { Safe = 1 };

432
      class color_ref
433
      {
434 435
      public:
        color_ref(color* c) :p(c)
436 437
	{
	}
438
        color get_color() const
439 440 441
	{
	  return *p;
	}
442
        void set_color(color c)
443 444 445 446
	{
	  assert(!is_white());
	  *p=c;
	}
447
        bool is_white() const
448 449 450
	{
	  return !p;
	}
451 452 453 454
      private:
        color *p;
      };

455
      explicit_magic_search_heap(size_t)
456 457 458 459 460 461 462 463 464 465 466
        {
        }

      ~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;
467
              ptr->destroy();
468 469 470 471 472 473
            }
        }

      color_ref get_color_ref(const state*& s)
        {
          hash_type::iterator it = h.find(s);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
474
          if (it == h.end())
475
            return color_ref(nullptr);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
476
          if (s != it->first)
477
            {
478
              s->destroy();
479 480
              s = it->first;
            }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
481
          return color_ref(&it->second);
482 483 484 485
        }

      void add_new_state(const state* s, color c)
        {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
486
          assert(h.find(s) == h.end());
487
          h.emplace(s, c);
488
        }
489

490
      void pop_notify(const state*) const
491 492 493
        {
        }

494
      bool has_been_visited(const state* s) const
495 496
        {
          hash_type::const_iterator it = h.find(s);
497
          return (it != h.end());
498 499
        }

500
      enum { Has_Size = 1 };
501 502 503 504 505
      int size() const
        {
          return h.size();
        }

506 507
    private:

508 509
      typedef std::unordered_map<const state*, color,
				 state_ptr_hash, state_ptr_equal> hash_type;
510 511 512
      hash_type h;
    };

513 514 515
    class bsh_magic_search_heap
    {
    public:
516 517
      enum { Safe = 0 };

518 519 520 521 522 523
      class color_ref
      {
      public:
        color_ref(unsigned char *b, unsigned char o): base(b), offset(o*2)
          {
          }
524
        color get_color() const
525 526 527
          {
            return color(((*base) >> offset) & 3U);
          }
528
        void set_color(color c)
529 530 531 532 533
          {
            *base =  (*base & ~(3U << offset)) | (c << offset);
          }
        bool is_white() const
          {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
534
            return get_color() == WHITE;
535 536 537 538 539 540 541 542
          }
      private:
        unsigned char *base;
        unsigned char offset;
      };

      bsh_magic_search_heap(size_t s)
        {
543 544 545
          size_ = s;
          h = new unsigned char[size_];
          memset(h, WHITE, size_);
546 547 548 549 550 551 552 553 554 555
        }

      ~bsh_magic_search_heap()
        {
          delete[] h;
        }

      color_ref get_color_ref(const state*& s)
        {
          size_t ha = s->hash();
556
          return color_ref(&(h[ha%size_]), ha%4);
557 558 559 560 561 562
        }

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

566
      void pop_notify(const state* s) const
567
        {
568
          s->destroy();
569 570
        }

571
      bool has_been_visited(const state* s) const
572 573
        {
          size_t ha = s->hash();
574 575 576
          return color((h[ha%size_] >> ((ha%4)*2)) & 3U) != WHITE;
        }

577
      enum { Has_Size = 0 };
578

579
    private:
580
      size_t size_;
581 582 583
      unsigned char* h;
    };

584 585
  } // anonymous

586
  emptiness_check_ptr
587
  explicit_magic_search(const const_twa_ptr& a, option_map o)
588
  {
589
    return std::make_shared<magic_search_<explicit_magic_search_heap>>(a, 0, o);
590 591
  }

592
  emptiness_check_ptr
593
  bit_state_hashing_magic_search(const const_twa_ptr& a,
594
				 size_t size, option_map o)
595
  {
596
    return std::make_shared<magic_search_<bsh_magic_search_heap>>(a, size, o);
597 598
  }

599
  emptiness_check_ptr
600
  magic_search(const const_twa_ptr& a, option_map o)
601 602 603 604 605
  {
    size_t size = o.get("bsh");
    if (size)
      return bit_state_hashing_magic_search(a, size, o);
    return explicit_magic_search(a, o);
606 607 608
  }

}