22 #include <spot/misc/common.hh> 24 #include <type_traits> 34 template <
typename State_Data,
typename Edge_Data>
40 template <
typename Of,
typename ...Args>
43 static const bool value =
false;
46 template <
typename Of,
typename Arg1,
typename ...Args>
49 static const bool value =
50 std::is_base_of<Of, typename std::decay<Arg1>::type>::value;
60 template <typename Data, bool boxed = !std::is_class<Data>::value>
67 template <
typename... Args,
68 typename =
typename std::enable_if<
70 boxed_label(Args&&... args)
71 noexcept(std::is_nothrow_constructible<Data, Args...>::value)
72 : label{std::forward<Args>(args)...}
79 explicit boxed_label()
80 noexcept(std::is_nothrow_constructible<Data>::value)
89 const Data& data()
const 94 bool operator<(
const boxed_label& other)
const 96 return label < other.label;
103 typedef std::tuple<> data_t;
109 const std::tuple<>& data()
const 116 template <
typename Data>
122 template <
typename... Args,
123 typename =
typename std::enable_if<
125 boxed_label(Args&&... args)
126 noexcept(std::is_nothrow_constructible<Data, Args...>::value)
127 : Data{std::forward<Args>(args)...}
134 explicit boxed_label()
135 noexcept(std::is_nothrow_constructible<Data>::value)
144 const Data& data()
const 157 template <
typename Edge,
typename State_Data>
164 template <
typename... Args,
165 typename =
typename std::enable_if<
167 distate_storage(Args&&... args)
168 noexcept(std::is_nothrow_constructible<State_Data, Args...>::value)
169 : State_Data{std::forward<Args>(args)...}
181 template <
typename StateIn,
182 typename StateOut,
typename Edge,
typename Edge_Data>
193 noexcept(std::is_nothrow_constructible<Edge_Data>::value)
199 template <
typename... Args>
201 StateIn src, Args&&... args)
202 noexcept(std::is_nothrow_constructible<Edge_Data, Args...>::value
203 && std::is_nothrow_constructible<StateOut, StateOut>::value
204 && std::is_nothrow_constructible<Edge, Edge>::value)
205 : Edge_Data{std::forward<Args>(args)...},
206 dst(dst), next_succ(next_succ), src(src)
222 return this->data() < other.data();
227 return src == other.src &&
229 this->data() == other.data();
241 template <
typename Graph>
245 typedef typename std::conditional<std::is_const<Graph>::value,
246 const typename Graph::edge_storage_t,
247 typename Graph::edge_storage_t>::type
249 typedef value_type& reference;
250 typedef value_type* pointer;
251 typedef std::ptrdiff_t difference_type;
252 typedef std::forward_iterator_tag iterator_category;
254 typedef typename Graph::edge edge;
276 reference operator*()
const 278 return g_->edge_storage(t_);
281 pointer operator->()
const 283 return &g_->edge_storage(t_);
288 t_ = operator*().next_succ;
295 t_ = operator*().next_succ;
299 operator bool()
const 314 template <
typename Graph>
319 typedef typename Graph::state_storage_t state_storage_t;
320 typedef typename Graph::edge edge;
323 : super(g, t), src_(src), prev_(0)
330 this->t_ = this->operator*().next_succ;
344 edge next = this->operator*().next_succ;
349 this->g_->edge_storage(prev_).next_succ = next;
353 if (src_.succ == this->t_)
356 if (src_.succ_tail == this->t_)
358 src_.succ_tail = prev_;
359 SPOT_ASSERT(next == 0);
363 this->operator*().next_succ = this->t_;
368 ++this->g_->killed_edge_;
372 state_storage_t& src_;
383 template <
typename Graph>
387 typedef typename Graph::edge edge;
417 template <
typename Graph>
421 typedef typename std::conditional<std::is_const<Graph>::value,
422 const typename Graph::edge_storage_t,
423 typename Graph::edge_storage_t>::type
425 typedef value_type& reference;
426 typedef value_type* pointer;
427 typedef std::ptrdiff_t difference_type;
428 typedef std::forward_iterator_tag iterator_category;
431 typedef typename std::conditional<std::is_const<Graph>::value,
432 const typename Graph::edge_vector_t,
433 typename Graph::edge_vector_t>::type
441 unsigned s = tv_.size();
444 while (t_ < s && tv_[t_].next_succ == t_);
455 : t_(tv.size()), tv_(tv)
482 reference operator*()
const 487 pointer operator->()
const 494 template <
typename Graph>
498 typedef typename std::conditional<std::is_const<Graph>::value,
499 const typename Graph::edge_vector_t,
500 typename Graph::edge_vector_t>::type
526 const unsigned* begin_;
527 const unsigned* end_;
531 : begin_(begin), end_(end)
536 : begin_(&tmp_), end_(&tmp_ + 1), tmp_(state)
540 const unsigned* begin()
const 545 const unsigned* end()
const 554 std::map<std::vector<unsigned>,
unsigned> uniq_;
564 unsigned new_univ_dests(I begin, I end)
566 std::vector<unsigned> tmp(begin, end);
567 std::sort(tmp.begin(), tmp.end());
568 tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
569 auto p = uniq_.emplace(tmp, 0);
571 p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end());
572 return p.first->second;
584 template <
typename State_Data,
typename Edge_Data>
596 typedef State_Data state_data_t;
597 typedef Edge_Data edge_data_t;
601 typedef unsigned state;
602 typedef unsigned edge;
610 typedef std::vector<state_storage_t> state_vector;
611 typedef std::vector<edge_storage_t> edge_vector_t;
615 typedef std::vector<unsigned> dests_vector_t;
618 state_vector states_;
619 edge_vector_t edges_;
620 dests_vector_t dests_;
622 unsigned killed_edge_;
630 digraph(
unsigned max_states = 10,
unsigned max_trans = 0)
633 states_.reserve(max_states);
635 max_trans = max_states * 2;
636 edges_.reserve(max_trans + 1);
641 edges_[0].next_succ = 0;
647 return states_.size();
655 return edges_.size() - killed_edge_ - 1;
661 return dests_.empty();
669 template <
typename... Args>
672 state s = states_.size();
673 states_.emplace_back(std::forward<Args>(args)...);
683 template <
typename... Args>
686 state s = states_.size();
687 states_.reserve(s + n);
689 states_.emplace_back(std::forward<Args>(args)...);
704 const state_storage_t&
716 typename state_storage_t::data_t&
719 return states_[s].data();
722 const typename state_storage_t::data_t&
725 return states_[s].data();
740 const edge_storage_t&
752 typename edge_storage_t::data_t&
755 return edges_[s].data();
758 const typename edge_storage_t::data_t&
761 return edges_[s].data();
770 template <
typename... Args>
774 edge t = edges_.size();
775 edges_.emplace_back(dst, 0, src, std::forward<Args>(args)...);
777 edge st = states_[src].succ_tail;
778 SPOT_ASSERT(st < t || !st);
780 states_[src].succ = t;
782 edges_[st].next_succ = t;
783 states_[src].succ_tail = t;
794 template <
typename I>
798 unsigned sz = std::distance(dst_begin, dst_end);
802 unsigned d = dests_.size();
803 dests_.emplace_back(sz);
804 dests_.insert(dests_.end(), dst_begin, dst_end);
814 template <
typename I,
typename... Args>
818 return new_edge(src, new_univ_dests(dst_begin, dst_end),
819 std::forward<Args>(args)...);
827 template <
typename... Args>
832 return new_univ_edge(src, dsts.begin(), dsts.end(),
833 std::forward<Args>(args)...);
841 const unsigned* d = dests_.data();
844 return { d + 1, d + num + 1 };
854 return univ_dests(e.dst);
860 SPOT_ASSERT(!states_.empty());
861 return &ss - &states_.front();
867 SPOT_ASSERT(!edges_.empty());
868 return &tt - &edges_.front();
876 return {
this, states_[src].succ};
882 return out(index_of_state(src));
888 return {
this, states_[src].succ};
892 out(state_storage_t& src)
const 894 return out(index_of_state(src));
905 return {
this, src.succ, src};
911 return out_iteraser(state_storage(src));
973 return (t < edges_.size() &&
974 edges_[t].next_succ != t);
983 return edges_[t].next_succ == t;
988 return t.next_succ == index_of_edge(t);
1011 unsigned tend = edges_.size();
1012 for (
unsigned t = 1; t < tend; ++t)
1014 o <<
't' << t <<
": (s" 1015 << edges_[t].src <<
", ";
1016 int d = edges_[t].dst;
1021 o <<
") t" << edges_[t].next_succ <<
'\n';
1023 unsigned send = states_.size();
1024 for (
unsigned s = 0; s < send; ++s)
1026 o <<
's' << s <<
": t" 1027 << states_[s].succ <<
" t" 1028 << states_[s].succ_tail <<
'\n';
1030 unsigned dend = dests_.size();
1032 for (
unsigned s = 0; s < dend; ++s)
1034 o <<
'd' << s <<
": ";
1045 o << dests_[s] <<
'\n';
1049 enum dump_storage_items {
1050 DSI_GraphHeader = 1,
1051 DSI_GraphFooter = 2,
1052 DSI_StatesHeader = 4,
1054 DSI_StatesFooter = 16,
1055 DSI_States = DSI_StatesHeader | DSI_StatesBody | DSI_StatesFooter,
1056 DSI_EdgesHeader = 32,
1058 DSI_EdgesFooter = 128,
1059 DSI_Edges = DSI_EdgesHeader | DSI_EdgesBody | DSI_EdgesFooter,
1060 DSI_DestsHeader = 256,
1061 DSI_DestsBody = 512,
1062 DSI_DestsFooter = 1024,
1063 DSI_Dests = DSI_DestsHeader | DSI_DestsBody | DSI_DestsFooter,
1065 DSI_GraphHeader | DSI_States | DSI_Edges | DSI_Dests | DSI_GraphFooter,
1071 if (dsi & DSI_GraphHeader)
1072 o <<
"digraph g { \nnode [shape=plaintext]\n";
1073 unsigned send = states_.size();
1074 if (dsi & DSI_StatesHeader)
1076 o << (
"states [label=<\n" 1077 "<table border='0' cellborder='1' cellspacing='0'>\n" 1078 "<tr><td sides='b' bgcolor='yellow' port='s'>states</td>\n");
1079 for (
unsigned s = 0; s < send; ++s)
1080 o <<
"<td sides='b' bgcolor='yellow' port='s" << s <<
"'>" 1084 if (dsi & DSI_StatesBody)
1086 o <<
"<tr><td port='ss'>succ</td>\n";
1087 for (
unsigned s = 0; s < send; ++s)
1089 o <<
"<td port='ss" << s;
1090 if (states_[s].succ)
1091 o <<
"' bgcolor='cyan";
1092 o <<
"'>" << states_[s].succ <<
"</td>\n";
1094 o <<
"</tr><tr><td port='st'>succ_tail</td>\n";
1095 for (
unsigned s = 0; s < send; ++s)
1097 o <<
"<td port='st" << s;
1098 if (states_[s].succ_tail)
1099 o <<
"' bgcolor='cyan";
1100 o <<
"'>" << states_[s].succ_tail <<
"</td>\n";
1104 if (dsi & DSI_StatesFooter)
1105 o <<
"</table>>]\n";
1106 unsigned eend = edges_.size();
1107 if (dsi & DSI_EdgesHeader)
1109 o << (
"edges [label=<\n" 1110 "<table border='0' cellborder='1' cellspacing='0'>\n" 1111 "<tr><td sides='b' bgcolor='cyan' port='e'>edges</td>\n");
1112 for (
unsigned e = 1; e < eend; ++e)
1114 o <<
"<td sides='b' bgcolor='" 1115 << (e != edges_[e].next_succ ?
"cyan" :
"gray")
1116 <<
"' port='e" << e <<
"'>" << e <<
"</td>\n";
1120 if (dsi & DSI_EdgesBody)
1122 o <<
"<tr><td port='ed'>dst</td>\n";
1123 for (
unsigned e = 1; e < eend; ++e)
1125 o <<
"<td port='ed" << e;
1126 int d = edges_[e].dst;
1128 o <<
"' bgcolor='pink'>~" << ~d;
1130 o <<
"' bgcolor='yellow'>" << d;
1133 o <<
"</tr><tr><td port='en'>next_succ</td>\n";
1134 for (
unsigned e = 1; e < eend; ++e)
1136 o <<
"<td port='en" << e;
1137 if (edges_[e].next_succ)
1139 if (edges_[e].next_succ != e)
1140 o <<
"' bgcolor='cyan";
1142 o <<
"' bgcolor='gray";
1144 o <<
"'>" << edges_[e].next_succ <<
"</td>\n";
1146 o <<
"</tr><tr><td port='es'>src</td>\n";
1147 for (
unsigned e = 1; e < eend; ++e)
1148 o <<
"<td port='es" << e <<
"' bgcolor='yellow'>" 1149 << edges_[e].src <<
"</td>\n";
1152 if (dsi & DSI_EdgesFooter)
1153 o <<
"</table>>]\n";
1154 if (!dests_.empty())
1156 unsigned dend = dests_.size();
1157 if (dsi & DSI_DestsHeader)
1159 o << (
"dests [label=<\n" 1160 "<table border='0' cellborder='1' cellspacing='0'>\n" 1161 "<tr><td sides='b' bgcolor='pink' port='d'>dests</td>\n");
1165 o <<
"<td sides='b' bgcolor='pink' port='d" 1166 << d <<
"'>~" << d <<
"</td>\n";
1167 unsigned cnt = dests_[d];
1170 o <<
"<td sides='b'></td>\n";
1174 if (dsi & DSI_DestsBody)
1176 o <<
"<tr><td port='dd'>#cnt/dst</td>\n";
1180 unsigned cnt = dests_[d];
1181 o <<
"<td port='d'>#" << cnt <<
"</td>\n";
1185 o <<
"<td bgcolor='yellow' port='dd" 1186 << d <<
"'>" << dests_[d] <<
"</td>\n";
1192 if (dsi & DSI_DestsFooter)
1193 o <<
"</table>>]\n";
1195 if (dsi & DSI_GraphFooter)
1206 if (killed_edge_ == 0)
1208 auto i = std::remove_if(edges_.begin() + 1, edges_.end(),
1209 [
this](
const edge_storage_t& t) {
1210 return this->is_dead_edge(t);
1212 edges_.erase(i, edges_.end());
1221 template<
class Predicate = std::less<edge_storage_t>>
1226 std::stable_sort(edges_.begin() + 1, edges_.end(), p);
1235 state last_src = -1
U;
1236 edge tend = edges_.size();
1237 for (edge t = 1; t < tend; ++t)
1239 state src = edges_[t].src;
1240 if (src != last_src)
1242 states_[src].succ = t;
1243 if (last_src != -1
U)
1245 states_[last_src].succ_tail = t - 1;
1246 edges_[t - 1].next_succ = 0;
1248 while (++last_src != src)
1250 states_[last_src].succ = 0;
1251 states_[last_src].succ_tail = 0;
1256 edges_[t - 1].next_succ = t;
1259 if (last_src != -1
U)
1261 states_[last_src].succ_tail = tend - 1;
1262 edges_[tend - 1].next_succ = 0;
1264 unsigned send = states_.size();
1265 while (++last_src != send)
1267 states_[last_src].succ = 0;
1268 states_[last_src].succ_tail = 0;
1281 SPOT_ASSERT(newst.size() == states_.size());
1282 unsigned tend = edges_.size();
1283 for (
unsigned t = 1; t < tend; t++)
1285 edges_[t].dst = newst[edges_[t].dst];
1286 edges_[t].src = newst[edges_[t].src];
1297 SPOT_ASSERT(newst.size() >= states_.size());
1298 SPOT_ASSERT(used_states > 0);
1304 unsigned send = states_.size();
1305 for (state s = 0; s < send; ++s)
1307 state dst = newst[s];
1315 auto t = states_[s].succ;
1317 std::swap(t, edges_[t].next_succ);
1320 states_[dst] = std::move(states_[s]);
1322 states_.resize(used_states);
1327 unsigned tend = edges_.size();
1328 std::vector<edge> newidx(tend);
1330 for (edge t = 1; t < tend; ++t)
1332 if (is_dead_edge(t))
1335 edges_[dest] = std::move(edges_[t]);
1339 edges_.resize(dest);
1343 for (edge t = 1; t < dest; ++t)
1345 auto& tr = edges_[t];
1346 tr.src = newst[tr.src];
1347 tr.dst = newst[tr.dst];
1348 tr.next_succ = newidx[tr.next_succ];
1352 for (
auto& s: states_)
1354 s.succ = newidx[s.succ];
1355 s.succ_tail = newidx[s.succ_tail];
state new_states(unsigned n, Args &&... args)
Create n new states.
Definition: graph.hh:684
Definition: automata.hh:26
state index_of_state(const state_storage_t &ss) const
Convert a storage reference into a state number.
Definition: graph.hh:858
const edge_storage_t::data_t & edge_data(edge s) const
return the Edgeg_Data of an edge.
Definition: graph.hh:759
internal::killer_edge_iterator< digraph > out_iteraser(state src)
Return a fake container with all edges leaving src, allowing erasure.
Definition: graph.hh:909
state_vector & states()
Return the vector of states.
Definition: graph.hh:923
const dests_vector_t & dests_vector() const
The vector used to store universal destinations.
Definition: graph.hh:997
internal::state_out< const digraph > out(state src) const
Return a fake container with all edges leaving src.
Definition: graph.hh:886
state new_state(Args &&... args)
Create a new states.
Definition: graph.hh:670
A directed graph.
Definition: graph.hh:35
void dump_storage(std::ostream &o) const
Dump the state and edge storage for debugging.
Definition: graph.hh:1009
void sort_edges_(Predicate p=Predicate())
Sort all edges according to a predicate.
Definition: graph.hh:1222
Abstract class for states.
Definition: twa.hh:50
bool is_existential() const
Whether the automaton uses only existential branching.
Definition: graph.hh:659
const state_storage_t::data_t & state_data(state s) const
return the State_Data associated to a state
Definition: graph.hh:723
internal::killer_edge_iterator< digraph > out_iteraser(state_storage_t &src)
Return a fake container with all edges leaving src, allowing erasure.
Definition: graph.hh:903
edge_storage_t & edge_storage(edge s)
return a reference to the storage of an edge
Definition: graph.hh:735
edge new_edge(state src, state dst, Args &&... args)
Create a new edge.
Definition: graph.hh:772
const state_vector & states() const
Return the vector of states.
Definition: graph.hh:918
state_storage_t::data_t & state_data(state s)
return the State_Data associated to a state
Definition: graph.hh:717
void dump_storage_as_dot(std::ostream &o, int dsi=DSI_All) const
Dump the state and edge storage for debugging.
Definition: graph.hh:1069
internal::state_out< const digraph > out(state_storage_t &src) const
Return a fake container with all edges leaving src.
Definition: graph.hh:892
void remove_dead_edges_()
Remove all dead edges.
Definition: graph.hh:1204
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:699
const state_storage_t & state_storage(state s) const
return a reference to the storage of a state
Definition: graph.hh:705
internal::all_trans< const digraph > edges() const
Return a fake container with all edges (exluding erased edges)
Definition: graph.hh:933
bool is_dead_edge(unsigned t) const
Tests whether an edge has been erased.
Definition: graph.hh:981
internal::all_trans< digraph > edges()
Return a fake container with all edges (exluding erased edges)
Definition: graph.hh:938
edge_storage_t::data_t & edge_data(edge s)
return the Edgeg_Data of an edge.
Definition: graph.hh:753
const edge_storage_t & edge_storage(edge s) const
return a reference to the storage of an edge
Definition: graph.hh:741
edge_vector_t & edge_vector()
Return the vector of all edges.
Definition: graph.hh:957
unsigned num_states() const
The number of states in the automaton.
Definition: graph.hh:645
const edge_vector_t & edge_vector() const
Return the vector of all edges.
Definition: graph.hh:952
dests_vector_t & dests_vector()
The vector used to store universal destinations.
Definition: graph.hh:1002
edge new_univ_edge(state src, const std::initializer_list< state > &dsts, Args &&... args)
Create a new universal edge.
Definition: graph.hh:829
unsigned num_edges() const
The number of edges in the automaton.
Definition: graph.hh:653
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:969
edge index_of_edge(const edge_storage_t &tt) const
Convert a storage reference into an edge number.
Definition: graph.hh:865
void rename_states_(const std::vector< unsigned > &newst)
Rename all the states in the edge vector.
Definition: graph.hh:1279
internal::state_out< digraph > out(state src)
Return a fake container with all edges leaving src.
Definition: graph.hh:874
void defrag_states(std::vector< unsigned > &&newst, unsigned used_states)
Rename and remove states.
Definition: graph.hh:1295
internal::state_out< digraph > out(state_storage_t &src)
Return a fake container with all edges leaving src.
Definition: graph.hh:880
state new_univ_dests(I dst_begin, I dst_end)
Create a new universal destination group.
Definition: graph.hh:796
digraph(unsigned max_states=10, unsigned max_trans=0)
Construct an empty graph.
Definition: graph.hh:630
edge new_univ_edge(state src, I dst_begin, I dst_end, Args &&... args)
Create a new universal edge.
Definition: graph.hh:816
void chain_edges_()
Reconstruct the chain of outgoing edges.
Definition: graph.hh:1233
bool is_dead_edge(const edge_storage_t &t) const
Tests whether an edge has been erased.
Definition: graph.hh:986