spot 2.12.2
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
30namespace 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.4