scc.hh 8.81 KB
Newer Older
1
// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
2
// Developpement de l'Epita.
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
//
// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

#ifndef SPOT_TGBAALGOS_SCC_HH
# define SPOT_TGBAALGOS_SCC_HH

#include <map>
#include <stack>
26
#include <vector>
27
28
#include "tgba/tgba.hh"
#include <iosfwd>
29
#include "misc/hash.hh"
30
#include "misc/bddlt.hh"
31
32
33
34
35
36

namespace spot
{

  struct scc_stats
  {
37
    /// Total number of SCCs.
38
    unsigned scc_total;
39
40
41
42
43
44
45
46
    /// Total number of accepting SCC.
    unsigned acc_scc;
    /// Total number of dead SCC.
    ///
    /// An SCC is dead if no accepting SCC is reachable from it.
    /// Note that an SCC can be neither dead nor accepting.
    unsigned dead_scc;

47
    /// Number of maximal accepting paths.
48
    ///
49
50
    /// A path is maximal and accepting if it ends in an accepting
    /// SCC that has only dead (i.e. non accepting) successors, or no
51
    /// successors at all.
52
53
54
55
56
    unsigned acc_paths;
    /// Number of paths to a terminal dead SCC.
    ///
    /// A terminal dead SCC is a dead SCC without successors.
    unsigned dead_paths;
Flix Abecassis's avatar
Flix Abecassis committed
57
    unsigned self_loops;
58

59
60
61
    /// A map of the useless SCCs.
    std::vector<bool> useless_scc_map;

62
63
64
65
66
    /// The set of useful acceptance conditions (i.e. acceptance
    /// conditions that are not always implied by other acceptance
    /// conditions).
    bdd useful_acc;

67
68
69
    std::ostream& dump(std::ostream& out) const;
  };

70
  /// Build a map of Strongly Connected components in in a TGBA.
71
72
73
  class scc_map
  {
  public:
74
    typedef std::map<unsigned, bdd> succ_type;
75
    typedef std::set<bdd, bdd_less_than> cond_set;
76

77
78
79
80
    /// \brief Constructor.
    ///
    /// This will note compute the map initially.  You should call
    /// build_map() to do so.
81
    scc_map(const tgba* aut);
82

83
    ~scc_map();
84

85
    /// Actually compute the graph of strongly connected components.
86
    void build_map();
87

88
    /// Get the automaton for which the map has been constructed.
89
90
    const tgba* get_aut() const;

91
92
    /// \brief Get the number of SCC in the automaton.
    ///
93
94
    /// SCCs are labelled from 0 to scc_count()-1.
    ///
95
    /// \pre This should only be called once build_map() has run.
96
    unsigned scc_count() const;
97

98
99
100
    /// \brief Get number of the SCC containing the initial state.
    ///
    /// \pre This should only be called once build_map() has run.
101
102
    unsigned initial() const;

103
104
105
    /// \brief Successor SCCs of a SCC.
    ///
    /// \pre This should only be called once build_map() has run.
106
    const succ_type& succ(unsigned n) const;
107

108
109
110
111
112
113
114
    /// \brief Return whether an SCC is trivial.
    ///
    /// Trivial SCCs have one state and no self-loop.
    ///
    /// \pre This should only be called once build_map() has run.
    bool trivial(unsigned n) const;

115
116
117
    /// \brief Return whether an SCC is accepting.
    ///
    /// \pre This should only be called once build_map() has run.
118
    bool accepting(unsigned n) const;
119
120
121
122

