Line data Source code
1 : // Author(s): Jeroen Keiren
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 : /// \file sigref.h
10 : /// \brief Implementation of LTS reductions using the signature refinement
11 : /// approach of S. Blom and S. Orzan.
12 : /// \author Jeroen Keiren
13 :
14 : #ifndef MCRL2_LTS_SIGREF_H
15 : #define MCRL2_LTS_SIGREF_H
16 :
17 : #include "mcrl2/lts/lts_utilities.h"
18 :
19 : namespace mcrl2
20 : {
21 : namespace lts
22 : {
23 :
24 : /** \brief A signature is a pair of an action label and a block */
25 : typedef std::set<std::pair<std::size_t, std::size_t> > signature_t;
26 :
27 : /** \brief Base class for signature computation */
28 : template < class LTS_T >
29 : class signature
30 : {
31 : protected:
32 : /** \brief The labelled transition system for which the signature is computed */
33 : const LTS_T& m_lts;
34 :
35 : /** \brief Signature stored per state */
36 : std::vector<signature_t> m_sig;
37 :
38 : public:
39 : /** \brief Constructor
40 : */
41 57 : signature(const LTS_T& lts_)
42 57 : : m_lts(lts_), m_sig(m_lts.num_states(), signature_t())
43 57 : {}
44 :
45 : /** \brief Compute a new signature based on \a partition.
46 : * \param[in] partition The current partition
47 : */
48 : virtual void compute_signature(const std::vector<std::size_t>& partition) = 0;
49 :
50 : /** \brief Compute the transitions for the quotient according to \a partition.
51 : * \param[in] partition The partition that is used to compute the quotient
52 : * \param[out] transitions A set to which the transitions of the quotient are written
53 : */
54 21 : virtual void quotient_transitions(std::set<transition>& transitions, const std::vector<std::size_t>& partition)
55 : {
56 254 : for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
57 : {
58 233 : transitions.insert(transition(partition[i->from()], i->label(), partition[i->to()]));
59 : }
60 21 : }
61 :
62 : /** \brief Return the signature for state \a i.
63 : * \param[in] i The state for which to return the signature.
64 : * \pre i < m_lts.num_states().
65 : */
66 5838 : virtual const signature_t& get_signature(std::size_t i) const
67 : {
68 5838 : return m_sig[i];
69 : }
70 : };
71 :
72 : /** \brief Class for computing the signature for strong bisimulation */
73 : template < class LTS_T >
74 : class signature_bisim: public signature<LTS_T>
75 : {
76 : protected:
77 : using signature<LTS_T>::m_lts;
78 : using signature<LTS_T>::m_sig;
79 :
80 : public:
81 : /** \brief Constructor */
82 21 : signature_bisim(const LTS_T& lts_)
83 21 : : signature<LTS_T>(lts_)
84 : {
85 21 : mCRL2log(log::verbose) << "initialising signature computation for strong bisimulation" << std::endl;
86 21 : }
87 :
88 : /** \overload */
89 : virtual void
90 62 : compute_signature(const std::vector<std::size_t>& partition)
91 : {
92 : // compute signatures
93 62 : m_sig = std::vector<signature_t>(m_lts.num_states(), signature_t());
94 1364 : for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
95 : {
96 1302 : m_sig[i->from()].insert(std::make_pair(m_lts.apply_hidden_label_map(i->label()), partition[i->to()]));
97 : }
98 62 : }
99 :
100 : };
101 :
102 : /** \brief Class for computing the signature for branching bisimulation */
103 : template < class LTS_T >
104 : class signature_branching_bisim: public signature<LTS_T>
105 : {
106 : protected:
107 : using signature<LTS_T>::m_lts;
108 : using signature<LTS_T>::m_sig;
109 :
110 : /** \brief Store the incoming transitions per state */
111 : outgoing_transitions_per_state_t m_prev_transitions;
112 :
113 : /** \brief Insert function
114 : * \param[in] partition The current partition
115 : * \param[in] t source state
116 : * \param[in] label_ transition label
117 : * \param[in] block target block
118 : *
119 : * Insert function as described in S. Blom, S. Orzan,
120 : * "Distributed Branching Bisimulation Reduction of State Spaces",
121 : * Proc. PDMC 2003.
122 : *
123 : * Inserts the pair (label_, block) in the signature of t, as well as
124 : * the signatures of all tau-predecessors of t within the same block.
125 : */
126 3497 : void insert(const std::vector<std::size_t>& partition, const std::size_t t, const std::size_t label_, const std::size_t block)
127 : {
128 3497 : if(m_sig[t].insert(std::make_pair(label_, block)).second)
129 : {
130 : // std::pair<outgoing_transitions_per_state_t::const_iterator, outgoing_transitions_per_state_t::const_iterator> pred_range
131 : // = m_prev_transitions.equal_range(t);
132 :
133 : // for(outgoing_transitions_per_state_t::const_iterator i = pred_range.first; i != pred_range.second; ++i)
134 : // for(const outgoing_pair_t& p: m_prev_transitions[t])
135 6881 : for (std::size_t i=m_prev_transitions.lowerbound(t); i<m_prev_transitions.upperbound(t); ++i)
136 : {
137 4180 : const outgoing_pair_t& p = m_prev_transitions.get_transitions()[i];
138 4180 : if(m_lts.is_tau(m_lts.apply_hidden_label_map(label(p))) && partition[t] == partition[to(p)])
139 : {
140 2297 : insert(partition, to(p), label_, block);
141 : }
142 : }
143 : }
144 3497 : }
145 :
146 : public:
147 : /** \brief Constructor */
148 36 : signature_branching_bisim(const LTS_T& lts_)
149 : : signature<LTS_T>(lts_),
150 36 : m_prev_transitions(lts_.get_transitions(),lts_.num_states(),false) // transitions stored backward.
151 : {
152 36 : mCRL2log(log::verbose) << "initialising signature computation for branching bisimulation" << std::endl;
153 36 : }
154 :
155 : /** \overload */
156 50 : virtual void compute_signature(const std::vector<std::size_t>& partition)
157 : {
158 : // compute signatures
159 50 : m_sig = std::vector<signature_t>(m_lts.num_states(), signature_t());
160 947 : for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
161 : {
162 897 : if (!(m_lts.is_tau(m_lts.apply_hidden_label_map(i->label())) && (partition[i->from()] == partition[i->to()])))
163 : {
164 543 : insert(partition, i->from(), m_lts.apply_hidden_label_map(i->label()), partition[i->to()]);
165 : }
166 : }
167 50 : }
168 :
169 : /** \overload */
170 21 : virtual void quotient_transitions(std::set<transition>& transitions, const std::vector<std::size_t>& partition)
171 : {
172 312 : for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
173 : {
174 291 : if(partition[i->from()] != partition[i->to()] || !m_lts.is_tau(m_lts.apply_hidden_label_map(i->label())))
175 : {
176 171 : transitions.insert(transition(partition[i->from()], m_lts.apply_hidden_label_map(i->label()), partition[i->to()]));
177 : }
178 : }
179 21 : }
180 : };
181 :
182 : /** \brief Class for computing the signature for divergence preserving branching bisimulation */
183 : template < class LTS_T >
184 : class signature_divergence_preserving_branching_bisim: public signature_branching_bisim<LTS_T>
185 : {
186 : protected:
187 : using signature_branching_bisim<LTS_T>::m_lts;
188 : using signature_branching_bisim<LTS_T>::m_sig;
189 : using signature_branching_bisim<LTS_T>::insert;
190 :
191 : /** \brief Record for each vertex whether it is in a tau-scc */
192 : std::vector<bool> m_divergent;
193 :
194 : /** \brief Iterative implementation of Tarjan's SCC algorithm.
195 : *
196 : * based on an earlier implementation by Sjoerd Cranen
197 : *
198 : * For the non-trivial tau-sccs (i.e. SCCs with more than one state, or
199 : * single-state SCCs with a tau-loop, we set \a m_divergent to true.
200 : */
201 15 : void compute_tau_sccs()
202 : {
203 15 : std::size_t unused = 1, lastscc = 1;
204 15 : std::vector<std::size_t> scc(m_lts.num_states(), 0);
205 15 : std::vector<std::size_t> low(m_lts.num_states(), 0);
206 15 : std::stack<std::size_t> stack;
207 15 : std::stack<std::size_t> sccstack;
208 :
209 : // Record forward transition relation sorted by state.
210 15 : outgoing_transitions_per_state_t m_lts_succ_transitions(m_lts.get_transitions(),m_lts.num_states(),true);
211 :
212 273 : for (std::size_t i = 0; i < m_lts.num_states(); ++i)
213 : {
214 258 : if (scc[i] == 0)
215 81 : stack.push(i);
216 778 : while (!stack.empty())
217 : {
218 520 : const std::size_t vi = stack.top();
219 :
220 : // Outgoing transitions of vi.
221 : // std::pair<outgoing_transitions_per_state_t::const_iterator, outgoing_transitions_per_state_t::const_iterator> succ_range
222 : // = m_lts_succ_transitions.equal_range(vi);
223 :
224 520 : if (low[vi] == 0 && scc[vi] == 0)
225 : {
226 258 : scc[vi] = unused;
227 258 : low[vi] = unused++;
228 258 : sccstack.push(vi);
229 :
230 : // for (outgoing_transitions_per_state_t::const_iterator t = succ_range.first; t != succ_range.second; ++t)
231 : // for (const outgoing_pair_t& t: m_lts_succ_transitions[vi])
232 : // for (const outgoing_pair_t& t: m_lts_succ_transitions[vi])
233 624 : for (std::size_t i=m_lts_succ_transitions.lowerbound(vi); i<m_lts_succ_transitions.upperbound(vi); ++i)
234 : {
235 366 : const outgoing_pair_t& t=m_lts_succ_transitions.get_transitions()[i];
236 366 : if ((low[to(t)] == 0) && (scc[to(t)] == 0) && (m_lts.is_tau(m_lts.apply_hidden_label_map(label(t)))))
237 : {
238 181 : stack.push(to(t));
239 : }
240 : }
241 : }
242 : else
243 : {
244 : // for (outgoing_transitions_per_state_t::const_iterator t = succ_range.first; t != succ_range.second; ++t)
245 629 : for (std::size_t i=m_lts_succ_transitions.lowerbound(vi); i<m_lts_succ_transitions.upperbound(vi); ++i)
246 : {
247 367 : const outgoing_pair_t& t=m_lts_succ_transitions.get_transitions()[i];
248 367 : if ((low[to(t)] != 0) && (m_lts.is_tau(m_lts.apply_hidden_label_map(label(t)))))
249 105 : low[vi] = low[vi] < low[to(t)] ? low[vi] : low[to(t)];
250 : }
251 262 : if (low[vi] == scc[vi])
252 : {
253 183 : std::size_t tos, scc_id = lastscc++;
254 183 : std::vector<std::size_t> this_scc;
255 : do
256 : {
257 258 : tos = sccstack.top();
258 258 : low[tos] = 0;
259 258 : scc[tos] = scc_id;
260 258 : sccstack.pop();
261 258 : this_scc.push_back(tos);
262 : }
263 258 : while (tos != vi);
264 :
265 : // We only consider non-trivial sccs, hence
266 : // if the scc consists of a single schate, check whether it has a tau-loop
267 183 : if(this_scc.size() == 1)
268 : {
269 : // for(outgoing_transitions_per_state_t::const_iterator i = succ_range.first; i != succ_range.second; ++i)
270 : // for (const outgoing_pair_t& i: m_lts_succ_transitions[vi])
271 390 : for (std::size_t i_=m_lts_succ_transitions.lowerbound(vi); i_<m_lts_succ_transitions.upperbound(vi); ++i_)
272 : {
273 223 : const outgoing_pair_t& i=m_lts_succ_transitions.get_transitions()[i_];
274 223 : if(vi == to(i) && m_lts.is_tau(m_lts.apply_hidden_label_map(label(i))))
275 : {
276 4 : m_divergent[tos] = true;
277 4 : break;
278 : }
279 : }
280 : }
281 : else
282 : {
283 12 : m_divergent[tos] = true;
284 : }
285 183 : }
286 262 : stack.pop();
287 : }
288 : }
289 : }
290 15 : }
291 :
292 : public:
293 : /** \brief Constructor
294 : *
295 : * This initialises \a m_divergent to record for each vertex whether it is
296 : * in a tau-scc.
297 : */
298 15 : signature_divergence_preserving_branching_bisim(const LTS_T& lts_)
299 : : signature_branching_bisim<LTS_T>(lts_),
300 15 : m_divergent(lts_.num_states(), false)
301 : {
302 15 : mCRL2log(log::verbose) << "initialising signature computation for divergence preserving branching bisimulation" << std::endl;
303 15 : compute_tau_sccs();
304 15 : }
305 :
306 : /** \overload
307 : *
308 : * Compute the signature as in branching bisimulation. In addition, add the
309 : * (tau, B) for edges s -tau-> t for which s,t in B and m_divergent[t]
310 : */
311 38 : virtual void compute_signature(const std::vector<std::size_t>& partition)
312 : {
313 : // compute signatures
314 38 : m_sig = std::vector<signature_t>(m_lts.num_states(), signature_t());
315 1345 : for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
316 : {
317 2102 : if(!(partition[i->from()] == partition[i->to()] && m_lts.is_tau(m_lts.apply_hidden_label_map(i->label())))
318 2102 : || m_divergent[i->to()])
319 : {
320 657 : insert(partition, i->from(), m_lts.apply_hidden_label_map(i->label()), partition[i->to()]);
321 : }
322 : }
323 38 : }
324 :
325 : /** \overload */
326 15 : virtual void quotient_transitions(std::set<transition>& transitions, const std::vector<std::size_t>& partition)
327 : {
328 381 : for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
329 : {
330 555 : if(!(partition[i->from()] == partition[i->to()] && m_lts.is_tau(m_lts.apply_hidden_label_map(i->label())))
331 555 : || m_sig[i->from()].find(std::make_pair(m_lts.apply_hidden_label_map(i->label()), partition[i->to()])) != m_sig[i->from()].end())
332 : {
333 309 : transitions.insert(transition(partition[i->from()], m_lts.apply_hidden_label_map(i->label()), partition[i->to()]));
334 : }
335 : }
336 15 : }
337 : };
338 :
339 :
340 : /** \brief Signature based reductions for labelled transition systems.
341 : *
342 : * The implementation is based on the description in
343 : * S. Blom, S. Orzan. "Distributed Branching Bisimulation Reduction of State
344 : * Spaces", in Proc. PDMC 2003.
345 : *
346 : * The specific signature is a parameter of the algorithm.
347 : */
348 : template < class LTS_T, typename Signature >
349 : class sigref
350 : {
351 :
352 : protected:
353 : /** \brief Current partition; for each state (std::size_t) the block in which
354 : it resides is recorded. */
355 : std::vector<std::size_t> m_partition;
356 :
357 : /** \brief The number of blocks in the current partition */
358 : std::size_t m_count;
359 :
360 : /** \brief The LTS that we are reducing */
361 : LTS_T& m_lts;
362 :
363 : /** \brief Instance of a class performing the signature computation for the
364 : current equivalence */
365 : Signature m_signature;
366 :
367 : /** \brief Print a signature (for debugging purposes) */
368 0 : std::string print_sig(const signature_t& sig)
369 : {
370 0 : std::stringstream os;
371 0 : os << "{ ";
372 0 : for(signature_t::const_iterator i = sig.begin(); i != sig.end() ; ++i)
373 : {
374 0 : os << " (" << pp(m_lts.action_label(i->first)) << ", " << i->second << ") ";
375 : }
376 0 : os << " }";
377 0 : return os.str();
378 0 : }
379 :
380 : /** \brief Compute the partition. Repeatedly updates the signatures, and
381 : the partition, until the partition stabilises */
382 57 : void compute_partition()
383 : {
384 57 : std::size_t count_prev = m_count;
385 57 : std::size_t iterations = 0;
386 :
387 57 : sort_transitions(m_lts.get_transitions(), m_lts.hidden_label_set(), mcrl2::lts::lbl_tgt_src);
388 :
389 : do
390 : {
391 150 : mCRL2log(log::verbose) << "Iteration " << iterations
392 0 : << " currently have " << m_count << " blocks" << std::endl;
393 :
394 150 : m_signature.compute_signature(m_partition);
395 :
396 150 : count_prev = m_count;
397 :
398 : // Map signatures to block numbers
399 150 : std::map<signature_t, std::size_t> hashtable;
400 150 : m_count = 0;
401 2629 : for(std::size_t i = 0; i < m_lts.num_states(); ++i)
402 : {
403 2479 : if(hashtable.find(m_signature.get_signature(i)) == hashtable.end())
404 : {
405 880 : mCRL2log(log::debug) << "Adding block for signature " << print_sig(m_signature.get_signature(i)) << std::endl;
406 880 : hashtable[m_signature.get_signature(i)] = m_count++;
407 : }
408 : }
409 :
410 : // Map states to block numbers
411 2629 : for(std::size_t i = 0; i < m_lts.num_states(); ++i)
412 : {
413 2479 : m_partition[i] = hashtable[m_signature.get_signature(i)];
414 : }
415 :
416 150 : ++iterations;
417 :
418 150 : } while (count_prev != m_count);
419 :
420 57 : mCRL2log(log::verbose) << "Done after " << iterations << " iterations with " << m_count << " blocks" << std::endl;
421 57 : }
422 :
423 : /** \brief Perform the quotient with respect to the partition that has
424 : been computed */
425 57 : void quotient()
426 : {
427 : // Assign the reduced LTS
428 57 : m_lts.set_num_states(m_count);
429 57 : m_lts.set_initial_state(m_partition[m_lts.initial_state()]);
430 :
431 : // Compute quotient transitions
432 : // implemented in the signature class because it differs per equivalence.
433 57 : std::set<transition> transitions;
434 57 : m_signature.quotient_transitions(transitions, m_partition);
435 :
436 : // Set quotient transitions
437 57 : m_lts.clear_transitions();
438 473 : for(std::set<transition>::const_iterator i = transitions.begin(); i != transitions.end(); ++i)
439 : {
440 416 : m_lts.add_transition(*i);
441 : }
442 57 : }
443 :
444 : public:
445 : /** \brief Constructor
446 : * \param[in] lts_ The LTS that is being reduced
447 : */
448 57 : sigref(LTS_T& lts_)
449 57 : : m_partition(std::vector<std::size_t>(lts_.num_states(), 0)),
450 57 : m_count(0),
451 57 : m_lts(lts_),
452 57 : m_signature(lts_)
453 57 : {}
454 :
455 : /** \brief Perform the reduction, modulo the equivalence for which the
456 : * signature has been passed in as template parameter
457 : */
458 57 : void run()
459 : {
460 : // No need for state labels in the reduced LTS.
461 57 : m_lts.clear_state_labels();
462 57 : compute_partition();
463 57 : quotient();
464 57 : }
465 : };
466 :
467 : } // namespace lts
468 : } // namespace mcrl2
469 :
470 : #endif // MCRL2_LTS_SIGREF_H
|
