mCRL2
Loading...
Searching...
No Matches
lts_utilities.h
Go to the documentation of this file.
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
18#ifndef MCRL2_LTS_LTS_UTILITIES_H
19#define MCRL2_LTS_LTS_UTILITIES_H
20
21#include "mcrl2/lts/lts_lts.h"
22
23namespace mcrl2
24{
25
26namespace lts
27{
28
36inline void sort_transitions(std::vector<transition>& transitions,
37 const std::set<transition::size_type>& hidden_label_set,
39{
40 switch (ts)
41 {
42 case lbl_tgt_src:
43 {
44 const detail::compare_transitions_lts compare(hidden_label_set);
45 sort(transitions.begin(),transitions.end(),compare);
46 break;
47 }
48 case src_lbl_tgt:
49 default:
50 {
51 const detail::compare_transitions_slt compare(hidden_label_set);
52 sort(transitions.begin(),transitions.end(),compare);
53 break;
54 }
55 }
56}
57
63inline void sort_transitions(std::vector<transition>& transitions, transition_sort_style ts = src_lbl_tgt)
64{
65 sort_transitions(transitions, std::set<transition::size_type>(), ts);
66}
67
68
69namespace 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.
80template <class CONTENT>
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
89 std::vector <size_t> m_indices;
90
91 public:
92
93 indexed_sorted_vector_for_transitions(const std::vector < transition >& transitions , state_type num_states, bool outgoing)
94 : m_indices(num_states+1,0)
95 {
96 // First count the number of outgoing transitions per state and put it in indices.
97 for(const transition& t: transitions)
98 {
99 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 size_t sum=0;
107 for(state_type& i: m_indices) // The vector is changed. This must be a reference.
108 {
109 sum=sum+i;
110 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.
116 for(const transition& t: transitions)
117 {
118 if (outgoing)
119 {
120 assert(t.from()<m_indices.size());
121 assert(m_indices[t.from()]>0);
122 m_indices[t.from()]--;
125 }
126 else
127 {
128 assert(t.to()<m_indices.size());
129 assert(m_indices[t.to()]>0);
130 m_indices[t.to()]--;
133 }
134 }
135 assert(m_indices.at(num_states)==m_states_with_outgoing_or_incoming_transition.size());
136 }
137
138 // Get the indexed transitions.
139 const std::vector<CONTENT>& get_transitions() const
140 {
142 }
143
144 // Get the lowest index of incoming/outging transitions stored in m_states_with_outgoing_or_incoming_transition.
145 size_t lowerbound(const state_type s) const
146 {
147 assert(s+1<m_indices.size());
148 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 size_t upperbound(const state_type s) const
153 {
154 assert(s+1<m_indices.size());
155 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//
171typedef std::pair<transition::size_type, transition::size_type> outgoing_pair_t;
172
173typedef detail::indexed_sorted_vector_for_transitions < outgoing_pair_t > outgoing_transitions_per_state_t;
174
176inline std::size_t label(const outgoing_pair_t& p)
177{
178 return p.first;
179}
180
182inline std::size_t to(const outgoing_pair_t& p)
183{
184 return p.second;
185}
186
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.
191typedef std::multimap<std::pair<transition::size_type, transition::size_type>, transition::size_type>
193
195inline std::size_t from(const outgoing_transitions_per_state_action_t::const_iterator& i)
196{
197 return i->first.first;
198}
199
201inline std::size_t label(const outgoing_transitions_per_state_action_t::const_iterator& i)
202{
203 return i->first.second;
204}
205
207inline std::size_t to(const outgoing_transitions_per_state_action_t::const_iterator& i)
208{
209 return i->second;
210}
211
214{
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
226 const std::vector<transition>& trans,
227 const std::set<transition::size_type>& hide_label_set)
228{
230 for (const transition& t: trans)
231 {
232 result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
233 std::pair<transition::size_type, transition::size_type>(t.from(), detail::apply_hidden_labels(t.label(),hide_label_set)), t.to()));
234 }
235 return result;
236}
237
240{
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
252 const std::vector<transition>& trans,
253 const std::set<transition::size_type>& hide_label_set)
254{
256 for (const transition& t: trans)
257 {
258 result.insert(std::pair<std::pair<transition::size_type, transition::size_type>, transition::size_type>(
259 std::pair<transition::size_type, transition::size_type>(t.to(), detail::apply_hidden_labels(t.label(),hide_label_set)), t.from()));
260 }
261 return result;
262}
263
264namespace detail
265{
266// Yields a label with an obscure name referring to divergence.
267
268template < class LABEL_TYPE >
269// LABEL_TYPE make_divergence_label(const std::string& s, const LABEL_TYPE& l)
270LABEL_TYPE make_divergence_label(const std::string& s)
271{
272 return LABEL_TYPE(s);
273}
274
275template <>
276inline mcrl2::lts::action_label_lts make_divergence_label<mcrl2::lts::action_label_lts>(const std::string& s)
277{
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.
285template < class LTS_TYPE >
287{
288 // Below we create an odd action label, representing divergence.
289 const typename LTS_TYPE::action_label_t lab=make_divergence_label<typename LTS_TYPE::action_label_t>("!@*&divergence&*@!");
290 std::size_t divergent_transition_label=l.add_action(lab);
291 assert(divergent_transition_label+1==l.num_action_labels());
292 for(transition& t: l.get_transitions())
293 {
294 if (l.is_tau(l.apply_hidden_label_map(t.label())) && t.to()==t.from())
295 {
296 t = transition(t.to(),divergent_transition_label,t.to());
297 }
298 }
299 return divergent_transition_label;
300}
301
302// Replace each transition in a state that is an outgoing divergent_transition with a tau_loop in that state.
303template < class LTS_TYPE >
304void unmark_explicit_divergence_transitions(LTS_TYPE& l, const std::size_t divergent_transition_label)
305{
306 for(transition& t: l.get_transitions())
307 {
308 if (t.label()==divergent_transition_label)
309 {
310 t = transition(t.from(),l.tau_label_index(),t.from());
311 }
312 }
313}
314
315} // namespace detail
316
317}
318}
319
320#endif // MCRL2_LTS_LTS_UTILITIES_H
Term containing a string.
A list of aterm objects.
Definition aterm_list.h:23
\brief A timed multi-action
A class containing the values for action labels for the .lts format.
Definition lts_lts.h:137
std::pair< label_type, state_type > label_state_pair
indexed_sorted_vector_for_transitions(const std::vector< transition > &transitions, state_type num_states, bool outgoing)
const std::vector< CONTENT > & get_transitions() const
A class containing triples, source label and target representing transitions.
Definition transition.h:43
std::size_t size_type
The type of the elements in a transition.
Definition transition.h:46
\brief An action label
This file contains a class that contains labelled transition systems in lts (mcrl2) format.
void unmark_explicit_divergence_transitions(LTS_TYPE &l, const std::size_t divergent_transition_label)
LABEL_TYPE make_divergence_label(const std::string &s)
std::size_t mark_explicit_divergence_transitions(LTS_TYPE &l)
std::size_t apply_hidden_labels(const std::size_t n, const std::set< std::size_t > &hidden_action_set)
Definition transition.h:25
transition_sort_style
Transition sort styles.
Definition transition.h:34
std::multimap< std::pair< transition::size_type, transition::size_type >, transition::size_type > outgoing_transitions_per_state_action_t
Type for exploring transitions per state and action.
outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair_reversed(const std::vector< transition > &trans)
Provide the transitions as a multimap accessible per from state and label, ordered backwardly.
std::size_t to(const outgoing_pair_t &p)
Target state of a label state pair.
outgoing_transitions_per_state_action_t transitions_per_outgoing_state_action_pair(const std::vector< transition > &trans)
Provide the transitions as a multimap accessible per from state and label.
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.
detail::indexed_sorted_vector_for_transitions< outgoing_pair_t > outgoing_transitions_per_state_t
std::size_t label(const outgoing_pair_t &p)
Label of a pair of a label and target state.
std::size_t from(const outgoing_transitions_per_state_action_t::const_iterator &i)
From state of an iterator exploring transitions per outgoing state and action.
std::pair< transition::size_type, transition::size_type > outgoing_pair_t
Type for exploring transitions per state.
bool compare(const LTS_TYPE &l1, const LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples=false, const std::string &counter_example_file="", const bool structured_output=false)
Checks whether this LTS is equivalent to another LTS.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72