sccinfo.hh 20.2 KB
Newer Older
1
// -*- coding: utf-8 -*-
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
3
// de l'Epita (LRDE).
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
//
// 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.

20
#pragma once
21
22

#include <vector>
23
#include <spot/twa/twagraph.hh>
24
25
26

namespace spot
{
27
28
29
30
31
32
  class scc_info;

  namespace internal
  {
    struct keep_all
    {
33
34
      template <typename Iterator>
      bool operator()(Iterator, Iterator) const noexcept
35
36
37
38
39
      {
        return true;
      }
    };

40
41
    // Keep only transitions that have at least one destination in the
    // current SCC.
42
43
44
45
46
47
48
49
50
51
52
    struct keep_inner_scc
    {
    private:
      const std::vector<unsigned>& sccof_;
      unsigned desired_scc_;
    public:
      keep_inner_scc(const std::vector<unsigned>& sccof, unsigned desired_scc)
        : sccof_(sccof), desired_scc_(desired_scc)
      {
      }

53
54
      template <typename Iterator>
      bool operator()(Iterator begin, Iterator end) const noexcept
55
      {
56
57
58
59
60
61
62
63
        bool want = false;
        while (begin != end)
          if (sccof_[*begin++] == desired_scc_)
            {
              want = true;
              break;
            }
        return want;
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
      }
    };

    template <typename Graph, typename Filter>
    class SPOT_API scc_edge_iterator
    {
    public:
      typedef typename std::conditional<std::is_const<Graph>::value,
                                        const typename Graph::edge_storage_t,
                                        typename Graph::edge_storage_t>::type
        value_type;
      typedef value_type& reference;
      typedef value_type* pointer;
      typedef std::ptrdiff_t difference_type;
      typedef std::forward_iterator_tag iterator_category;

      typedef std::vector<unsigned>::const_iterator state_iterator;

      typedef typename std::conditional<std::is_const<Graph>::value,
                                        const typename Graph::edge_vector_t,
                                        typename Graph::edge_vector_t>::type
        tv_t;

      typedef typename std::conditional<std::is_const<Graph>::value,
                                        const typename Graph::state_vector,
                                        typename Graph::state_vector>::type
        sv_t;
91
      typedef const typename Graph::dests_vector_t dv_t;
92
93
94
95
96
97
98
    protected:

      state_iterator pos_;
      state_iterator end_;
      unsigned t_;
      tv_t* tv_;
      sv_t* sv_;
99
100
      dv_t* dv_;

101
102
103
104
105
106
107
108
109
110
111
112
113
114
      Filter filt_;

      void inc_state_maybe_()
      {
        while (!t_ && (++pos_ != end_))
          t_ = (*sv_)[*pos_].succ;
      }

      void inc_()
      {
        t_ = (*tv_)[t_].next_succ;
        inc_state_maybe_();
      }

115
116
117
118
119
120
121
122
123
124
125
      bool ignore_current()
      {
        unsigned dst = (*this)->dst;
        if ((int)dst >= 0)
          // Non-universal branching => a single destination.
          return !filt_(&(*this)->dst, 1 + &(*this)->dst);
        // Universal branching => multiple destinations.
        const unsigned* d = dv_->data() + ~dst;
        return !filt_(d + 1, d + *d + 1);
      }

126
127
    public:
      scc_edge_iterator(state_iterator begin, state_iterator end,
128
129
                        tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
        : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
130
131
132
133
134
135
      {
        if (pos_ == end_)
          return;

        t_ = (*sv_)[*pos_].succ;
        inc_state_maybe_();
136
        while (pos_ != end_ && ignore_current())
137
138
139
140
141
142
143
          inc_();
      }

      scc_edge_iterator& operator++()
      {
        do
          inc_();
144
        while (pos_ != end_ && ignore_current());
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
        return *this;
      }

      scc_edge_iterator operator++(int)
      {
        scc_edge_iterator old = *this;
        ++*this;
        return old;
      }

      bool operator==(scc_edge_iterator o) const
      {
        return pos_ == o.pos_ && t_ == o.t_;
      }

      bool operator!=(scc_edge_iterator o) const
      {
        return pos_ != o.pos_ || t_ != o.t_;
      }

      reference operator*() const
      {
        return (*tv_)[t_];
      }

      pointer operator->() const
      {
        return &**this;
      }
    };


