spot  2.12.1
taproduct.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/ta/ta.hh>
22 #include <spot/kripke/kripke.hh>
23 
24 namespace spot
25 {
26 
32  class SPOT_API state_ta_product : public state
33  {
34  public:
38  state_ta_product(const state* ta_state, const state* kripke_state) :
39  ta_state_(ta_state), kripke_state_(kripke_state)
40  {
41  }
42 
43  state_ta_product(const state_ta_product& o) = delete;
44 
45  virtual
47 
48  const state*
49  get_ta_state() const
50  {
51  return ta_state_;
52  }
53 
54  const state*
55  get_kripke_state() const
56  {
57  return kripke_state_;
58  }
59 
60  virtual int
61  compare(const state* other) const override;
62  virtual size_t
63  hash() const override;
64  virtual state_ta_product*
65  clone() const override;
66 
67  private:
68  const state* ta_state_;
69  const state* kripke_state_;
70  };
71 
74  {
75  public:
76  ta_succ_iterator_product(const state_ta_product* s, const ta* t,
77  const kripke* k);
78 
79  virtual
81 
82  // iteration
83  virtual bool first() override;
84  virtual bool next() override;
85  virtual bool done() const override;
86 
87  // inspection
88  virtual state_ta_product* dst() const override;
89  virtual bdd cond() const override;
90  virtual acc_cond::mark_t acc() const override;
91 
94 
95  protected:
97  void step_();
99  bool next_non_stuttering_();
100 
102  void
104 
106 
107  protected:
108  const state_ta_product* source_;
109  const ta* ta_;
110  const kripke* kripke_;
111  ta_succ_iterator* ta_succ_it_;
112  twa_succ_iterator* kripke_succ_it_;
113  const state_ta_product* current_state_;
114  bdd current_condition_;
115  acc_cond::mark_t current_acceptance_conditions_;
116  bool is_stuttering_transition_;
117  bdd kripke_source_condition;
118  const state* kripke_current_dest_state;
119 
120  };
121 
125  class SPOT_API ta_product final: public ta
126  {
127  public:
131  ta_product(const const_ta_ptr& testing_automaton,
132  const const_kripke_ptr& kripke_structure);
133 
134  virtual
135  ~ta_product();
136 
137  virtual ta::const_states_set_t
138  get_initial_states_set() const override;
139 
140  virtual ta_succ_iterator_product*
141  succ_iter(const spot::state* s) const override;
142 
143  virtual ta_succ_iterator_product*
144  succ_iter(const spot::state* s, bdd changeset) const override;
145 
146  bdd_dict_ptr
147  get_dict() const;
148 
149  virtual std::string
150  format_state(const spot::state* s) const override;
151 
152  virtual bool
153  is_accepting_state(const spot::state* s) const override;
154 
155  virtual bool
156  is_livelock_accepting_state(const spot::state* s) const override;
157 
158  virtual bool
159  is_initial_state(const spot::state* s) const override;
160 
163  bool
165 
166  virtual bdd
167  get_state_condition(const spot::state* s) const override;
168 
169  virtual void
170  free_state(const spot::state* s) const override;
171 
172  const const_ta_ptr&
173  get_ta() const
174  {
175  return ta_;
176  }
177 
178  const const_kripke_ptr&
179  get_kripke() const
180  {
181  return kripke_;
182  }
183 
184  private:
185  bdd_dict_ptr dict_;
186  const_ta_ptr ta_;
187  const_kripke_ptr kripke_;
188 
189  // Disallow copy.
190  ta_product(const ta_product&) = delete;
191  ta_product& operator=(const ta_product&) = delete;
192  };
193 
194 
195  typedef std::shared_ptr<ta_product> ta_product_ptr;
196  typedef std::shared_ptr<const ta_product> const_ta_product_ptr;
197  inline ta_product_ptr product(const const_ta_ptr& testing_automaton,
198  const const_kripke_ptr& kripke_structure)
199  {
200  return std::make_shared<ta_product>(testing_automaton, kripke_structure);
201  }
202 
205  {
206  public:
208  const ta* t, const kripke* k,
209  bdd changeset);
210 
213  };
214 }
Interface for a Kripke structure.
Definition: kripke.hh:177
A state for spot::ta_product.
Definition: taproduct.hh:33
virtual int compare(const state *other) const override
Compares two states (that come from the same automaton).
state_ta_product(const state *ta_state, const state *kripke_state)
Constructor.
Definition: taproduct.hh:38
virtual size_t hash() const override
Hash a state.
virtual state_ta_product * clone() const override
Duplicate a state.
Abstract class for states.
Definition: twa.hh:47
A lazy product between a Testing automaton and a Kripke structure. (States are computed on the fly....
Definition: taproduct.hh:126
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_product * succ_iter(const spot::state *s) const override
Get an iterator over the successors of state.
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 bool is_initial_state(const spot::state *s) const override
Return true if s is an initial state, otherwise false.
ta_product(const const_ta_ptr &testing_automaton, const const_kripke_ptr &kripke_structure)
Constructor.
virtual std::string format_state(const spot::state *s) const override
Format the state as a string for printing.
virtual ta::const_states_set_t get_initial_states_set() const override
Get the initial states set of the automaton.
virtual bool is_accepting_state(const spot::state *s) const override
Return true if s is a Buchi-accepting state, otherwise false.
bool is_hole_state_in_ta_component(const spot::state *s) const
Return true if the state s has no successor in the TA automaton (the TA component of the product auto...
virtual void free_state(const spot::state *s) const override
Release a state s.
virtual ta_succ_iterator_product * succ_iter(const spot::state *s, bdd changeset) const override
Get an iterator over the successors of state filtred by the changeset on transitions.
void next_kripke_dest()
Move to the next successor in the Kripke structure.
Iterate over the successors of a product computed on the fly.
Definition: taproduct.hh:74
virtual bool first() override
Position the iterator on the first successor (if any).
virtual state_ta_product * dst() const override
Get the destination state of the current edge.
virtual bool done() const override
Check whether the iteration is finished.
bool is_stuttering_transition() const
Return true if the changeset of the current transition is empty.
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.
void next_kripke_dest()
Move to the next successor in the kripke structure.
virtual acc_cond::mark_t acc() const override
Get the acceptance mark of the edge leading to this successor.
Iterate over the successors of a state.
Definition: ta.hh:197
A Testing Automaton.
Definition: ta.hh:75
Iterate over the successors of a state.
Definition: twa.hh:394
Definition: automata.hh:26
An acceptance mark.
Definition: acc.hh:84

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