spot 2.11.5.dev
ta.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2010, 2012-2017 Laboratoire de Recherche et
3// Developpement de l Epita (LRDE).
4//
5// This file is part of Spot, a model checking library.
6//
7// Spot is free software; you can redistribute it and/or modify it
8// under the terms of the GNU General Public License as published by
9// the Free Software Foundation; either version 3 of the License, or
10// (at your option) any later version.
11//
12// Spot is distributed in the hope that it will be useful, but WITHOUT
13// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15// License for more details.
16//
17// You should have received a copy of the GNU General Public License
18// along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20#pragma once
21
22#include <set>
23
24#include <cassert>
25#include <spot/misc/bddlt.hh>
26#include <spot/twa/twa.hh>
27
28namespace spot
29{
30
31 // Forward declarations. See below.
32 class ta_succ_iterator;
33
41
44
74
75 class SPOT_API ta
76 {
77 protected:
78 acc_cond acc_;
79 bdd_dict_ptr dict_;
80
81 public:
82 ta(const bdd_dict_ptr& d)
83 : dict_(d)
84 {
85 }
86
87 virtual
88 ~ta()
89 {
90 }
91
92 typedef std::set<state*, state_ptr_less_than> states_set_t;
93 typedef std::set<const state*, state_ptr_less_than> const_states_set_t;
94
96 virtual const_states_set_t
98
106 virtual const spot::state*
108 {
109 return nullptr;
110 }
111
118 virtual ta_succ_iterator*
119 succ_iter(const spot::state* state) const = 0;
120
128 virtual ta_succ_iterator*
129 succ_iter(const spot::state* state, bdd changeset) const = 0;
130
138 bdd_dict_ptr
139 get_dict() const
140 {
141 return dict_;
142 }
143
148 virtual std::string
149 format_state(const spot::state* s) const = 0;
150
152 virtual bool
153 is_accepting_state(const spot::state* s) const = 0;
154
157 virtual bool
159
161 virtual bool
162 is_initial_state(const spot::state* s) const = 0;
163
166 virtual bdd
167 get_state_condition(const spot::state* s) const = 0;
168
170 virtual void
171 free_state(const spot::state* s) const = 0;
172
173
174 const acc_cond& acc() const
175 {
176 return acc_;
177 }
178
179 acc_cond& acc()
180 {
181 return acc_;
182 }
183
184 };
185
186 typedef std::shared_ptr<ta> ta_ptr;
187 typedef std::shared_ptr<const ta> const_ta_ptr;
188
198 {
199 public:
200 virtual
202 {
203 }
204 };
205
206#ifndef SWIG
207 // A stack of Strongly-Connected Components
209 {
210 public:
212 {
213 public:
214 connected_component(int index = -1) noexcept;
215
217 int index;
218
219 bool is_accepting;
220
224
225 std::list<const state*> rem;
226 };
227
229 void
230 push(int index);
231
235
238 top() const;
239
241 void
243
245 size_t
246 size() const;
247
249 std::list<const state*>&
251
253 bool
254 empty() const;
255
256 typedef std::list<connected_component> stack_type;
257 stack_type s;
258 };
259#endif // !SWIG
260
263
266
269
272
273
276
279
282}
An acceptance condition.
Definition: acc.hh:62
Definition: ta.hh:209
const connected_component & top() const
Access the top SCC.
size_t size() const
How many SCC are in stack.
bool empty() const
Is the stack empty?
void pop()
Pop the top SCC.
void push(int index)
Stack a new SCC with index index.
std::list< const state * > & rem()
The rem member of the top SCC.
connected_component & top()
Access the top SCC.
Abstract class for states.
Definition: twa.hh:51
Iterate over the successors of a state.
Definition: ta.hh:198
A Testing Automaton.
Definition: ta.hh:76
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 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.
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:107
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.
virtual ta_succ_iterator * succ_iter(const spot::state *state) const =0
Get an iterator over the successors of state.
bdd_dict_ptr get_dict() const
Get the dictionary associated to the automaton.
Definition: ta.hh:139
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.
Iterate over the successors of a state.
Definition: twa.hh:398
Definition: automata.hh:27
An acceptance mark.
Definition: acc.hh:90
acc_cond::mark_t condition
Definition: ta.hh:223
int index
Index of the SCC.
Definition: ta.hh:217

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