21#include <spot/mc/intersect.hh>
22#include <spot/twa/twa.hh>
23#include <spot/twacube_algos/convert.hh>
29 template<
typename State,
typename SuccIterator,
30 typename StateHash,
typename StateEqual>
36 sys_(sys), dict_(dict)
39 State, SuccIterator>::value,
40 "error: does not match the kripkecube requirements");
51 State initial = sys_.initial(0);
52 if (SPOT_LIKELY(push(initial, dfs_number_+1)))
54 visited_[initial] = dfs_number_++;
55 todo_.push_back({initial, sys_.succ(initial, 0)});
57 while (!todo_.empty())
59 if (todo_.back().it->done())
61 if (SPOT_LIKELY(pop(todo_.back().s)))
63 sys_.recycle(todo_.back().it, 0);
70 State dst = todo_.back().it->state();
71 auto it = visited_.find(dst);
72 if (it == visited_.end())
74 if (SPOT_LIKELY(push(dst, dfs_number_+1)))
76 visited_[dst] = dfs_number_++;
77 todo_.back().it->next();
78 todo_.push_back({dst, sys_.succ(dst, 0)});
83 edge(visited_[todo_.back().s], visited_[dst]);
84 todo_.back().it->next();
93 auto d = spot::make_bdd_dict();
95 names_ =
new std::vector<std::string>();
98 for (
auto ap : sys_.ap())
100 auto idx = res_->register_ap(
ap);
101 reverse_binder_[i++] = idx;
105 bool push(State s,
unsigned i)
108 unsigned st = res_->new_state();
109 names_->push_back(sys_.to_string(s));
112 edge(visited_[todo_.back().s], st);
115 SPOT_ASSERT(st+1 == i);
124 void edge(
unsigned src,
unsigned dst)
127 bdd cond =
cube_to_bdd(todo_.back().it->condition(),
128 cs, reverse_binder_);
129 res_->new_edge(src, dst, cond);
134 res_->purge_unreachable_states();
135 res_->set_named_prop<std::vector<std::string>>(
"state-names", names_);
150 typedef std::unordered_map<
const State, int,
151 StateHash, StateEqual> visited__map;
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_;
161 std::unordered_map<int, int> reverse_binder_;
166 template<
typename State,
typename SuccIterator,
167 typename StateHash,
typename StateEqual>
176 struct product_state_equal
179 operator()(
const product_state lhs,
180 const product_state rhs)
const
183 return (lhs.st_prop == rhs.st_prop) &&
184 equal(lhs.st_kripke, rhs.st_kripke);
188 struct product_state_hash
191 operator()(
const product_state lhs)
const noexcept
194 unsigned u = hash(lhs.st_kripke) % (1<<30);
207 State, SuccIterator>::value,
208 "error: does not match the kripkecube requirements");
219 product_state initial = {sys_.initial(0), twa_->get_initial()};
220 if (SPOT_LIKELY(push_state(initial, dfs_number_+1, {})))
222 todo_.push_back({initial, sys_.succ(initial.st_kripke, 0),
223 twa_->succ(initial.st_prop)});
226 if (todo_.back().it_prop->done())
229 forward_iterators(sys_, twa_, todo_.back().it_kripke,
230 todo_.back().it_prop,
true, 0);
231 map[initial] = ++dfs_number_;
233 while (!todo_.empty())
237 if (todo_.back().it_kripke->done())
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],
247 sys_.recycle(todo_.back().it_kripke, 0);
254 product_state dst = {
255 todo_.back().it_kripke->state(),
256 twa_->trans_storage(todo_.back().it_prop, 0).dst
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);
264 if (SPOT_LIKELY(push_state(dst, dfs_number_+1, acc)))
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);
273 else if (SPOT_UNLIKELY(update(todo_.back().st, dfs_number_,
274 dst, map[dst], acc)))
283 res_->purge_unreachable_states();
284 res_->
set_named_prop<std::vector<std::string>>(
"state-names", names_);
290 auto d = spot::make_bdd_dict();
292 names_ =
new std::vector<std::string>();
295 for (
auto ap : sys_.ap())
297 auto idx = res_->register_ap(
ap);
298 reverse_binder_[i++] = idx;
304 unsigned st = res_->new_state();
308 auto c = twa_->get_cubeset()
309 .intersection(twa_->trans_data
310 (todo_.back().it_prop).cube_,
311 todo_.back().it_kripke->condition());
315 twa_->get_cubeset().release(c);
316 res_->new_edge(map[todo_.back().st]-1, st, x,
318 (todo_.back().it_prop).acc_);
322 names_->push_back(sys_.to_string(s.st_kripke) +
323 (
'*' + std::to_string(s.st_prop)));
324 SPOT_ASSERT(st+1 == i);
328 bool update(product_state,
unsigned src,
329 product_state,
unsigned dst,
332 auto c = twa_->get_cubeset()
333 .intersection(twa_->trans_data
334 (todo_.back().it_prop).cube_,
335 todo_.back().it_kripke->condition());
339 twa_->get_cubeset().release(c);
340 res_->new_edge(src-1, dst-1, x, cond);
344 bool pop_state(product_state,
unsigned,
bool, product_state,
unsigned)
353 SuccIterator* it_kripke;
354 std::shared_ptr<trans_index> it_prop;
357 typedef std::unordered_map<
const product_state, int,
359 product_state_equal> visited_map;
363 std::vector<todo__element> todo_;
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_;
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
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