spot  2.12
twacube.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 <vector>
22 #include <iosfwd>
23 #include <spot/graph/graph.hh>
24 #include <spot/misc/hash.hh>
25 #include <spot/twa/acc.hh>
26 #include <spot/twacube/cube.hh>
27 #include <spot/twacube/fwd.hh>
28 
29 namespace spot
30 {
32  class SPOT_API cstate
33  {
34  public:
35  cstate() = default;
36  cstate(const cstate& s) = delete;
37  cstate(cstate&& s) noexcept;
38  ~cstate() = default;
39  };
40 
42  class SPOT_API transition
43  {
44  public:
45  transition() = default;
46  transition(const transition& t) = delete;
47  transition(transition&& t) noexcept;
48  transition(const cube& cube, acc_cond::mark_t acc);
49  ~transition() = default;
50 
51  cube cube_;
52  acc_cond::mark_t acc_;
53  };
54 
56  class SPOT_API trans_index final:
57  public std::enable_shared_from_this<trans_index>
58  {
59  public:
62 
63  trans_index(trans_index& ci) = delete;
64  trans_index(unsigned state, const graph_t& g):
65  st_(g.state_storage(state))
66  {
67  reset();
68  }
69 
71  idx_(ci.idx_),
72  st_(ci.st_)
73  {
74  }
75 
77  inline void reset()
78  {
79  idx_ = st_.succ;
80  }
81 
83  inline void next()
84  {
85  ++idx_;
86  }
87 
90  inline bool done() const
91  {
92  return !idx_ || idx_ > st_.succ_tail;
93  }
94 
97  inline unsigned current(unsigned seed = 0) const
98  {
99  // no-swarming : since twacube are dedicated for parallelism, i.e.
100  // swarming, we expect swarming is activated.
101  if (SPOT_UNLIKELY(!seed))
102  return idx_;
103  // Here swarming performs a technique called "primitive
104  // root modulo n", i. e. for i in [1..n]: i*seed (mod n). We
105  // also must have seed prime with n: to solve this, we use
106  // precomputed primes and seed access one of this primes. Note
107  // that the chosen prime must be greater than n.
108  SPOT_ASSERT(primes[seed] > (st_.succ_tail-st_.succ+1));
109  unsigned long long c = (idx_-st_.succ) + 1;
110  unsigned long long p = primes[seed];
111  unsigned long long s = (st_.succ_tail-st_.succ+1);
112  return (unsigned) (((c*p) % s)+st_.succ);
113  }
114 
115  private:
116  unsigned idx_;
117  const graph_t::state_storage_t& st_;
118  };
119 
121  class SPOT_API twacube final: public std::enable_shared_from_this<twacube>
122  {
123  public:
124  twacube() = delete;
125 
127  twacube(const std::vector<std::string> aps);
128 
129  virtual ~twacube();
130 
133 
135  std::vector<std::string> ap() const;
136 
138  unsigned new_state();
139 
141  void set_initial(unsigned init);
142 
144  unsigned get_initial() const;
145 
147  cstate* state_from_int(unsigned i);
148 
151  void create_transition(unsigned src,
152  const cube& cube,
153  const acc_cond::mark_t& mark,
154  unsigned dst);
155 
157  const cubeset& get_cubeset() const;
158 
161  bool succ_contiguous() const;
162 
163  unsigned num_states() const
164  {
165  return theg_.num_states();
166  }
167 
168  unsigned num_edges() const
169  {
170  return theg_.num_edges();
171  }
172 
173  typedef digraph<cstate, transition> graph_t;
174 
177  {
178  return theg_;
179  }
180  typedef graph_t::edge_storage_t edge_storage_t;
181 
183  const graph_t::edge_storage_t&
184  trans_storage(std::shared_ptr<trans_index> ci,
185  unsigned seed = 0) const
186  {
187  return theg_.edge_storage(ci->current(seed));
188  }
189 
191  const transition& trans_data(std::shared_ptr<trans_index> ci,
192  unsigned seed = 0) const
193  {
194  return theg_.edge_data(ci->current(seed));
195  }
196 
198  std::shared_ptr<trans_index> succ(unsigned i) const
199  {
200  return std::make_shared<trans_index>(i, theg_);
201  }
202 
203  friend SPOT_API std::ostream& operator<<(std::ostream& os,
204  const twacube& twa);
205  private:
206  unsigned init_;
207  acc_cond acc_;
208  const std::vector<std::string> aps_;
209  graph_t theg_;
210  cubeset cubeset_;
211  };
212 
213  inline twacube_ptr make_twacube(const std::vector<std::string> aps)
214  {
215  return std::make_shared<twacube>(aps);
216  }
217 }
An acceptance condition.
Definition: acc.hh:61
Class for thread-safe states.
Definition: twacube.hh:33
Definition: cube.hh:68
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:711
Abstract class for states.
Definition: twa.hh:47
Class for iterators over transitions.
Definition: twacube.hh:58
bool done() const
Returns a boolean indicating wether all the transitions have been iterated.
Definition: twacube.hh:90
unsigned current(unsigned seed=0) const
Returns the current transition according to a specific seed. The seed is traditionally the thread ide...
Definition: twacube.hh:97
void reset()
Reset the iterator on the first element.
Definition: twacube.hh:77
void next()
Iterate over the next transition.
Definition: twacube.hh:83
Class for representing a transition.
Definition: twacube.hh:43
Class for representing a thread-safe twa.
Definition: twacube.hh:122
const graph_t & get_graph()
Returns the underlying graph for this automaton.
Definition: twacube.hh:176
unsigned new_state()
This method creates a new state.
acc_cond & acc()
Returns the acceptance condition associated to the automaton.
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 transition & trans_data(std::shared_ptr< trans_index > ci, unsigned seed=0) const
Returns the data associated to a transition.
Definition: twacube.hh:191
const cubeset & get_cubeset() const
Accessor the cube's manipulator.
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:184
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.
cstate * state_from_int(unsigned i)
Accessor for a state from its id.
std::vector< std::string > ap() const
Returns the names of the atomic properties.
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
Definition: graph.hh:187

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