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

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