sccinfo.hh 15 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement
// 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
214
215
216
217
218
219
220
221
222

  /// Storage for SCC related information.
  class SPOT_API scc_info_node
  {
  public:
    typedef std::vector<unsigned> scc_succs;
    friend class scc_info;
  protected:
    scc_succs succ_;
    acc_cond::mark_t acc_;
223
    acc_cond::mark_t common_;
224
225
226
227
228
229
230
231
232
233
234
235
    std::vector<unsigned> states_; // States of the component
    bool trivial_:1;
    bool accepting_:1;        // Necessarily accepting
    bool rejecting_:1;        // Necessarily rejecting
    bool useful_:1;
  public:
    scc_info_node():
      acc_(0U), trivial_(true), accepting_(false),
      rejecting_(false), useful_(false)
    {
    }

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

    bool is_trivial() const
    {
      return trivial_;
    }

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

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

    bool is_useful() const
    {
      return useful_;
    }

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

279
280
281
282
283
    acc_cond::mark_t common_marks() const
    {
      return common_;
    }

284
285
286
287
288
289
290
291
292
293
294
295
    const std::vector<unsigned>& states() const
    {
      return states_;
    }

    const scc_succs& succ() const
    {
      return succ_;
    }
  };


296
297
298
299
  /// \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.
300
  /// It allows iterating over all SCCs of the automaton, and checks
301
302
  /// their acceptance or non-acceptance.
  ///
303
304
305
306
307
  /// 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.
  ///
308
309
310
311
312
  /// 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.
313
314
315
  class SPOT_API scc_info
  {
  public:
316
317
318
319
    // 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;
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
    /// @{
    /// \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);
    /// @}
350
351
352
353
354

  protected:

    std::vector<unsigned> sccof_;
    std::vector<scc_node> node_;
355
    const_twa_graph_ptr aut_;
356
357
358
    unsigned initial_state_;
    edge_filter filter_;
    void* filter_data_;
359

360
361
    // Update the useful_ bits.  Called automatically.
    void determine_usefulness();
362

363
    const scc_node& node(unsigned scc) const
364
365
366
367
368
    {
      return node_[scc];
    }

  public:
369
370
371
372
373
374
375

    // Use ~0U instead of -1U to work around a bug in Swig.
    // See https://github.com/swig/swig/issues/993
    scc_info(const_twa_graph_ptr aut,
             unsigned initial_state = ~0U,
             edge_filter filter = nullptr,
             void* filter_data = nullptr);
376

377
    const_twa_graph_ptr get_aut() const
378
379
380
381
382
    {
      return aut_;
    }

    unsigned scc_count() const
383
384
385
386
    {
      return node_.size();
    }

387
388
389
390
391
    bool reachable_state(unsigned st) const
    {
      return scc_of(st) != -1U;
    }

392
    unsigned scc_of(unsigned st) const
393
394
395
396
    {
      return sccof_[st];
    }

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
    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();
    }
426

427
    const std::vector<unsigned>& states_of(unsigned scc) const
428
    {
429
      return node(scc).states();
430
431
    }

432
433
434
435
436
437
438
439
440
441
442
    /// \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(),
443
              &aut_->get_graph().dests_vector(),
444
445
446
447
448
449
              internal::keep_all()};
    }

    /// \brief A fake container to iterate over all edges between
    /// states of an SCC.
    ///
450
    /// The difference with edges_of() is that inner_edges_of()
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
451
    /// ignores edges leaving the SCC.  In the case of an
452
453
    /// alternating automaton, an edge is considered to be part of the
    /// SCC of one of its destination is in the SCC.
454
455
456
457
458
459
    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(),
460
              &aut_->get_graph().dests_vector(),
461
462
463
              internal::keep_inner_scc(sccof_, scc)};
    }

464
465
466
467
468
469
470
471
    unsigned one_state_of(unsigned scc) const
    {
      return states_of(scc).front();
    }

    /// \brief Get number of the SCC containing the initial state.
    unsigned initial() const
    {
472
473
      SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
      return scc_of(initial_state_);
474
475
    }

476
    const scc_succs& succ(unsigned scc) const
477
    {
478
      return node(scc).succ();
479
480
    }

481
    bool is_trivial(unsigned scc) const
482
    {
483
      return node(scc).is_trivial();
484
485
    }

486
    acc_cond::mark_t acc(unsigned scc) const
487
    {
488
      return node(scc).acc_marks();
489
490
    }

491
    bool is_accepting_scc(unsigned scc) const
492
    {
493
      return node(scc).is_accepting();
494
495
    }

496
497
498
499
500
    bool is_rejecting_scc(unsigned scc) const
    {
      return node(scc).is_rejecting();
    }

501
502
503
504
    // Study the SCC that are currently reported neither as accepting
    // nor rejecting because of the presence of Fin sets
    void determine_unknown_acceptance();

505
    bool is_useful_scc(unsigned scc) const
506
    {
507
      return node(scc).is_useful();
508
509
    }

510
    bool is_useful_state(unsigned st) const
511
    {
512
      return reachable_state(st) && node(scc_of(st)).is_useful();
513
514
    }

515
516
517
    /// \brief Return the set of all used acceptance combinations, for
    /// each accepting SCC.
    std::vector<std::set<acc_cond::mark_t>> used_acc() const;
518

519
520
    std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const;

521
522
523
524
525
526
527
528
529
530
531
532
    /// sets that contain at least one transition of the SCC
    acc_cond::mark_t acc_sets_of(unsigned scc) const
    {
      // FIXME: Why do we have two name for this method?
      return acc(scc);
    }

    /// sets that contain the entire SCC
    acc_cond::mark_t common_sets_of(unsigned scc) const
    {
      return node(scc).common_marks();
    }
533

534
535
    std::vector<bool> weak_sccs() const;

536
    bdd scc_ap_support(unsigned scc) const;
537
538
539
540
541
542
543
544
  };


  /// \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,
545
                    const_twa_graph_ptr aut, scc_info* sccinfo = nullptr);
546
547

}