spot  2.1.1
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
reachiter.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2008, 2009, 2011, 2013, 2016 Laboratoire de Recherche
3 // et Développement de l'Epita (LRDE).
4 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
5 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
6 // Pierre et Marie Curie.
7 //
8 // This file is part of Spot, a model checking library.
9 //
10 // Spot is free software; you can redistribute it and/or modify it
11 // under the terms of the GNU General Public License as published by
12 // the Free Software Foundation; either version 3 of the License, or
13 // (at your option) any later version.
14 //
15 // Spot is distributed in the hope that it will be useful, but WITHOUT
16 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
17 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
18 // License for more details.
19 //
20 // You should have received a copy of the GNU General Public License
21 // along with this program. If not, see <http://www.gnu.org/licenses/>.
22 
23 #pragma once
24 
25 #include <spot/misc/hash.hh>
26 #include <spot/twa/twa.hh>
27 #include <stack>
28 #include <deque>
29 
30 namespace spot
31 {
34  class SPOT_API twa_reachable_iterator
35  {
36  public:
37  twa_reachable_iterator(const const_twa_ptr& a);
38  virtual ~twa_reachable_iterator();
39 
45  virtual void run();
46 
54  virtual void add_state(const state* s) = 0;
56  virtual const state* next_state() = 0;
58 
61  virtual bool want_state(const state* s) const;
62 
64  virtual void start();
66  virtual void end();
67 
73  virtual void process_state(const state* s, int n, twa_succ_iterator* si);
86  virtual void process_link(const state* in_s, int in,
87  const state* out_s, int out,
88  const twa_succ_iterator* si);
89 
90  protected:
91  const_twa_ptr aut_;
92 
93  state_map<int> seen;
94  };
95 
101  {
102  public:
103  twa_reachable_iterator_breadth_first(const const_twa_ptr& a);
104 
105  virtual void add_state(const state* s) override;
106  virtual const state* next_state() override;
107 
108  protected:
109  std::deque<const state*> todo;
110  };
111 
115  {
116  public:
117  twa_reachable_iterator_depth_first(const const_twa_ptr& a);
119 
125  virtual void run();
126 
129  virtual bool want_state(const state* s) const;
130 
132  virtual void start();
134  virtual void end();
135 
141  virtual void process_state(const state* s, int n, twa_succ_iterator* si);
154  virtual void process_link(const state* in_s, int in,
155  const state* out_s, int out,
156  const twa_succ_iterator* si);
157 
158  protected:
159  const_twa_ptr aut_;
160 
161  state_map<int> seen;
162  struct stack_item
163  {
164  const state* src;
165  int src_n;
166  twa_succ_iterator* it;
167  };
168  std::deque<stack_item> todo;
169 
171  virtual void push(const state* s, int sn);
173  virtual void pop();
174  };
175 
183  {
184  public:
185  twa_reachable_iterator_depth_first_stack(const const_twa_ptr& a);
190  bool on_stack(int sn) const;
191  protected:
192  virtual void push(const state* s, int sn) override;
193  virtual void pop() override;
194 
195  std::unordered_set<int> stack_;
196  };
197 }
Definition: graph.hh:32
Iterate over all states of an automaton using a DFS.
Definition: reachiter.hh:114
std::deque< stack_item > todo
the DFS stack
Definition: reachiter.hh:168
state_map< int > seen
States already seen.
Definition: reachiter.hh:93
virtual void push(const state *s, int sn) override
Push a new state in todo.
Abstract class for states.
Definition: twa.hh:50
Iterate over all reachable states of a spot::tgba.
Definition: reachiter.hh:34
An implementation of spot::twa_reachable_iterator that browses states breadth first.
Definition: reachiter.hh:99
Iterate over all states of an automaton using a DFS.
Definition: reachiter.hh:181
Iterate over the successors of a state.
Definition: twa.hh:397
state_map< int > seen
States already seen.
Definition: reachiter.hh:161
const_twa_ptr aut_
The spot::tgba to explore.
Definition: reachiter.hh:159
const_twa_ptr aut_
The spot::tgba to explore.
Definition: reachiter.hh:91
virtual void pop() override
Pop the DFS stack.
std::deque< const state * > todo
A queue of states yet to explore.
Definition: reachiter.hh:109
bool on_stack(int sn) const
Whether state sn is on the DFS stack.

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Tue Sep 20 2016 07:13:02 for spot by doxygen 1.8.8