ndfs_result.hxx 21.4 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2011, 2013, 2014, 2015, 2016, 2018 Laboratoire de recherche
3
// et 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
37
38
39
40
#include <spot/misc/hash.hh>
#include <spot/twa/twa.hh>
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/emptiness_stats.hh>
#include <spot/twaalgos/bfssteps.hh>
41
42
43
44
45

namespace spot
{
  struct stack_item
  {
46
    stack_item(const state* n, twa_succ_iterator* i, bdd l, acc_cond::mark_t a)
47
      noexcept : s(n), it(i), label(l), acc(a) {};
48
49
50
    /// The visited state.
    const state* s;
    /// Design the next successor of \a s which has to be visited.
51
    twa_succ_iterator* it;
52
53
54
55
56
    /// 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).
57
    acc_cond::mark_t acc;
58
59
60
61
  };

  typedef std::list<stack_item> stack_type;

62
63
64
65
66
67
  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>
68
69
    struct stats_interface
      : public ars_statistics
70
71
72
73
    {
    };

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

  }


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

    virtual ~ndfs_result()
102
103
    {
    }
104

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

110
      SPOT_ASSERT(!stb.empty());
111

112
      acc_cond::mark_t covered_acc = {};
113
      accepting_transitions_list acc_trans;
114

115
      const state* start;
116

117
118
119
      start = stb.front().s->clone();
      if (!str.empty())
        {
120
          if (a_->num_sets() == 0)
121
122
123
124
125
126
127
            {
              // 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,
128
                               j->s->clone() };
129
130
              SPOT_ASSERT(h_.has_been_visited(t.source));
              SPOT_ASSERT(h_.has_been_visited(t.dest));
131
132
133
134
135
136
              acc_trans.push_back(t);
            }
          else
            {
              // ignore the prefix
              stack_type::const_reverse_iterator i, j;
137

138
139
              i = j = stb.rbegin(); ++j;
              while (i->s->compare(start) != 0)
140
                ++i, ++j;
141
142
143
144
145
146
147

              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,
148
                                       j->s->clone() };
149
150
                      SPOT_ASSERT(h_.has_been_visited(t.source));
                      SPOT_ASSERT(h_.has_been_visited(t.dest));
151
152
153
154
155
156
157
158
159
                      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,
160
                                   j->s->clone() };
161
162
                  SPOT_ASSERT(h_.has_been_visited(t.source));
                  SPOT_ASSERT(h_.has_been_visited(t.dest));
163
                  acc_trans.push_back(t);
164
                  covered_acc |= j->acc;
165
166
167
168
169
170
171
172
173
                }

              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,
174
                                       j->s->clone() };
175
176
                      SPOT_ASSERT(h_.has_been_visited(t.source));
                      SPOT_ASSERT(h_.has_been_visited(t.dest));
177
178
179
180
181
182
                      acc_trans.push_back(t);
                      covered_acc |= j->acc;
                    }
                }
            }
        }
183

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

191
      start->destroy();
192

193
      SPOT_ASSERT(!acc_trans.empty());
194

195
      auto run = std::make_shared<twa_run>(automaton());
196
197
198
199
200
201
      // 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);
202

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

      return run;
    }
212
213

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

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

227
    typedef std::unordered_set<const state*,
228
                               state_ptr_hash, state_ptr_equal> state_set;
229

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

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

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

      seen.insert(start);
262
      twa_succ_iterator* i = a_->succ_iter(start);
263
      i->first();
264
      st1.emplace_front(start, i, bddfalse, acc_cond::mark_t({}));
265
266
267
268
269
270
271

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

365
      clean(a_, st1, seen, dead);
366
367
      return false;
    }
368
369

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      m_source_trans target;
      typename accepting_transitions_list::const_iterator i =
543
        acc_trans.begin();
544
545
      ndfsr_trace << "targets are the source states: ";
      for (++i; i != acc_trans.end(); ++i)
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
        {
          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) ";
              twa_run::step st = { i->source->clone(), i->label, i->acc };
              run->cycle.push_back(st);
            }
          else
            {
              ndfsr_trace << a_->format_state(i->source) << " (-> "
                          << a_->format_state(i->dest) << ") ";
              target.emplace(i->source, *i);
            }
        }
563
564
      ndfsr_trace << std::endl;

565
      twa_run::step st = { current.source->clone(), current.label,
566
                            current.acc };
567
568
569
      run->cycle.push_back(st);

      while (!target.empty())
570
571
572
573
574
575
576
577
578
579
580
        {
          // 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())
            {
              min_path<true> s(this, a_, target, h_);
              const state* res = s.search(current.dest->clone(), run->cycle);
              // init current to the corresponding transition.
581
              SPOT_ASSERT(res);
582
583
              ndfsr_trace << a_->format_state(res) << " reached" << std::endl;
              i = target.find(res);
584
              SPOT_ASSERT(i != target.end());
585
586
587
588
589
590
591
592
593
594
595
596
597
            }
          else
            {
              ndfsr_trace << "this is a target" << std::endl;
            }
          current = i->second;
          // complete the path with the corresponding transition
          twa_run::step st = { current.source->clone(), current.label,
                                current.acc };
          run->cycle.push_back(st);
          // remove this source state of target
          target.erase(i);
        }
598
599

      if (current.dest->compare(begin) != 0)
600
601
602
603
604
605
606
607
608
        {
          // 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;
          // Initialize to please GCC 4.0.1 (Darwin).
          tmp.source = tmp.dest = nullptr;
609
          tmp.acc = {};
610
611
612
          target.emplace(begin, tmp);
          min_path<true> s(this, a_, target, h_);
          const state* res = s.search(current.dest->clone(), run->cycle);
613
614
          SPOT_ASSERT(res);
          SPOT_ASSERT(res->compare(begin) == 0);
615
616
          (void)res;
        }
617
    }
618

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

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

      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.
642
          prefix_start->destroy();
643
644
645
646
647
          cycle_entry_point = ps->first->clone();
        }
      else
        {
          // This initial state is outside the cycle.  Compute the prefix.
648
          min_path<false> s(this, a_, target, h_);
649
          cycle_entry_point = s.search(prefix_start, run->prefix);
650
          SPOT_ASSUME(cycle_entry_point);
651
652
653
654
          cycle_entry_point = cycle_entry_point->clone();
        }

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

      // 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);
    }
667
668
669
670
  };

}

671
#undef ndfsr_trace