mCRL2
Loading...
Searching...
No Matches
liblts_scc.h
Go to the documentation of this file.
1// Author(s): Muck van Weerdenburg, 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//
10
11#ifndef _LIBLTS_SCC_H
12#define _LIBLTS_SCC_H
13#include <unordered_set>
14#include "mcrl2/lts/lts.h"
16
17namespace mcrl2
18{
19namespace lts
20{
21
22namespace detail
23{
24 // An indexed sorted vector below contains the outgoing or incoming tau transitions per state,
25 // grouped per state. The input consists of an automaton with transitions. The incoming/outcoming
26 // tau transitions are grouped by state in the m_states_with_outgoing_or_incoming_tau_transition.
27 // It is as long as the lts aut has tau transitions. The vector m_indices is as long as the number
28 // of states. For each state it contains the place in the other vector where its tau transitions
29 // start. So, the tau transitions reside at position indices[s] to indices[s+1]. These indices
30 // can be acquired using the functions lowerbound and upperbound.
31 // This data structure is chosen due to its minimal memory and time footprint.
32 template <class LTS_TYPE>
34 {
35 protected:
36 typedef std::size_t state_type;
37 typedef std::size_t label_type;
38
40 std::vector <size_t> m_indices;
41
42 public:
43
44 indexed_sorted_vector_for_tau_transitions(const LTS_TYPE& aut, bool outgoing)
45 : m_indices(aut.num_states()+1,0)
46 {
47 // First count the number of outgoing transitions per state and put it in indices.
48 for(const transition& t: aut.get_transitions())
49 {
50 if (aut.is_tau(aut.apply_hidden_label_map(t.label())))
51 {
52 m_indices[outgoing?t.from():t.to()]++;
53 }
54 }
55
56 // Calculate the m_indices where the states with outgoing/incoming tau transition must be placed.
57 // Put the starting index for state i at position i-1. When placing the transitions these indices
58 // are decremented properly.
59
60 size_t sum=0;
61 for(state_type& i: m_indices) // The vector is changed. This must be a reference.
62 {
63 sum=sum+i;
64 i=sum;
65 }
66
67 // Now declare enough space for all transitions and store them in reverse order, while
68 // at the same time decrementing the indices in m_indices.
70 for(const transition& t: aut.get_transitions())
71 {
72 if (aut.is_tau(aut.apply_hidden_label_map(t.label())))
73 {
74 if (outgoing)
75 {
76 assert(t.from()<m_indices.size());
77 assert(m_indices[t.from()]>0);
78 m_indices[t.from()]--;
81 }
82 else
83 {
84 assert(t.to()<m_indices.size());
85 assert(m_indices[t.to()]>0);
86 m_indices[t.to()]--;
89 }
90 }
91 }
92 assert(m_indices.at(aut.num_states())==m_states_with_outgoing_or_incoming_tau_transition.size());
93 }
94
95 // Get the indexed transitions.
96 const std::vector<state_type>& get_transitions() const
97 {
99 }
100
101 // Get the lowest index of incoming/outging transitions stored in m_states_with_outgoing_or_incoming_tau_transition.
102 size_t lowerbound(const state_type s) const
103 {
104 assert(s+1<m_indices.size());
105 return m_indices[s];
106 }
107
108 // Get 1 beyond the higest index of incoming/outging transitions stored in m_states_with_outgoing_or_incoming_tau_transition.
109 size_t upperbound(const state_type s) const
110 {
111 assert(s+1<m_indices.size());
112 return m_indices[s+1];
113 }
114
115 // Drastically clear the vectors by resetting its memory usage to minimal.
116 void clear()
117 {
118 std::vector <state_type>().swap(m_states_with_outgoing_or_incoming_tau_transition);
119 std::vector <size_t>().swap(m_indices);
120
121 }
122 };
123
125
126template < class LTS_TYPE>
128{
129
130 public:
144 scc_partitioner(LTS_TYPE& l);
145
148
163 void replace_transition_system(const bool preserve_divergence_loops);
164
168 std::size_t num_eq_classes() const;
169
176 std::size_t get_eq_class(const std::size_t s) const;
177
185 bool in_same_class(const std::size_t s, const std::size_t t) const;
186
187 private:
188
189 typedef std::size_t state_type;
190 typedef std::size_t label_type;
191
192 LTS_TYPE& aut;
193
194 std::vector < state_type > block_index_of_a_state;
195 std::vector < state_type > dfsn2state;
197
198 void group_components(const state_type t,
201 std::vector < bool >& visited);
202 void dfs_numbering(const state_type t,
204 std::vector < bool >& visited);
205
206};
207
208
209template < class LTS_TYPE>
211 :aut(l),
212 block_index_of_a_state(aut.num_states(),0),
213 equivalence_class_index(0)
214{
215 mCRL2log(log::debug) << "Tau loop (SCC) partitioner created for " << l.num_states() << " states and " <<
216 l.num_transitions() << " transitions" << std::endl;
217
218 dfsn2state.reserve(aut.num_states());
219
220 // Initialise the data structures used in the recursive DFS procedure.
221 std::vector<bool> visited(aut.num_states(),false);
222 indexed_sorted_vector_for_tau_transitions<LTS_TYPE> src_tgt(aut,true); // Group the tau transitions ordered per outgoing states.
223
224 // Number the states via a depth first search
225 for (state_type i=0; i<aut.num_states(); ++i)
226 {
227 dfs_numbering(i,src_tgt,visited);
228 }
229 src_tgt.clear();
230
232 for (std::vector < state_type >::reverse_iterator i=dfsn2state.rbegin();
233 i!=dfsn2state.rend(); ++i)
234 {
235 if (visited[*i]) // Visited is used inversely here.
236 {
237 group_components(*i,equivalence_class_index,tgt_src,visited);
239 }
240 }
241 mCRL2log(log::debug) << "Tau loop (SCC) partitioner reduces lts to " << equivalence_class_index << " states." << std::endl;
242
243 dfsn2state.clear();
244}
245
246
247template < class LTS_TYPE>
248void scc_partitioner<LTS_TYPE>::replace_transition_system(const bool preserve_divergence_loops)
249{
250 // Put all the non inert transitions in a set. Add the transitions that form a self
251 // loop. Such transitions only exist in case divergence preserving branching bisimulation is
252 // used. A set is used to remove double occurrences of transitions.
253 std::unordered_set < transition > resulting_transitions;
254 for (const transition& t: aut.get_transitions())
255 {
256 if (!aut.is_tau(aut.apply_hidden_label_map(t.label())) ||
257 preserve_divergence_loops ||
258 block_index_of_a_state[t.from()]!=block_index_of_a_state[t.to()])
259 {
260 resulting_transitions.insert(
262 block_index_of_a_state[t.from()],
263 aut.apply_hidden_label_map(t.label()),
264 block_index_of_a_state[t.to()]));
265 }
266 }
267
268 aut.clear_transitions(resulting_transitions.size());
269 // Copy the transitions from the set into the transition system.
270
271 for (const transition& t: resulting_transitions)
272 {
273 aut.add_transition(transition(t.from(),t.label(),t.to()));
274 }
275
276 // Merge the states, by setting the state labels of each state to the concatenation of the state labels of its
277 // equivalence class.
278 if (aut.has_state_info()) /* If there are no state labels this step can be ignored */
279 {
280 /* Create a vector for the new labels */
281 std::vector<typename LTS_TYPE::state_label_t> new_labels(num_eq_classes());
282
283 for(std::size_t i=aut.num_states(); i>0; )
284 {
285 --i;
286 const std::size_t new_index=block_index_of_a_state[i];
287 new_labels[new_index]=new_labels[new_index]+aut.state_label(i);
288 }
289
290 for(std::size_t i=0; i<num_eq_classes(); ++i)
291 {
292 aut.set_state_label(i,new_labels[i]);
293 }
294 }
295
296 aut.set_num_states(num_eq_classes());
297 aut.set_initial_state(get_eq_class(aut.initial_state()));
298}
299
300template < class LTS_TYPE>
302{
303 return equivalence_class_index;
304}
305
306template < class LTS_TYPE>
307std::size_t scc_partitioner<LTS_TYPE>::get_eq_class(const std::size_t s) const
308{
309 return block_index_of_a_state[s];
310}
311
312template < class LTS_TYPE>
313bool scc_partitioner<LTS_TYPE>::in_same_class(const std::size_t s, const std::size_t t) const
314{
315 return get_eq_class(s)==get_eq_class(t);
316}
317
318// Private methods of scc_partitioner
319
320template < class LTS_TYPE>
322 const state_type s,
323 const state_type equivalence_class_index,
325 std::vector < bool >& visited)
326{
327 if (!visited[s])
328 {
329 return;
330 }
331 visited[s] = false;
332 const size_t u=tgt_src.upperbound(s); // only calculate the upperbound once.
333 for(state_type i=tgt_src.lowerbound(s); i<u; ++i)
334 {
335 group_components(tgt_src.get_transitions()[i],equivalence_class_index,tgt_src,visited);
336 }
337 block_index_of_a_state[s]=equivalence_class_index;
338}
339
340template < class LTS_TYPE>
342 const state_type s,
344 std::vector < bool >& visited)
345{
346 if (visited[s])
347 {
348 return;
349 }
350 visited[s] = true;
351 const size_t u=src_tgt.upperbound(s); // only calculate the upperbound once.
352 for(state_type i=src_tgt.lowerbound(s); i<u; ++i)
353 {
354 dfs_numbering(src_tgt.get_transitions()[i],src_tgt,visited);
355 }
356 dfsn2state.push_back(s);
357}
358
359} // namespace detail
360
361template < class LTS_TYPE>
362void scc_reduce(LTS_TYPE& l,const bool preserve_divergence_loops = false)
363{
365 scc_part.replace_transition_system(preserve_divergence_loops);
366}
367
368}
369}
370#endif // _LIBLTS_SCC_H
indexed_sorted_vector_for_tau_transitions(const LTS_TYPE &aut, bool outgoing)
Definition liblts_scc.h:44
const std::vector< state_type > & get_transitions() const
Definition liblts_scc.h:96
std::vector< state_type > m_states_with_outgoing_or_incoming_tau_transition
Definition liblts_scc.h:39
This class contains an scc partitioner removing inert tau loops.
Definition liblts_scc.h:128
std::size_t get_eq_class(const std::size_t s) const
Gives the equivalence class number of a state. The equivalence class numbers range from 0 upto (and e...
Definition liblts_scc.h:307
void dfs_numbering(const state_type t, const indexed_sorted_vector_for_tau_transitions< LTS_TYPE > &src_tgt, std::vector< bool > &visited)
Definition liblts_scc.h:341
std::size_t num_eq_classes() const
Gives the number of bisimulation equivalence classes of the LTS.
Definition liblts_scc.h:301
void group_components(const state_type t, const state_type equivalence_class_index, const indexed_sorted_vector_for_tau_transitions< LTS_TYPE > &src_tgt_src, std::vector< bool > &visited)
Definition liblts_scc.h:321
void replace_transition_system(const bool preserve_divergence_loops)
The lts for which this partioner is created is replaced by the lts modulo the calculated partition.
Definition liblts_scc.h:248
~scc_partitioner()=default
Destroys this partitioner.
bool in_same_class(const std::size_t s, const std::size_t t) const
Returns whether two states are in the same bisimulation equivalence class.
Definition liblts_scc.h:313
std::vector< state_type > block_index_of_a_state
Definition liblts_scc.h:194
std::vector< state_type > dfsn2state
Definition liblts_scc.h:195
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
The file containing the core class for transition systems.
void scc_reduce(LTS_TYPE &l, const bool preserve_divergence_loops=false)
Definition liblts_scc.h:362
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72