22 #include <spot/misc/common.hh>
24 #include <type_traits>
35 template <
typename State_Data,
typename Edge_Data>
36 class SPOT_API digraph;
41 template <
typename Of,
typename ...Args>
44 static const bool value =
false;
47 template <
typename Of,
typename Arg1,
typename ...Args>
50 static const bool value =
51 std::is_base_of<Of, typename std::decay<Arg1>::type>::value;
61 template <typename Data, bool boxed = !std::is_class<Data>::value>
68 template <
typename... Args,
69 typename =
typename std::enable_if<
72 noexcept(std::is_nothrow_constructible<Data, Args...>::value)
73 : label{std::forward<Args>(args)...}
81 noexcept(std::is_nothrow_constructible<Data>::value)
90 const Data& data()
const
97 return label < other.label;
104 typedef std::tuple<> data_t;
110 const std::tuple<>& data()
const
117 template <
typename Data>
123 template <
typename... Args,
124 typename =
typename std::enable_if<
127 noexcept(std::is_nothrow_constructible<Data, Args...>::value)
128 : Data{std::forward<Args>(args)...}
136 noexcept(std::is_nothrow_constructible<Data>::value)
145 const Data& data()
const
158 template <
typename Edge,
typename State_Data>
165 template <
typename... Args,
166 typename =
typename std::enable_if<
169 noexcept(std::is_nothrow_constructible<State_Data, Args...>::value)
170 : State_Data{std::forward<Args>(args)...}
182 template <
typename StateIn,
183 typename StateOut,
typename Edge,
typename Edge_Data>
194 noexcept(std::is_nothrow_constructible<Edge_Data>::value)
200 template <
typename... Args>
202 StateIn src, Args&&... args)
203 noexcept(std::is_nothrow_constructible<Edge_Data, Args...>::value
204 && std::is_nothrow_constructible<StateOut, StateOut>::value
205 && std::is_nothrow_constructible<Edge, Edge>::value)
206 : Edge_Data{std::forward<Args>(args)...},
207 dst(dst), next_succ(next_succ), src(src)
223 return this->data() < other.data();
228 return src == other.src &&
230 this->data() == other.data();
242 template <
typename Graph>
246 typedef typename std::conditional<std::is_const<Graph>::value,
247 const typename Graph::edge_storage_t,
248 typename Graph::edge_storage_t>::type
250 typedef value_type& reference;
251 typedef value_type* pointer;
252 typedef std::ptrdiff_t difference_type;
253 typedef std::forward_iterator_tag iterator_category;
255 typedef typename Graph::edge edge;
277 reference operator*()
const
279 return g_->edge_storage(t_);
282 pointer operator->()
const
284 return &g_->edge_storage(t_);
289 t_ = operator*().next_succ;
296 t_ = operator*().next_succ;
300 operator bool()
const
315 template <
typename Graph>
320 typedef typename Graph::state_storage_t state_storage_t;
321 typedef typename Graph::edge edge;
324 :
super(g, t), src_(src), prev_(0)
331 this->t_ = this->operator*().next_succ;
345 edge next = this->operator*().next_succ;
350 this->g_->edge_storage(prev_).next_succ = next;
354 if (src_.succ == this->t_)
357 if (src_.succ_tail == this->t_)
359 src_.succ_tail = prev_;
360 SPOT_ASSERT(next == 0);
364 this->operator*().next_succ = this->t_;
369 ++this->g_->killed_edge_;
373 state_storage_t& src_;
384 template <
typename Graph>
388 typedef typename Graph::edge edge;
418 template <
typename Graph>
422 typedef typename std::conditional<std::is_const<Graph>::value,
423 const typename Graph::edge_storage_t,
424 typename Graph::edge_storage_t>::type
426 typedef value_type& reference;
427 typedef value_type* pointer;
428 typedef std::ptrdiff_t difference_type;
429 typedef std::forward_iterator_tag iterator_category;
432 typedef typename std::conditional<std::is_const<Graph>::value,
433 const typename Graph::edge_vector_t,
434 typename Graph::edge_vector_t>::type
442 unsigned s = tv_.size();
445 while (t_ < s && tv_[t_].next_succ == t_);
456 : t_(tv.size()), tv_(tv)
483 reference operator*()
const
488 pointer operator->()
const
495 template <
typename Graph>
499 typedef typename std::conditional<std::is_const<Graph>::value,
500 const typename Graph::edge_vector_t,
501 typename Graph::edge_vector_t>::type
527 const unsigned* begin_;
528 const unsigned* end_;
532 : begin_(begin), end_(end)
537 : begin_(&tmp_), end_(&tmp_ + 1), tmp_(
state)
541 const unsigned* begin()
const
546 const unsigned* end()
const
555 std::map<std::vector<unsigned>,
unsigned> uniq_;
565 unsigned new_univ_dests(I begin, I end)
567 std::vector<unsigned> tmp(begin, end);
568 std::sort(tmp.begin(), tmp.end());
569 tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
570 auto p = uniq_.emplace(tmp, 0);
572 p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end());
573 return p.first->second;
585 template <
typename State_Data,
typename Edge_Data>
597 typedef State_Data state_data_t;
598 typedef Edge_Data edge_data_t;
602 typedef unsigned state;
603 typedef unsigned edge;
611 typedef std::vector<state_storage_t> state_vector;
612 typedef std::vector<edge_storage_t> edge_vector_t;
616 typedef std::vector<unsigned> dests_vector_t;
619 state_vector states_;
620 edge_vector_t edges_;
621 dests_vector_t dests_;
623 unsigned killed_edge_;
631 digraph(
unsigned max_states = 10,
unsigned max_trans = 0)
634 states_.reserve(max_states);
636 max_trans = max_states * 2;
637 edges_.reserve(max_trans + 1);
642 edges_[0].next_succ = 0;
648 return states_.size();
656 return edges_.size() - killed_edge_ - 1;
662 return dests_.empty();
670 template <
typename... Args>
673 state s = states_.size();
674 states_.emplace_back(std::forward<Args>(args)...);
684 template <
typename... Args>
687 state s = states_.size();
688 states_.reserve(s + n);
690 states_.emplace_back(std::forward<Args>(args)...);
705 const state_storage_t&
717 typename state_storage_t::data_t&
720 return states_[s].data();
723 const typename state_storage_t::data_t&
726 return states_[s].data();
741 const edge_storage_t&
753 typename edge_storage_t::data_t&
756 return edges_[s].data();
759 const typename edge_storage_t::data_t&
762 return edges_[s].data();
771 template <
typename... Args>
775 edge t = edges_.size();
776 edges_.emplace_back(dst, 0, src, std::forward<Args>(args)...);
778 edge st = states_[src].succ_tail;
779 SPOT_ASSERT(st < t || !st);
781 states_[src].succ = t;
783 edges_[st].next_succ = t;
784 states_[src].succ_tail = t;
795 template <
typename I>
799 unsigned sz = std::distance(dst_begin, dst_end);
803 unsigned d = dests_.size();
804 dests_.emplace_back(sz);
805 dests_.insert(dests_.end(), dst_begin, dst_end);
815 template <
typename I,
typename... Args>
820 std::forward<Args>(args)...);
828 template <
typename... Args>
834 std::forward<Args>(args)...);
842 const unsigned* d = dests_.data();
845 return { d + 1, d + num + 1 };
853 internal::const_universal_dests univ_dests(
const edge_storage_t& e)
const
855 return univ_dests(e.dst);
861 SPOT_ASSERT(!states_.empty());
862 return &ss - &states_.front();
868 SPOT_ASSERT(!edges_.empty());
869 return &
tt - &edges_.front();
877 return {
this, states_[src].succ};
889 return {
this, states_[src].succ};
906 return {
this, src.succ, src};
974 return (t < edges_.size() &&
975 edges_[t].next_succ != t);
984 return edges_[t].next_succ == t;
1012 unsigned tend = edges_.size();
1013 for (
unsigned t = 1; t < tend; ++t)
1015 o <<
't' << t <<
": (s"
1016 << edges_[t].src <<
", ";
1017 int d = edges_[t].dst;
1022 o <<
") t" << edges_[t].next_succ <<
'\n';
1024 unsigned send = states_.size();
1025 for (
unsigned s = 0; s < send; ++s)
1027 o <<
's' << s <<
": t"
1028 << states_[s].succ <<
" t"
1029 << states_[s].succ_tail <<
'\n';
1031 unsigned dend = dests_.size();
1033 for (
unsigned s = 0; s < dend; ++s)
1035 o <<
'd' << s <<
": ";
1046 o << dests_[s] <<
'\n';
1050 enum dump_storage_items {
1051 DSI_GraphHeader = 1,
1052 DSI_GraphFooter = 2,
1053 DSI_StatesHeader = 4,
1055 DSI_StatesFooter = 16,
1056 DSI_States = DSI_StatesHeader | DSI_StatesBody | DSI_StatesFooter,
1057 DSI_EdgesHeader = 32,
1059 DSI_EdgesFooter = 128,
1060 DSI_Edges = DSI_EdgesHeader | DSI_EdgesBody | DSI_EdgesFooter,
1061 DSI_DestsHeader = 256,
1062 DSI_DestsBody = 512,
1063 DSI_DestsFooter = 1024,
1064 DSI_Dests = DSI_DestsHeader | DSI_DestsBody | DSI_DestsFooter,
1066 DSI_GraphHeader | DSI_States | DSI_Edges | DSI_Dests | DSI_GraphFooter,
1072 if (dsi & DSI_GraphHeader)
1073 o <<
"digraph g { \nnode [shape=plaintext]\n";
1074 unsigned send = states_.size();
1075 if (dsi & DSI_StatesHeader)
1077 o << (
"states [label=<\n"
1078 "<table border='0' cellborder='1' cellspacing='0'>\n"
1079 "<tr><td sides='b' bgcolor='yellow' port='s'>states</td>\n");
1080 for (
unsigned s = 0; s < send; ++s)
1081 o <<
"<td sides='b' bgcolor='yellow' port='s" << s <<
"'>"
1085 if (dsi & DSI_StatesBody)
1087 o <<
"<tr><td port='ss'>succ</td>\n";
1088 for (
unsigned s = 0; s < send; ++s)
1090 o <<
"<td port='ss" << s;
1091 if (states_[s].succ)
1092 o <<
"' bgcolor='cyan";
1093 o <<
"'>" << states_[s].succ <<
"</td>\n";
1095 o <<
"</tr><tr><td port='st'>succ_tail</td>\n";
1096 for (
unsigned s = 0; s < send; ++s)
1098 o <<
"<td port='st" << s;
1099 if (states_[s].succ_tail)
1100 o <<
"' bgcolor='cyan";
1101 o <<
"'>" << states_[s].succ_tail <<
"</td>\n";
1105 if (dsi & DSI_StatesFooter)
1106 o <<
"</table>>]\n";
1107 unsigned eend = edges_.size();
1108 if (dsi & DSI_EdgesHeader)
1110 o << (
"edges [label=<\n"
1111 "<table border='0' cellborder='1' cellspacing='0'>\n"
1112 "<tr><td sides='b' bgcolor='cyan' port='e'>edges</td>\n");
1113 for (
unsigned e = 1; e < eend; ++e)
1115 o <<
"<td sides='b' bgcolor='"
1116 << (e != edges_[e].next_succ ?
"cyan" :
"gray")
1117 <<
"' port='e" << e <<
"'>" << e <<
"</td>\n";
1121 if (dsi & DSI_EdgesBody)
1123 o <<
"<tr><td port='ed'>dst</td>\n";
1124 for (
unsigned e = 1; e < eend; ++e)
1126 o <<
"<td port='ed" << e;
1127 int d = edges_[e].dst;
1129 o <<
"' bgcolor='pink'>~" << ~d;
1131 o <<
"' bgcolor='yellow'>" << d;
1134 o <<
"</tr><tr><td port='en'>next_succ</td>\n";
1135 for (
unsigned e = 1; e < eend; ++e)
1137 o <<
"<td port='en" << e;
1138 if (edges_[e].next_succ)
1140 if (edges_[e].next_succ != e)
1141 o <<
"' bgcolor='cyan";
1143 o <<
"' bgcolor='gray";
1145 o <<
"'>" << edges_[e].next_succ <<
"</td>\n";
1147 o <<
"</tr><tr><td port='es'>src</td>\n";
1148 for (
unsigned e = 1; e < eend; ++e)
1149 o <<
"<td port='es" << e <<
"' bgcolor='yellow'>"
1150 << edges_[e].src <<
"</td>\n";
1153 if (dsi & DSI_EdgesFooter)
1154 o <<
"</table>>]\n";
1155 if (!dests_.empty())
1157 unsigned dend = dests_.size();
1158 if (dsi & DSI_DestsHeader)
1160 o << (
"dests [label=<\n"
1161 "<table border='0' cellborder='1' cellspacing='0'>\n"
1162 "<tr><td sides='b' bgcolor='pink' port='d'>dests</td>\n");
1166 o <<
"<td sides='b' bgcolor='pink' port='d"
1167 << d <<
"'>~" << d <<
"</td>\n";
1168 unsigned cnt = dests_[d];
1171 o <<
"<td sides='b'></td>\n";
1175 if (dsi & DSI_DestsBody)
1177 o <<
"<tr><td port='dd'>#cnt/dst</td>\n";
1181 unsigned cnt = dests_[d];
1182 o <<
"<td port='d'>#" << cnt <<
"</td>\n";
1186 o <<
"<td bgcolor='yellow' port='dd"
1187 << d <<
"'>" << dests_[d] <<
"</td>\n";
1193 if (dsi & DSI_DestsFooter)
1194 o <<
"</table>>]\n";
1196 if (dsi & DSI_GraphFooter)
1207 if (killed_edge_ == 0)
1209 auto i = std::remove_if(edges_.begin() + 1, edges_.end(),
1211 return this->is_dead_edge(t);
1213 edges_.erase(i, edges_.end());
1222 template<
class Predicate = std::less<edge_storage_t>>
1227 std::stable_sort(edges_.begin() + 1, edges_.end(), p);
1239 template<
class Predicate = std::less<edge_storage_t>>
1246 const unsigned nthreads = get_nthreads();
1248 auto idx_list = std::vector<unsigned>(N+1);
1249 auto new_edges = edge_vector_t();
1250 new_edges.reserve(edges_.size());
1251 if (SPOT_UNLIKELY(edges_.empty()))
1252 throw std::runtime_error(
"Empty edge vector!");
1253 new_edges.resize(1);
1255 new_edges[0].next_succ = 0;
1257 for (
auto s = 0u; s < N; ++s)
1259 idx_list[s] = new_edges.size();
1260 for (
const auto& e :
out(s))
1261 new_edges.push_back(e);
1263 idx_list[N] = new_edges.size();
1267 auto bne = new_edges.begin();
1268 if (nthreads == 1 || edges_.size() < 1000)
1270 for (
auto s = 0u; s < N; ++s)
1271 std::stable_sort(bne + idx_list[s],
1272 bne + idx_list[s+1],
1277 static auto tv = std::vector<std::thread>();
1278 SPOT_ASSERT(tv.empty());
1279 tv.resize(nthreads);
1280 for (
unsigned id = 0;
id < nthreads; ++id)
1281 tv[
id] = std::thread(
1282 [bne,
id, N, &idx_list, p, nthreads]()
1284 for (
auto s =
id; s < N; s+=nthreads)
1285 std::stable_sort(bne + idx_list[s],
1286 bne + idx_list[s+1],
1295 std::swap(edges_, new_edges);
1306 template<
bool Stable = false,
class Predicate = std::less<edge_storage_t>>
1308 const std::vector<bool>* to_sort_ptr =
nullptr)
1310 SPOT_ASSERT((to_sort_ptr ==
nullptr)
1314 auto pi = [&](
unsigned t1,
unsigned t2)
1315 {
return p(edges_[t1], edges_[t2]); };
1319 std::vector<unsigned> sort_idx_;
1321 for (
unsigned i = 0; i < ns; ++i)
1323 if (to_sort_ptr && !(*to_sort_ptr)[i])
1325 unsigned t = states_[i].succ;
1331 sort_idx_.push_back(t);
1332 t = edges_[t].next_succ;
1334 if constexpr (Stable)
1335 std::stable_sort(sort_idx_.begin(), sort_idx_.end(), pi);
1337 std::sort(sort_idx_.begin(), sort_idx_.end(), pi);
1339 states_[i].succ = sort_idx_.front();
1340 states_[i].succ_tail = sort_idx_.back();
1341 const unsigned n_outs_n1 = sort_idx_.size() - 1;
1342 for (
unsigned k = 0; k < n_outs_n1; ++k)
1343 edges_[sort_idx_[k]].next_succ = sort_idx_[k+1];
1344 edges_[sort_idx_.back()].next_succ = 0;
1355 state last_src = -1U;
1356 edge tend = edges_.size();
1357 for (edge t = 1; t < tend; ++t)
1359 state src = edges_[t].src;
1360 if (src != last_src)
1362 states_[src].succ = t;
1363 if (last_src != -1U)
1365 states_[last_src].succ_tail = t - 1;
1366 edges_[t - 1].next_succ = 0;
1368 while (++last_src != src)
1370 states_[last_src].succ = 0;
1371 states_[last_src].succ_tail = 0;
1376 edges_[t - 1].next_succ = t;
1379 if (last_src != -1U)
1381 states_[last_src].succ_tail = tend - 1;
1382 edges_[tend - 1].next_succ = 0;
1384 unsigned send = states_.size();
1385 while (++last_src != send)
1387 states_[last_src].succ = 0;
1388 states_[last_src].succ_tail = 0;
1401 SPOT_ASSERT(newst.size() == states_.size());
1402 unsigned tend = edges_.size();
1403 for (
unsigned t = 1; t < tend; t++)
1405 edges_[t].dst = newst[edges_[t].dst];
1406 edges_[t].src = newst[edges_[t].src];
1429 SPOT_ASSERT(newst.size() >= states_.size());
1430 SPOT_ASSERT(used_states > 0);
1436 unsigned send = states_.size();
1437 for (state s = 0; s < send; ++s)
1439 state dst = newst[s];
1447 auto t = states_[s].succ;
1449 std::swap(t, edges_[t].next_succ);
1452 states_[dst] = std::move(states_[s]);
1454 states_.resize(used_states);
1459 unsigned tend = edges_.size();
1460 std::vector<edge> newidx(tend);
1462 for (edge t = 1; t < tend; ++t)
1467 edges_[dest] = std::move(edges_[t]);
1471 edges_.resize(dest);
1475 for (edge t = 1; t < dest; ++t)
1477 auto& tr = edges_[t];
1478 tr.src = newst[tr.src];
1479 tr.dst = newst[tr.dst];
1480 tr.next_succ = newidx[tr.next_succ];
1484 for (
auto& s: states_)
1486 s.succ = newidx[s.succ];
1487 s.succ_tail = newidx[s.succ_tail];
A directed graph.
Definition: graph.hh:587
unsigned num_states() const
The number of states in the automaton.
Definition: graph.hh:646
void dump_storage_as_dot(std::ostream &o, int dsi=DSI_All) const
Dump the state and edge storage for debugging.
Definition: graph.hh:1070
bool is_dead_edge(const edge_storage_t &t) const
Tests whether an edge has been erased.
Definition: graph.hh:987
void dump_storage(std::ostream &o) const
Dump the state and edge storage for debugging.
Definition: graph.hh:1010
const edge_storage_t::data_t & edge_data(edge s) const
return the Edgeg_Data of an edge.
Definition: graph.hh:760
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:904
internal::state_out< digraph > out(state_storage_t &src)
Return a fake container with all edges leaving src.
Definition: graph.hh:881
const state_vector & states() const
Return the vector of states.
Definition: graph.hh:919
void sort_edges_of_(Predicate p=Predicate(), const std::vector< bool > *to_sort_ptr=nullptr)
Sort edges of the given states.
Definition: graph.hh:1307
state new_states(unsigned n, Args &&... args)
Create n new states.
Definition: graph.hh:685
state new_state(Args &&... args)
Create a new states.
Definition: graph.hh:671
edge index_of_edge(const edge_storage_t &tt) const
Convert a storage reference into an edge number.
Definition: graph.hh:866
internal::state_out< const digraph > out(state_storage_t &src) const
Return a fake container with all edges leaving src.
Definition: graph.hh:893
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:970
edge_storage_t::data_t & edge_data(edge s)
return the Edgeg_Data of an edge.
Definition: graph.hh:754
const dests_vector_t & dests_vector() const
The vector used to store universal destinations.
Definition: graph.hh:998
dests_vector_t & dests_vector()
The vector used to store universal destinations.
Definition: graph.hh:1003
edge_storage_t & edge_storage(edge s)
return a reference to the storage of an edge
Definition: graph.hh:736
const edge_storage_t & edge_storage(edge s) const
return a reference to the storage of an edge
Definition: graph.hh:742
edge new_univ_edge(state src, const std::initializer_list< state > &dsts, Args &&... args)
Create a new universal edge.
Definition: graph.hh:830
bool is_existential() const
Whether the automaton uses only existential branching.
Definition: graph.hh:660
const state_storage_t & state_storage(state s) const
return a reference to the storage of a state
Definition: graph.hh:706
internal::state_out< digraph > out(state src)
Return a fake container with all edges leaving src.
Definition: graph.hh:875
internal::killer_edge_iterator< digraph > out_iteraser(state src)
Return a fake container with all edges leaving src, allowing erasure.
Definition: graph.hh:910
void remove_dead_edges_()
Remove all dead edges.
Definition: graph.hh:1205
digraph(unsigned max_states=10, unsigned max_trans=0)
Construct an empty graph.
Definition: graph.hh:631
state new_univ_dests(I dst_begin, I dst_end)
Create a new universal destination group.
Definition: graph.hh:797
state_vector & states()
Return the vector of states.
Definition: graph.hh:924
void rename_states_(const std::vector< unsigned > &newst)
Rename all the states in the edge vector.
Definition: graph.hh:1399
void defrag_states(const std::vector< unsigned > &newst, unsigned used_states)
Rename and remove states.
Definition: graph.hh:1427
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:1240
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:700
internal::state_out< const digraph > out(state src) const
Return a fake container with all edges leaving src.
Definition: graph.hh:887
unsigned num_edges() const
The number of edges in the automaton.
Definition: graph.hh:654
state_storage_t::data_t & state_data(state s)
return the State_Data associated to a state
Definition: graph.hh:718
const edge_vector_t & edge_vector() const
Return the vector of all edges.
Definition: graph.hh:953
state index_of_state(const state_storage_t &ss) const
Convert a storage reference into a state number.
Definition: graph.hh:859
void sort_edges_(Predicate p=Predicate())
Sort all edges according to a predicate.
Definition: graph.hh:1223
bool is_dead_edge(unsigned t) const
Tests whether an edge has been erased.
Definition: graph.hh:982
edge_vector_t & edge_vector()
Return the vector of all edges.
Definition: graph.hh:958
edge new_univ_edge(state src, I dst_begin, I dst_end, Args &&... args)
Create a new universal edge.
Definition: graph.hh:817
void chain_edges_()
Reconstruct the chain of outgoing edges.
Definition: graph.hh:1353
internal::all_trans< digraph > edges()
Return a fake container with all edges (exluding erased edges)
Definition: graph.hh:939
edge new_edge(state src, state dst, Args &&... args)
Create a new edge.
Definition: graph.hh:773
internal::all_trans< const digraph > edges() const
Return a fake container with all edges (exluding erased edges)
Definition: graph.hh:934
const state_storage_t::data_t & state_data(state s) const
return the State_Data associated to a state
Definition: graph.hh:724
Abstract class for states.
Definition: twa.hh:51
Definition: automata.hh:27