Line data Source code
1 : // Author(s): Jan Friso Groote
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 :
10 : /** \file
11 : *
12 : * \brief This file contains some utility functions to manipulate lts's
13 : * \details The function in this file typically allow to present the
14 : * transitions of a state space differently.
15 : * \author Jan Friso Groote
16 : */
17 :
18 : #ifndef MCRL2_LTS_LTS_UTILITIES_H
19 : #define MCRL2_LTS_LTS_UTILITIES_H
20 :
21 : #include "mcrl2/lts/lts_lts.h"
22 :
23 : namespace mcrl2
24 : {
25 :
26 : namespace lts
27 : {
28 :
29 : /** \brief Sorts the transitions using a sort style.
30 : * \param[in/out] transitions A vector of transitions to be sorted.
31 : * \param[in] hidden_label_set A set that tells which actions are to be interpreted as being hidden.
32 : * Sorting takes place after mapping hidden actions to zero.
33 : * \param[in] ts The sort style to use.
34 : */
35 :
36 293 : inline void sort_transitions(std::vector<transition>& transitions,
37 : const std::set<transition::size_type>& hidden_label_set,
38 : transition_sort_style ts = src_lbl_tgt)
39 : {
40 293 : switch (ts)
41 : {
42 132 : case lbl_tgt_src:
43 : {
44 132 : const detail::compare_transitions_lts compare(hidden_label_set);
45 132 : sort(transitions.begin(),transitions.end(),compare);
46 132 : break;
47 : }
48 161 : case src_lbl_tgt:
49 : default:
50 : {
51 161 : const detail::compare_transitions_slt compare(hidden_label_set);
52 161 : sort(transitions.begin(),transitions.end(),compare);
53 161 : break;
54 : }
55 : }
56 293 : }
57 :
58 : /** \brief Sorts the transitions using a sort style.
59 : * \param[in/out] transitions A vector of transitions to be sorted.
60 : * \param[in] ts The sort style to use.
61 : */
62 :
63 1 : inline void sort_transitions(std::vector<transition>& transitions, transition_sort_style ts = src_lbl_tgt)
64 : {
65 1 : sort_transitions(transitions, std::set<transition::size_type>(), ts);
66 1 : }
67 :
68 :
69 : namespace detail
70 : {
71 :
72 : // An indexed sorted vector below contains the outgoing or incoming transitions per state,
73 : // grouped per state. The input consists of a vector of transitions. The incoming/outcoming
74 : // tau transitions are grouped by state in the m_states_with_outgoing_or_incoming_transition.
75 : // It is as long as the lts aut has transitions. The vector m_indices is as long as the number
76 : // of states plus 1. For each state it contains the place in the other vector where its tau transitions
77 : // start. So, the tau transitions reside at position indices[s] to indices[s+1]. These indices
78 : // can be acquired using the functions lowerbound and upperbound.
79 : // This data structure is chosen due to its minimal memory and time footprint.
80 : template <class CONTENT>
81 : class indexed_sorted_vector_for_transitions
82 : {
83 : protected:
84 : typedef std::size_t state_type;
85 : typedef std::size_t label_type;
86 : typedef std::pair<label_type,state_type> label_state_pair;
87 :
88 : std::vector < CONTENT > m_states_with_outgoing_or_incoming_transition;
89 : std::vector <size_t> m_indices;
90 :
91 : public:
92 :
93 200 : indexed_sorted_vector_for_transitions(const std::vector < transition >& transitions , state_type num_states, bool outgoing)
94 200 : : m_indices(num_states+1,0)
95 : {
96 : // First count the number of outgoing transitions per state and put it in indices.
97 2281 : for(const transition& t: transitions)
98 : {
99 2081 : m_indices[outgoing?t.from():t.to()]++;
100 : }
101 :
102 : // Calculate the m_indices where the states with outgoing/incoming tau transition must be placed.
103 : // Put the starting index for state i at position i-1. When placing the transitions these indices
104 : // are decremented properly.
105 :
106 200 : size_t sum=0;
107 1857 : for(state_type& i: m_indices) // The vector is changed. This must be a reference.
108 : {
109 1657 : sum=sum+i;
110 1657 : i=sum;
111 : }
112 :
113 : // Now declare enough space for all transitions and store them in reverse order, while
114 : // at the same time decrementing the indices in m_indices.
115 200 : m_states_with_outgoing_or_incoming_transition.resize(sum);
116 2281 : for(const transition& t: transitions)
117 : {
118 2081 : if (outgoing)
119 : {
120 1424 : assert(t.from()<m_indices.size());
121 1424 : assert(m_indices[t.from()]>0);
122 1424 : m_indices[t.from()]--;
123 1424 : assert(m_indices[t.from()] < m_states_with_outgoing_or_incoming_transition.size());
124 1424 : m_states_with_outgoing_or_incoming_transition[m_indices[t.from()]]=label_state_pair(t.label(), t.to());
125 : }
126 : else
127 : {
128 657 : assert(t.to()<m_indices.size());
129 657 : assert(m_indices[t.to()]>0);
130 657 : m_indices[t.to()]--;
131 657 : assert(m_indices[t.to()] < m_states_with_outgoing_or_incoming_transition.size());
132 657 : m_states_with_outgoing_or_incoming_transition[m_indices[t.to()]]=label_state_pair(t.label(), t.from());
133 : }
134 : }
135 200 : assert(m_indices.at(num_states)==m_states_with_outgoing_or_incoming_transition.size());
136 200 : }
137 :
138 : // Get the indexed transitions.
139 7911 : const std::vector<CONTENT>& get_transitions() const
140 : {
141 7911 : return m_states_with_outgoing_or_incoming_transition;
142 : }
143 :
144 : // Get the lowest index of incoming/outging transitions stored in m_states_with_outgoing_or_incoming_transition.
145 4816 : size_t lowerbound(const state_type s) const
146 : {
147 4816 : assert(s+1<m_indices.size());
148 4816 : return m_indices[s];
149 : }
150 :
151 : // Get 1 beyond the higest index of incoming/outging transitions stored in m_states_with_outgoing_or_incoming_transition.
152 12626 : size_t upperbound(const state_type s) const
153 : {
154 12626 : assert(s+1<m_indices.size());
155 12626 : return m_indices[s+1];
156 : }
157 :
158 : // Drastically clear the vectors by resetting its memory usage to minimal.
159 : void clear()
160 : {
161 : std::vector <state_type>().swap(m_states_with_outgoing_or_incoming_transition);
162 : std::vector <size_t>().swap(m_indices);
163 :
164 : }
165 : };
166 :
167 : } // end namespace detail
168 :
169 : //
170 : /// \brief Type for exploring transitions per state.
171 : typedef std::pair<transition::size_type, transition::size_type> outgoing_pair_t;
172 :
173 : typedef detail::indexed_sorted_vector_for_transitions < outgoing_pair_t > outgoing_transitions_per_state_t;
174 :
175 : /// \brief Label of a pair of a label and target state.
176 7777 : inline std::size_t label(const outgoing_pair_t& p)
177 : {
178 7777 : return p.first;
179 : }
180 :
181 : /// \brief Target state of a label state pair.
182 9122 : inline std::size_t to(const outgoing_pair_t& p)
183 : {
184 9122 : return p.second;
185 : }
186 :
187 : /// \brief Type for exploring transitions per state and action.
188 : // It can be considered to replace this function with an unordered_multimap.
189 : // This may increase memory requirements, but would allow for constant versus logarithmic access times
190 : // of elements.
191 : typedef std::multimap<std::pair<transition::size_type, transition::size_type>, transition::size_type>
192 : outgoing_transitions_per_state_action_t;
193 :
194 : /// \brief From state of an iterator exploring transitions per outgoing state and action.
195 : inline std::size_t from(const outgoing_transitions_per_state_action_t::const_iterator& i)
196 : {
197 : return i->first.first;
198 : }
199 :
200 : /// \brief Label of an iterator exploring transitions per outgoing state and action.
201 : inline std::size_t label(const outgoing_transitions_per_state_action_t::const_iterator& i)
202 : {
203 : return i->first.second;
204 : }
205 :
206 : /// \brief To state of an iterator exploring transitions per outgoing state and action.
207 5556 : inline std::size_t to(const outgoing_transitions_per_state_action_t::const_iterator& i)
208 : {
209 5556 : return i->second;
210 : }
211 :
212 : /// \brief Provide the transitions as a multimap accessible per from state and label.
213 : inline outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair(const std::vector<transition>& trans)
214 : {
215 : outgoing_transitions_per_state_action_t result;
216 : for (const transition& t: trans)
217 : {
218 : result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
219 : std::pair<transition::size_type, transition::size_type>(t.from(), t.label()), t.to()));
220 : }
221 : return result;
222 : }
223 :
224 : /// \brief Provide the transitions as a multimap accessible per from state and label.
225 0 : inline outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair(
226 : const std::vector<transition>& trans,
227 : const std::set<transition::size_type>& hide_label_set)
228 : {
229 0 : outgoing_transitions_per_state_action_t result;
230 0 : for (const transition& t: trans)
231 : {
232 0 : result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
233 0 : std::pair<transition::size_type, transition::size_type>(t.from(), detail::apply_hidden_labels(t.label(),hide_label_set)), t.to()));
234 : }
235 0 : return result;
236 0 : }
237 :
238 : /// \brief Provide the transitions as a multimap accessible per from state and label, ordered backwardly.
239 : inline outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair_reversed(const std::vector<transition>& trans)
240 : {
241 : outgoing_transitions_per_state_action_t result;
242 : for (const transition& t: trans)
243 : {
244 : result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
245 : std::pair<transition::size_type, transition::size_type>(t.to(), t.label()), t.from()));
246 : }
247 : return result;
248 : }
249 :
250 : /// \brief Provide the transitions as a multimap accessible per from state and label, ordered backwardly.
251 54 : inline outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair_reversed(
252 : const std::vector<transition>& trans,
253 : const std::set<transition::size_type>& hide_label_set)
254 : {
255 54 : outgoing_transitions_per_state_action_t result;
256 619 : for (const transition& t: trans)
257 : {
258 565 : result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
259 1130 : std::pair<transition::size_type, transition::size_type>(t.to(), detail::apply_hidden_labels(t.label(),hide_label_set)), t.from()));
260 : }
261 54 : return result;
262 0 : }
263 :
264 : namespace detail
265 : {
266 : // Yields a label with an obscure name referring to divergence.
267 :
268 : template < class LABEL_TYPE >
269 : // LABEL_TYPE make_divergence_label(const std::string& s, const LABEL_TYPE& l)
270 16 : LABEL_TYPE make_divergence_label(const std::string& s)
271 : {
272 16 : return LABEL_TYPE(s);
273 : }
274 :
275 : template <>
276 : inline mcrl2::lts::action_label_lts make_divergence_label<mcrl2::lts::action_label_lts>(const std::string& s)
277 : {
278 : return action_label_lts(lps::multi_action(process::action(process::action_label(core::identifier_string(s),
279 : data::sort_expression_list()),
280 : data::data_expression_list())));
281 : }
282 :
283 : // Make a new divergent_transition_label and replace each self loop with it.
284 : // Return the number of the divergent transition label.
285 : template < class LTS_TYPE >
286 16 : std::size_t mark_explicit_divergence_transitions(LTS_TYPE& l)
287 : {
288 : // Below we create an odd action label, representing divergence.
289 32 : const typename LTS_TYPE::action_label_t lab=make_divergence_label<typename LTS_TYPE::action_label_t>("!@*&divergence&*@!");
290 16 : std::size_t divergent_transition_label=l.add_action(lab);
291 16 : assert(divergent_transition_label+1==l.num_action_labels());
292 107 : for(transition& t: l.get_transitions())
293 : {
294 91 : if (l.is_tau(l.apply_hidden_label_map(t.label())) && t.to()==t.from())
295 : {
296 8 : t = transition(t.to(),divergent_transition_label,t.to());
297 : }
298 : }
299 16 : return divergent_transition_label;
300 16 : }
301 :
302 : // Replace each transition in a state that is an outgoing divergent_transition with a tau_loop in that state.
303 : template < class LTS_TYPE >
304 16 : void unmark_explicit_divergence_transitions(LTS_TYPE& l, const std::size_t divergent_transition_label)
305 : {
306 103 : for(transition& t: l.get_transitions())
307 : {
308 87 : if (t.label()==divergent_transition_label)
309 : {
310 8 : t = transition(t.from(),l.tau_label_index(),t.from());
311 : }
312 : }
313 16 : }
314 :
315 : } // namespace detail
316 :
317 : }
318 : }
319 :
320 : #endif // MCRL2_LTS_LTS_UTILITIES_H
|
