spot 2.12.2
reachiter.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) by the Spot authors, see the AUTHORS file for details.
3//
4// This file is part of Spot, a model checking library.
5//
6// Spot is free software; you can redistribute it and/or modify it
7// under the terms of the GNU General Public License as published by
8// the Free Software Foundation; either version 3 of the License, or
9// (at your option) any later version.
10//
11// Spot is distributed in the hope that it will be useful, but WITHOUT
12// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14// License for more details.
15//
16// You should have received a copy of the GNU General Public License
17// along with this program. If not, see <http://www.gnu.org/licenses/>.
18
19#pragma once
20
21#include <spot/misc/hash.hh>
22#include <spot/ta/ta.hh>
23#include <stack>
24#include <deque>
25
26namespace spot
27{
30 class SPOT_API ta_reachable_iterator
31 {
32 public:
33 ta_reachable_iterator(const const_ta_ptr& a);
34 virtual
36
42 void
43 run();
44
52 virtual void
53 add_state(const state* s) = 0;
55 virtual const state*
58
61 virtual bool
62 want_state(const state* s) const;
63
65 virtual void
68 virtual void
69 end();
70
75 virtual void
76 process_state(const state* s, int n);
83 virtual void
84 process_link(int in, int out, const ta_succ_iterator* si);
85
86 protected:
87
88 const_ta_ptr t_automata_;
89
91 };
92
98 {
99 public:
100 ta_reachable_iterator_depth_first(const const_ta_ptr& a);
101
102 virtual void add_state(const state* s) override;
103 virtual const state* next_state() override;
104
105 protected:
106 std::stack<const state*> todo;
107 };
108
113 : public ta_reachable_iterator
114 {
115 public:
116 ta_reachable_iterator_breadth_first(const const_ta_ptr& a);
117
118 virtual void add_state(const state* s) override;
119 virtual const state* next_state() override;
120
121 protected:
122 std::deque<const state*> todo;
123 };
124}
Abstract class for states.
Definition: twa.hh:47
An implementation of spot::ta_reachable_iterator that browses states breadth first.
Definition: reachiter.hh:114
virtual void add_state(const state *s) override
Called by run() to obtain the next state to process.
std::deque< const state * > todo
A queue of states yet to explore.
Definition: reachiter.hh:122
virtual const state * next_state() override
Called by run() to obtain the next state to process.
An implementation of spot::ta_reachable_iterator that browses states depth first.
Definition: reachiter.hh:98
virtual const state * next_state() override
Called by run() to obtain the next state to process.
virtual void add_state(const state *s) override
Called by run() to obtain the next state to process.
std::stack< const state * > todo
A stack of states yet to explore.
Definition: reachiter.hh:106
Iterate over all reachable states of a spot::ta.
Definition: reachiter.hh:31
void run()
Iterate over all reachable states of a spot::ta.
virtual void add_state(const state *s)=0
Called by run() to obtain the next state to process.
virtual bool want_state(const state *s) const
const_ta_ptr t_automata_
The spot::ta to explore.
Definition: reachiter.hh:88
virtual const state * next_state()=0
Called by run() to obtain the next state to process.
state_map< int > seen
States already seen.
Definition: reachiter.hh:90
virtual void process_state(const state *s, int n)
virtual void process_link(int in, int out, const ta_succ_iterator *si)
virtual void start()
Called by run() before starting its iteration.
virtual void end()
Called by run() once all states have been explored.
Iterate over the successors of a state.
Definition: ta.hh:197
Definition: automata.hh:26
std::unordered_map< const state *, val, state_ptr_hash, state_ptr_equal > state_map
Unordered map of abstract states.
Definition: twa.hh:193

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.4