spot 2.10.6.dev
kripke.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2009, 2010, 2013, 2014, 2016, 2017, 2019, 2020 Laboratoire
3// de Recherche et Developpement de l'Epita
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/kripke/fairkripke.hh>
23#include <spot/twacube/cube.hh>
24#include <memory>
25#include <type_traits>
26
27namespace spot
28{
38 template<typename State, typename SuccIterator>
39 class SPOT_API kripkecube:
40 public std::enable_shared_from_this<kripkecube<State, SuccIterator>>
41 {
42 public:
45 State initial(unsigned tid);
46
48 unsigned get_threads();
49
51 std::string to_string(const State, unsigned tid) const;
52
54 SuccIterator* succ(const State, unsigned tid);
55
58 void recycle(SuccIterator*, unsigned tid);
59
61 const std::vector<std::string> ap();
62 };
63
64#ifndef SWIG
65
70 template <typename T, typename State, typename SuccIter>
71 class SPOT_API is_a_kripkecube_ptr
72 {
73 private:
74 using yes = std::true_type;
75 using no = std::false_type;
76
77 // Hardly waiting C++ concepts...
78 template<typename U, typename V> static auto test_kripke(U u, V v)
79 -> decltype(
80 // Check the kripke
81 std::is_same<State, decltype(u->initial(0))>::value &&
82 std::is_same<unsigned, decltype(u->get_threads())>::value &&
83 std::is_same<std::string, decltype(u->to_string(State(), 0))>::value &&
84 std::is_same<SuccIter*, decltype(u->succ(State(), 0))>::value &&
85 std::is_same<void, decltype(u->recycle(nullptr, 0))>::value &&
86 std::is_same<const std::vector<std::string>,
87 decltype(u->ap())>::value &&
88 std::is_same<void, decltype(u->recycle(nullptr, 0))>::value &&
89
90 // Check the SuccIterator
91 std::is_same<void, decltype(v->next())>::value &&
92 std::is_same<bool, decltype(v->done())>::value &&
93 std::is_same<State, decltype(v->state())>::value &&
94 std::is_same<spot::cube, decltype(v->condition())>::value
95
96 // finally return the type "yes"
97 , yes());
98
99 // For all other cases return the type "no"
100 template<typename, typename> static no test_kripke(...);
101
102 public:
103
106 static constexpr bool value =
107 std::is_same< decltype(test_kripke<T, SuccIter*>(nullptr, nullptr)), yes
108 >::value;
109 };
110
111#endif
112
113
131 {
132 public:
137 kripke_succ_iterator(const bdd& cond)
138 : cond_(cond)
139 {
140 }
141
142 void recycle(const bdd& cond)
143 {
144 cond_ = cond;
145 }
146
147 virtual ~kripke_succ_iterator();
148
149 virtual bdd cond() const override;
150 virtual acc_cond::mark_t acc() const override;
151 protected:
152 bdd cond_;
153 };
154
177 class SPOT_API kripke: public fair_kripke
178 {
179 public:
180 kripke(const bdd_dict_ptr& d)
181 : fair_kripke(d)
182 {
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:88
This class allows to ensure (at compile time) if a given parameter is of type kripkecube....
Definition: kripke.hh:72
Iterator code for Kripke structure.
Definition: kripke.hh:131
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:137
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:178
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:41
std::string to_string(const State, unsigned tid) const
Provides a string representation of the parameter state.
SuccIterator * succ(const State, unsigned tid)
Returns an iterator over the successors of the parameter state.
unsigned get_threads()
Returns the number of threads that are handled by the kripkecube.
State initial(unsigned tid)
Returns the initial State of the System. The tid parameter is used internally for sharing this struct...
const std::vector< std::string > ap()
This method allow to deallocate a given state.
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:51
Iterate over the successors of a state.
Definition: twa.hh:398
@ U
until
Definition: automata.hh:27
unsigned * cube
A cube is only a set of bits in memory.
Definition: cube.hh:66
An acceptance mark.
Definition: acc.hh:90

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