    template <typename Graph, typename Filter>
    class SPOT_API scc_edges
    {
    public:
      typedef scc_edge_iterator<Graph, Filter> iter_t;
      typedef typename iter_t::tv_t tv_t;
      typedef typename iter_t::sv_t sv_t;
184
      typedef typename iter_t::dv_t dv_t;
185
186
187
188
189
190
      typedef typename iter_t::state_iterator state_iterator;
    private:
      state_iterator begin_;
      state_iterator end_;
      tv_t* tv_;
      sv_t* sv_;
191
      dv_t* dv_;
192
193
194
195
      Filter filt_;
    public:

      scc_edges(state_iterator begin, state_iterator end,
196
197
                tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
        : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
198
199
200
201
202
      {
      }

      iter_t begin() const
      {
203
        return {begin_, end_, tv_, sv_, dv_, filt_};
204
205
206
207
      }

      iter_t end() const
      {
208
        return {end_, end_, nullptr, nullptr, nullptr, filt_};
209
210
211
212
      }
    };
  }

213

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
214
215
  /// \ingroup twa_misc
  /// \brief Storage for SCC related information.
216
217
218
219
220
221
222
  class SPOT_API scc_info_node
  {
  public:
    typedef std::vector<unsigned> scc_succs;
    friend class scc_info;
  protected:
    scc_succs succ_;
223
224
    std::vector<unsigned> states_; // States of the component
    unsigned one_state_;
225
    acc_cond::mark_t acc_;
226
    acc_cond::mark_t common_;
227
228
229
230
231
    bool trivial_:1;
    bool accepting_:1;        // Necessarily accepting
    bool rejecting_:1;        // Necessarily rejecting
    bool useful_:1;
  public:
232
    scc_info_node() noexcept:
233
      acc_({}), trivial_(true), accepting_(false),
234
235
236
237
      rejecting_(false), useful_(false)
    {
    }

238
    scc_info_node(acc_cond::mark_t acc,
239
240
                  acc_cond::mark_t common, bool trivial) noexcept
      : acc_(acc), common_(common),
241
      trivial_(trivial), accepting_(false),
242
243
244
245
246
247
248
249
250
      rejecting_(false), useful_(false)
    {
    }

    bool is_trivial() const
    {
      return trivial_;
    }

251
    /// \brief True if we know that the SCC has an accepting cycle
252
253
254
    ///
    /// Note that both is_accepting() and is_rejecting() may return
    /// false if an SCC interesects a mix of Fin and Inf sets.
255
    /// Call determine_unknown_acceptance() to decide.
256
257
258
259
260
    bool is_accepting() const
    {
      return accepting_;
    }

261
    /// \brief True if we know that all cycles in the SCC are rejecting
262
263
264
    ///
    /// Note that both is_accepting() and is_rejecting() may return
    /// false if an SCC interesects a mix of Fin and Inf sets.
265
    /// Call determine_unknown_acceptance() to decide.
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
    bool is_rejecting() const
    {
      return rejecting_;
    }

    bool is_useful() const
    {
      return useful_;
    }

    acc_cond::mark_t acc_marks() const
    {
      return acc_;
    }

281
282
283
284
285
    acc_cond::mark_t common_marks() const
    {
      return common_;
    }

286
287
288
289
290
    const std::vector<unsigned>& states() const
    {
      return states_;
    }

291
292
293
294
295
    unsigned one_state() const
    {
      return one_state_;
    }

296
297
298
299
300
301
    const scc_succs& succ() const
    {
      return succ_;
    }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
302
303
  /// \ingroup twa_misc
  /// \brief Options to alter the behavior of scc_info
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
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
  enum class scc_info_options
  {
    /// Stop exploring when an accepting SCC is found, and do not track
    /// the states of each SCC.
    NONE = 0,
    /// Stop exploring after an accepting SCC has been found.
    /// Using this option forbids future uses of is_useful_scc() and
    /// is_useful_state().  Using it will also cause the output of
    /// succ() to be incomplete.
    STOP_ON_ACC = 1,
    /// Keep a vector of all states belonging to each SCC.  Using this
    /// option is a precondition for using states_of(), edges_of(),
    /// inner_edges_of(), states_on_acc_cycle_of(), and
    /// determine_unknown_acceptance().
    TRACK_STATES = 2,
    /// Keep a list of successors of each SCCs.
    /// Using this option is a precondition for using succ(),
    /// is_useful_scc(), and is_useful_state().
    TRACK_SUCCS = 4,
    /// Conditionally track states if the acceptance conditions uses Fin.
    /// This is sufficiant for determine_unknown_acceptance().
    TRACK_STATES_IF_FIN_USED = 8,
    /// Default behavior: explore everything and track states and succs.
    ALL = TRACK_STATES | TRACK_SUCCS,
  };

