ndfs_result.hxx 19.9 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 5 6
// Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
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
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/>.
22

23
#pragma once
24

25
//#define NDFSR_TRACE
26 27

#include <iostream>
28 29
#ifdef NDFSR_TRACE
#define ndfsr_trace std::cerr
30
#else
31
#define ndfsr_trace while (0) std::cerr
32 33
#endif

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


namespace spot
{
  struct stack_item
  {
48
    stack_item(const state* n, twa_succ_iterator* i, bdd l, acc_cond::mark_t a)
49 50 51 52
      : 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.
53
    twa_succ_iterator* it;
54 55 56 57 58
    /// The label of the transition traversed to reach \a s
    /// (false for the first one).
    bdd label;
    /// The acceptance set of the transition traversed to reach \a s
    /// (false for the first one).
59
    acc_cond::mark_t acc;
60 61 62 63
  };

  typedef std::list<stack_item> stack_type;

64 65 66 67 68 69
  namespace
  {
    // The acss_statistics is available only when the heap has a
    // size() method (which we indicate using n==1).

    template <typename T, int n>
70 71
    struct stats_interface
      : public ars_statistics
72 73 74 75
    {
    };

    template <typename T>
76
    struct stats_interface<T, 1>
77 78
      : public acss_statistics
    {
79
      unsigned
80 81 82
      acss_states() const
      {
	// all visited states are in the state space search
83
	return static_cast<const T*>(this)->h_.size();
84 85 86 87 88 89
      }
    };

  }


90
  template <typename ndfs_search, typename heap>
91 92
  class ndfs_result:
    public emptiness_check_result,
93 94
    // Conditionally inherit from acss_statistics or ars_statistics.
    public stats_interface<ndfs_result<ndfs_search, heap>, heap::Has_Size>
95 96
  {
  public:
97 98 99
    ndfs_result(const std::shared_ptr<ndfs_search>& ms)
      : emptiness_check_result(ms->automaton()), ms_(ms),
        h_(ms->get_heap())
100 101
    {
    }
102 103

    virtual ~ndfs_result()
104 105
    {
    }
106

107
    virtual twa_run_ptr accepting_run()
108
    {
109 110
      const stack_type& stb = ms_->get_st_blue();
      const stack_type& str = ms_->get_st_red();
111

112
      assert(!stb.empty());
113

114
      acc_cond::mark_t covered_acc = 0U;
115
      accepting_transitions_list acc_trans;
116

117
      const state* start;
118

119 120 121
      start = stb.front().s->clone();
      if (!str.empty())
        {
122
          if (a_->num_sets() == 0)
123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
            {
              // take arbitrarily the last transition on the red stack
              stack_type::const_iterator i, j;
              i = j = str.begin(); ++i;
              if (i == str.end())
                i = stb.begin();
              transition t = { i->s->clone(), j->label, j->acc,
			       j->s->clone() };
              assert(h_.has_been_visited(t.source));
              assert(h_.has_been_visited(t.dest));
              acc_trans.push_back(t);
            }
          else
            {
              // ignore the prefix
              stack_type::const_reverse_iterator i, j;
139

140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165
              i = j = stb.rbegin(); ++j;
              while (i->s->compare(start) != 0)
		++i, ++j;

              stack_type::const_reverse_iterator end = stb.rend();
              for (; j != end; ++i, ++j)
                {
                  if ((covered_acc & j->acc) != j->acc)
                    {
                      transition t = { i->s->clone(), j->label, j->acc,
				       j->s->clone() };
                      assert(h_.has_been_visited(t.source));
                      assert(h_.has_been_visited(t.dest));
                      acc_trans.push_back(t);
                      covered_acc |= j->acc;
                    }
                }

              j = str.rbegin();
              if ((covered_acc & j->acc) != j->acc)
                {
                  transition t = { i->s->clone(), j->label, j->acc,
				   j->s->clone() };
                  assert(h_.has_been_visited(t.source));
                  assert(h_.has_been_visited(t.dest));
                  acc_trans.push_back(t);
166
		  covered_acc |= j->acc;
167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184
                }

              i = j; ++j;
              end = str.rend();
              for (; j != end; ++i, ++j)
                {
                  if ((covered_acc & j->acc) != j->acc)
                    {
                      transition t = { i->s->clone(), j->label, j->acc,
				       j->s->clone() };
                      assert(h_.has_been_visited(t.source));
                      assert(h_.has_been_visited(t.dest));
                      acc_trans.push_back(t);
                      covered_acc |= j->acc;
                    }
                }
            }
        }
185

186
      if (!a_->acc().accepting(covered_acc))
187 188 189 190 191
        {
          bool b = dfs(start, acc_trans, covered_acc);
          assert(b);
          (void) b;
        }
192

193
      start->destroy();
194

195
      assert(!acc_trans.empty());
196

197
      auto run = std::make_shared<twa_run>();
198 199 200 201 202 203
      // construct run->cycle from acc_trans.
      construct_cycle(run, acc_trans);
      // construct run->prefix (a minimal path from the initial state to any
      // state of run->cycle) and adjust the cycle to the state reached by the
      // prefix.
      construct_prefix(run);
204

205 206 207
      for (typename accepting_transitions_list::const_iterator i =
	     acc_trans.begin(); i != acc_trans.end(); ++i)
        {
208 209
          i->source->destroy();
          i->dest->destroy();
210 211 212 213
        }

      return run;
    }
214 215

  private:
216
    std::shared_ptr<ndfs_search> ms_;
217
    const heap& h_;
218
    template <typename T, int n>
219
    friend struct stats_interface;
220 221 222 223

    struct transition {
      const state* source;
      bdd label;
224
      acc_cond::mark_t acc;
225 226 227
      const state* dest;
    };
    typedef std::list<transition> accepting_transitions_list;
228

229 230
    typedef std::unordered_set<const state*,
			       state_ptr_hash, state_ptr_equal> state_set;
231

232
    void clean(const const_twa_ptr& a, stack_type& st1,
233
	       state_set& seen, state_set& dead)
234 235 236
    {
      while (!st1.empty())
	{
237
	  a->release_iter(st1.front().it);
238 239 240 241 242 243
	  st1.pop_front();
	}
      for (state_set::iterator i = seen.begin(); i != seen.end();)
	{
	  const state* s = *i;
	  ++i;
244
	  s->destroy();
245 246 247 248 249
	}
      for (state_set::iterator i = dead.begin(); i != dead.end();)
	{
	  const state* s = *i;
	  ++i;
250
	  s->destroy();
251 252 253 254
	}
    }

    bool dfs(const state* target, accepting_transitions_list& acc_trans,
255
	     acc_cond::mark_t& covered_acc)
256 257 258 259 260 261 262 263
    {
      assert(h_.has_been_visited(target));
      stack_type st1;

      state_set seen, dead;
      const state* start = target->clone();

      seen.insert(start);
264
      twa_succ_iterator* i = a_->succ_iter(start);
265
      i->first();
266
      st1.emplace_front(start, i, bddfalse, 0U);
267 268 269 270 271 272 273

      while (!st1.empty())
        {
          stack_item& f = st1.front();
          ndfsr_trace << "DFS1 treats: " << a_->format_state(f.s)
                      << std::endl;
          if (!f.it->done())
274
            {
275 276 277 278
              const state *s_prime = f.it->current_state();
              ndfsr_trace << "  Visit the successor: "
                          << a_->format_state(s_prime) << std::endl;
              bdd label = f.it->current_condition();
279
	      auto acc = f.it->current_acceptance_conditions();
280 281 282 283 284 285
              f.it->next();
              if (h_.has_been_visited(s_prime))
                {
                  if (dead.find(s_prime) != dead.end())
                    {
                      ndfsr_trace << "  it is dead, pop it" << std::endl;
286
                      s_prime->destroy();
287 288 289
                    }
                  else if (seen.find(s_prime) == seen.end())
                    {
290
		      this->inc_ars_cycle_states();
291 292
                      ndfsr_trace << "  it is not seen, go down" << std::endl;
                      seen.insert(s_prime);
293
                      twa_succ_iterator* i = a_->succ_iter(s_prime);
294
                      i->first();
295
                      st1.emplace_front(s_prime, i, label, acc);
296 297 298
                    }
                  else if ((acc & covered_acc) != acc)
                    {
299
		      this->inc_ars_cycle_states();
300 301 302 303 304 305 306 307 308 309
                      ndfsr_trace << "  a propagation is needed, "
                                  << "start a search" << std::endl;
                      if (search(s_prime, target, dead))
                        {
                          transition t = { f.s->clone(), label, acc,
					   s_prime->clone() };
                          assert(h_.has_been_visited(t.source));
                          assert(h_.has_been_visited(t.dest));
                          acc_trans.push_back(t);
                          covered_acc |= acc;
310
                          if (a_->acc().accepting(covered_acc))
311
                            {
312
                              clean(a_, st1, seen, dead);
313
                              s_prime->destroy();
314 315 316
                              return true;
                            }
                        }
317
                      s_prime->destroy();
318 319 320 321
                    }
                  else
                    {
                      ndfsr_trace << "  already seen, pop it" << std::endl;
322
                      s_prime->destroy();
323 324 325 326 327 328
                    }
                }
              else
                {
                  ndfsr_trace << "  not seen during the search, pop it"
                              << std::endl;
329
                  s_prime->destroy();
330
                }
331
            }
332
          else
333
            {
334 335 336
              ndfsr_trace << "  all the successors have been visited"
                          << std::endl;
              stack_item f_dest(f);
337
              a_->release_iter(st1.front().it);
338
              st1.pop_front();
339
              if (!st1.empty() && ((f_dest.acc & covered_acc) != f_dest.acc))
340 341 342 343 344 345 346 347 348 349 350
                {
                  ndfsr_trace << "  a propagation is needed, start a search"
                              << std::endl;
                  if (search(f_dest.s, target, dead))
                    {
		      transition t = { st1.front().s->clone(),
				       f_dest.label, f_dest.acc,
				       f_dest.s->clone() };
                      assert(h_.has_been_visited(t.source));
                      assert(h_.has_been_visited(t.dest));
                      acc_trans.push_back(t);
351 352
		      covered_acc |= f_dest.acc;
                      if (a_->acc().accepting(covered_acc))
353
                        {
354
                          clean(a_, st1, seen, dead);
355 356 357 358 359 360 361 362 363
                          return true;
                        }
                    }
                }
              else
                {
                  ndfsr_trace << "  no propagation needed, pop it"
                              << std::endl;
                }
364
            }
365
        }
366

367
      clean(a_, st1, seen, dead);
368 369
      return false;
    }
370 371

    class test_path: public bfs_steps
372 373
    {
    public:
374
      test_path(ars_statistics* ars,
375
		const const_twa_ptr& a, const state* t,
376
		const state_set& d, const heap& h)
377
        : bfs_steps(a), ars(ars), target(t), dead(d), h(h)
378 379 380
      {
      }

381
      ~test_path()
382
      {
383 384 385 386 387
        state_set::const_iterator i = seen.begin();
        while (i != seen.end())
          {
            const state* ptr = *i;
            ++i;
388
            ptr->destroy();
389
          }
390 391
      }

392
      const state* search(const state* start, twa_run::steps& l)
393 394 395 396 397
      {
        const state* s = filter(start);
        if (s)
          return this->bfs_steps::search(s, l);
        else
398
          return nullptr;
399 400
      }

401
      const state* filter(const state* s)
402
      {
403 404 405
        if (!h.has_been_visited(s)
	    || seen.find(s) != seen.end()
	    || dead.find(s) != dead.end())
406
          {
407
            s->destroy();
408
            return nullptr;
409
          }
410
	ars->inc_ars_cycle_states();
411 412 413 414
        seen.insert(s);
        return s;
      }

415
      void finalize(const std::map<const state*, twa_run::step,
416
		                   state_ptr_less_than>&,
417
		    const twa_run::step&, const state*, twa_run::steps&)
418 419 420 421
      {
      }

      const state_set& get_seen() const
422 423 424 425
      {
        return seen;
      }

426
      bool match(twa_run::step&, const state* dest)
427 428 429 430 431
      {
        return target->compare(dest) == 0;
      }

    private:
432
      ars_statistics* ars;
433 434 435 436 437 438
      state_set seen;
      const state* target;
      const state_set& dead;
      const heap& h;
    };

439
    bool search(const state* start, const state* target, state_set& dead)
440
    {
441
      twa_run::steps path;
442 443 444
      if (start->compare(target) == 0)
	return true;

445
      test_path s(this, a_, target, dead, h_);
446 447 448 449 450 451 452 453 454 455 456 457 458 459
      const state* res = s.search(start->clone(), path);
      if (res)
	{
	  assert(res->compare(target) == 0);
	  return true;
	}
      else
	{
	  state_set::const_iterator it;
	  for (it = s.get_seen().begin(); it != s.get_seen().end(); ++it)
	    dead.insert((*it)->clone());
	  return false;
	}
    }
460

461 462 463
    typedef std::unordered_multimap<const state*, transition,
				    state_ptr_hash,
				    state_ptr_equal> m_source_trans;
464

465
    template<bool cycle>
466 467 468
    class min_path: public bfs_steps
    {
    public:
469
      min_path(ars_statistics* ars,
470
	       const const_twa_ptr& a,
471
	       const m_source_trans& target, const heap& h)
472
        : bfs_steps(a), ars(ars), target(target), h(h)
473 474
      {
      }
475

476 477 478 479 480 481 482
      ~min_path()
      {
        state_set::const_iterator i = seen.begin();
        while (i != seen.end())
          {
            const state* ptr = *i;
            ++i;
483
            ptr->destroy();
484
          }
485 486
      }

487
      const state* search(const state* start, twa_run::steps& l)
488
      {
489 490 491 492
        const state* s = filter(start);
        if (s)
          return this->bfs_steps::search(s, l);
        else
493
          return nullptr;
494
      }
495

496 497 498 499
      const state* filter(const state* s)
      {
        ndfsr_trace << "filter: " << a_->format_state(s);
        if (!h.has_been_visited(s) || seen.find(s) != seen.end())
500
          {
501 502 503 504
            if (!h.has_been_visited(s))
              ndfsr_trace << " not visited" << std::endl;
            else
              ndfsr_trace << " already seen" << std::endl;
505
            s->destroy();
506
            return nullptr;
507 508
          }
        ndfsr_trace << " OK" << std::endl;
509 510 511 512
	if (cycle)
	  ars->inc_ars_cycle_states();
	else
	  ars->inc_ars_prefix_states();
513 514 515 516
        seen.insert(s);
        return s;
      }

517
      bool match(twa_run::step&, const state* dest)
518 519 520 521 522 523 524
      {
        ndfsr_trace << "match: " << a_->format_state(dest)
                    << std::endl;
        return target.find(dest) != target.end();
      }

    private:
525
      ars_statistics* ars;
526 527 528 529 530
      state_set seen;
      const m_source_trans& target;
      const heap& h;
    };

531
    void construct_cycle(twa_run_ptr run,
532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553
			 const accepting_transitions_list& acc_trans)
    {
      assert(!acc_trans.empty());
      transition current = acc_trans.front();
      // insert the first accepting transition in the cycle
      ndfsr_trace << "the initial accepting transition is from "
		  << a_->format_state(current.source) << " to "
		  << a_->format_state(current.dest) << std::endl;
      const state* begin = current.source;

      m_source_trans target;
      typename accepting_transitions_list::const_iterator i =
	acc_trans.begin();
      ndfsr_trace << "targets are the source states: ";
      for (++i; i != acc_trans.end(); ++i)
	{
	  if (i->source->compare(begin) == 0 &&
	      i->source->compare(i->dest) == 0)
	    {
	      ndfsr_trace << "(self loop " << a_->format_state(i->source)
			  << " -> " << a_->format_state(i->dest)
			  << " ignored) ";
554
	      twa_run::step st = { i->source->clone(), i->label, i->acc };
555 556 557 558 559 560
	      run->cycle.push_back(st);
	    }
	  else
	    {
	      ndfsr_trace << a_->format_state(i->source) << " (-> "
			  << a_->format_state(i->dest) << ") ";
561
	      target.emplace(i->source, *i);
562 563 564 565
	    }
	}
      ndfsr_trace << std::endl;

566
      twa_run::step st = { current.source->clone(), current.label,
567 568 569 570 571 572 573 574 575 576 577 578
			    current.acc };
      run->cycle.push_back(st);

      while (!target.empty())
	{
	  // find a minimal path from current.dest to any source state in
	  // target.
	  ndfsr_trace << "looking for a path from "
		      << a_->format_state(current.dest) << std::endl;
	  typename m_source_trans::iterator i = target.find(current.dest);
	  if (i == target.end())
	    {
579
	      min_path<true> s(this, a_, target, h_);
580 581 582 583 584 585 586 587 588 589 590 591 592
	      const state* res = s.search(current.dest->clone(), run->cycle);
	      // init current to the corresponding transition.
	      assert(res);
	      ndfsr_trace << a_->format_state(res) << " reached" << std::endl;
	      i = target.find(res);
	      assert(i != target.end());
	    }
	  else
	    {
	      ndfsr_trace << "this is a target" << std::endl;
	    }
	  current = i->second;
	  // complete the path with the corresponding transition
593
	  twa_run::step st = { current.source->clone(), current.label,
594 595 596 597 598 599 600 601 602 603 604 605 606 607
				current.acc };
	  run->cycle.push_back(st);
	  // remove this source state of target
	  target.erase(i);
	}

      if (current.dest->compare(begin) != 0)
	{
	  // close the cycle by adding a path from the destination of the
	  // last inserted transition to the source of the first one
	  ndfsr_trace << std::endl << "looking for a path from "
		      << a_->format_state(current.dest) << " to "
		      << a_->format_state(begin) << std::endl;
	  transition tmp;
608 609
	  // Initialize to please GCC 4.0.1 (Darwin).
	  tmp.source = tmp.dest = nullptr;
610
	  tmp.acc = 0U;
611
	  target.emplace(begin, tmp);
612
	  min_path<true> s(this, a_, target, h_);
613 614 615 616 617 618
	  const state* res = s.search(current.dest->clone(), run->cycle);
	  assert(res);
	  assert(res->compare(begin) == 0);
	  (void)res;
	}
    }
619

620
    void construct_prefix(twa_run_ptr run)
621 622 623
    {
      m_source_trans target;
      transition tmp;
624
      tmp.source = tmp.dest = nullptr; // Initialize to please GCC 4.0.
625
      tmp.acc = 0U;
626 627

      // Register all states from the cycle as target of the BFS.
628
      for (twa_run::steps::const_iterator i = run->cycle.begin();
629
	   i != run->cycle.end(); ++i)
630
        target.emplace(i->s, tmp);
631 632 633 634 635 636 637 638 639 640 641 642

      const state* prefix_start = a_->get_init_state();
      // There are two cases: either the initial state is already on
      // the cycle, or it is not.  If it is, we will have to rotate
      // the cycle so it begins on this position.  Otherwise we will shift
      // the cycle so it begins on the state that follows the prefix.
      // cycle_entry_point is that state.
      const state* cycle_entry_point;
      typename m_source_trans::const_iterator ps = target.find(prefix_start);
      if (ps != target.end())
        {
          // The initial state is on the cycle.
643
          prefix_start->destroy();
644 645 646 647 648
          cycle_entry_point = ps->first->clone();
        }
      else
        {
          // This initial state is outside the cycle.  Compute the prefix.
649
          min_path<false> s(this, a_, target, h_);
650 651 652 653 654 655
          cycle_entry_point = s.search(prefix_start, run->prefix);
          assert(cycle_entry_point);
          cycle_entry_point = cycle_entry_point->clone();
        }

      // Locate cycle_entry_point on the cycle.
656
      twa_run::steps::iterator cycle_ep_it;
657 658 659 660 661
      for (cycle_ep_it = run->cycle.begin();
	   cycle_ep_it != run->cycle.end()
	     && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it)
        continue;
      assert(cycle_ep_it != run->cycle.end());
662
      cycle_entry_point->destroy();
663 664 665 666 667

      // Now shift the cycle so it starts on cycle_entry_point.
      run->cycle.splice(run->cycle.end(), run->cycle,
                        run->cycle.begin(), cycle_ep_it);
    }
668 669 670 671
  };

}

672
#undef ndfsr_trace