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

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