spot  2.0.3
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
taproduct.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2011, 2012, 2013, 2014, 2016 Laboratoire de Recherche
3 // 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/ta/ta.hh>
23 #include <spot/kripke/kripke.hh>
24 
25 namespace spot
26 {
27 
33  class SPOT_API state_ta_product : public state
34  {
35  public:
39  state_ta_product(const state* ta_state, const state* kripke_state) :
40  ta_state_(ta_state), kripke_state_(kripke_state)
41  {
42  }
43 
46 
47  virtual
49 
50  const state*
51  get_ta_state() const
52  {
53  return ta_state_;
54  }
55 
56  const state*
57  get_kripke_state() const
58  {
59  return kripke_state_;
60  }
61 
62  virtual int
63  compare(const state* other) const override;
64  virtual size_t
65  hash() const override;
66  virtual state_ta_product*
67  clone() const override;
68 
69  private:
70  const state* ta_state_;
71  const state* kripke_state_;
72  };
73 
76  {
77  public:
78  ta_succ_iterator_product(const state_ta_product* s, const ta* t,
79  const kripke* k);
80 
81  virtual
83 
84  // iteration
85  virtual bool first() override;
86  virtual bool next() override;
87  virtual bool done() const override;
88 
89  // inspection
90  virtual state_ta_product* dst() const override;
91  virtual bdd cond() const override;
92  virtual acc_cond::mark_t acc() const override;
93 
95  bool is_stuttering_transition() const;
96 
97  protected:
99  void step_();
101  bool next_non_stuttering_();
102 
104  void
105  next_kripke_dest();
106 
108 
109  protected:
110  const state_ta_product* source_;
111  const ta* ta_;
112  const kripke* kripke_;
113  ta_succ_iterator* ta_succ_it_;
114  twa_succ_iterator* kripke_succ_it_;
115  const state_ta_product* current_state_;
116  bdd current_condition_;
117  acc_cond::mark_t current_acceptance_conditions_;
118  bool is_stuttering_transition_;
119  bdd kripke_source_condition;
120  const state* kripke_current_dest_state;
121 
122  };
123 
127  class SPOT_API ta_product final: public ta
128  {
129  public:
133  ta_product(const const_ta_ptr& testing_automaton,
134  const const_kripke_ptr& kripke_structure);
135 
136  virtual
137  ~ta_product();
138 
139  virtual ta::const_states_set_t
140  get_initial_states_set() const override;
141 
142  virtual ta_succ_iterator_product*
143  succ_iter(const spot::state* s) const override;
144 
145  virtual ta_succ_iterator_product*
146  succ_iter(const spot::state* s, bdd changeset) const override;
147 
148  bdd_dict_ptr
149  get_dict() const;
150 
151  virtual std::string
152  format_state(const spot::state* s) const override;
153 
154  virtual bool
155  is_accepting_state(const spot::state* s) const override;
156 
157  virtual bool
158  is_livelock_accepting_state(const spot::state* s) const override;
159 
160  virtual bool
161  is_initial_state(const spot::state* s) const override;
162 
165  bool
166  is_hole_state_in_ta_component(const spot::state* s) const;
167 
168  virtual bdd
169  get_state_condition(const spot::state* s) const override;
170 
171  virtual void
172  free_state(const spot::state* s) const override;
173 
174  const const_ta_ptr&
175  get_ta() const
176  {
177  return ta_;
178  }
179 
180  const const_kripke_ptr&
181  get_kripke() const
182  {
183  return kripke_;
184  }
185 
186  private:
187  bdd_dict_ptr dict_;
188  const_ta_ptr ta_;
189  const_kripke_ptr kripke_;
190 
191  // Disallow copy.
192  ta_product(const ta_product&) = delete;
193  ta_product& operator=(const ta_product&) = delete;
194  };
195 
196 
197  typedef std::shared_ptr<ta_product> ta_product_ptr;
198  typedef std::shared_ptr<const ta_product> const_ta_product_ptr;
199  inline ta_product_ptr product(const const_ta_ptr& testing_automaton,
200  const const_kripke_ptr& kripke_structure)
201  {
202  return std::make_shared<ta_product>(testing_automaton, kripke_structure);
203  }
204 
207  {
208  public:
210  const ta* t, const kripke* k,
211  bdd changeset);
212 
214  void next_kripke_dest();
215  };
216 }
Definition: graph.hh:32
A lazy product between a Testing automaton and a Kripke structure. (States are computed on the fly...
Definition: taproduct.hh:127
Interface for a Kripke structure.
Definition: kripke.hh:90
Abstract class for states.
Definition: twa.hh:43
Iterate over the successors of a state.
Definition: twa.hh:390
Iterate over the successors of a product computed on the fly.
Definition: taproduct.hh:75
A Testing Automaton.
Definition: ta.hh:75
state_ta_product(const state *ta_state, const state *kripke_state)
Constructor.
Definition: taproduct.hh:39
A state for spot::ta_product.
Definition: taproduct.hh:33
Iterate over the successors of a state.
Definition: ta.hh:197
Definition: acc.hh:34

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Jul 11 2016 09:54:34 for spot by doxygen 1.8.8