spot  2.12
lpar13.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 <spot/twa/acc.hh>
23 #include <spot/mc/unionfind.hh>
24 #include <spot/mc/intersect.hh>
25 #include <spot/mc/mc.hh>
26 #include <spot/misc/timer.hh>
27 #include <spot/twacube/twacube.hh>
28 #include <spot/twacube/fwd.hh>
29 
30 namespace spot
31 {
37  template<typename State, typename SuccIterator,
38  typename StateHash, typename StateEqual>
39  class SPOT_API lpar13
40  {
41  struct product_state
42  {
43  State st_kripke;
44  unsigned st_prop;
45  };
46 
47  struct product_state_equal
48  {
49  bool
50  operator()(const product_state lhs,
51  const product_state rhs) const
52  {
53  StateEqual equal;
54  return (lhs.st_prop == rhs.st_prop) &&
55  equal(lhs.st_kripke, rhs.st_kripke);
56  }
57  };
58 
59  struct product_state_hash
60  {
61  size_t
62  operator()(const product_state that) const noexcept
63  {
64  // FIXME: wang32_hash(that.st_prop) could have been
65  // pre-calculated!
66  StateHash hasher;
67  return wang32_hash(that.st_prop) ^ hasher(that.st_kripke);
68  }
69  };
70 
71  public:
72 
73  using shared_map = int; // Useless here.
74  using shared_struct = int; // Useless here.
75 
76  static shared_struct* make_shared_structure(shared_map m, unsigned i)
77  {
78  return nullptr; // Useless
79  }
80 
82  twacube_ptr twa,
83  shared_map& map, /* useless here */
84  shared_struct*, /* useless here */
85  unsigned tid,
86  std::atomic<bool>& stop)
87  : sys_(sys), twa_(twa), tid_(tid), stop_(stop),
88  acc_(twa->acc()), sccs_(0U)
89  {
90  static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
91  State, SuccIterator>::value,
92  "error: does not match the kripkecube requirements");
93  }
94 
95  virtual ~lpar13()
96  {
97  map.clear();
98  while (!todo.empty())
99  {
100  sys_.recycle(todo.back().it_kripke, tid_);
101  todo.pop_back();
102  }
103  }
104 
105  bool run()
106  {
107  setup();
108  product_state initial = {sys_.initial(tid_), twa_->get_initial()};
109  if (SPOT_LIKELY(push_state(initial, dfs_number+1, {})))
110  {
111  todo.push_back({initial, sys_.succ(initial.st_kripke, tid_),
112  twa_->succ(initial.st_prop)});
113 
114  // Not going further! It's a product with a single state.
115  if (todo.back().it_prop->done())
116  return false;
117 
118  forward_iterators(sys_, twa_, todo.back().it_kripke,
119  todo.back().it_prop, true, 0);
120  map[initial] = ++dfs_number;
121  }
122  while (!todo.empty() && !stop_.load(std::memory_order_relaxed))
123  {
124  // Check the kripke is enough since it's the outer loop. More
125  // details in forward_iterators.
126  if (todo.back().it_kripke->done())
127  {
128  bool is_init = todo.size() == 1;
129  auto newtop = is_init? todo.back().st: todo[todo.size() -2].st;
130  if (SPOT_LIKELY(pop_state(todo.back().st,
131  map[todo.back().st],
132  is_init,
133  newtop,
134  map[newtop])))
135  {
136  sys_.recycle(todo.back().it_kripke, tid_);
137  // FIXME: a local storage for twacube iterator?
138  todo.pop_back();
139  if (SPOT_UNLIKELY(found_))
140  {
141  finalize();
142  return true;
143  }
144  }
145  }
146  else
147  {
148  ++trans_;
149  product_state dst =
150  {
151  todo.back().it_kripke->state(),
152  twa_->trans_storage(todo.back().it_prop, tid_).dst
153  };
154  auto acc = twa_->trans_data(todo.back().it_prop, tid_).acc_;
155  forward_iterators(sys_, twa_, todo.back().it_kripke,
156  todo.back().it_prop, false, 0);
157  auto it = map.find(dst);
158  if (it == map.end())
159  {
160  if (SPOT_LIKELY(push_state(dst, dfs_number+1, acc)))
161  {
162  map[dst] = ++dfs_number;
163  todo.push_back({dst, sys_.succ(dst.st_kripke, tid_),
164  twa_->succ(dst.st_prop)});
165  forward_iterators(sys_, twa_, todo.back().it_kripke,
166  todo.back().it_prop, true, 0);
167  }
168  }
169  else if (SPOT_UNLIKELY(update(todo.back().st,
170  dfs_number,
171  dst, map[dst], acc)))
172  {
173  finalize();
174  return true;
175  }
176  }
177  }
178  finalize();
179  return false;
180  }
181 
182  void setup()
183  {
184  tm_.start("DFS thread " + std::to_string(tid_));
185  }
186 
187  bool push_state(product_state, unsigned dfsnum, acc_cond::mark_t cond)
188  {
189  uf_.makeset(dfsnum);
190  roots_.push_back({dfsnum, cond, {}});
191  return true;
192  }
193 
201  bool pop_state(product_state, unsigned top_dfsnum, bool,
202  product_state, unsigned)
203  {
204  if (top_dfsnum == roots_.back().dfsnum)
205  {
206  roots_.pop_back();
207  ++sccs_;
208  uf_.markdead(top_dfsnum);
209  }
210  dfs_ = todo.size() > dfs_ ? todo.size() : dfs_;
211  return true;
212  }
213 
216  bool update(product_state, unsigned,
217  product_state, unsigned dst_dfsnum,
218  acc_cond::mark_t cond)
219  {
220  if (uf_.isdead(dst_dfsnum))
221  return false;
222 
223  while (!uf_.sameset(dst_dfsnum, roots_.back().dfsnum))
224  {
225  auto& el = roots_.back();
226  roots_.pop_back();
227  uf_.unite(dst_dfsnum, el.dfsnum);
228  cond |= el.acc | el.ingoing;
229  }
230  roots_.back().acc |= cond;
231  found_ = acc_.accepting(roots_.back().acc);
232  if (SPOT_UNLIKELY(found_))
233  stop_ = true;
234  return found_;
235  }
236 
237  void finalize()
238  {
239  bool tst_val = false;
240  bool new_val = true;
241  bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
242  if (exchanged)
243  finisher_ = true;
244  tm_.stop("DFS thread " + std::to_string(tid_));
245  }
246 
247  bool finisher()
248  {
249  return finisher_;
250  }
251 
252  unsigned int states()
253  {
254  return dfs_number;
255  }
256 
257  unsigned int transitions()
258  {
259  return trans_;
260  }
261 
262  unsigned walltime()
263  {
264  return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
265  }
266 
267  std::string name()
268  {
269  return "renault_lpar13";
270  }
271 
272  int sccs()
273  {
274  return sccs_;
275  }
276 
277  mc_rvalue result()
278  {
279  return !found_ ? mc_rvalue::EMPTY : mc_rvalue::NOT_EMPTY;
280  }
281 
282  std::string trace()
283  {
284  SPOT_ASSERT(found_);
285  std::string res = "Prefix:\n";
286 
287  // Compute the prefix of the accepting run
288  for (auto& s : todo)
289  res += " " + std::to_string(s.st.st_prop) +
290  + "*" + sys_.to_string(s.st.st_kripke) + "\n";
291 
292  // Compute the accepting cycle
293  res += "Cycle:\n";
294 
295  struct ctrx_element
296  {
297  const product_state* prod_st;
298  ctrx_element* parent_st;
299  SuccIterator* it_kripke;
300  std::shared_ptr<trans_index> it_prop;
301  };
302  std::queue<ctrx_element*> bfs;
303 
304  acc_cond::mark_t acc = {};
305 
306  bfs.push(new ctrx_element({&todo.back().st, nullptr,
307  sys_.succ(todo.back().st.st_kripke, tid_),
308  twa_->succ(todo.back().st.st_prop)}));
309  while (true)
310  {
311  here:
312  auto* front = bfs.front();
313  bfs.pop();
314  // PUSH all successors of the state.
315  while (!front->it_kripke->done())
316  {
317  while (!front->it_prop->done())
318  {
319  if (twa_->get_cubeset().intersect
320  (twa_->trans_data(front->it_prop, tid_).cube_,
321  front->it_kripke->condition()))
322  {
323  const product_state dst = {
324  front->it_kripke->state(),
325  twa_->trans_storage(front->it_prop).dst
326  };
327 
328  // Skip Unknown states or not same SCC
329  auto it = map.find(dst);
330  if (it == map.end() ||
331  !uf_.sameset(it->second,
332  map[todo.back().st]))
333  {
334  front->it_prop->next();
335  continue;
336  }
337 
338  // This is a valid transition. If this transition
339  // is the one we are looking for, update the counter-
340  // -example and flush the bfs queue.
341  auto mark = twa_->trans_data(front->it_prop,
342  tid_).acc_;
343  if (!(acc & mark))
344  {
345  ctrx_element* current = front;
346  while (current != nullptr)
347  {
348  // FIXME: also display acc?
349  res = res + " " +
350  std::to_string(current->prod_st->st_prop) +
351  + "*" +
352  sys_. to_string(current->prod_st->st_kripke) +
353  "\n";
354  current = current->parent_st;
355  }
356 
357  // empty the queue
358  while (!bfs.empty())
359  {
360  auto* e = bfs.front();
361  sys_.recycle(e->it_kripke, tid_);
362  bfs.pop();
363  delete e;
364  }
365  sys_.recycle(front->it_kripke, tid_);
366  delete front;
367 
368  // update acceptance
369  acc |= mark;
370  if (twa_->acc().accepting(acc))
371  {
372  return res;
373  }
374 
375  const product_state* q = &(it->first);
376  ctrx_element* root = new ctrx_element({
377  q , nullptr,
378  sys_.succ(q->st_kripke, tid_),
379  twa_->succ(q->st_prop)
380  });
381  bfs.push(root);
382  goto here;
383  }
384 
385  // Otherwise increment iterator and push successor.
386  const product_state* q = &(it->first);
387  ctrx_element* root = new ctrx_element({
388  q , nullptr,
389  sys_.succ(q->st_kripke, tid_),
390  twa_->succ(q->st_prop)
391  });
392  bfs.push(root);
393  }
394  front->it_prop->next();
395  }
396  front->it_prop->reset();
397  front->it_kripke->next();
398  }
399  sys_.recycle(front->it_kripke, tid_);
400  delete front;
401  }
402 
403  // never reach here;
404  return res;
405  }
406 
407  private:
408 
409  struct todo_element
410  {
411  product_state st;
412  SuccIterator* it_kripke;
413  std::shared_ptr<trans_index> it_prop;
414  };
415 
416  struct root_element {
417  unsigned dfsnum;
418  acc_cond::mark_t ingoing;
419  acc_cond::mark_t acc;
420  };
421 
422  typedef std::unordered_map<const product_state, int,
423  product_state_hash,
424  product_state_equal> visited_map;
425 
426  kripkecube<State, SuccIterator>& sys_;
427  twacube_ptr twa_;
428  std::vector<todo_element> todo;
429  visited_map map;
430  unsigned int dfs_number = 0;
431  unsigned int trans_ = 0;
432  unsigned tid_;
433  std::atomic<bool>& stop_;
434  bool found_ = false;
435  std::vector<root_element> roots_;
436  int_unionfind uf_;
437  acc_cond acc_;
438  unsigned sccs_;
439  unsigned dfs_;
440  spot::timer_map tm_;
441  bool finisher_ = false;
442  };
443 }
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
This class implements the sequential emptiness check as presented in "Three SCC-based Emptiness Check...
Definition: lpar13.hh:40
bool update(product_state, unsigned, product_state, unsigned dst_dfsnum, acc_cond::mark_t cond)
This method is called for every closing, back, or forward edge. Return true if a counterexample has b...
Definition: lpar13.hh:216
bool pop_state(product_state, unsigned top_dfsnum, bool, product_state, unsigned)
This method is called to notify the emptiness checks that a state will be popped. If the method retur...
Definition: lpar13.hh:201
A map of timer, where each timer has a name.
Definition: timer.hh:225
A Transition-based ω-Automaton.
Definition: twa.hh:619
const acc_cond & acc() const
The acceptance condition of the automaton.
Definition: twa.hh:812
size_t wang32_hash(size_t key)
Thomas Wang's 32 bit hash function.
Definition: hashfunc.hh:37
@ U
until
Definition: automata.hh:26
mc_rvalue
Definition: mc.hh:43
@ NOT_EMPTY
The product is not empty.
@ EMPTY
The product is empty.
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