spot  2.12.2
cndfs.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 <atomic>
22 #include <thread>
23 #include <vector>
24 
25 #include <spot/bricks/brick-hashset>
26 #include <spot/kripke/kripke.hh>
27 #include <spot/misc/common.hh>
28 #include <spot/misc/fixpool.hh>
29 #include <spot/misc/timer.hh>
30 #include <spot/twacube/twacube.hh>
31 #include <spot/mc/mc.hh>
32 
33 namespace spot
34 {
35  template<typename State, typename SuccIterator,
36  typename StateHash, typename StateEqual>
37  class SPOT_API swarmed_cndfs
38  {
39  struct local_colors
40  {
41  bool cyan;
42  bool is_in_Rp;
43  };
44 
46  struct cndfs_colors
47  {
48  std::atomic<bool> blue;
49  std::atomic<bool> red;
50  local_colors l[1];
51  };
52 
53  struct product_state
54  {
55  State st_kripke;
56  unsigned st_prop;
57  cndfs_colors* colors;
58  };
59 
61  struct state_hasher
62  {
63  state_hasher(const product_state&)
64  { }
65 
66  state_hasher() = default;
67 
68  brick::hash::hash128_t
69  hash(const product_state& lhs) const
70  {
71  StateHash hash;
72  // Not modulo 31 according to brick::hashset specifications.
73  unsigned u = hash(lhs.st_kripke) % (1<<30);
74  u = wang32_hash(lhs.st_prop) ^ u;
75  u = u % (1<<30);
76  return {u, u};
77  }
78 
79  bool equal(const product_state& lhs,
80  const product_state& rhs) const
81  {
82  StateEqual equal;
83  return (lhs.st_prop == rhs.st_prop)
84  && equal(lhs.st_kripke, rhs.st_kripke);
85  }
86  };
87 
88  struct todo_element
89  {
90  product_state st;
91  SuccIterator* it_kripke;
92  std::shared_ptr<trans_index> it_prop;
93  bool from_accepting;
94  };
95 
96  public:
97 
99  using shared_map = brick::hashset::FastConcurrent <product_state,
100  state_hasher>;
101  using shared_struct = shared_map;
102 
103  static shared_struct* make_shared_structure(shared_map m, unsigned i)
104  {
105  return nullptr; // Useless here.
106  }
107 
109  shared_map& map, shared_struct* /* useless here*/,
110  unsigned tid, std::atomic<bool>& stop):
111  sys_(sys), twa_(twa), tid_(tid), map_(map),
112  nb_th_(std::thread::hardware_concurrency()),
113  p_colors_(sizeof(cndfs_colors) +
114  sizeof(local_colors)*(std::thread::hardware_concurrency() - 1)),
115  stop_(stop)
116  {
117  static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
118  State, SuccIterator>::value,
119  "error: does not match the kripkecube requirements");
120  SPOT_ASSERT(nb_th_ > tid);
121  }
122 
123  virtual ~swarmed_cndfs()
124  {
125  while (!todo_blue_.empty())
126  {
127  sys_.recycle(todo_blue_.back().it_kripke, tid_);
128  todo_blue_.pop_back();
129  }
130  while (!todo_red_.empty())
131  {
132  sys_.recycle(todo_red_.back().it_kripke, tid_);
133  todo_red_.pop_back();
134  }
135  }
136 
137  void run()
138  {
139  setup();
140  blue_dfs();
141  finalize();
142  }
143 
144  void setup()
145  {
146  tm_.start("DFS thread " + std::to_string(tid_));
147  }
148 
149  std::pair<bool, product_state>
150  push_blue(product_state s, bool from_accepting)
151  {
152  cndfs_colors* c = (cndfs_colors*) p_colors_.allocate();
153  c->red = false;
154  c->blue = false;
155  for (unsigned i = 0; i < nb_th_; ++i)
156  {
157  c->l[i].cyan = false;
158  c->l[i].is_in_Rp = false;
159  }
160 
161  s.colors = c;
162 
163  // Try to insert the new state in the shared map.
164  auto it = map_.insert(s);
165  bool b = it.isnew();
166 
167  // Insertion failed, delete element
168  // FIXME Should we add a local cache to avoid useless allocations?
169  if (!b)
170  {
171  p_colors_.deallocate(c);
172  bool blue = ((*it)).colors->blue.load();
173  bool cyan = ((*it)).colors->l[tid_].cyan;
174  if (blue || cyan)
175  return {false, *it};
176  }
177 
178  // Mark state as visited.
179  ((*it)).colors->l[tid_].cyan = true;
180  ++states_;
181  todo_blue_.push_back({*it,
182  sys_.succ(((*it)).st_kripke, tid_),
183  twa_->succ(((*it)).st_prop),
184  from_accepting});
185  return {true, *it};
186  }
187 
188  std::pair<bool, product_state>
189  push_red(product_state s, bool ignore_cyan)
190  {
191  // Try to insert the new state in the shared map.
192  auto it = map_.insert(s);
193  SPOT_ASSERT(!it.isnew()); // should never be new in a red DFS
194  bool red = ((*it)).colors->red.load();
195  bool cyan = ((*it)).colors->l[tid_].cyan;
196  bool in_Rp = ((*it)).colors->l[tid_].is_in_Rp;
197  if (red || (cyan && !ignore_cyan) || in_Rp)
198  return {false, *it}; // couldn't insert
199 
200  // Mark state as visited.
201  ((*it)).colors->l[tid_].is_in_Rp = true;
202  Rp_.push_back(*it);
203  ++states_;
204  todo_red_.push_back({*it,
205  sys_.succ(((*it)).st_kripke, tid_),
206  twa_->succ(((*it)).st_prop),
207  false});
208  return {true, *it};
209  }
210 
211  bool pop_blue()
212  {
213  // Track maximum dfs size
214  dfs_ = todo_blue_.size() > dfs_ ? todo_blue_.size() : dfs_;
215 
216  todo_blue_.back().st.colors->l[tid_].cyan = false;
217  sys_.recycle(todo_blue_.back().it_kripke, tid_);
218  todo_blue_.pop_back();
219  return true;
220  }
221 
222  bool pop_red()
223  {
224  // Track maximum dfs size
225  dfs_ = todo_blue_.size() + todo_red_.size() > dfs_ ?
226  todo_blue_.size() + todo_red_.size() : dfs_;
227 
228 
229  sys_.recycle(todo_red_.back().it_kripke, tid_);
230  todo_red_.pop_back();
231  return true;
232  }
233 
234  void finalize()
235  {
236  bool tst_val = false;
237  bool new_val = true;
238  bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
239  if (exchanged)
240  finisher_ = true;
241  tm_.stop("DFS thread " + std::to_string(tid_));
242  }
243 
244  bool finisher()
245  {
246  return finisher_;
247  }
248 
249  unsigned states()
250  {
251  return states_;
252  }
253 
254  unsigned transitions()
255  {
256  return transitions_;
257  }
258 
259  unsigned walltime()
260  {
261  return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
262  }
263 
264  std::string name()
265  {
266  return "cndfs";
267  }
268 
269  int sccs()
270  {
271  return -1;
272  }
273 
274  mc_rvalue result()
275  {
276  return is_empty_ ? mc_rvalue::EMPTY : mc_rvalue::NOT_EMPTY;
277  }
278 
279  std::string trace()
280  {
281  SPOT_ASSERT(!is_empty_);
282  StateEqual equal;
283  auto state_equal = [equal](product_state a, product_state b)
284  {
285  return a.st_prop == b.st_prop
286  && equal(a.st_kripke, b.st_kripke);
287  };
288 
289  std::string res = "Prefix:\n";
290 
291  auto it = todo_blue_.begin();
292  while (it != todo_blue_.end())
293  {
294  if (state_equal(((*it)).st, cycle_start_))
295  break;
296  res += " " + std::to_string(((*it)).st.st_prop)
297  + "*" + sys_.to_string(((*it)).st.st_kripke) + "\n";
298  ++it;
299  }
300 
301  res += "Cycle:\n";
302  while (it != todo_blue_.end())
303  {
304  res += " " + std::to_string(((*it)).st.st_prop)
305  + "*" + sys_.to_string(((*it)).st.st_kripke) + "\n";
306  ++it;
307  }
308 
309  if (!todo_red_.empty())
310  {
311  it = todo_red_.begin() + 1; // skip first element, also in blue
312  while (it != todo_red_.end())
313  {
314  res += " " + std::to_string(((*it)).st.st_prop)
315  + "*" + sys_.to_string(((*it)).st.st_kripke) + "\n";
316  ++it;
317  }
318  }
319  res += " " + std::to_string(cycle_start_.st_prop)
320  + "*" + sys_.to_string(cycle_start_.st_kripke) + "\n";
321 
322  return res;
323  }
324 
325  private:
326  void blue_dfs()
327  {
328  product_state initial = {sys_.initial(tid_),
329  twa_->get_initial(),
330  nullptr};
331  if (!push_blue(initial, false).first)
332  return;
333 
334  // Property automaton has only one state
335  if (todo_blue_.back().it_prop->done())
336  return;
337 
338  forward_iterators(sys_, twa_, todo_blue_.back().it_kripke,
339  todo_blue_.back().it_prop, true, tid_);
340 
341  while (!todo_blue_.empty() && !stop_.load(std::memory_order_relaxed))
342  {
343  auto current = todo_blue_.back();
344 
345  if (!current.it_kripke->done())
346  {
347  ++transitions_;
348  product_state s = {
349  current.it_kripke->state(),
350  twa_->trans_storage(current.it_prop, tid_).dst,
351  nullptr
352  };
353 
354  bool acc = (bool) twa_->trans_storage(current.it_prop, tid_).acc_;
355  forward_iterators(sys_, twa_, todo_blue_.back().it_kripke,
356  todo_blue_.back().it_prop, false, tid_);
357 
358  auto tmp = push_blue(s, acc);
359  if (tmp.first)
360  forward_iterators(sys_, twa_, todo_blue_.back().it_kripke,
361  todo_blue_.back().it_prop, true, tid_);
362  else if (acc)
363  {
364  // The state cyan and we can reach it through an
365  // accepting transition, a accepting cycle has been
366  // found without launching a red dfs
367  if (tmp.second.colors->l[tid_].cyan)
368  {
369  cycle_start_ = s;
370  is_empty_ = false;
371  stop_.store(true);
372  return;
373  }
374 
375  SPOT_ASSERT(tmp.second.colors->blue);
376 
377  red_dfs(s);
378  if (!is_empty_)
379  return;
380  post_red_dfs();
381  }
382  }
383  else
384  {
385  current.st.colors->blue.store(true);
386 
387  // backtracked an accepting transition; launch red DFS
388  if (current.from_accepting)
389  {
390  red_dfs(todo_blue_.back().st);
391  if (!is_empty_)
392  return;
393  post_red_dfs();
394  }
395 
396  pop_blue();
397  }
398  }
399  }
400 
401  void post_red_dfs()
402  {
403  for (product_state& s: Rp_acc_)
404  {
405  while (s.colors->red.load() && !stop_.load())
406  {
407  // await
408  }
409  }
410  for (product_state& s: Rp_)
411  {
412  s.colors->red.store(true);
413  s.colors->l[tid_].is_in_Rp = false; // empty Rp
414  }
415 
416  Rp_.clear();
417  Rp_acc_.clear();
418  }
419 
420  void red_dfs(product_state initial)
421  {
422  auto init_push = push_red(initial, true);
423  SPOT_ASSERT(init_push.second.colors->blue);
424 
425  if (!init_push.first)
426  return;
427 
428  forward_iterators(sys_, twa_, todo_red_.back().it_kripke,
429  todo_red_.back().it_prop, true, tid_);
430 
431  while (!todo_red_.empty() && !stop_.load(std::memory_order_relaxed))
432  {
433  auto current = todo_red_.back();
434 
435  if (!current.it_kripke->done())
436  {
437  ++transitions_;
438  product_state s = {
439  current.it_kripke->state(),
440  twa_->trans_storage(current.it_prop, tid_).dst,
441  nullptr
442  };
443  bool acc = (bool) twa_->trans_storage(current.it_prop, tid_).acc_;
444  forward_iterators(sys_, twa_, todo_red_.back().it_kripke,
445  todo_red_.back().it_prop, false, tid_);
446 
447  auto res = push_red(s, false);
448  if (res.first) // could push properly
449  {
450  forward_iterators(sys_, twa_, todo_red_.back().it_kripke,
451  todo_red_.back().it_prop, true, tid_);
452 
453  SPOT_ASSERT(res.second.colors->blue);
454 
455  // The transition is accepting, we want to keep
456  // track of this state
457  if (acc)
458  {
459  // Do not insert twice a state
460  bool found = false;
461  for (auto& st: Rp_acc_)
462  {
463  if (st.colors == res.second.colors)
464  {
465  found = true;
466  break;
467  }
468  }
469  if (!found)
470  Rp_acc_.push_back(Rp_.back());
471  }
472  }
473  else
474  {
475  if (res.second.colors->l[tid_].cyan)
476  {
477  // color pointers are unique to each element,
478  // comparing them is equivalent (but faster) to comparing
479  // st_kripke and st_prop individually.
480  if (init_push.second.colors == res.second.colors && !acc)
481  continue;
482  is_empty_ = false;
483  cycle_start_ = s;
484  stop_.store(true);
485  return;
486  }
487  else if (acc && res.second.colors->l[tid_].is_in_Rp)
488  {
489  auto it = map_.insert(s);
490  Rp_acc_.push_back(*it);
491  }
492  }
493  }
494  else
495  {
496  pop_red();
497  }
498  }
499  }
500 
501  kripkecube<State, SuccIterator>& sys_;
502  twacube_ptr twa_;
503  std::vector<todo_element> todo_blue_;
504  std::vector<todo_element> todo_red_;
505  unsigned transitions_ = 0;
506  unsigned tid_;
507  shared_map map_;
508  spot::timer_map tm_;
509  unsigned states_ = 0;
510  unsigned dfs_ = 0;
511  unsigned nb_th_ = 0;
512  fixed_size_pool<pool_type::Unsafe> p_colors_;
513  bool is_empty_ = true;
514  std::atomic<bool>& stop_;
515  std::vector<product_state> Rp_;
516  std::vector<product_state> Rp_acc_;
517  product_state cycle_start_;
518  bool finisher_ = false;
519  };
520 }
This class allows to ensure (at compile time) if a given parameter is of type kripkecube....
Definition: kripke.hh:71
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:40
Definition: cndfs.hh:38
brick::hashset::FastConcurrent< product_state, state_hasher > shared_map
<
Definition: cndfs.hh:100
A map of timer, where each timer has a name.
Definition: timer.hh:225
A Transition-based ω-Automaton.
Definition: twa.hh:619
size_t wang32_hash(size_t key)
Thomas Wang's 32 bit hash function.
Definition: hashfunc.hh:37
Definition: automata.hh:26
mc_rvalue
Definition: mc.hh:43
@ NOT_EMPTY
The product is not empty.
@ EMPTY
The product is empty.

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