spot 2.11.6.dev
taexplicit.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2018 Laboratoire
3// de Recherche et Développement 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 <spot/misc/hash.hh>
23#include <list>
24#include <spot/twa/twa.hh>
25#include <set>
26#include <spot/tl/formula.hh>
27#include <cassert>
28#include <spot/misc/bddlt.hh>
29#include <spot/ta/ta.hh>
30
31namespace spot
32{
33 // Forward declarations. See below.
34 class state_ta_explicit;
35 class ta_explicit;
36
39 class SPOT_API ta_explicit : public ta
40 {
41 public:
42 ta_explicit(const const_twa_ptr& tgba,
43 unsigned n_acc,
44 state_ta_explicit* artificial_initial_state = nullptr);
45
46 const_twa_ptr
47 get_tgba() const;
48
50 add_state(state_ta_explicit* s);
51
52 void
53 add_to_initial_states_set(state* s, bdd condition = bddfalse);
54
55 void
56 create_transition(state_ta_explicit* source, bdd condition,
57 acc_cond::mark_t acceptance_conditions,
58 const state_ta_explicit* dest,
59 bool add_at_beginning = false);
60
61 void
62 delete_stuttering_transitions();
63 // ta interface
64 virtual
66 virtual const_states_set_t get_initial_states_set() const override;
67
68 virtual ta_succ_iterator* succ_iter(const spot::state* s) const override;
69
70 virtual ta_succ_iterator*
71 succ_iter(const spot::state* s, bdd condition) const override;
72
73 bdd_dict_ptr get_dict() const;
74
75 virtual std::string
76 format_state(const spot::state* s) const override;
77
78 virtual bool
79 is_accepting_state(const spot::state* s) const override;
80
81 virtual bool
82 is_livelock_accepting_state(const spot::state* s) const override;
83
84 virtual bool
85 is_initial_state(const spot::state* s) const override;
86
87 virtual bdd
88 get_state_condition(const spot::state* s) const override;
89
90 virtual void
91 free_state(const spot::state* s) const override;
92
93 virtual spot::state*
95 {
96 return (spot::state*) artificial_initial_state_;
97 }
98
99 void
100 set_artificial_initial_state(state_ta_explicit* s)
101 {
102 artificial_initial_state_ = s;
103
104 }
105
106 void
107 delete_stuttering_and_hole_successors(const spot::state* s);
108
109 ta::states_set_t
111 {
112 return states_set_;
113 }
114
115 private:
116 // Disallow copy.
117 ta_explicit(const ta_explicit& other) = delete;
118 ta_explicit& operator=(const ta_explicit& other) = delete;
119
120 const_twa_ptr tgba_;
121 state_ta_explicit* artificial_initial_state_;
122 ta::states_set_t states_set_;
123 ta::const_states_set_t initial_states_set_;
124 };
125
128 class SPOT_API state_ta_explicit final: public spot::state
129 {
130#ifndef SWIG
131 public:
132
135 {
136 bdd condition;
137 acc_cond::mark_t acceptance_conditions;
138 const state_ta_explicit* dest;
139 };
140
141 typedef std::list<transition*> transitions;
142
143 state_ta_explicit(const state* tgba_state, const bdd tgba_condition,
144 bool is_initial_state = false,
145 bool is_accepting_state = false,
146 bool is_livelock_accepting_state = false,
147 transitions* trans = nullptr) :
148 tgba_state_(tgba_state), tgba_condition_(tgba_condition),
149 is_initial_state_(is_initial_state), is_accepting_state_(
150 is_accepting_state), is_livelock_accepting_state_(
151 is_livelock_accepting_state), transitions_(trans)
152 {
153 }
154
155 virtual int compare(const spot::state* other) const override;
156 virtual size_t hash() const override;
157 virtual state_ta_explicit* clone() const override;
158
159 virtual void destroy() const override
160 {
161 }
162
163 virtual
165 {
166 }
167
168 transitions*
169 get_transitions() const;
170
171 // return transitions filtred by condition
172 transitions*
173 get_transitions(bdd condition) const;
174
175 void
176 add_transition(transition* t, bool add_at_beginning = false);
177
178 const state*
179 get_tgba_state() const;
180 const bdd
181 get_tgba_condition() const;
182 bool
183 is_accepting_state() const;
184 void
185 set_accepting_state(bool is_accepting_state);
186 bool
187 is_livelock_accepting_state() const;
188 void
189 set_livelock_accepting_state(bool is_livelock_accepting_state);
190
191 bool
192 is_initial_state() const;
193 void
194 set_initial_state(bool is_initial_state);
195
197 bool
199
202 void
204
205 void
206 free_transitions();
207
208 state_ta_explicit* stuttering_reachable_livelock;
209 private:
210 const state* tgba_state_;
211 const bdd tgba_condition_;
212 bool is_initial_state_;
213 bool is_accepting_state_;
214 bool is_livelock_accepting_state_;
215 transitions* transitions_;
216 std::unordered_map<int, transitions*, std::hash<int>>
217 transitions_by_condition;
218#endif // !SWIG
219 };
220
222 class SPOT_API ta_explicit_succ_iterator final: public ta_succ_iterator
223 {
224 public:
226
227 ta_explicit_succ_iterator(const state_ta_explicit* s, bdd condition);
228
229 virtual bool first() override;
230 virtual bool next() override;
231 virtual bool done() const override;
232
233 virtual const state* dst() const override;
234 virtual bdd cond() const override;
235
236 virtual acc_cond::mark_t acc() const override;
237
238 private:
239 state_ta_explicit::transitions* transitions_;
240 state_ta_explicit::transitions::const_iterator i_;
241 };
242
243 typedef std::shared_ptr<ta_explicit> ta_explicit_ptr;
244 typedef std::shared_ptr<const ta_explicit> const_ta_explicit_ptr;
245
246 inline ta_explicit_ptr
247 make_ta_explicit(const const_twa_ptr& tgba,
248 unsigned n_acc,
249 state_ta_explicit* artificial_initial_state = nullptr)
250 {
251 return std::make_shared<ta_explicit>(tgba, n_acc, artificial_initial_state);
252 }
253}
Definition: taexplicit.hh:129
void delete_stuttering_and_hole_successors()
Remove stuttering transitions and transitions leading to states having no successors.
virtual state_ta_explicit * clone() const override
Duplicate a state.
virtual void destroy() const override
Release a state.
Definition: taexplicit.hh:159
virtual size_t hash() const override
Hash a state.
virtual int compare(const spot::state *other) const override
Compares two states (that come from the same automaton).
bool is_hole_state() const
Return true if the state has no successors.
Abstract class for states.
Definition: twa.hh:51
Successor iterators used by spot::ta_explicit.
Definition: taexplicit.hh:223
virtual bool next() override
Jump to the next successor (if any).
virtual bdd cond() const override
Get the condition on the edge leading to this successor.
virtual bool done() const override
Check whether the iteration is finished.
virtual const state * dst() const override
Get the destination state of the current edge.
virtual acc_cond::mark_t acc() const override
Get the acceptance mark of the edge leading to this successor.
virtual bool first() override
Position the iterator on the first successor (if any).
Definition: taexplicit.hh:40
virtual bool is_initial_state(const spot::state *s) const override
Return true if s is an initial state, otherwise false.
virtual bool is_accepting_state(const spot::state *s) const override
Return true if s is a Buchi-accepting state, otherwise false.
virtual const_states_set_t get_initial_states_set() const override
Get the initial states set of the automaton.
virtual std::string format_state(const spot::state *s) const override
Format the state as a string for printing.
virtual spot::state * get_artificial_initial_state() const override
Get the artificial initial state set of the automaton. Return 0 if this artificial state is not imple...
Definition: taexplicit.hh:94
virtual bool is_livelock_accepting_state(const spot::state *s) const override
Return true if s is a livelock-accepting state , otherwise false.
virtual ta_succ_iterator * succ_iter(const spot::state *s, bdd condition) const override
Get an iterator over the successors of state filtred by the changeset on transitions.
virtual void free_state(const spot::state *s) const override
Release a state s.
virtual bdd get_state_condition(const spot::state *s) const override
Return a BDD condition that represents the valuation of atomic propositions in the state s.
virtual ta_succ_iterator * succ_iter(const spot::state *s) const override
Get an iterator over the successors of state.
Iterate over the successors of a state.
Definition: ta.hh:198
A Testing Automaton.
Definition: ta.hh:76
LTL/PSL formula interface.
Definition: automata.hh:27
std::set< const state * > get_states_set(const const_ta_ptr &t)
Compute states set for an automaton.
An acceptance mark.
Definition: acc.hh:85
Explicit transitions.
Definition: taexplicit.hh:135

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