  inline
  bool operator!(scc_info_options me)
  {
    return me == scc_info_options::NONE;
  }

  inline
  scc_info_options operator&(scc_info_options left, scc_info_options right)
  {
    typedef std::underlying_type_t<scc_info_options> ut;
    return static_cast<scc_info_options>(static_cast<ut>(left)
                                         & static_cast<ut>(right));
  }

  inline
  scc_info_options operator|(scc_info_options left, scc_info_options right)
  {
    typedef std::underlying_type_t<scc_info_options> ut;
    return static_cast<scc_info_options>(static_cast<ut>(left)
                                         | static_cast<ut>(right));
  }
351

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
352
  /// \ingroup twa_misc
353
354
355
356
  /// \brief Compute an SCC map and gather assorted information.
  ///
  /// This takes twa_graph as input and compute its SCCs.  This
  /// class maps all input states to their SCCs, and vice-versa.
357
  /// It allows iterating over all SCCs of the automaton, and checks
358
359
  /// their acceptance or non-acceptance.
  ///
360
361
362
363
364
  /// SCC are numbered in reverse topological order, i.e. the SCC of the
  /// initial state has the highest number, and if s1 is reachable from
  /// s2, then s1 < s2. Many algorithms depend on this property to
  /// determine in what order to iterate the SCCs.
  ///
365
366
367
368
369
  /// Additionally this class can be used on alternating automata, but
  /// in this case, universal transitions are handled like existential
  /// transitions.  It still make sense to check which states belong
  /// to the same SCC, but the acceptance information computed by
  /// this class is meaningless.
370
371
372
  class SPOT_API scc_info
  {
  public:
373
374
375
376
    // scc_node used to be an inner class, but Swig 3.0.10 does not
    // support that yet.
    typedef scc_info_node scc_node;
    typedef scc_info_node::scc_succs scc_succs;
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
    /// @{
    /// \brief An edge_filter may be called on each edge to decide what
    /// to do with it.
    ///
    /// The edge filter is called with an edge and a destination.  (In
    /// existential automata the destination is already given by the
    /// edge, but in alternating automata, one edge may have several
    /// destinations, and in this case the filter will be called for
    /// each destination.)  The filter should return a value from
    /// edge_filter_choice.
    ///
    /// \c keep means to use the edge normally, as if no filter had
    /// been given.  \c ignore means to pretend the edge does not
    /// exist (if the destination is only reachable through this edge,
    /// it will not be visited). \c cut also ignores the edge, but
    /// it remembers to visit the destination state (as if it were an
    /// initial state) in case it is not reachable otherwise.
    ///
    /// Note that successors between SCCs can only be maintained for
    /// edges that are kept.  If some edges are ignored or cut, the
    /// SCC graph that you can explore with scc_info::initial() and
    /// scc_info::succ() will be restricted to the portion reachable
    /// with "keep" edges.  Additionally SCCs might be created when
    /// edges are cut, but those will not be reachable from
    /// scc_info::initial()..
    enum class edge_filter_choice { keep, ignore, cut };
    typedef edge_filter_choice
      (*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst,
                     void* filter_data);
    /// @}
407
408
409
410
411

  protected:

    std::vector<unsigned> sccof_;
    std::vector<scc_node> node_;
412
    const_twa_graph_ptr aut_;
413
414
415
    unsigned initial_state_;
    edge_filter filter_;
    void* filter_data_;
416
417
    int one_acc_scc_ = -1;
    scc_info_options options_;
418

419
420
    // Update the useful_ bits.  Called automatically.
    void determine_usefulness();
421

422
    const scc_node& node(unsigned scc) const
423
424
425
426
    {
      return node_[scc];
    }

427
428
429
430
431
432
#ifndef SWIG
  private:
    [[noreturn]] static void report_need_track_states();
    [[noreturn]] static void report_need_track_succs();
    [[noreturn]] static void report_incompatible_stop_on_acc();
#endif
433

434
435
436
  public:
    /// @{
    /// \brief Create the scc_info map for \a aut
437
    scc_info(const_twa_graph_ptr aut,
438
439
             // Use ~0U instead of -1U to work around a bug in Swig.
             // See https://github.com/swig/swig/issues/993
440
441
             unsigned initial_state = ~0U,
             edge_filter filter = nullptr,
442
443
444
445
446
447
448
449
             void* filter_data = nullptr,
             scc_info_options options = scc_info_options::ALL);

