22 #include <unordered_map>
24 #include <spot/graph/graph.hh>
28 template <
typename Graph,
30 typename Name_Hash = std::hash<State_Name>,
31 typename Name_Equal = std::equal_to<State_Name>>
38 typedef typename Graph::state state;
39 typedef typename Graph::edge edge;
40 typedef State_Name name;
42 typedef std::unordered_map<name, state,
43 Name_Hash, Name_Equal> name_to_state_t;
44 name_to_state_t name_to_state;
45 typedef std::vector<name> state_to_name_t;
46 state_to_name_t state_to_name;
63 template <
typename... Args>
64 state new_state(name n, Args&&... args)
66 auto p = name_to_state.emplace(n, 0
U);
69 unsigned s = g_.new_state(std::forward<Args>(args)...);
71 if (state_to_name.size() < s + 1)
72 state_to_name.resize(s + 1);
76 return p.first->second;
86 auto p = name_to_state.emplace(newname, s);
90 auto old = p.first->second;
93 auto& trans = g_.edge_vector();
94 auto& states = g_.states();
95 trans[states[s].succ_tail].next_succ = states[old].succ;
96 states[s].succ_tail = states[old].succ_tail;
98 states[old].succ_tail = 0;
100 unsigned tend = trans.size();
101 for (
unsigned t = 1; t < tend; ++t)
103 if (trans[t].src == old)
105 if (trans[t].dst == old)
112 state get_state(name n)
const
114 return name_to_state.at(n);
117 name get_name(state s)
const
119 return state_to_name.at(s);
122 bool has_state(name n)
const
124 return name_to_state.find(n) != name_to_state.end();
127 const state_to_name_t& names()
const
129 return state_to_name;
132 template <
typename... Args>
134 new_edge(name src, name dst, Args&&... args)
136 return g_.new_edge(get_state(src), get_state(dst),
137 std::forward<Args>(args)...);
140 template <
typename I,
typename... Args>
142 new_univ_edge(name src, I dst_begin, I dst_end, Args&&... args)
144 std::vector<unsigned> d;
145 d.reserve(std::distance(dst_begin, dst_end));
146 while (dst_begin != dst_end)
147 d.emplace_back(get_state(*dst_begin++));
148 return g_.new_univ_edge(get_state(src), d.begin(), d.end(),
149 std::forward<Args>(args)...);
152 template <
typename... Args>
154 new_univ_edge(name src,
155 const std::initializer_list<State_Name>& dsts, Args&&... args)
157 return new_univ_edge(src, dsts.begin(), dsts.end(),
158 std::forward<Args>(args)...);
bool alias_state(state s, name newname)
Give an alternate name to a state.
Definition: ngraph.hh:84
Abstract class for states.
Definition: twa.hh:51
Definition: automata.hh:27