spot  2.12
kripke.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/kripke/fairkripke.hh>
22 #include <spot/twacube/cube.hh>
23 #include <memory>
24 #include <type_traits>
25 
26 namespace spot
27 {
37  template<typename State, typename SuccIterator>
38  class SPOT_API kripkecube:
39  public std::enable_shared_from_this<kripkecube<State, SuccIterator>>
40  {
41  public:
44  State initial(unsigned tid);
45 
47  unsigned get_threads();
48 
50  std::string to_string(const State, unsigned tid) const;
51 
53  SuccIterator* succ(const State, unsigned tid);
54 
57  void recycle(SuccIterator*, unsigned tid);
58 
60  const std::vector<std::string> ap();
61  };
62 
63 #ifndef SWIG
64 
69  template <typename T, typename State, typename SuccIter>
70  class SPOT_API is_a_kripkecube_ptr
71  {
72  private:
73  using yes = std::true_type;
74  using no = std::false_type;
75 
76  // Hardly waiting C++ concepts...
77  template<typename U, typename V> static auto test_kripke(U u, V v)
78  -> decltype(
79  // Check the kripke
80  std::is_same<State, decltype(u->initial(0))>::value &&
81  std::is_same<unsigned, decltype(u->get_threads())>::value &&
82  std::is_same<std::string, decltype(u->to_string(State(), 0))>::value &&
83  std::is_same<SuccIter*, decltype(u->succ(State(), 0))>::value &&
84  std::is_same<void, decltype(u->recycle(nullptr, 0))>::value &&
85  std::is_same<const std::vector<std::string>,
86  decltype(u->ap())>::value &&
87  std::is_same<void, decltype(u->recycle(nullptr, 0))>::value &&
88 
89  // Check the SuccIterator
90  std::is_same<void, decltype(v->next())>::value &&
91  std::is_same<bool, decltype(v->done())>::value &&
92  std::is_same<State, decltype(v->state())>::value &&
93  std::is_same<spot::cube, decltype(v->condition())>::value
94 
95  // finally return the type "yes"
96  , yes());
97 
98  // For all other cases return the type "no"
99  template<typename, typename> static no test_kripke(...);
100 
101  public:
102 
105  static constexpr bool value =
106  std::is_same< decltype(test_kripke<T, SuccIter*>(nullptr, nullptr)), yes
107  >::value;
108  };
109 
110 #endif
111 
112 
129  class SPOT_API kripke_succ_iterator : public twa_succ_iterator
130  {
131  public:
136  kripke_succ_iterator(const bdd& cond)
137  : cond_(cond)
138  {
139  }
140 
141  void recycle(const bdd& cond)
142  {
143  cond_ = cond;
144  }
145 
146  virtual ~kripke_succ_iterator();
147 
148  virtual bdd cond() const override;
149  virtual acc_cond::mark_t acc() const override;
150  protected:
151  bdd cond_;
152  };
153 
176  class SPOT_API kripke: public fair_kripke
177  {
178  public:
179  kripke(const bdd_dict_ptr& d)
180  : fair_kripke(d)
181  {
182  prop_weak(true);
183  }
184 
185  virtual ~kripke();
186 
187  virtual
189  };
190 
191  typedef std::shared_ptr<kripke> kripke_ptr;
192  typedef std::shared_ptr<const kripke> const_kripke_ptr;
193 }
Interface for a Fair Kripke structure.
Definition: fairkripke.hh:87
This class allows to ensure (at compile time) if a given parameter is of type kripkecube....
Definition: kripke.hh:71
Iterator code for Kripke structure.
Definition: kripke.hh:130
virtual bdd cond() const override
Get the condition on the edge leading to this successor.
kripke_succ_iterator(const bdd &cond)
Constructor.
Definition: kripke.hh:136
virtual acc_cond::mark_t acc() const override
Get the acceptance mark of the edge leading to this successor.
Interface for a Kripke structure.
Definition: kripke.hh:177
virtual acc_cond::mark_t state_acceptance_mark(const state *) const override
The acceptance mark that labels state s.
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:40
std::string to_string(const State, unsigned tid) const
Provides a string representation of the parameter state.
const std::vector< std::string > ap()
This method allow to deallocate a given state.
unsigned get_threads()
Returns the number of threads that are handled by the kripkecube.
SuccIterator * succ(const State, unsigned tid)
Returns an iterator over the successors of the parameter state.
State initial(unsigned tid)
Returns the initial State of the System. The tid parameter is used internally for sharing this struct...
void recycle(SuccIterator *, unsigned tid)
Allocation and deallocation of iterator is costly. This method allows to reuse old iterators.
Abstract class for states.
Definition: twa.hh:47
Iterate over the successors of a state.
Definition: twa.hh:394
@ U
until
Definition: automata.hh:26
unsigned * cube
A cube is only a set of bits in memory.
Definition: cube.hh:65
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