    scc_info(const_twa_graph_ptr aut, scc_info_options options)
      : scc_info(aut, ~0U, nullptr, nullptr, options)
      {
      }
    /// @}
450

451
    const_twa_graph_ptr get_aut() const
452
453
454
455
456
    {
      return aut_;
    }

    unsigned scc_count() const
457
458
459
460
    {
      return node_.size();
    }

461
462
463
464
465
466
    /// Return the number of one accepting SCC if any, -1 otherwise.
    int one_accepting_scc() const
    {
      return one_acc_scc_;
    }

467
468
469
470
471
    bool reachable_state(unsigned st) const
    {
      return scc_of(st) != -1U;
    }

472
    unsigned scc_of(unsigned st) const
473
474
475
476
    {
      return sccof_[st];
    }

477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
    std::vector<scc_node>::const_iterator begin() const
    {
      return node_.begin();
    }

    std::vector<scc_node>::const_iterator end() const
    {
      return node_.end();
    }

    std::vector<scc_node>::const_iterator cbegin() const
    {
      return node_.cbegin();
    }

    std::vector<scc_node>::const_iterator cend() const
    {
      return node_.cend();
    }

    std::vector<scc_node>::const_reverse_iterator rbegin() const
    {
      return node_.rbegin();
    }

    std::vector<scc_node>::const_reverse_iterator rend() const
    {
      return node_.rend();
    }
506

507
    const std::vector<unsigned>& states_of(unsigned scc) const
508
    {
509
510
      if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
        report_need_track_states();
511
      return node(scc).states();
512
513
    }

514
515
516
517
518
519
520
521
522
523
524
    /// \brief A fake container to iterate over all edges leaving any
    /// state of an SCC.
    ///
    /// The difference with inner_edges_of() is that edges_of() include
    /// outgoing edges from all the states, even if they leave the SCC.
    internal::scc_edges<const twa_graph::graph_t, internal::keep_all>
    edges_of(unsigned scc) const
    {
      auto& states = states_of(scc);
      return {states.begin(), states.end(),
              &aut_->edge_vector(), &aut_->states(),
525
              &aut_->get_graph().dests_vector(),
526
527
528
529
530
531
              internal::keep_all()};
    }

    /// \brief A fake container to iterate over all edges between
    /// states of an SCC.
    ///
532
    /// The difference with edges_of() is that inner_edges_of()
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
533
    /// ignores edges leaving the SCC.  In the case of an
534
535
    /// alternating automaton, an edge is considered to be part of the
    /// SCC of one of its destination is in the SCC.
536
537
538
539
540
541
    internal::scc_edges<const twa_graph::graph_t, internal::keep_inner_scc>
    inner_edges_of(unsigned scc) const
    {
      auto& states = states_of(scc);
      return {states.begin(), states.end(),
              &aut_->edge_vector(), &aut_->states(),
542
              &aut_->get_graph().dests_vector(),
543
544
545
              internal::keep_inner_scc(sccof_, scc)};
    }

546
547
    unsigned one_state_of(unsigned scc) const
    {
548
      return node(scc).one_state();
549
550
551
552
553
    }

