spot  2.12
utils.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/mc/intersect.hh>
22 #include <spot/twa/twa.hh>
23 #include <spot/twacube_algos/convert.hh>
24 
25 namespace spot
26 {
29  template<typename State, typename SuccIterator,
30  typename StateHash, typename StateEqual>
31  class SPOT_API kripkecube_to_twa
32  {
33  public:
34 
35  kripkecube_to_twa(kripkecube<State, SuccIterator>& sys, bdd_dict_ptr dict):
36  sys_(sys), dict_(dict)
37  {
38  static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
39  State, SuccIterator>::value,
40  "error: does not match the kripkecube requirements");
41  }
42 
44  {
45  visited_.clear();
46  }
47 
48  void run()
49  {
50  setup();
51  State initial = sys_.initial(0);
52  if (SPOT_LIKELY(push(initial, dfs_number_+1)))
53  {
54  visited_[initial] = dfs_number_++;
55  todo_.push_back({initial, sys_.succ(initial, 0)});
56  }
57  while (!todo_.empty())
58  {
59  if (todo_.back().it->done())
60  {
61  if (SPOT_LIKELY(pop(todo_.back().s)))
62  {
63  sys_.recycle(todo_.back().it, 0);
64  todo_.pop_back();
65  }
66  }
67  else
68  {
69  ++transitions_;
70  State dst = todo_.back().it->state();
71  auto it = visited_.find(dst);
72  if (it == visited_.end())
73  {
74  if (SPOT_LIKELY(push(dst, dfs_number_+1)))
75  {
76  visited_[dst] = dfs_number_++;
77  todo_.back().it->next();
78  todo_.push_back({dst, sys_.succ(dst, 0)});
79  }
80  }
81  else
82  {
83  edge(visited_[todo_.back().s], visited_[dst]);
84  todo_.back().it->next();
85  }
86  }
87  }
88  finalize();
89  }
90 
91  void setup()
92  {
93  auto d = spot::make_bdd_dict();
94  res_ = make_twa_graph(d);
95  names_ = new std::vector<std::string>();
96 
97  int i = 0;
98  for (auto ap : sys_.ap())
99  {
100  auto idx = res_->register_ap(ap);
101  reverse_binder_[i++] = idx;
102  }
103  }
104 
105  bool push(State s, unsigned i)
106  {
107 
108  unsigned st = res_->new_state();
109  names_->push_back(sys_.to_string(s));
110  if (!todo_.empty())
111  {
112  edge(visited_[todo_.back().s], st);
113  }
114 
115  SPOT_ASSERT(st+1 == i);
116  return true;
117  }
118 
119  bool pop(State)
120  {
121  return true;
122  }
123 
124  void edge(unsigned src, unsigned dst)
125  {
126  cubeset cs(sys_.ap().size());
127  bdd cond = cube_to_bdd(todo_.back().it->condition(),
128  cs, reverse_binder_);
129  res_->new_edge(src, dst, cond);
130  }
131 
132  void finalize()
133  {
134  res_->purge_unreachable_states();
135  res_->set_named_prop<std::vector<std::string>>("state-names", names_);
136  }
137 
138  twa_graph_ptr twa()
139  {
140  return res_;
141  }
142 
143  protected:
145  {
146  State s;
147  SuccIterator* it;
148  };
149 
150  typedef std::unordered_map<const State, int,
151  StateHash, StateEqual> visited__map;
152 
154  std::vector<todo__element> todo_;
155  visited__map visited_;
156  unsigned int dfs_number_ = 0;
157  unsigned int transitions_ = 0;
158  spot::twa_graph_ptr res_;
159  std::vector<std::string>* names_;
160  bdd_dict_ptr dict_;
161  std::unordered_map<int, int> reverse_binder_;
162  };
163 
166  template<typename State, typename SuccIterator,
167  typename StateHash, typename StateEqual>
168  class SPOT_API product_to_twa
169  {
170  struct product_state
171  {
172  State st_kripke;
173  unsigned st_prop;
174  };
175 
176  struct product_state_equal
177  {
178  bool
179  operator()(const product_state lhs,
180  const product_state rhs) const
181  {
182  StateEqual equal;
183  return (lhs.st_prop == rhs.st_prop) &&
184  equal(lhs.st_kripke, rhs.st_kripke);
185  }
186  };
187 
188  struct product_state_hash
189  {
190  size_t
191  operator()(const product_state lhs) const noexcept
192  {
193  StateHash hash;
194  unsigned u = hash(lhs.st_kripke) % (1<<30);
195  u = wang32_hash(lhs.st_prop) ^ u;
196  u = u % (1<<30);
197  return u;
198  }
199  };
200 
201  public:
203  twacube_ptr twa):
204  sys_(sys), twa_(twa)
205  {
206  static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
207  State, SuccIterator>::value,
208  "error: does not match the kripkecube requirements");
209  }
210 
211  virtual ~product_to_twa()
212  {
213  map.clear();
214  }
215 
216  bool run()
217  {
218  setup();
219  product_state initial = {sys_.initial(0), twa_->get_initial()};
220  if (SPOT_LIKELY(push_state(initial, dfs_number_+1, {})))
221  {
222  todo_.push_back({initial, sys_.succ(initial.st_kripke, 0),
223  twa_->succ(initial.st_prop)});
224 
225  // Not going further! It's a product with a single state.
226  if (todo_.back().it_prop->done())
227  return false;
228 
229  forward_iterators(sys_, twa_, todo_.back().it_kripke,
230  todo_.back().it_prop, true, 0);
231  map[initial] = ++dfs_number_;
232  }
233  while (!todo_.empty())
234  {
235  // Check the kripke is enough since it's the outer loop. More
236  // details in forward_iterators.
237  if (todo_.back().it_kripke->done())
238  {
239  bool is_init = todo_.size() == 1;
240  auto newtop = is_init? todo_.back().st: todo_[todo_.size() -2].st;
241  if (SPOT_LIKELY(pop_state(todo_.back().st,
242  map[todo_.back().st],
243  is_init,
244  newtop,
245  map[newtop])))
246  {
247  sys_.recycle(todo_.back().it_kripke, 0);
248  todo_.pop_back();
249  }
250  }
251  else
252  {
253  ++transitions_;
254  product_state dst = {
255  todo_.back().it_kripke->state(),
256  twa_->trans_storage(todo_.back().it_prop, 0).dst
257  };
258  auto acc = twa_->trans_data(todo_.back().it_prop, 0).acc_;
259  forward_iterators(sys_, twa_, todo_.back().it_kripke,
260  todo_.back().it_prop, false, 0);
261  auto it = map.find(dst);
262  if (it == map.end())
263  {
264  if (SPOT_LIKELY(push_state(dst, dfs_number_+1, acc)))
265  {
266  map[dst] = ++dfs_number_;
267  todo_.push_back({dst, sys_.succ(dst.st_kripke, 0),
268  twa_->succ(dst.st_prop)});
269  forward_iterators(sys_, twa_, todo_.back().it_kripke,
270  todo_.back().it_prop, true, 0);
271  }
272  }
273  else if (SPOT_UNLIKELY(update(todo_.back().st, dfs_number_,
274  dst, map[dst], acc)))
275  return true;
276  }
277  }
278  return false;
279  }
280 
281  twa_graph_ptr twa()
282  {
283  res_->purge_unreachable_states();
284  res_->set_named_prop<std::vector<std::string>>("state-names", names_);
285  return res_;
286  }
287 
288  void setup()
289  {
290  auto d = spot::make_bdd_dict();
291  res_ = make_twa_graph(d);
292  names_ = new std::vector<std::string>();
293 
294  int i = 0;
295  for (auto ap : sys_.ap())
296  {
297  auto idx = res_->register_ap(ap);
298  reverse_binder_[i++] = idx;
299  }
300  }
301 
302  bool push_state(product_state s, unsigned i, acc_cond::mark_t)
303  {
304  unsigned st = res_->new_state();
305 
306  if (!todo_.empty())
307  {
308  auto c = twa_->get_cubeset()
309  .intersection(twa_->trans_data
310  (todo_.back().it_prop).cube_,
311  todo_.back().it_kripke->condition());
312 
313  bdd x = spot::cube_to_bdd(c, twa_->get_cubeset(),
314  reverse_binder_);
315  twa_->get_cubeset().release(c);
316  res_->new_edge(map[todo_.back().st]-1, st, x,
317  twa_->trans_data
318  (todo_.back().it_prop).acc_);
319  }
320 
321 
322  names_->push_back(sys_.to_string(s.st_kripke) +
323  ('*' + std::to_string(s.st_prop)));
324  SPOT_ASSERT(st+1 == i);
325  return true;
326  }
327 
328  bool update(product_state, unsigned src,
329  product_state, unsigned dst,
330  acc_cond::mark_t cond)
331  {
332  auto c = twa_->get_cubeset()
333  .intersection(twa_->trans_data
334  (todo_.back().it_prop).cube_,
335  todo_.back().it_kripke->condition());
336 
337  bdd x = spot::cube_to_bdd(c, twa_->get_cubeset(),
338  reverse_binder_);
339  twa_->get_cubeset().release(c);
340  res_->new_edge(src-1, dst-1, x, cond);
341  return false;
342  }
343 
344  bool pop_state(product_state, unsigned, bool, product_state, unsigned)
345  {
346  return true;
347  }
348 
349  private:
350  struct todo__element
351  {
352  product_state st;
353  SuccIterator* it_kripke;
354  std::shared_ptr<trans_index> it_prop;
355  };
356 
357  typedef std::unordered_map<const product_state, int,
358  product_state_hash,
359  product_state_equal> visited_map;
360 
362  twacube_ptr twa_;
363  std::vector<todo__element> todo_;
364  visited_map map;
365  unsigned int dfs_number_ = 0;
366  unsigned int transitions_ = 0;
367  spot::twa_graph_ptr res_;
368  std::vector<std::string>* names_;
369  std::unordered_map<int, int> reverse_binder_;
370  };
371 }
Definition: cube.hh:68
This class allows to ensure (at compile time) if a given parameter is of type kripkecube....
Definition: kripke.hh:71
convert a (cube) model into a twa. Note that this algorithm cannot be run in parallel but could.
Definition: utils.hh:32
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:40
convert a (cube) product automaton into a twa Note that this algorithm cannot be run in parallel.
Definition: utils.hh:169
A Transition-based ω-Automaton.
Definition: twa.hh:619
void set_named_prop(std::string s, void *val, std::function< void(void *)> destructor)
Declare a named property.
size_t wang32_hash(size_t key)
Thomas Wang's 32 bit hash function.
Definition: hashfunc.hh:37
@ ap
Atomic proposition.
twa_graph_ptr make_twa_graph(const bdd_dict_ptr &dict)
Build an explicit automaton from all states of aut,.
Definition: twagraph.hh:787
Definition: automata.hh:26
bdd cube_to_bdd(spot::cube cube, const cubeset &cubeset, std::unordered_map< int, int > &reverse_binder)
Transform a cube cube into bdd using the map that bind cube indexes to bdd indexes.
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