22 #include <spot/twa/twagraph.hh>
41 template<
typename Trans>
42 void transform_accessible(
const const_twa_graph_ptr& old,
44 Trans trans,
unsigned int init)
46 if (!old->is_existential())
47 throw std::runtime_error
48 (
"transform_accessible() does not support alternation");
50 std::vector<unsigned> todo;
51 std::vector<unsigned> seen(old->num_states(), -1
U);
54 [&](
unsigned old_state) ->
unsigned
56 unsigned tmp = seen[old_state];
59 tmp = cpy->new_state();
60 seen[old_state] = tmp;
61 todo.emplace_back(old_state);
66 cpy->set_init_state(new_state(init));
69 unsigned old_src = todo.back();
72 unsigned new_src = seen[old_src];
73 SPOT_ASSERT(new_src != -1
U);
75 for (
auto& t: old->out(old_src))
78 acc_cond::mark_t acc = t.acc;
79 trans(t.src, cond, acc, t.dst);
82 cpy->new_edge(new_src,
103 template<
typename Trans>
104 void transform_copy(
const const_twa_graph_ptr& old,
106 Trans trans,
unsigned int init)
108 if (!old->is_existential())
109 throw std::runtime_error
110 (
"transform_copy() does not support alternation");
113 cpy->new_states(old->num_states());
114 cpy->set_init_state(init);
116 for (
auto& t: old->edges())
119 acc_cond::mark_t acc = t.acc;
120 trans(t.src, cond, acc, t.dst);
123 SPOT_ASSERT(t.src < cpy->num_states() && t.dst < cpy->num_states());
124 if (cond != bddfalse)
125 cpy->new_edge(t.src, t.dst, cond, acc);
129 template<
typename Trans>
130 void transform_accessible(
const const_twa_graph_ptr& old,
134 transform_accessible(old, cpy, trans, old->get_init_state_number());
136 template<
typename Trans>
137 void transform_copy(
const const_twa_graph_ptr& old,
141 transform_copy(old, cpy, trans, old->get_init_state_number());
146 twa_graph_ptr mask_acc_sets(
const const_twa_graph_ptr& in,
147 acc_cond::mark_t to_remove);
160 twa_graph_ptr mask_keep_states(
const const_twa_graph_ptr& in,
161 std::vector<bool>& to_keep,
173 twa_graph_ptr mask_keep_accessible_states(
const const_twa_graph_ptr& in,
174 std::vector<bool>& to_keep,