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

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