spot  2.12.1
ta.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 <set>
22 
23 #include <cassert>
24 #include <spot/misc/bddlt.hh>
25 #include <spot/twa/twa.hh>
26 
27 namespace spot
28 {
29 
30  // Forward declarations. See below.
31  class ta_succ_iterator;
32 
40 
43 
73 
74  class SPOT_API ta
75  {
76  protected:
77  acc_cond acc_;
78  bdd_dict_ptr dict_;
79 
80  public:
81  ta(const bdd_dict_ptr& d)
82  : dict_(d)
83  {
84  }
85 
86  virtual
87  ~ta()
88  {
89  }
90 
91  typedef std::set<state*, state_ptr_less_than> states_set_t;
92  typedef std::set<const state*, state_ptr_less_than> const_states_set_t;
93 
95  virtual const_states_set_t
97 
105  virtual const spot::state*
107  {
108  return nullptr;
109  }
110 
117  virtual ta_succ_iterator*
118  succ_iter(const spot::state* state) const = 0;
119 
127  virtual ta_succ_iterator*
128  succ_iter(const spot::state* state, bdd changeset) const = 0;
129 
137  bdd_dict_ptr
138  get_dict() const
139  {
140  return dict_;
141  }
142 
147  virtual std::string
148  format_state(const spot::state* s) const = 0;
149 
151  virtual bool
152  is_accepting_state(const spot::state* s) const = 0;
153 
156  virtual bool
158 
160  virtual bool
161  is_initial_state(const spot::state* s) const = 0;
162 
165  virtual bdd
166  get_state_condition(const spot::state* s) const = 0;
167 
169  virtual void
170  free_state(const spot::state* s) const = 0;
171 
172 
173  const acc_cond& acc() const
174  {
175  return acc_;
176  }
177 
178  acc_cond& acc()
179  {
180  return acc_;
181  }
182 
183  };
184 
185  typedef std::shared_ptr<ta> ta_ptr;
186  typedef std::shared_ptr<const ta> const_ta_ptr;
187 
197  {
198  public:
199  virtual
201  {
202  }
203  };
204 
205 #ifndef SWIG
206  // A stack of Strongly-Connected Components
208  {
209  public:
211  {
212  public:
213  connected_component(int index = -1) noexcept;
214 
216  int index;
217 
218  bool is_accepting;
219 
223 
224  std::list<const state*> rem;
225  };
226 
228  void
229  push(int index);
230 
233  top();
234 
236  const connected_component&
237  top() const;
238 
240  void
241  pop();
242 
244  size_t
245  size() const;
246 
248  std::list<const state*>&
249  rem();
250 
252  bool
253  empty() const;
254 
255  typedef std::list<connected_component> stack_type;
256  stack_type s;
257  };
258 #endif // !SWIG
259 
262 
265 
268 
271 
272 
275 
278 
281 }
An acceptance condition.
Definition: acc.hh:61
Definition: ta.hh:208
size_t size() const
How many SCC are in stack.
bool empty() const
Is the stack empty?
void pop()
Pop the top SCC.
std::list< const state * > & rem()
The rem member of the top SCC.
void push(int index)
Stack a new SCC with index index.
connected_component & top()
Access the top SCC.
const connected_component & top() const
Access the top SCC.
Abstract class for states.
Definition: twa.hh:47
Iterate over the successors of a state.
Definition: ta.hh:197
A Testing Automaton.
Definition: ta.hh:75
virtual bool is_accepting_state(const spot::state *s) const =0
Return true if s is a Buchi-accepting state, otherwise false.
virtual std::string format_state(const spot::state *s) const =0
Format the state as a string for printing.
virtual const_states_set_t get_initial_states_set() const =0
Get the initial states set of the automaton.
virtual bool is_livelock_accepting_state(const spot::state *s) const =0
Return true if s is a livelock-accepting state , otherwise false.
bdd_dict_ptr get_dict() const
Get the dictionary associated to the automaton.
Definition: ta.hh:138
virtual bdd get_state_condition(const spot::state *s) const =0
Return a BDD condition that represents the valuation of atomic propositions in the state s.
virtual void free_state(const spot::state *s) const =0
Release a state s.
virtual bool is_initial_state(const spot::state *s) const =0
Return true if s is an initial state, otherwise false.
virtual const spot::state * get_artificial_initial_state() const
Get the artificial initial state set of the automaton. Return 0 if this artificial state is not imple...
Definition: ta.hh:106
virtual ta_succ_iterator * succ_iter(const spot::state *state) const =0
Get an iterator over the successors of state.
virtual ta_succ_iterator * succ_iter(const spot::state *state, bdd changeset) const =0
Get an iterator over the successors of state filtred by the changeset on transitions.
Iterate over the successors of a state.
Definition: twa.hh:394
Definition: automata.hh:26
An acceptance mark.
Definition: acc.hh:84
acc_cond::mark_t condition
Definition: ta.hh:222
int index
Index of the SCC.
Definition: ta.hh:216

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.1