spot  2.9.2
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 
31 namespace 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
65  ~ta_explicit();
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
110  get_states_set()
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 
134  struct transition
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
198  is_hole_state() const;
199 
202  void
203  delete_stuttering_and_hole_successors();
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: 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:94
Successor iterators used by spot::ta_explicit.
Definition: taexplicit.hh:222
LTL/PSL formula interface.
Abstract class for states.
Definition: twa.hh:50
Explicit transitions.
Definition: taexplicit.hh:134
Definition: taexplicit.hh:39
virtual void destroy() const override
Release a state.
Definition: taexplicit.hh:159
Definition: taexplicit.hh:128
A Testing Automaton.
Definition: ta.hh:75
Iterate over the successors of a state.
Definition: ta.hh:197
An acceptance mark.
Definition: acc.hh:87

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