scc.hh 7.25 KB
Newer Older
1
// Copyright (C) 2008, 2009  Laboratoire de Recherche et Developpement de
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
// l'Epita.
//
// 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
51
    /// An path is maximal and accepting if it ends in an accepting
    /// SCC that is only dead (i.e. non accepting) successors, or no
    /// 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
    std::ostream& dump(std::ostream& out) const;
  };

65
  /// Build a map of Strongly Connected components in in a TGBA.
66
67
68
  class scc_map
  {
  public:
69
    typedef std::map<unsigned, bdd> succ_type;
70
    typedef std::set<bdd, bdd_less_than> cond_set;
71

72
73
74
75
    /// \brief Constructor.
    ///
    /// This will note compute the map initially.  You should call
    /// build_map() to do so.
76
    scc_map(const tgba* aut);
77

78
    ~scc_map();
79

80
    /// Actually compute the graph of strongly connected components.
81
    void build_map();
82

83
    /// Get the automaton for which the map has been constructed.
84
85
    const tgba* get_aut() const;

86
87
88
    /// \brief Get the number of SCC in the automaton.
    ///
    /// \pre This should only be called once build_map() has run.
89
    unsigned scc_count() const;
90

91
92
93
    /// \brief Get number of the SCC containing the initial state.
    ///
    /// \pre This should only be called once build_map() has run.
94
95
    unsigned initial() const;

96
97
98
    /// \brief Successor SCCs of a SCC.
    ///
    /// \pre This should only be called once build_map() has run.
99
    const succ_type& succ(unsigned n) const;
100
101
102
103

    /// \brief Return whether an SCC is accepting.
    ///
    /// \pre This should only be called once build_map() has run.
104
    bool accepting(unsigned n) const;
105
106
107
108

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

111
112
113
114
115
116
117
118
    /// \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;

119
120
121
122
123
124
125
126
    /// \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;

127
128
129
    /// \brief Return the set of acceptance conditions occurring in an SCC.
    ///
    /// \pre This should only be called once build_map() has run.
130
    bdd acc_set_of(unsigned n) const;
131
132
133
134
135
136
137

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

140
141
142
    /// \brief Return the number of the SCC a state belongs too.
    ///
    /// \pre This should only be called once build_map() has run.
143
    unsigned scc_of_state(const state* s) const;
144

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

148
  protected:
149
    bdd update_supp_rec(unsigned state);
150
151
    int relabel_component();

152
153
154
    struct scc
    {
    public:
155
      scc(int index) : index(index), acc(bddfalse),
156
157
		       supp(bddtrue), supp_rec(bddfalse),
		       trivial(true) {};
158
159
160
161
162
163
164
      /// 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;
165
166
      /// Set of conditions used in the SCC.
      cond_set conds;
167
168
      /// Conjunction of atomic propositions used in the SCC.
      bdd supp;
169
170
      /// Conjunction of atomic propositions used in the SCC.
      bdd supp_rec;
171
172
      /// Successor SCC.
      succ_type succ;
173
174
      /// Trivial SCC have one state and no self-loops.
      bool trivial;
175
176
177
178
179
    };

    const tgba* aut_;		// Automata to decompose.
    typedef std::list<scc> stack_type;
    stack_type root_;		// Stack of SCC roots.
180
181
182
    std::stack<bdd> arc_acc_;	// A stack of acceptance conditions
				// between each of these SCC.
    std::stack<bdd> arc_cond_;	// A stack of conditions
183
184
185
				// between each of these SCC.
    typedef Sgi::hash_map<const state*, int,
			  state_ptr_hash, state_ptr_equal> hash_type;
186
187
188
189
190
    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.
191
192
193
194
195
196
197
198
199
200
    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.

201
    typedef std::vector<scc> scc_map_type;
202
    scc_map_type scc_map_; // Map of constructed maximal SCC.
203
			   // SCC number "n" in H_ corresponds to entry
204
                           // "n" in SCC_MAP_.
Flix Abecassis's avatar
Flix Abecassis committed
205
    unsigned self_loops_; // Self loops count.
206
 };
207
208
209
210

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

211
212
213
214
  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);
215
216
217
}

#endif // SPOT_TGBAALGOS_SCC_HH