reachiter.cc 2.48 KB
Newer Older
1
#include <cassert>
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
77
78
79
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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
#include "reachiter.hh"

namespace spot
{
  // tgba_reachable_iterator
  //////////////////////////////////////////////////////////////////////

  tgba_reachable_iterator::tgba_reachable_iterator(const tgba* a)
    : automata_(a)
  {
  }

  tgba_reachable_iterator::~tgba_reachable_iterator()
  {
    for (seen_map::const_iterator s = seen.begin(); s != seen.end(); ++s)
      delete s->first;
  }

  void
  tgba_reachable_iterator::run()
  {
    int n = 0;
    start();
    state* i = automata_->get_init_state();
    add_state(i);
    seen[i] = ++n;
    const state* t;
    while ((t = next_state()))
      {
	assert(seen.find(t) != seen.end());
	int tn = seen[t];
	tgba_succ_iterator* si = automata_->succ_iter(t);
	process_state(t, tn, si);
	for (si->first(); ! si->done(); si->next())
	  {
	    const state* current = si->current_state();
	    seen_map::const_iterator s = seen.find(current);
	    if (s == seen.end())
	      {
		seen[current] = ++n;
		add_state(current);
		process_link(tn, n, si);
	      }
	    else
	      {
		process_link(tn, seen[current], si);
		delete current;
	      }
	  }
	delete si;
      }
    end();
  }

  void
  tgba_reachable_iterator::start()
  {
  }

  void
  tgba_reachable_iterator::end()
  {
  }

  void
  tgba_reachable_iterator::process_state(const state*, int,
					 tgba_succ_iterator*)
  {
  }

  void
  tgba_reachable_iterator::process_link(int, int, const tgba_succ_iterator*)
  {
  }

  // tgba_reachable_iterator_depth_first
  //////////////////////////////////////////////////////////////////////

  tgba_reachable_iterator_depth_first::
    tgba_reachable_iterator_depth_first(const tgba* a)
      : tgba_reachable_iterator(a)
  {
  }

  void
  tgba_reachable_iterator_depth_first::add_state(const state* s)
  {
    todo.push(s);
  }

  const state*
  tgba_reachable_iterator_depth_first::next_state()
  {
    if (todo.empty())
      return 0;
    const state* s = todo.top();
    todo.pop();
    return s;
  }

  // tgba_reachable_iterator_breadth_first
  //////////////////////////////////////////////////////////////////////

  tgba_reachable_iterator_breadth_first::
    tgba_reachable_iterator_breadth_first(const tgba* a)
      : tgba_reachable_iterator(a)
  {
  }

  void
  tgba_reachable_iterator_breadth_first::add_state(const state* s)
  {
    todo.push_back(s);
  }

  const state*
  tgba_reachable_iterator_breadth_first::next_state()
  {
    if (todo.empty())
      return 0;
    const state* s = todo.front();
    todo.pop_front();
    return s;
  }

}