    /// \brief Return the set of conditions occurring in an SCC.
    ///
    /// \pre This should only be called once build_map() has run.
123
    const cond_set& cond_set_of(unsigned n) const;
124

125
126
127
128
129
130
131
132
    /// \brief Return the set of atomic properties occurring in an SCC.
    ///
    /// \return a BDD that is a conjuction of all atomic properties
    /// occurring on the transitions in the SCC n.
    ///
    /// \pre This should only be called once build_map() has run.
    bdd ap_set_of(unsigned n) const;

133
134
135
136
137
138
139
140
    /// \brief Return the set of atomic properties reachable from this SCC.
    ///
    /// \return a BDD that is a conjuction of all atomic properties
    /// occurring on the transitions reachable from this SCC n.
    ///
    /// \pre This should only be called once build_map() has run.
    bdd aprec_set_of(unsigned n) const;

141
142
143
    /// \brief Return the set of acceptance conditions occurring in an SCC.
    ///
    /// \pre This should only be called once build_map() has run.
144
    bdd acc_set_of(unsigned n) const;
145

146
    /// \brief Return the set of useful acceptance conditions of SCC \a n.
147
148
149
150
151
    ///
    /// Useless acceptances conditions are always implied by other acceptances
    /// conditions.  This returns all the other acceptance conditions.
    bdd useful_acc_of(unsigned n) const;

152
153
154
    /// \brief Return the set of states of an SCC.
    ///
    /// The states in the returned list are still owned by the scc_map
155
    /// instance.  They should NOT be destroyed by the client code.
156
157
    ///
    /// \pre This should only be called once build_map() has run.
158
    const std::list<const state*>& states_of(unsigned n) const;
159

160
161
162
    /// \brief Return one state of an SCC.
    ///
    /// The state in the returned list is still owned by the scc_map
163
    /// instance.  It should NOT be destroyed by the client code.
164
165
166
167
    ///
    /// \pre This should only be called once build_map() has run.
    const state* one_state_of(unsigned n) const;

168
169
170
    /// \brief Return the number of the SCC a state belongs too.
    ///
    /// \pre This should only be called once build_map() has run.
171
    unsigned scc_of_state(const state* s) const;
172

Flix Abecassis's avatar
Flix Abecassis committed
173
174
175
    /// \brief Return the number of self loops in the automaton.
    unsigned self_loops() const;

176
  protected:
177
    bdd update_supp_rec(unsigned state);
178
179
    int relabel_component();

180
181
182
    struct scc
    {
    public:
183
      scc(int index) : index(index), acc(bddfalse),
184
		       supp(bddtrue), supp_rec(bddfalse),
185
		       trivial(true), useful_acc(bddfalse) {};
186
187
188
189
190
191
192
      /// Index of the SCC.
      int index;
      /// The union of all acceptance conditions of transitions which
      /// connect the states of the connected component.
      bdd acc;
      /// States of the component.
      std::list<const state*> states;
193
194
      /// Set of conditions used in the SCC.
      cond_set conds;
195
196
      /// Conjunction of atomic propositions used in the SCC.
      bdd supp;
197
198
      /// Conjunction of atomic propositions used in the SCC.
      bdd supp_rec;
199
200
      /// Successor SCC.
      succ_type succ;
201
202
      /// Trivial SCC have one state and no self-loops.
      bool trivial;
203
204
205
206
207
208
209
210
211
212
      /// \brief Set of acceptance combinations used in the SCC.
      ///
      /// Note that the encoding used here differs from the
      /// encoding used in automata.
      /// If some transitions of the automaton are labeled by
      ///      Acc[a]&!Acc[b]&!Acc[c]  |  !Acc[a]&Acc[b]&!Acc[c]
      /// an other transitions are labeled by
      ///      !Acc[a]&Acc[b]&!Acc[c]  |  !Acc[a]&!Acc[b]&Acc[c]
      /// then useful_acc will contain
      ///      Acc[a]&Acc[b]&!Acc[c] | !Acc[a]&Acc[b]&Acc[c]
213
      bdd useful_acc;
214
215
216
217
218
    };

    const tgba* aut_;		// Automata to decompose.
    typedef std::list<scc> stack_type;
    stack_type root_;		// Stack of SCC roots.
219
220
221
    std::stack<bdd> arc_acc_;	// A stack of acceptance conditions
				// between each of these SCC.
    std::stack<bdd> arc_cond_;	// A stack of conditions
222
223
224
				// between each of these SCC.
    typedef Sgi::hash_map<const state*, int,
			  state_ptr_hash, state_ptr_equal> hash_type;
225
226
227
228
229
    hash_type h_;		// Map of visited states.  Values >= 0
                                // designate maximal SCC.  Values < 0
                                // number states that are part of
                                // incomplete SCCs being completed.
    int num_;			// Number of visited nodes, negated.
230
231
232
233
234
235
236
237
238
239
    typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
    std::stack<pair_state_iter> todo_; // DFS stack.  Holds (STATE,
				       // ITERATOR) pairs where
				       // ITERATOR is an iterator over
				       // the successors of STATE.
				       // ITERATOR should always be
				       // freed when TODO is popped,
				       // but STATE should not because
				       // it is used as a key in H.

240
    typedef std::vector<scc> scc_map_type;
241
    scc_map_type scc_map_; // Map of constructed maximal SCC.
242
			   // SCC number "n" in H_ corresponds to entry
243
                           // "n" in SCC_MAP_.
Flix Abecassis's avatar
Flix Abecassis committed
244
    unsigned self_loops_; // Self loops count.
245
 };
246
247
248
249

  scc_stats build_scc_stats(const tgba* a);
  scc_stats build_scc_stats(const scc_map& m);

250
251
252
253
  std::ostream& dump_scc_dot(const tgba* a, std::ostream& out,
			     bool verbose = false);
  std::ostream& dump_scc_dot(const scc_map& m, std::ostream& out,
			     bool verbose = false);
254
255
256
}

#endif // SPOT_TGBAALGOS_SCC_HH