mCRL2
Loading...
Searching...
No Matches
sigref.h
Go to the documentation of this file.
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//
13
14#ifndef MCRL2_LTS_SIGREF_H
15#define MCRL2_LTS_SIGREF_H
16
18
19namespace mcrl2
20{
21namespace lts
22{
23
25typedef std::set<std::pair<std::size_t, std::size_t> > signature_t;
26
28template < class LTS_T >
30{
31protected:
33 const LTS_T& m_lts;
34
36 std::vector<signature_t> m_sig;
37
38public:
41 signature(const LTS_T& lts_)
42 : m_lts(lts_), m_sig(m_lts.num_states(), signature_t())
43 {}
44
48 virtual void compute_signature(const std::vector<std::size_t>& partition) = 0;
49
54 virtual void quotient_transitions(std::set<transition>& transitions, const std::vector<std::size_t>& partition)
55 {
56 for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
57 {
58 transitions.insert(transition(partition[i->from()], i->label(), partition[i->to()]));
59 }
60 }
61
66 virtual const signature_t& get_signature(std::size_t i) const
67 {
68 return m_sig[i];
69 }
70};
71
73template < class LTS_T >
74class signature_bisim: public signature<LTS_T>
75{
76protected:
77 using signature<LTS_T>::m_lts;
78 using signature<LTS_T>::m_sig;
79
80public:
82 signature_bisim(const LTS_T& lts_)
83 : signature<LTS_T>(lts_)
84 {
85 mCRL2log(log::verbose) << "initialising signature computation for strong bisimulation" << std::endl;
86 }
87
89 virtual void
90 compute_signature(const std::vector<std::size_t>& partition)
91 {
92 // compute signatures
93 m_sig = std::vector<signature_t>(m_lts.num_states(), signature_t());
94 for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
95 {
96 m_sig[i->from()].insert(std::make_pair(m_lts.apply_hidden_label_map(i->label()), partition[i->to()]));
97 }
98 }
99
100};
101
103template < class LTS_T >
105{
106protected:
107 using signature<LTS_T>::m_lts;
108 using signature<LTS_T>::m_sig;
109
112
126 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 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 for (std::size_t i=m_prev_transitions.lowerbound(t); i<m_prev_transitions.upperbound(t); ++i)
136 {
138 if(m_lts.is_tau(m_lts.apply_hidden_label_map(label(p))) && partition[t] == partition[to(p)])
139 {
140 insert(partition, to(p), label_, block);
141 }
142 }
143 }
144 }
145
146public:
148 signature_branching_bisim(const LTS_T& lts_)
149 : signature<LTS_T>(lts_),
150 m_prev_transitions(lts_.get_transitions(),lts_.num_states(),false) // transitions stored backward.
151 {
152 mCRL2log(log::verbose) << "initialising signature computation for branching bisimulation" << std::endl;
153 }
154
156 virtual void compute_signature(const std::vector<std::size_t>& partition)
157 {
158 // compute signatures
159 m_sig = std::vector<signature_t>(m_lts.num_states(), signature_t());
160 for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
161 {
162 if (!(m_lts.is_tau(m_lts.apply_hidden_label_map(i->label())) && (partition[i->from()] == partition[i->to()])))
163 {
164 insert(partition, i->from(), m_lts.apply_hidden_label_map(i->label()), partition[i->to()]);
165 }
166 }
167 }
168
170 virtual void quotient_transitions(std::set<transition>& transitions, const std::vector<std::size_t>& partition)
171 {
172 for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
173 {
174 if(partition[i->from()] != partition[i->to()] || !m_lts.is_tau(m_lts.apply_hidden_label_map(i->label())))
175 {
176 transitions.insert(transition(partition[i->from()], m_lts.apply_hidden_label_map(i->label()), partition[i->to()]));
177 }
178 }
179 }
180};
181
183template < class LTS_T >
185{
186protected:
190
192 std::vector<bool> m_divergent;
193
202 {
203 std::size_t unused = 1, lastscc = 1;
204 std::vector<std::size_t> scc(m_lts.num_states(), 0);
205 std::vector<std::size_t> low(m_lts.num_states(), 0);
206 std::stack<std::size_t> stack;
207 std::stack<std::size_t> sccstack;
208
209 // Record forward transition relation sorted by state.
210 outgoing_transitions_per_state_t m_lts_succ_transitions(m_lts.get_transitions(),m_lts.num_states(),true);
211
212 for (std::size_t i = 0; i < m_lts.num_states(); ++i)
213 {
214 if (scc[i] == 0)
215 stack.push(i);
216 while (!stack.empty())
217 {
218 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 if (low[vi] == 0 && scc[vi] == 0)
225 {
226 scc[vi] = unused;
227 low[vi] = unused++;
228 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 for (std::size_t i=m_lts_succ_transitions.lowerbound(vi); i<m_lts_succ_transitions.upperbound(vi); ++i)
234 {
235 const outgoing_pair_t& t=m_lts_succ_transitions.get_transitions()[i];
236 if ((low[to(t)] == 0) && (scc[to(t)] == 0) && (m_lts.is_tau(m_lts.apply_hidden_label_map(label(t)))))
237 {
238 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 for (std::size_t i=m_lts_succ_transitions.lowerbound(vi); i<m_lts_succ_transitions.upperbound(vi); ++i)
246 {
247 const outgoing_pair_t& t=m_lts_succ_transitions.get_transitions()[i];
248 if ((low[to(t)] != 0) && (m_lts.is_tau(m_lts.apply_hidden_label_map(label(t)))))
249 low[vi] = low[vi] < low[to(t)] ? low[vi] : low[to(t)];
250 }
251 if (low[vi] == scc[vi])
252 {
253 std::size_t tos, scc_id = lastscc++;
254 std::vector<std::size_t> this_scc;
255 do
256 {
257 tos = sccstack.top();
258 low[tos] = 0;
259 scc[tos] = scc_id;
260 sccstack.pop();
261 this_scc.push_back(tos);
262 }
263 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 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 for (std::size_t i_=m_lts_succ_transitions.lowerbound(vi); i_<m_lts_succ_transitions.upperbound(vi); ++i_)
272 {
273 const outgoing_pair_t& i=m_lts_succ_transitions.get_transitions()[i_];
274 if(vi == to(i) && m_lts.is_tau(m_lts.apply_hidden_label_map(label(i))))
275 {
276 m_divergent[tos] = true;
277 break;
278 }
279 }
280 }
281 else
282 {
283 m_divergent[tos] = true;
284 }
285 }
286 stack.pop();
287 }
288 }
289 }
290 }
291
292public:
299 : signature_branching_bisim<LTS_T>(lts_),
300 m_divergent(lts_.num_states(), false)
301 {
302 mCRL2log(log::verbose) << "initialising signature computation for divergence preserving branching bisimulation" << std::endl;
304 }
305
311 virtual void compute_signature(const std::vector<std::size_t>& partition)
312 {
313 // compute signatures
314 m_sig = std::vector<signature_t>(m_lts.num_states(), signature_t());
315 for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
316 {
317 if(!(partition[i->from()] == partition[i->to()] && m_lts.is_tau(m_lts.apply_hidden_label_map(i->label())))
318 || m_divergent[i->to()])
319 {
320 insert(partition, i->from(), m_lts.apply_hidden_label_map(i->label()), partition[i->to()]);
321 }
322 }
323 }
324
326 virtual void quotient_transitions(std::set<transition>& transitions, const std::vector<std::size_t>& partition)
327 {
328 for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
329 {
330 if(!(partition[i->from()] == partition[i->to()] && m_lts.is_tau(m_lts.apply_hidden_label_map(i->label())))
331 || 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 transitions.insert(transition(partition[i->from()], m_lts.apply_hidden_label_map(i->label()), partition[i->to()]));
334 }
335 }
336 }
337};
338
339
348template < class LTS_T, typename Signature >
350{
351
352protected:
355 std::vector<std::size_t> m_partition;
356
358 std::size_t m_count;
359
361 LTS_T& m_lts;
362
365 Signature m_signature;
366
368 std::string print_sig(const signature_t& sig)
369 {
370 std::stringstream os;
371 os << "{ ";
372 for(signature_t::const_iterator i = sig.begin(); i != sig.end() ; ++i)
373 {
374 os << " (" << pp(m_lts.action_label(i->first)) << ", " << i->second << ") ";
375 }
376 os << " }";
377 return os.str();
378 }
379
383 {
384 std::size_t count_prev = m_count;
385 std::size_t iterations = 0;
386
387 sort_transitions(m_lts.get_transitions(), m_lts.hidden_label_set(), mcrl2::lts::lbl_tgt_src);
388
389 do
390 {
391 mCRL2log(log::verbose) << "Iteration " << iterations
392 << " currently have " << m_count << " blocks" << std::endl;
393
394 m_signature.compute_signature(m_partition);
395
396 count_prev = m_count;
397
398 // Map signatures to block numbers
399 std::map<signature_t, std::size_t> hashtable;
400 m_count = 0;
401 for(std::size_t i = 0; i < m_lts.num_states(); ++i)
402 {
403 if(hashtable.find(m_signature.get_signature(i)) == hashtable.end())
404 {
405 mCRL2log(log::debug) << "Adding block for signature " << print_sig(m_signature.get_signature(i)) << std::endl;
406 hashtable[m_signature.get_signature(i)] = m_count++;
407 }
408 }
409
410 // Map states to block numbers
411 for(std::size_t i = 0; i < m_lts.num_states(); ++i)
412 {
413 m_partition[i] = hashtable[m_signature.get_signature(i)];
414 }
415
416 ++iterations;
417
418 } while (count_prev != m_count);
419
420 mCRL2log(log::verbose) << "Done after " << iterations << " iterations with " << m_count << " blocks" << std::endl;
421 }
422
425 void quotient()
426 {
427 // Assign the reduced LTS
428 m_lts.set_num_states(m_count);
429 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 std::set<transition> transitions;
434 m_signature.quotient_transitions(transitions, m_partition);
435
436 // Set quotient transitions
437 m_lts.clear_transitions();
438 for(std::set<transition>::const_iterator i = transitions.begin(); i != transitions.end(); ++i)
439 {
440 m_lts.add_transition(*i);
441 }
442 }
443
444public:
448 sigref(LTS_T& lts_)
449 : m_partition(std::vector<std::size_t>(lts_.num_states(), 0)),
450 m_count(0),
451 m_lts(lts_),
452 m_signature(lts_)
453 {}
454
458 void run()
459 {
460 // No need for state labels in the reduced LTS.
461 m_lts.clear_state_labels();
463 quotient();
464 }
465};
466
467} // namespace lts
468} // namespace mcrl2
469
470#endif // MCRL2_LTS_SIGREF_H
const std::vector< CONTENT > & get_transitions() const
Class for computing the signature for strong bisimulation.
Definition sigref.h:75
virtual void compute_signature(const std::vector< std::size_t > &partition)
Definition sigref.h:90
signature_bisim(const LTS_T &lts_)
Constructor.
Definition sigref.h:82
Class for computing the signature for branching bisimulation.
Definition sigref.h:105
virtual void compute_signature(const std::vector< std::size_t > &partition)
Definition sigref.h:156
outgoing_transitions_per_state_t m_prev_transitions
Store the incoming transitions per state.
Definition sigref.h:111
signature_branching_bisim(const LTS_T &lts_)
Constructor
Definition sigref.h:148
void insert(const std::vector< std::size_t > &partition, const std::size_t t, const std::size_t label_, const std::size_t block)
Insert function.
Definition sigref.h:126
virtual void quotient_transitions(std::set< transition > &transitions, const std::vector< std::size_t > &partition)
Definition sigref.h:170
Class for computing the signature for divergence preserving branching bisimulation.
Definition sigref.h:185
virtual void quotient_transitions(std::set< transition > &transitions, const std::vector< std::size_t > &partition)
Definition sigref.h:326
virtual void compute_signature(const std::vector< std::size_t > &partition)
Definition sigref.h:311
signature_divergence_preserving_branching_bisim(const LTS_T &lts_)
Constructor.
Definition sigref.h:298
void compute_tau_sccs()
Iterative implementation of Tarjan's SCC algorithm.
Definition sigref.h:201
std::vector< bool > m_divergent
Record for each vertex whether it is in a tau-scc.
Definition sigref.h:192
Base class for signature computation.
Definition sigref.h:30
const LTS_T & m_lts
The labelled transition system for which the signature is computed.
Definition sigref.h:33
virtual const signature_t & get_signature(std::size_t i) const
Return the signature for state i.
Definition sigref.h:66
virtual void quotient_transitions(std::set< transition > &transitions, const std::vector< std::size_t > &partition)
Compute the transitions for the quotient according to partition.
Definition sigref.h:54
virtual void compute_signature(const std::vector< std::size_t > &partition)=0
Compute a new signature based on partition.
std::vector< signature_t > m_sig
Signature stored per state.
Definition sigref.h:36
signature(const LTS_T &lts_)
Constructor.
Definition sigref.h:41
Signature based reductions for labelled transition systems.
Definition sigref.h:350
void compute_partition()
Compute the partition. Repeatedly updates the signatures, and the partition, until the partition stab...
Definition sigref.h:382
LTS_T & m_lts
The LTS that we are reducing.
Definition sigref.h:361
void run()
Perform the reduction, modulo the equivalence for which the signature has been passed in as template ...
Definition sigref.h:458
std::vector< std::size_t > m_partition
Current partition; for each state (std::size_t) the block in which it resides is recorded.
Definition sigref.h:355
std::size_t m_count
The number of blocks in the current partition.
Definition sigref.h:358
std::string print_sig(const signature_t &sig)
Print a signature (for debugging purposes)
Definition sigref.h:368
sigref(LTS_T &lts_)
Constructor.
Definition sigref.h:448
Signature m_signature
Instance of a class performing the signature computation for the current equivalence.
Definition sigref.h:365
void quotient()
Perform the quotient with respect to the partition that has been computed.
Definition sigref.h:425
A class containing triples, source label and target representing transitions.
Definition transition.h:43
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
This file contains some utility functions to manipulate lts's.
std::string pp(const abstraction &x)
Definition data.cpp:39
@ verbose
Definition logger.h:35
std::size_t to(const outgoing_pair_t &p)
Target state of a label state pair.
std::set< std::pair< std::size_t, std::size_t > > signature_t
A signature is a pair of an action label and a block.
Definition sigref.h:25
void sort_transitions(std::vector< transition > &transitions, const std::set< transition::size_type > &hidden_label_set, transition_sort_style ts=src_lbl_tgt)
Sorts the transitions using a sort style.
std::size_t label(const outgoing_pair_t &p)
Label of a pair of a label and target state.
std::pair< transition::size_type, transition::size_type > outgoing_pair_t
Type for exploring transitions per state.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.