22 #include <spot/misc/common.hh>
23 #include <spot/misc/_config.h>
25 #include <type_traits>
32 #ifdef SPOT_ENABLE_PTHREAD
38 template <
typename State_Data,
typename Edge_Data>
39 class SPOT_API digraph;
44 template <
typename Of,
typename ...Args>
47 static const bool value =
false;
50 template <
typename Of,
typename Arg1,
typename ...Args>
53 static const bool value =
54 std::is_base_of<Of, typename std::decay<Arg1>::type>::value;
64 template <typename Data, bool boxed = !std::is_class<Data>::value>
71 template <
typename... Args,
72 typename =
typename std::enable_if<
75 noexcept(std::is_nothrow_constructible<Data, Args...>::value)
76 : label{std::forward<Args>(args)...}
84 noexcept(std::is_nothrow_constructible<Data>::value)
93 const Data& data()
const
100 return label < other.label;
107 typedef std::tuple<> data_t;
113 const std::tuple<>& data()
const
120 template <
typename Data>
126 template <
typename... Args,
127 typename =
typename std::enable_if<
130 noexcept(std::is_nothrow_constructible<Data, Args...>::value)
131 : Data{std::forward<Args>(args)...}
139 noexcept(std::is_nothrow_constructible<Data>::value)
148 const Data& data()
const
161 template <
typename Edge,
typename State_Data>
168 template <
typename... Args,
169 typename =
typename std::enable_if<
172 noexcept(std::is_nothrow_constructible<State_Data, Args...>::value)
173 : State_Data{std::forward<Args>(args)...}
185 template <
typename StateIn,
186 typename StateOut,
typename Edge,
typename Edge_Data>
197 noexcept(std::is_nothrow_constructible<Edge_Data>::value)
203 template <
typename... Args>
205 StateIn src, Args&&... args)
206 noexcept(std::is_nothrow_constructible<Edge_Data, Args...>::value
207 && std::is_nothrow_constructible<StateOut, StateOut>::value
208 && std::is_nothrow_constructible<Edge, Edge>::value)
209 : Edge_Data{std::forward<Args>(args)...},
210 dst(dst), next_succ(next_succ), src(src)
226 return this->data() < other.data();
231 return src == other.src &&
233 this->data() == other.data();
245 template <
typename Graph>
249 typedef typename std::conditional<std::is_const<Graph>::value,
250 const typename Graph::edge_storage_t,
251 typename Graph::edge_storage_t>::type
253 typedef value_type& reference;
254 typedef value_type* pointer;
255 typedef std::ptrdiff_t difference_type;
256 typedef std::forward_iterator_tag iterator_category;
258 typedef typename Graph::edge edge;
280 reference operator*()
const
282 return g_->edge_storage(t_);
285 pointer operator->()
const
287 return &g_->edge_storage(t_);
292 t_ = operator*().next_succ;
299 t_ = operator*().next_succ;
303 operator bool()
const
318 template <
typename Graph>
323 typedef typename Graph::state_storage_t state_storage_t;
324 typedef typename Graph::edge edge;
327 :
super(g, t), src_(src), prev_(0)
334 this->t_ = this->operator*().next_succ;
348 edge next = this->operator*().next_succ;
353 this->g_->edge_storage(prev_).next_succ = next;
357 if (src_.succ == this->t_)
360 if (src_.succ_tail == this->t_)
362 src_.succ_tail = prev_;
363 SPOT_ASSERT(next == 0);
367 this->operator*().next_succ = this->t_;
372 ++this->g_->killed_edge_;
376 state_storage_t& src_;
387 template <
typename Graph>
391 typedef typename Graph::edge edge;
421 template <
typename Graph>
425 typedef typename std::conditional<std::is_const<Graph>::value,
426 const typename Graph::edge_storage_t,
427 typename Graph::edge_storage_t>::type
429 typedef value_type& reference;
430 typedef value_type* pointer;
431 typedef std::ptrdiff_t difference_type;
432 typedef std::forward_iterator_tag iterator_category;
435 typedef typename std::conditional<std::is_const<Graph>::value,
436 const typename Graph::edge_vector_t,
437 typename Graph::edge_vector_t>::type
445 unsigned s = tv_.size();
448 while (t_ < s && tv_[t_].next_succ == t_);
459 : t_(tv.size()), tv_(tv)
486 reference operator*()
const
491 pointer operator->()
const
498 template <
typename Graph>
502 typedef typename std::conditional<std::is_const<Graph>::value,
503 const typename Graph::edge_vector_t,
504 typename Graph::edge_vector_t>::type
530 const unsigned* begin_;
531 const unsigned* end_;
535 : begin_(begin), end_(end)
540 : begin_(&tmp_), end_(&tmp_ + 1), tmp_(
state)
544 const unsigned* begin()
const
549 const unsigned* end()
const
558 std::map<std::vector<unsigned>,
unsigned> uniq_;
568 unsigned new_univ_dests(I begin, I end)
570 std::vector<unsigned> tmp(begin, end);
571 std::sort(tmp.begin(), tmp.end());
572 tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
573 auto p = uniq_.emplace(tmp, 0);
575 p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end());
576 return p.first->second;
588 template <
typename State_Data,
typename Edge_Data>
600 typedef State_Data state_data_t;
601 typedef Edge_Data edge_data_t;
605 typedef unsigned state;
606 typedef unsigned edge;
614 typedef std::vector<state_storage_t> state_vector;
615 typedef std::vector<edge_storage_t> edge_vector_t;
619 typedef std::vector<unsigned> dests_vector_t;
622 state_vector states_;
623 edge_vector_t edges_;
624 dests_vector_t dests_;
626 unsigned killed_edge_;
634 digraph(
unsigned max_states = 10,
unsigned max_trans = 0)
637 states_.reserve(max_states);
639 max_trans = max_states * 2;
640 edges_.reserve(max_trans + 1);
645 edges_[0].next_succ = 0;
651 return states_.size();
659 return edges_.size() - killed_edge_ - 1;
665 return dests_.empty();
673 template <
typename... Args>
676 state s = states_.size();
677 states_.emplace_back(std::forward<Args>(args)...);
687 template <
typename... Args>
690 state s = states_.size();
691 states_.reserve(s + n);
693 states_.emplace_back(std::forward<Args>(args)...);
708 const state_storage_t&
720 typename state_storage_t::data_t&
723 return states_[s].data();
726 const typename state_storage_t::data_t&
729 return states_[s].data();
744 const edge_storage_t&
756 typename edge_storage_t::data_t&
759 return edges_[s].data();
762 const typename edge_storage_t::data_t&
765 return edges_[s].data();
774 template <
typename... Args>
778 edge t = edges_.size();
779 edges_.emplace_back(dst, 0, src, std::forward<Args>(args)...);
781 edge st = states_[src].succ_tail;
782 SPOT_ASSERT(st < t || !st);
784 states_[src].succ = t;
786 edges_[st].next_succ = t;
787 states_[src].succ_tail = t;
798 template <
typename I>
802 unsigned sz = std::distance(dst_begin, dst_end);
806 unsigned d = dests_.size();
808 && &*dst_begin >= &dests_.front()
809 && &*dst_begin <= &dests_.back()
810 && (dests_.capacity() - dests_.size()) < (sz + 1))
815 std::vector<unsigned> tmp(dst_begin, dst_end);
816 dests_.emplace_back(sz);
817 dests_.insert(dests_.end(), tmp.begin(), tmp.end());
821 dests_.emplace_back(sz);
822 dests_.insert(dests_.end(), dst_begin, dst_end);
833 template <
typename I,
typename... Args>
838 std::forward<Args>(args)...);
846 template <
typename... Args>
852 std::forward<Args>(args)...);
860 const unsigned* d = dests_.data();
863 return { d + 1, d + num + 1 };
871 internal::const_universal_dests univ_dests(
const edge_storage_t& e)
const
873 return univ_dests(e.dst);
879 SPOT_ASSERT(!states_.empty());
880 return &ss - &states_.front();
886 SPOT_ASSERT(!edges_.empty());
887 return &
tt - &edges_.front();
895 return {
this, states_[src].succ};
907 return {
this, states_[src].succ};
924 return {
this, src.succ, src};
992 return (t < edges_.size() &&
993 edges_[t].next_succ != t);
1002 return edges_[t].next_succ == t;
1030 unsigned tend = edges_.size();
1031 for (
unsigned t = 1; t < tend; ++t)
1033 o <<
't' << t <<
": (s"
1034 << edges_[t].src <<
", ";
1035 int d = edges_[t].dst;
1040 o <<
") t" << edges_[t].next_succ <<
'\n';
1042 unsigned send = states_.size();
1043 for (
unsigned s = 0; s < send; ++s)
1045 o <<
's' << s <<
": t"
1046 << states_[s].succ <<
" t"
1047 << states_[s].succ_tail <<
'\n';
1049 unsigned dend = dests_.size();
1051 for (
unsigned s = 0; s < dend; ++s)
1053 o <<
'd' << s <<
": ";
1064 o << dests_[s] <<
'\n';
1068 enum dump_storage_items {
1069 DSI_GraphHeader = 1,
1070 DSI_GraphFooter = 2,
1071 DSI_StatesHeader = 4,
1073 DSI_StatesFooter = 16,
1074 DSI_States = DSI_StatesHeader | DSI_StatesBody | DSI_StatesFooter,
1075 DSI_EdgesHeader = 32,
1077 DSI_EdgesFooter = 128,
1078 DSI_Edges = DSI_EdgesHeader | DSI_EdgesBody | DSI_EdgesFooter,
1079 DSI_DestsHeader = 256,
1080 DSI_DestsBody = 512,
1081 DSI_DestsFooter = 1024,
1082 DSI_Dests = DSI_DestsHeader | DSI_DestsBody | DSI_DestsFooter,
1084 DSI_GraphHeader | DSI_States | DSI_Edges | DSI_Dests | DSI_GraphFooter,
1090 if (dsi & DSI_GraphHeader)
1091 o <<
"digraph g { \nnode [shape=plaintext]\n";
1092 unsigned send = states_.size();
1093 if (dsi & DSI_StatesHeader)
1095 o << (
"states [label=<\n"
1096 "<table border='0' cellborder='1' cellspacing='0'>\n"
1097 "<tr><td sides='b' bgcolor='yellow' port='s'>states</td>\n");
1098 for (
unsigned s = 0; s < send; ++s)
1099 o <<
"<td sides='b' bgcolor='yellow' port='s" << s <<
"'>"
1103 if (dsi & DSI_StatesBody)
1105 o <<
"<tr><td port='ss'>succ</td>\n";
1106 for (
unsigned s = 0; s < send; ++s)
1108 o <<
"<td port='ss" << s;
1109 if (states_[s].succ)
1110 o <<
"' bgcolor='cyan";
1111 o <<
"'>" << states_[s].succ <<
"</td>\n";
1113 o <<
"</tr><tr><td port='st'>succ_tail</td>\n";
1114 for (
unsigned s = 0; s < send; ++s)
1116 o <<
"<td port='st" << s;
1117 if (states_[s].succ_tail)
1118 o <<
"' bgcolor='cyan";
1119 o <<
"'>" << states_[s].succ_tail <<
"</td>\n";
1123 if (dsi & DSI_StatesFooter)
1124 o <<
"</table>>]\n";
1125 unsigned eend = edges_.size();
1126 if (dsi & DSI_EdgesHeader)
1128 o << (
"edges [label=<\n"
1129 "<table border='0' cellborder='1' cellspacing='0'>\n"
1130 "<tr><td sides='b' bgcolor='cyan' port='e'>edges</td>\n");
1131 for (
unsigned e = 1; e < eend; ++e)
1133 o <<
"<td sides='b' bgcolor='"
1134 << (e != edges_[e].next_succ ?
"cyan" :
"gray")
1135 <<
"' port='e" << e <<
"'>" << e <<
"</td>\n";
1139 if (dsi & DSI_EdgesBody)
1141 o <<
"<tr><td port='ed'>dst</td>\n";
1142 for (
unsigned e = 1; e < eend; ++e)
1144 o <<
"<td port='ed" << e;
1145 int d = edges_[e].dst;
1147 o <<
"' bgcolor='pink'>~" << ~d;
1149 o <<
"' bgcolor='yellow'>" << d;
1152 o <<
"</tr><tr><td port='en'>next_succ</td>\n";
1153 for (
unsigned e = 1; e < eend; ++e)
1155 o <<
"<td port='en" << e;
1156 if (edges_[e].next_succ)
1158 if (edges_[e].next_succ != e)
1159 o <<
"' bgcolor='cyan";
1161 o <<
"' bgcolor='gray";
1163 o <<
"'>" << edges_[e].next_succ <<
"</td>\n";
1165 o <<
"</tr><tr><td port='es'>src</td>\n";
1166 for (
unsigned e = 1; e < eend; ++e)
1167 o <<
"<td port='es" << e <<
"' bgcolor='yellow'>"
1168 << edges_[e].src <<
"</td>\n";
1171 if (dsi & DSI_EdgesFooter)
1172 o <<
"</table>>]\n";
1173 if (!dests_.empty())
1175 unsigned dend = dests_.size();
1176 if (dsi & DSI_DestsHeader)
1178 o << (
"dests [label=<\n"
1179 "<table border='0' cellborder='1' cellspacing='0'>\n"
1180 "<tr><td sides='b' bgcolor='pink' port='d'>dests</td>\n");
1184 o <<
"<td sides='b' bgcolor='pink' port='d"
1185 << d <<
"'>~" << d <<
"</td>\n";
1186 unsigned cnt = dests_[d];
1189 o <<
"<td sides='b'></td>\n";
1193 if (dsi & DSI_DestsBody)
1195 o <<
"<tr><td port='dd'>#cnt/dst</td>\n";
1199 unsigned cnt = dests_[d];
1200 o <<
"<td port='d'>#" << cnt <<
"</td>\n";
1204 o <<
"<td bgcolor='yellow' port='dd"
1205 << d <<
"'>" << dests_[d] <<
"</td>\n";
1211 if (dsi & DSI_DestsFooter)
1212 o <<
"</table>>]\n";
1214 if (dsi & DSI_GraphFooter)
1225 if (killed_edge_ == 0)
1227 auto i = std::remove_if(edges_.begin() + 1, edges_.end(),
1229 return this->is_dead_edge(t);
1231 edges_.erase(i, edges_.end());
1240 template<
class Predicate = std::less<edge_storage_t>>
1245 std::stable_sort(edges_.begin() + 1, edges_.end(), p);
1257 template<
class Predicate = std::less<edge_storage_t>>
1264 auto idx_list = std::vector<unsigned>(N+1);
1265 auto new_edges = edge_vector_t();
1266 new_edges.reserve(edges_.size());
1267 if (SPOT_UNLIKELY(edges_.empty()))
1268 throw std::runtime_error(
"Empty edge vector!");
1269 new_edges.resize(1);
1271 new_edges[0].next_succ = 0;
1273 for (
auto s = 0u; s < N; ++s)
1275 idx_list[s] = new_edges.size();
1276 for (
const auto& e :
out(s))
1277 new_edges.push_back(e);
1279 idx_list[N] = new_edges.size();
1283 auto bne = new_edges.begin();
1284 #ifdef SPOT_ENABLE_PTHREAD
1285 const unsigned nthreads = get_nthreads();
1286 if (nthreads == 1 || edges_.size() < 1000)
1289 for (
auto s = 0u; s < N; ++s)
1290 std::stable_sort(bne + idx_list[s],
1291 bne + idx_list[s+1],
1294 #ifdef SPOT_ENABLE_PTHREAD
1297 static auto tv = std::vector<std::thread>();
1298 SPOT_ASSERT(tv.empty());
1299 tv.resize(nthreads);
1300 for (
unsigned id = 0;
id < nthreads; ++id)
1301 tv[
id] = std::thread(
1302 [bne,
id, N, &idx_list, p, nthreads]()
1304 for (
auto s =
id; s < N; s+=nthreads)
1305 std::stable_sort(bne + idx_list[s],
1306 bne + idx_list[s+1],
1315 std::swap(edges_, new_edges);
1326 template<
bool Stable = false,
class Predicate = std::less<edge_storage_t>>
1328 const std::vector<bool>* to_sort_ptr =
nullptr)
1330 SPOT_ASSERT((to_sort_ptr ==
nullptr)
1334 auto pi = [&](
unsigned t1,
unsigned t2)
1335 {
return p(edges_[t1], edges_[t2]); };
1339 std::vector<unsigned> sort_idx_;
1341 for (
unsigned i = 0; i < ns; ++i)
1343 if (to_sort_ptr && !(*to_sort_ptr)[i])
1345 unsigned t = states_[i].succ;
1351 sort_idx_.push_back(t);
1352 t = edges_[t].next_succ;
1354 if constexpr (Stable)
1355 std::stable_sort(sort_idx_.begin(), sort_idx_.end(), pi);
1357 std::sort(sort_idx_.begin(), sort_idx_.end(), pi);
1359 states_[i].succ = sort_idx_.front();
1360 states_[i].succ_tail = sort_idx_.back();
1361 const unsigned n_outs_n1 = sort_idx_.size() - 1;
1362 for (
unsigned k = 0; k < n_outs_n1; ++k)
1363 edges_[sort_idx_[k]].next_succ = sort_idx_[k+1];
1364 edges_[sort_idx_.back()].next_succ = 0;
1375 state last_src = -1U;
1376 edge tend = edges_.size();
1377 for (edge t = 1; t < tend; ++t)
1379 state src = edges_[t].src;
1380 if (src != last_src)
1382 states_[src].succ = t;
1383 if (last_src != -1U)
1385 states_[last_src].succ_tail = t - 1;
1386 edges_[t - 1].next_succ = 0;
1388 while (++last_src != src)
1390 states_[last_src].succ = 0;
1391 states_[last_src].succ_tail = 0;
1396 edges_[t - 1].next_succ = t;
1399 if (last_src != -1U)
1401 states_[last_src].succ_tail = tend - 1;
1402 edges_[tend - 1].next_succ = 0;
1404 unsigned send = states_.size();
1405 while (++last_src != send)
1407 states_[last_src].succ = 0;
1408 states_[last_src].succ_tail = 0;
1421 SPOT_ASSERT(newst.size() == states_.size());
1422 unsigned tend = edges_.size();
1423 for (
unsigned t = 1; t < tend; t++)
1425 edges_[t].dst = newst[edges_[t].dst];
1426 edges_[t].src = newst[edges_[t].src];
1449 SPOT_ASSERT(newst.size() >= states_.size());
1450 SPOT_ASSERT(used_states > 0);
1456 unsigned send = states_.size();
1457 for (state s = 0; s < send; ++s)
1459 state dst = newst[s];
1467 auto t = states_[s].succ;
1469 std::swap(t, edges_[t].next_succ);
1472 states_[dst] = std::move(states_[s]);
1474 states_.resize(used_states);
1479 unsigned tend = edges_.size();
1480 std::vector<edge> newidx(tend);
1482 for (edge t = 1; t < tend; ++t)
1487 edges_[dest] = std::move(edges_[t]);
1491 edges_.resize(dest);
1495 for (edge t = 1; t < dest; ++t)
1497 auto& tr = edges_[t];
1498 tr.src = newst[tr.src];
1499 tr.dst = newst[tr.dst];
1500 tr.next_succ = newidx[tr.next_succ];
1504 for (
auto& s: states_)
1506 s.succ = newidx[s.succ];
1507 s.succ_tail = newidx[s.succ_tail];
A directed graph.
Definition: graph.hh:590
unsigned num_states() const
The number of states in the automaton.
Definition: graph.hh:649
void dump_storage_as_dot(std::ostream &o, int dsi=DSI_All) const
Dump the state and edge storage for debugging.
Definition: graph.hh:1088
bool is_dead_edge(const edge_storage_t &t) const
Tests whether an edge has been erased.
Definition: graph.hh:1005
void dump_storage(std::ostream &o) const
Dump the state and edge storage for debugging.
Definition: graph.hh:1028
const edge_storage_t::data_t & edge_data(edge s) const
return the Edgeg_Data of an edge.
Definition: graph.hh:763
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:922
internal::state_out< digraph > out(state_storage_t &src)
Return a fake container with all edges leaving src.
Definition: graph.hh:899
const state_vector & states() const
Return the vector of states.
Definition: graph.hh:937
void sort_edges_of_(Predicate p=Predicate(), const std::vector< bool > *to_sort_ptr=nullptr)
Sort edges of the given states.
Definition: graph.hh:1327
state new_states(unsigned n, Args &&... args)
Create n new states.
Definition: graph.hh:688
state new_state(Args &&... args)
Create a new states.
Definition: graph.hh:674
edge index_of_edge(const edge_storage_t &tt) const
Convert a storage reference into an edge number.
Definition: graph.hh:884
internal::state_out< const digraph > out(state_storage_t &src) const
Return a fake container with all edges leaving src.
Definition: graph.hh:911
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:988
edge_storage_t::data_t & edge_data(edge s)
return the Edgeg_Data of an edge.
Definition: graph.hh:757
const dests_vector_t & dests_vector() const
The vector used to store universal destinations.
Definition: graph.hh:1016
dests_vector_t & dests_vector()
The vector used to store universal destinations.
Definition: graph.hh:1021
edge_storage_t & edge_storage(edge s)
return a reference to the storage of an edge
Definition: graph.hh:739
const edge_storage_t & edge_storage(edge s) const
return a reference to the storage of an edge
Definition: graph.hh:745
edge new_univ_edge(state src, const std::initializer_list< state > &dsts, Args &&... args)
Create a new universal edge.
Definition: graph.hh:848
bool is_existential() const
Whether the automaton uses only existential branching.
Definition: graph.hh:663
const state_storage_t & state_storage(state s) const
return a reference to the storage of a state
Definition: graph.hh:709
internal::state_out< digraph > out(state src)
Return a fake container with all edges leaving src.
Definition: graph.hh:893
internal::killer_edge_iterator< digraph > out_iteraser(state src)
Return a fake container with all edges leaving src, allowing erasure.
Definition: graph.hh:928
void remove_dead_edges_()
Remove all dead edges.
Definition: graph.hh:1223
digraph(unsigned max_states=10, unsigned max_trans=0)
Construct an empty graph.
Definition: graph.hh:634
state new_univ_dests(I dst_begin, I dst_end)
Create a new universal destination group.
Definition: graph.hh:800
state_vector & states()
Return the vector of states.
Definition: graph.hh:942
void rename_states_(const std::vector< unsigned > &newst)
Rename all the states in the edge vector.
Definition: graph.hh:1419
void defrag_states(const std::vector< unsigned > &newst, unsigned used_states)
Rename and remove states.
Definition: graph.hh:1447
void sort_edges_srcfirst_(Predicate p=Predicate())
Sort all edges by src first, then, within edges of the same source use the predicate.
Definition: graph.hh:1258
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:703
internal::state_out< const digraph > out(state src) const
Return a fake container with all edges leaving src.
Definition: graph.hh:905
unsigned num_edges() const
The number of edges in the automaton.
Definition: graph.hh:657
state_storage_t::data_t & state_data(state s)
return the State_Data associated to a state
Definition: graph.hh:721
const edge_vector_t & edge_vector() const
Return the vector of all edges.
Definition: graph.hh:971
state index_of_state(const state_storage_t &ss) const
Convert a storage reference into a state number.
Definition: graph.hh:877
void sort_edges_(Predicate p=Predicate())
Sort all edges according to a predicate.
Definition: graph.hh:1241
bool is_dead_edge(unsigned t) const
Tests whether an edge has been erased.
Definition: graph.hh:1000
edge_vector_t & edge_vector()
Return the vector of all edges.
Definition: graph.hh:976
edge new_univ_edge(state src, I dst_begin, I dst_end, Args &&... args)
Create a new universal edge.
Definition: graph.hh:835
void chain_edges_()
Reconstruct the chain of outgoing edges.
Definition: graph.hh:1373
internal::all_trans< digraph > edges()
Return a fake container with all edges (exluding erased edges)
Definition: graph.hh:957
edge new_edge(state src, state dst, Args &&... args)
Create a new edge.
Definition: graph.hh:776
internal::all_trans< const digraph > edges() const
Return a fake container with all edges (exluding erased edges)
Definition: graph.hh:952
const state_storage_t::data_t & state_data(state s) const
return the State_Data associated to a state
Definition: graph.hh:727
Abstract class for states.
Definition: twa.hh:51
Definition: automata.hh:27