    /// \brief Get number of the SCC containing the initial state.
    unsigned initial() const
    {
554
555
      SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
      return scc_of(initial_state_);
556
557
    }

558
    const scc_succs& succ(unsigned scc) const
559
    {
560
561
      if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
        report_need_track_succs();
562
      return node(scc).succ();
563
564
    }

565
    bool is_trivial(unsigned scc) const
566
    {
567
      return node(scc).is_trivial();
568
569
    }

570
    SPOT_DEPRECATED("use acc_sets_of() instead")
571
    acc_cond::mark_t acc(unsigned scc) const
572
    {
573
      return acc_sets_of(scc);
574
575
    }

576
    bool is_accepting_scc(unsigned scc) const
577
    {
578
      return node(scc).is_accepting();
579
580
    }

581
582
583
584
585
    bool is_rejecting_scc(unsigned scc) const
    {
      return node(scc).is_rejecting();
    }

586
587
588
589
    /// \brief Study the SCCs that are currently reported neither as
    /// accepting nor as rejecting because of the presence of Fin sets
    ///
    /// This simply calls check_scc_emptiness() on undeterminate SCCs.
590
591
    void determine_unknown_acceptance();

592
593
594
    /// \brief Recompute whether an SCC is accepting or not.
    ///
    /// This is an internal function of
595
596
    /// determine_unknown_acceptance().
    bool check_scc_emptiness(unsigned n);
597

598
    bool is_useful_scc(unsigned scc) const
599
    {
600
601
602
603
      if (SPOT_UNLIKELY(!!(options_ & scc_info_options::STOP_ON_ACC)))
        report_incompatible_stop_on_acc();
      if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS)))
        report_need_track_succs();
604
      return node(scc).is_useful();
605
606
    }

607
    bool is_useful_state(unsigned st) const
608
    {
609
      return reachable_state(st) && is_useful_scc(scc_of(st));
610
611
    }

612
613
614
615
    /// \brief Returns, for each accepting SCC, the set of all marks appearing
    /// in it.
    std::vector<std::set<acc_cond::mark_t>> marks() const;
    std::set<acc_cond::mark_t> marks_of(unsigned scc) const;
616

617
618
619
620
621
622
623
624
625
626
627
    // Same as above, with old names.
    SPOT_DEPRECATED("use marks() instead")
    std::vector<std::set<acc_cond::mark_t>> used_acc() const
    {
      return marks();
    }
    SPOT_DEPRECATED("use marks_of() instead")
    std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const
    {
      return marks_of(scc);
    }
628

629
630
631
    /// \brief Returns, for a given SCC, the set of all colors appearing in it.
    /// It is the set of colors that appear in some mark among those returned by
    /// marks_of().
632
633
    acc_cond::mark_t acc_sets_of(unsigned scc) const
    {
634
      return node(scc).acc_marks();
635
636
    }

637
638
    /// Returns, for a given SCC, the set of colors that appear on all of its
    /// transitions.
639
640
641
642
    acc_cond::mark_t common_sets_of(unsigned scc) const
    {
      return node(scc).common_marks();
    }
643

644
645
    std::vector<bool> weak_sccs() const;

646
    bdd scc_ap_support(unsigned scc) const;
647

648
649
    /// \brief Split an SCC into multiple automata separated by some
    /// acceptance sets.
650
    ///
651
652
653
654
655
656
657
658
659
660
    /// Pretend that the transitions of SCC \a scc that belong to any
    /// of the sets given in \a sets have been removed, and return a
    /// set of automata necessary to cover all remaining states.
    ///
    /// Set \a preserve_names to True if you want to keep the original
    /// name of each states for display.  (This is a bit slower.)
    std::vector<twa_graph_ptr> split_on_sets(unsigned scc,
                                             acc_cond::mark_t sets,
                                             bool preserve_names = false) const;
  protected:
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
    /// \brief: Recursive function used by states_on_acc_cycle_of().
    void
    states_on_acc_cycle_of_rec(unsigned scc,
                               acc_cond::mark_t all_fin,
                               acc_cond::mark_t all_inf,
                               unsigned nb_pairs,
                               std::vector<acc_cond::rs_pair>& pairs,
                               std::vector<unsigned>& res,
                               std::vector<unsigned>& old) const;
  public:
    /// \brief: Get all states visited by any accepting cycles of the 'scc'.
    ///
    /// Throws an exception if the automaton does not have a 'Streett-like'
    /// acceptance condition.
    std::vector<unsigned>
    states_on_acc_cycle_of(unsigned scc) const;
677
678
679
680
681
682
683
684
  };


  /// \brief Dump the SCC graph of \a aut on \a out.
  ///
  /// If \a sccinfo is not given, it will be computed.
  SPOT_API std::ostream&
  dump_scc_info_dot(std::ostream& out,
685
                    const_twa_graph_ptr aut, scc_info* sccinfo = nullptr);
686
687

}