spot 2.11.6.dev
Loading...
Searching...
No Matches
twacube.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2015, 2016, 2020 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 <vector>
23#include <iosfwd>
24#include <spot/graph/graph.hh>
25#include <spot/misc/hash.hh>
26#include <spot/twa/acc.hh>
27#include <spot/twacube/cube.hh>
28#include <spot/twacube/fwd.hh>
29
30namespace spot
31{
33 class SPOT_API cstate
34 {
35 public:
36 cstate() = default;
37 cstate(const cstate& s) = delete;
38 cstate(cstate&& s) noexcept;
39 ~cstate() = default;
40 };
41
43 class SPOT_API transition
44 {
45 public:
46 transition() = default;
47 transition(const transition& t) = delete;
48 transition(transition&& t) noexcept;
50 ~transition() = default;
51
52 cube cube_;
54 };
55
57 class SPOT_API trans_index final:
58 public std::enable_shared_from_this<trans_index>
59 {
60 public:
63
64 trans_index(trans_index& ci) = delete;
65 trans_index(unsigned state, const graph_t& g):
66 st_(g.state_storage(state))
67 {
68 reset();
69 }
70
72 idx_(ci.idx_),
73 st_(ci.st_)
74 {
75 }
76
78 inline void reset()
79 {
80 idx_ = st_.succ;
81 }
82
84 inline void next()
85 {
86 ++idx_;
87 }
88
91 inline bool done() const
92 {
93 return !idx_ || idx_ > st_.succ_tail;
94 }
95
98 inline unsigned current(unsigned seed = 0) const
99 {
100 // no-swarming : since twacube are dedicated for parallelism, i.e.
101 // swarming, we expect swarming is activated.
102 if (SPOT_UNLIKELY(!seed))
103 return idx_;
104 // Here swarming performs a technique called "primitive
105 // root modulo n", i. e. for i in [1..n]: i*seed (mod n). We
106 // also must have seed prime with n: to solve this, we use
107 // precomputed primes and seed access one of this primes. Note
108 // that the chosen prime must be greater than n.
109 SPOT_ASSERT(primes[seed] > (st_.succ_tail-st_.succ+1));
110 unsigned long long c = (idx_-st_.succ) + 1;
111 unsigned long long p = primes[seed];
112 unsigned long long s = (st_.succ_tail-st_.succ+1);
113 return (unsigned) (((c*p) % s)+st_.succ);
114 }
115
116 private:
117 unsigned idx_;
118 const graph_t::state_storage_t& st_;
119 };
120
122 class SPOT_API twacube final: public std::enable_shared_from_this<twacube>
123 {
124 public:
125 twacube() = delete;
126
128 twacube(const std::vector<std::string> aps);
129
130 virtual ~twacube();
131
134
136 std::vector<std::string> ap() const;
137
139 unsigned new_state();
140
142 void set_initial(unsigned init);
143
145 unsigned get_initial() const;
146
148 cstate* state_from_int(unsigned i);
149
152 void create_transition(unsigned src,
153 const cube& cube,
154 const acc_cond::mark_t& mark,
155 unsigned dst);
156
158 const cubeset& get_cubeset() const;
159
162 bool succ_contiguous() const;
163
164 unsigned num_states() const
165 {
166 return theg_.num_states();
167 }
168
169 unsigned num_edges() const
170 {
171 return theg_.num_edges();
172 }
173
174 typedef digraph<cstate, transition> graph_t;
175
178 {
179 return theg_;
180 }
181 typedef graph_t::edge_storage_t edge_storage_t;
182
184 const graph_t::edge_storage_t&
185 trans_storage(std::shared_ptr<trans_index> ci,
186 unsigned seed = 0) const
187 {
188 return theg_.edge_storage(ci->current(seed));
189 }
190
192 const transition& trans_data(std::shared_ptr<trans_index> ci,
193 unsigned seed = 0) const
194 {
195 return theg_.edge_data(ci->current(seed));
196 }
197
199 std::shared_ptr<trans_index> succ(unsigned i) const
200 {
201 return std::make_shared<trans_index>(i, theg_);
202 }
203
204 friend SPOT_API std::ostream& operator<<(std::ostream& os,
205 const twacube& twa);
206 private:
207 unsigned init_;
208 acc_cond acc_;
209 const std::vector<std::string> aps_;
210 graph_t theg_;
211 cubeset cubeset_;
212 };
213
214 inline twacube_ptr make_twacube(const std::vector<std::string> aps)
215 {
216 return std::make_shared<twacube>(aps);
217 }
218}
An acceptance condition.
Definition acc.hh:62
Class for thread-safe states.
Definition twacube.hh:34
Definition cube.hh:69
A directed graph.
Definition graph.hh:599
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition graph.hh:712
Abstract class for states.
Definition twa.hh:51
Class for iterators over transitions.
Definition twacube.hh:59
bool done() const
Returns a boolean indicating wether all the transitions have been iterated.
Definition twacube.hh:91
unsigned current(unsigned seed=0) const
Returns the current transition according to a specific seed. The seed is traditionnally the thread id...
Definition twacube.hh:98
void reset()
Reset the iterator on the first element.
Definition twacube.hh:78
void next()
Iterate over the next transition.
Definition twacube.hh:84
Class for representing a transition.
Definition twacube.hh:44
Class for representing a thread-safe twa.
Definition twacube.hh:123
unsigned new_state()
This method creates a new state.
acc_cond & acc()
Returns the acceptance condition associated to the automaton.
std::vector< std::string > ap() const
Returns the names of the atomic properties.
void create_transition(unsigned src, const cube &cube, const acc_cond::mark_t &mark, unsigned dst)
create a transition between state src and state dst, using cube as the labelling cube and mark as the...
unsigned get_initial() const
Returns the id of the initial state in the automaton.
bool succ_contiguous() const
Check if all the successors of a state are located contiguously in memory. This is mandatory for swar...
const graph_t::edge_storage_t & trans_storage(std::shared_ptr< trans_index > ci, unsigned seed=0) const
Returns the storage associated to a transition.
Definition twacube.hh:185
const cubeset & get_cubeset() const
Accessor the cube's manipulator.
const transition & trans_data(std::shared_ptr< trans_index > ci, unsigned seed=0) const
Returns the data associated to a transition.
Definition twacube.hh:192
cstate * state_from_int(unsigned i)
Accessor for a state from its id.
const graph_t & get_graph()
Returns the underlying graph for this automaton.
Definition twacube.hh:177
twacube(const std::vector< std::string > aps)
Build a new automaton from a list of atomic propositions.
void set_initial(unsigned init)
Updates the initial state to init.
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:85
Definition graph.hh:188

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