22 #include <spot/mc/intersect.hh>
23 #include <spot/twa/twa.hh>
24 #include <spot/twacube_algos/convert.hh>
30 template<
typename State,
typename SuccIterator,
31 typename StateHash,
typename StateEqual>
37 sys_(sys), dict_(dict)
40 State, SuccIterator>::value,
41 "error: does not match the kripkecube requirements");
52 State initial = sys_.initial(0);
53 if (SPOT_LIKELY(push(initial, dfs_number_+1)))
55 visited_[initial] = dfs_number_++;
56 todo_.push_back({initial, sys_.succ(initial, 0)});
58 while (!todo_.empty())
60 if (todo_.back().it->done())
62 if (SPOT_LIKELY(pop(todo_.back().s)))
64 sys_.recycle(todo_.back().it, 0);
71 State dst = todo_.back().it->state();
72 auto it = visited_.find(dst);
73 if (it == visited_.end())
75 if (SPOT_LIKELY(push(dst, dfs_number_+1)))
77 visited_[dst] = dfs_number_++;
78 todo_.back().it->next();
79 todo_.push_back({dst, sys_.succ(dst, 0)});
84 edge(visited_[todo_.back().s], visited_[dst]);
85 todo_.back().it->next();
94 auto d = spot::make_bdd_dict();
96 names_ =
new std::vector<std::string>();
99 for (
auto ap : sys_.ap())
101 auto idx = res_->register_ap(
ap);
102 reverse_binder_[i++] = idx;
106 bool push(State s,
unsigned i)
109 unsigned st = res_->new_state();
110 names_->push_back(sys_.to_string(s));
113 edge(visited_[todo_.back().s], st);
116 SPOT_ASSERT(st+1 == i);
125 void edge(
unsigned src,
unsigned dst)
128 bdd cond =
cube_to_bdd(todo_.back().it->condition(),
129 cs, reverse_binder_);
130 res_->new_edge(src, dst, cond);
135 res_->purge_unreachable_states();
136 res_->set_named_prop<std::vector<std::string>>(
"state-names", names_);
151 typedef std::unordered_map<
const State, int,
152 StateHash, StateEqual> visited__map;
155 std::vector<todo__element> todo_;
156 visited__map visited_;
157 unsigned int dfs_number_ = 0;
158 unsigned int transitions_ = 0;
159 spot::twa_graph_ptr res_;
160 std::vector<std::string>* names_;
162 std::unordered_map<int, int> reverse_binder_;
167 template<
typename State,
typename SuccIterator,
168 typename StateHash,
typename StateEqual>
177 struct product_state_equal
180 operator()(
const product_state lhs,
181 const product_state rhs)
const
184 return (lhs.st_prop == rhs.st_prop) &&
185 equal(lhs.st_kripke, rhs.st_kripke);
189 struct product_state_hash
192 operator()(
const product_state lhs)
const noexcept
195 unsigned u = hash(lhs.st_kripke) % (1<<30);
208 State, SuccIterator>::value,
209 "error: does not match the kripkecube requirements");
220 product_state initial = {sys_.initial(0), twa_->get_initial()};
221 if (SPOT_LIKELY(push_state(initial, dfs_number_+1, {})))
223 todo_.push_back({initial, sys_.succ(initial.st_kripke, 0),
224 twa_->succ(initial.st_prop)});
227 if (todo_.back().it_prop->done())
230 forward_iterators(sys_, twa_, todo_.back().it_kripke,
231 todo_.back().it_prop,
true, 0);
232 map[initial] = ++dfs_number_;
234 while (!todo_.empty())
238 if (todo_.back().it_kripke->done())
240 bool is_init = todo_.size() == 1;
241 auto newtop = is_init? todo_.back().st: todo_[todo_.size() -2].st;
242 if (SPOT_LIKELY(pop_state(todo_.back().st,
243 map[todo_.back().st],
248 sys_.recycle(todo_.back().it_kripke, 0);
255 product_state dst = {
256 todo_.back().it_kripke->state(),
257 twa_->trans_storage(todo_.back().it_prop, 0).dst
259 auto acc = twa_->trans_data(todo_.back().it_prop, 0).acc_;
260 forward_iterators(sys_, twa_, todo_.back().it_kripke,
261 todo_.back().it_prop,
false, 0);
262 auto it = map.find(dst);
265 if (SPOT_LIKELY(push_state(dst, dfs_number_+1, acc)))
267 map[dst] = ++dfs_number_;
268 todo_.push_back({dst, sys_.succ(dst.st_kripke, 0),
269 twa_->succ(dst.st_prop)});
270 forward_iterators(sys_, twa_, todo_.back().it_kripke,
271 todo_.back().it_prop,
true, 0);
274 else if (SPOT_UNLIKELY(update(todo_.back().st, dfs_number_,
275 dst, map[dst], acc)))
284 res_->purge_unreachable_states();
285 res_->
set_named_prop<std::vector<std::string>>(
"state-names", names_);
291 auto d = spot::make_bdd_dict();
293 names_ =
new std::vector<std::string>();
296 for (
auto ap : sys_.ap())
298 auto idx = res_->register_ap(
ap);
299 reverse_binder_[i++] = idx;
305 unsigned st = res_->new_state();
309 auto c = twa_->get_cubeset()
310 .intersection(twa_->trans_data
311 (todo_.back().it_prop).cube_,
312 todo_.back().it_kripke->condition());
316 twa_->get_cubeset().release(c);
317 res_->new_edge(map[todo_.back().st]-1, st, x,
319 (todo_.back().it_prop).acc_);
323 names_->push_back(sys_.to_string(s.st_kripke) +
324 (
'*' + std::to_string(s.st_prop)));
325 SPOT_ASSERT(st+1 == i);
329 bool update(product_state,
unsigned src,
330 product_state,
unsigned dst,
333 auto c = twa_->get_cubeset()
334 .intersection(twa_->trans_data
335 (todo_.back().it_prop).cube_,
336 todo_.back().it_kripke->condition());
340 twa_->get_cubeset().release(c);
341 res_->new_edge(src-1, dst-1, x, cond);
345 bool pop_state(product_state,
unsigned,
bool, product_state,
unsigned)
354 SuccIterator* it_kripke;
355 std::shared_ptr<trans_index> it_prop;
358 typedef std::unordered_map<
const product_state, int,
360 product_state_equal> visited_map;
364 std::vector<todo__element> todo_;
366 unsigned int dfs_number_ = 0;
367 unsigned int transitions_ = 0;
368 spot::twa_graph_ptr res_;
369 std::vector<std::string>* names_;
370 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:72
convert a (cube) model into a twa. Note that this algorithm cannot be run in parallel but could.
Definition: utils.hh:33
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:41
convert a (cube) product automaton into a twa Note that this algorithm cannot be run in parallel.
Definition: utils.hh:170
A Transition-based ω-Automaton.
Definition: twa.hh:623
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:41
twa_graph_ptr make_twa_graph(const bdd_dict_ptr &dict)
Build an explicit automaton from all states of aut,.
Definition: twagraph.hh:788
Definition: automata.hh:27
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:85