scc.hh 3.13 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
// Copyright (C) 2008  Laboratoire de Recherche et Developpement de
// 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>
#include "tgba/tgba.hh"
#include <iosfwd>

namespace spot
{

  struct scc_stats
  {
    unsigned scc_total;

    std::ostream& dump(std::ostream& out) const;
  };

  class scc_map
  {
  public:
    typedef std::map<int, bdd> succ_type;

    scc_map(const tgba* aut);

    void build_map();
    void relabel_component(int n);

    const tgba* get_aut() const;

    int scc_count() const;

    int initial() const;

    const succ_type& succ(int i) const;
    bool accepting(int i) const;

  protected:
    struct scc
    {
    public:
      scc(int index) : index(index), acc(bddfalse) {};
      /// 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;
      /// Successor SCC.
      succ_type succ;
    };

    const tgba* aut_;		// Automata to decompose.
    typedef std::list<scc> stack_type;
    stack_type root_;		// Stack of SCC roots.
77
78
79
    std::stack<bdd> arc_acc_;	// A stack of acceptance conditions
				// between each of these SCC.
    std::stack<bdd> arc_cond_;	// A stack of conditions
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
				// between each of these SCC.
    typedef Sgi::hash_map<const state*, int,
			  state_ptr_hash, state_ptr_equal> hash_type;
    hash_type h_;		// Map of visited states.
    int num_;			// Number of visited nodes.
    int scc_num_;		// Opposite of the number of
				// maximal SCC constructed.
    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.

    std::map<int, scc> scc_map_; // Map of constructed maximal SCC.
  };

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

  std::ostream& dump_scc_dot(const tgba* a, std::ostream& out);
  std::ostream& dump_scc_dot(const scc_map& m, std::ostream& out);
}

#endif // SPOT_TGBAALGOS_SCC_HH