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();
807 dests_.emplace_back(sz);
808 dests_.insert(dests_.end(), dst_begin, dst_end);
818 template <
typename I,
typename... Args>
823 std::forward<Args>(args)...);
831 template <
typename... Args>
837 std::forward<Args>(args)...);
845 const unsigned* d = dests_.data();
848 return { d + 1, d + num + 1 };
856 internal::const_universal_dests univ_dests(
const edge_storage_t& e)
const
858 return univ_dests(e.dst);
864 SPOT_ASSERT(!states_.empty());
865 return &ss - &states_.front();
871 SPOT_ASSERT(!edges_.empty());
872 return &
tt - &edges_.front();
880 return {
this, states_[src].succ};
892 return {
this, states_[src].succ};
909 return {
this, src.succ, src};
977 return (t < edges_.size() &&
978 edges_[t].next_succ != t);
987 return edges_[t].next_succ == t;
1015 unsigned tend = edges_.size();
1016 for (
unsigned t = 1; t < tend; ++t)
1018 o <<
't' << t <<
": (s"
1019 << edges_[t].src <<
", ";
1020 int d = edges_[t].dst;
1025 o <<
") t" << edges_[t].next_succ <<
'\n';
1027 unsigned send = states_.size();
1028 for (
unsigned s = 0; s < send; ++s)
1030 o <<
's' << s <<
": t"
1031 << states_[s].succ <<
" t"
1032 << states_[s].succ_tail <<
'\n';
1034 unsigned dend = dests_.size();
1036 for (
unsigned s = 0; s < dend; ++s)
1038 o <<
'd' << s <<
": ";
1049 o << dests_[s] <<
'\n';
1053 enum dump_storage_items {
1054 DSI_GraphHeader = 1,
1055 DSI_GraphFooter = 2,
1056 DSI_StatesHeader = 4,
1058 DSI_StatesFooter = 16,
1059 DSI_States = DSI_StatesHeader | DSI_StatesBody | DSI_StatesFooter,
1060 DSI_EdgesHeader = 32,
1062 DSI_EdgesFooter = 128,
1063 DSI_Edges = DSI_EdgesHeader | DSI_EdgesBody | DSI_EdgesFooter,
1064 DSI_DestsHeader = 256,
1065 DSI_DestsBody = 512,
1066 DSI_DestsFooter = 1024,
1067 DSI_Dests = DSI_DestsHeader | DSI_DestsBody | DSI_DestsFooter,
1069 DSI_GraphHeader | DSI_States | DSI_Edges | DSI_Dests | DSI_GraphFooter,
1075 if (dsi & DSI_GraphHeader)
1076 o <<
"digraph g { \nnode [shape=plaintext]\n";
1077 unsigned send = states_.size();
1078 if (dsi & DSI_StatesHeader)
1080 o << (
"states [label=<\n"
1081 "<table border='0' cellborder='1' cellspacing='0'>\n"
1082 "<tr><td sides='b' bgcolor='yellow' port='s'>states</td>\n");
1083 for (
unsigned s = 0; s < send; ++s)
1084 o <<
"<td sides='b' bgcolor='yellow' port='s" << s <<
"'>"
1088 if (dsi & DSI_StatesBody)
1090 o <<
"<tr><td port='ss'>succ</td>\n";
1091 for (
unsigned s = 0; s < send; ++s)
1093 o <<
"<td port='ss" << s;
1094 if (states_[s].succ)
1095 o <<
"' bgcolor='cyan";
1096 o <<
"'>" << states_[s].succ <<
"</td>\n";
1098 o <<
"</tr><tr><td port='st'>succ_tail</td>\n";
1099 for (
unsigned s = 0; s < send; ++s)
1101 o <<
"<td port='st" << s;
1102 if (states_[s].succ_tail)
1103 o <<
"' bgcolor='cyan";
1104 o <<
"'>" << states_[s].succ_tail <<
"</td>\n";
1108 if (dsi & DSI_StatesFooter)
1109 o <<
"</table>>]\n";
1110 unsigned eend = edges_.size();
1111 if (dsi & DSI_EdgesHeader)
1113 o << (
"edges [label=<\n"
1114 "<table border='0' cellborder='1' cellspacing='0'>\n"
1115 "<tr><td sides='b' bgcolor='cyan' port='e'>edges</td>\n");
1116 for (
unsigned e = 1; e < eend; ++e)
1118 o <<
"<td sides='b' bgcolor='"
1119 << (e != edges_[e].next_succ ?
"cyan" :
"gray")
1120 <<
"' port='e" << e <<
"'>" << e <<
"</td>\n";
1124 if (dsi & DSI_EdgesBody)
1126 o <<
"<tr><td port='ed'>dst</td>\n";
1127 for (
unsigned e = 1; e < eend; ++e)
1129 o <<
"<td port='ed" << e;
1130 int d = edges_[e].dst;
1132 o <<
"' bgcolor='pink'>~" << ~d;
1134 o <<
"' bgcolor='yellow'>" << d;
1137 o <<
"</tr><tr><td port='en'>next_succ</td>\n";
1138 for (
unsigned e = 1; e < eend; ++e)
1140 o <<
"<td port='en" << e;
1141 if (edges_[e].next_succ)
1143 if (edges_[e].next_succ != e)
1144 o <<
"' bgcolor='cyan";
1146 o <<
"' bgcolor='gray";
1148 o <<
"'>" << edges_[e].next_succ <<
"</td>\n";
1150 o <<
"</tr><tr><td port='es'>src</td>\n";
1151 for (
unsigned e = 1; e < eend; ++e)
1152 o <<
"<td port='es" << e <<
"' bgcolor='yellow'>"
1153 << edges_[e].src <<
"</td>\n";
1156 if (dsi & DSI_EdgesFooter)
1157 o <<
"</table>>]\n";
1158 if (!dests_.empty())
1160 unsigned dend = dests_.size();
1161 if (dsi & DSI_DestsHeader)
1163 o << (
"dests [label=<\n"
1164 "<table border='0' cellborder='1' cellspacing='0'>\n"
1165 "<tr><td sides='b' bgcolor='pink' port='d'>dests</td>\n");
1169 o <<
"<td sides='b' bgcolor='pink' port='d"
1170 << d <<
"'>~" << d <<
"</td>\n";
1171 unsigned cnt = dests_[d];
1174 o <<
"<td sides='b'></td>\n";
1178 if (dsi & DSI_DestsBody)
1180 o <<
"<tr><td port='dd'>#cnt/dst</td>\n";
1184 unsigned cnt = dests_[d];
1185 o <<
"<td port='d'>#" << cnt <<
"</td>\n";
1189 o <<
"<td bgcolor='yellow' port='dd"
1190 << d <<
"'>" << dests_[d] <<
"</td>\n";
1196 if (dsi & DSI_DestsFooter)
1197 o <<
"</table>>]\n";
1199 if (dsi & DSI_GraphFooter)
1210 if (killed_edge_ == 0)
1212 auto i = std::remove_if(edges_.begin() + 1, edges_.end(),
1214 return this->is_dead_edge(t);
1216 edges_.erase(i, edges_.end());
1225 template<
class Predicate = std::less<edge_storage_t>>
1230 std::stable_sort(edges_.begin() + 1, edges_.end(), p);
1242 template<
class Predicate = std::less<edge_storage_t>>
1249 auto idx_list = std::vector<unsigned>(N+1);
1250 auto new_edges = edge_vector_t();
1251 new_edges.reserve(edges_.size());
1252 if (SPOT_UNLIKELY(edges_.empty()))
1253 throw std::runtime_error(
"Empty edge vector!");
1254 new_edges.resize(1);
1256 new_edges[0].next_succ = 0;
1258 for (
auto s = 0u; s < N; ++s)
1260 idx_list[s] = new_edges.size();
1261 for (
const auto& e :
out(s))
1262 new_edges.push_back(e);
1264 idx_list[N] = new_edges.size();
1268 auto bne = new_edges.begin();
1269 #ifdef SPOT_ENABLE_PTHREAD
1270 const unsigned nthreads = get_nthreads();
1271 if (nthreads == 1 || edges_.size() < 1000)
1274 for (
auto s = 0u; s < N; ++s)
1275 std::stable_sort(bne + idx_list[s],
1276 bne + idx_list[s+1],
1279 #ifdef SPOT_ENABLE_PTHREAD
1282 static auto tv = std::vector<std::thread>();
1283 SPOT_ASSERT(tv.empty());
1284 tv.resize(nthreads);
1285 for (
unsigned id = 0;
id < nthreads; ++id)
1286 tv[
id] = std::thread(
1287 [bne,
id, N, &idx_list, p, nthreads]()
1289 for (
auto s =
id; s < N; s+=nthreads)
1290 std::stable_sort(bne + idx_list[s],
1291 bne + idx_list[s+1],
1300 std::swap(edges_, new_edges);
1311 template<
bool Stable = false,
class Predicate = std::less<edge_storage_t>>
1313 const std::vector<bool>* to_sort_ptr =
nullptr)
1315 SPOT_ASSERT((to_sort_ptr ==
nullptr)
1319 auto pi = [&](
unsigned t1,
unsigned t2)
1320 {
return p(edges_[t1], edges_[t2]); };
1324 std::vector<unsigned> sort_idx_;
1326 for (
unsigned i = 0; i < ns; ++i)
1328 if (to_sort_ptr && !(*to_sort_ptr)[i])
1330 unsigned t = states_[i].succ;
1336 sort_idx_.push_back(t);
1337 t = edges_[t].next_succ;
1339 if constexpr (Stable)
1340 std::stable_sort(sort_idx_.begin(), sort_idx_.end(), pi);
1342 std::sort(sort_idx_.begin(), sort_idx_.end(), pi);
1344 states_[i].succ = sort_idx_.front();
1345 states_[i].succ_tail = sort_idx_.back();
1346 const unsigned n_outs_n1 = sort_idx_.size() - 1;
1347 for (
unsigned k = 0; k < n_outs_n1; ++k)
1348 edges_[sort_idx_[k]].next_succ = sort_idx_[k+1];
1349 edges_[sort_idx_.back()].next_succ = 0;
1360 state last_src = -1U;
1361 edge tend = edges_.size();
1362 for (edge t = 1; t < tend; ++t)
1364 state src = edges_[t].src;
1365 if (src != last_src)
1367 states_[src].succ = t;
1368 if (last_src != -1U)
1370 states_[last_src].succ_tail = t - 1;
1371 edges_[t - 1].next_succ = 0;
1373 while (++last_src != src)
1375 states_[last_src].succ = 0;
1376 states_[last_src].succ_tail = 0;
1381 edges_[t - 1].next_succ = t;
1384 if (last_src != -1U)
1386 states_[last_src].succ_tail = tend - 1;
1387 edges_[tend - 1].next_succ = 0;
1389 unsigned send = states_.size();
1390 while (++last_src != send)
1392 states_[last_src].succ = 0;
1393 states_[last_src].succ_tail = 0;
1406 SPOT_ASSERT(newst.size() == states_.size());
1407 unsigned tend = edges_.size();
1408 for (
unsigned t = 1; t < tend; t++)
1410 edges_[t].dst = newst[edges_[t].dst];
1411 edges_[t].src = newst[edges_[t].src];
1434 SPOT_ASSERT(newst.size() >= states_.size());
1435 SPOT_ASSERT(used_states > 0);
1441 unsigned send = states_.size();
1442 for (state s = 0; s < send; ++s)
1444 state dst = newst[s];
1452 auto t = states_[s].succ;
1454 std::swap(t, edges_[t].next_succ);
1457 states_[dst] = std::move(states_[s]);
1459 states_.resize(used_states);
1464 unsigned tend = edges_.size();
1465 std::vector<edge> newidx(tend);
1467 for (edge t = 1; t < tend; ++t)
1472 edges_[dest] = std::move(edges_[t]);
1476 edges_.resize(dest);
1480 for (edge t = 1; t < dest; ++t)
1482 auto& tr = edges_[t];
1483 tr.src = newst[tr.src];
1484 tr.dst = newst[tr.dst];
1485 tr.next_succ = newidx[tr.next_succ];
1489 for (
auto& s: states_)
1491 s.succ = newidx[s.succ];
1492 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:1073
bool is_dead_edge(const edge_storage_t &t) const
Tests whether an edge has been erased.
Definition: graph.hh:990
void dump_storage(std::ostream &o) const
Dump the state and edge storage for debugging.
Definition: graph.hh:1013
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:907
internal::state_out< digraph > out(state_storage_t &src)
Return a fake container with all edges leaving src.
Definition: graph.hh:884
const state_vector & states() const
Return the vector of states.
Definition: graph.hh:922
void sort_edges_of_(Predicate p=Predicate(), const std::vector< bool > *to_sort_ptr=nullptr)
Sort edges of the given states.
Definition: graph.hh:1312
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:869
internal::state_out< const digraph > out(state_storage_t &src) const
Return a fake container with all edges leaving src.
Definition: graph.hh:896
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:973
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:1001
dests_vector_t & dests_vector()
The vector used to store universal destinations.
Definition: graph.hh:1006
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:833
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:878
internal::killer_edge_iterator< digraph > out_iteraser(state src)
Return a fake container with all edges leaving src, allowing erasure.
Definition: graph.hh:913
void remove_dead_edges_()
Remove all dead edges.
Definition: graph.hh:1208
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:927
void rename_states_(const std::vector< unsigned > &newst)
Rename all the states in the edge vector.
Definition: graph.hh:1404
void defrag_states(const std::vector< unsigned > &newst, unsigned used_states)
Rename and remove states.
Definition: graph.hh:1432
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:1243
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:890
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:956
state index_of_state(const state_storage_t &ss) const
Convert a storage reference into a state number.
Definition: graph.hh:862
void sort_edges_(Predicate p=Predicate())
Sort all edges according to a predicate.
Definition: graph.hh:1226
bool is_dead_edge(unsigned t) const
Tests whether an edge has been erased.
Definition: graph.hh:985
edge_vector_t & edge_vector()
Return the vector of all edges.
Definition: graph.hh:961
edge new_univ_edge(state src, I dst_begin, I dst_end, Args &&... args)
Create a new universal edge.
Definition: graph.hh:820
void chain_edges_()
Reconstruct the chain of outgoing edges.
Definition: graph.hh:1358
internal::all_trans< digraph > edges()
Return a fake container with all edges (exluding erased edges)
Definition: graph.hh:942
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:937
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