mCRL2
Loading...
Searching...
No Matches
liblts_tau_star_reduce.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_TAUSTARREDUCE_H
12#define _LIBLTS_TAUSTARREDUCE_H
13
15
16namespace mcrl2
17{
18namespace lts
19{
20namespace detail
21{
22
23//Replace sequences tau* a tau* by a single action a.
24
25
27
33// points forward, to the next state, or backward, to the previous state.
35// states that can be reached by one or more tau_steps.
36
37template < class STATE_LABEL_T, class ACTION_LABEL_T, class LTS_BASE_CLASS >
38std::map < std::size_t,
39 std::set <typename lts<STATE_LABEL_T,ACTION_LABEL_T, LTS_BASE_CLASS>::states_size_type > >
41 const bool forward)
42{
44
45 typedef std::map < state_t,std::set < state_t > > map_from_states_to_states;
46 map_from_states_to_states resulting_tau_transitions;
47
48 // Copy the internal transitions into the result.
49 for(std::vector < mcrl2::lts::transition>::const_iterator i=l.get_transitions().begin(); i!=l.get_transitions().end(); ++i)
50 {
51 if (l.is_tau(l.apply_hidden_label_map(i->label())))
52 {
53 if (forward)
54 {
55 resulting_tau_transitions[i->from()].insert(i->to());
56 }
57 else
58 {
59 resulting_tau_transitions[i->to()].insert(i->from());
60 }
61 }
62 }
63
64 bool new_state_added=true;
65 while (new_state_added)
66 {
67 new_state_added=false;
68 for(typename map_from_states_to_states::iterator i=resulting_tau_transitions.begin();
69 i!=resulting_tau_transitions.end(); ++i)
70 {
71 const std::set<std::size_t>& outgoing_states= i->second;
72 std::set<std::size_t> new_outgoing_states=outgoing_states;
73 for(std::set<std::size_t>::const_iterator j=outgoing_states.begin(); j!=outgoing_states.end(); j++)
74 {
75 new_outgoing_states.insert(resulting_tau_transitions[*j].begin(),
76 resulting_tau_transitions[*j].end());
77 }
78 if (i->second.size()<new_outgoing_states.size())
79 {
80 i->second=new_outgoing_states;
81 new_state_added=true;
82 }
83 }
84 }
85
86 return resulting_tau_transitions;
87}
88
89
90template < class STATE_LABEL_T, class ACTION_LABEL_T, class LTS_BASE_CLASS >
92// This method assumes there are no tau loops!
93{
95 const std::vector < transition >& original_transitions=l.get_transitions();
96 std::set < transition> new_transitions;
97
98 // Add for every tau*.a tau* transitions sequence a single transition a;
99 std::map <state_t, std::set <state_t> > backward_tau_closure=calculate_non_reflexive_transitive_tau_closure(l,false);
100 std::map <state_t, std::set <state_t> > forward_tau_closure=calculate_non_reflexive_transitive_tau_closure(l,true);
101 for(const transition& t: original_transitions)
102 {
103 new_transitions.insert(t);
104 std::set<state_t>& new_from_states=backward_tau_closure[t.from()];
105 std::set<state_t>& new_to_states=forward_tau_closure[t.to()];
106 for(typename std::set<state_t>::const_iterator j_from=new_from_states.begin(); j_from!=new_from_states.end(); ++j_from)
107 {
108 new_transitions.insert(transition(*j_from,t.label(),t.to()));
109 for(typename std::set<state_t>::const_iterator j_to=new_to_states.begin(); j_to!=new_to_states.end(); ++j_to)
110 {
111 new_transitions.insert(transition(*j_from,t.label(),*j_to));
112 }
113 }
114 for(typename std::set<state_t>::const_iterator j_to=new_to_states.begin(); j_to!=new_to_states.end(); ++j_to)
115 {
116 new_transitions.insert(transition(t.from(),t.label(),*j_to));
117 }
118 }
119
120 l.clear_transitions();
121
122 for(state_t i=0; i<l.num_states(); ++i)
123 {
124 new_transitions.insert(transition(i,l.tau_label_index(),i));
125 }
126
127 // Add the newly generated transitions
128 for(std::set < transition >::const_iterator i=new_transitions.begin();
129 i!=new_transitions.end(); ++i)
130 {
131 l.add_transition(*i);
132 }
133}
134
135
138template < class STATE_LABEL_T, class ACTION_LABEL_T, class LTS_BASE_CLASS >
140{
143
144 outgoing_transitions_per_state_t outgoing_transitions(l.get_transitions(),l.num_states(),true);
145 l.clear_transitions();
146 std::set < state_type > states_reachable_in_one_visible_action;
147 std::set < state_type > states_reachable_in_one_hidden_action;
148
149 // for(outgoing_transitions_per_state_t::const_iterator i=outgoing_transitions.begin(); i!=outgoing_transitions.end(); ++i)
150
151 // for(const outgoing_transitions_t& vec: outgoing_transitions)
152 for(state_type from=0; from < l.num_states(); from++)
153 {
154 // for(const outgoing_pair_t& p: vec)
155 for(size_t j=outgoing_transitions.lowerbound(from); j<outgoing_transitions.upperbound(from); ++j)
156 {
157 const outgoing_pair_t& p = outgoing_transitions.get_transitions()[j];
158 const state_type from_=from; // the start state of a transition under consideration.
159 const label_type label_=label(p); // the label
160 const state_type to_=to(p); // the target state
161
162 states_reachable_in_one_visible_action.clear();
163 states_reachable_in_one_hidden_action.clear();
164
165 // For every transition from-label->to we calculate the sets { s | from -a->s } and { s | from -tau-> s }.
166 // assert(from_<outgoing_transitions.size());
167 // for(const outgoing_pair_t& j: outgoing_transitions[from_])
168 for(size_t j_=outgoing_transitions.lowerbound(from_); j_<outgoing_transitions.upperbound(from_); ++j_)
169 {
170 const outgoing_pair_t& j = outgoing_transitions.get_transitions()[j_];
171 if (l.is_tau(l.apply_hidden_label_map(label(j))))
172 {
173 states_reachable_in_one_hidden_action.insert(to(j));
174 }
175 else if (label_==label(j))
176 {
177 assert(!l.is_tau(l.apply_hidden_label_map(label_)));
178 states_reachable_in_one_visible_action.insert(to(j));
179 }
180 }
181
182 // Now check whether to is reachable in one step from one of the two sets constructed above. If no,
183 // insert the transition in l.transitions.
184 bool found=false;
185
186 for(const state_type& middle: states_reachable_in_one_hidden_action)
187 {
188 // Find a visible step from state middle to state to, unless label is hidden, in which case we search
189 // a hidden step.
190 // for(const outgoing_pair_t& j: outgoing_transitions[middle])
191 for(size_t j_=outgoing_transitions.lowerbound(middle); j_<outgoing_transitions.upperbound(middle); ++j_)
192 {
193 const outgoing_pair_t& j=outgoing_transitions.get_transitions()[j_];
194 if (l.is_tau(l.apply_hidden_label_map(label_)))
195 {
196 if (l.is_tau(l.apply_hidden_label_map(label(j))) && to(j)==to_)
197 {
198 assert(!found);
199 found=true; break;
200 }
201 }
202 else // label is visible.
203 {
204 if (label(j)==label_ && to(j)==to_)
205 {
206 assert(!found);
207 found=true; break;
208 }
209 }
210 }
211 if (found) break;
212 }
213
214 if (!found && !l.is_tau(l.apply_hidden_label_map(label_)))
215 {
216 for(const state_type& middle: states_reachable_in_one_visible_action)
217 {
218 // Find a hidden step from state middle to state to.
219 // for(const outgoing_pair_t& j: outgoing_transitions[middle])
220 for(size_t j_=outgoing_transitions.lowerbound(middle); j_<outgoing_transitions.upperbound(middle); ++j_)
221 {
222 const outgoing_pair_t& j=outgoing_transitions.get_transitions()[j_];
223 if (l.is_tau(l.apply_hidden_label_map(label(j))) && to(j)==to_)
224 {
225 assert(!found);
226 found=true; break;
227 }
228 }
229 if (found) break;
230 }
231 }
232
233 // If no alternative transition is found, add this transition to l.transitions().
234 if (!found)
235 {
236 l.add_transition(transition(from_, label_, to_));
237 }
238 }
239 // from++;
240 }
241}
242
243
244template < class STATE_LABEL_T, class ACTION_LABEL_T, class LTS_BASE_CLASS >
246// This method assumes there are no tau loops!
247{
249 std::vector < transition >& original_transitions=l.get_transitions();
250 std::set < transition> new_transitions;
251
252 // Add all the original non tau transitions.
253 for(std::vector < transition >::const_iterator i=original_transitions.begin(); i!=original_transitions.end(); ++i)
254 {
255 if (!l.is_tau(l.apply_hidden_label_map(i->label())))
256 {
257 new_transitions.insert(*i);
258 }
259 }
260
261 // Add for every tau*.a transitions sequence a single transition a, provided a is not tau.
262 std::map <state_t, std::set <state_t> > backward_tau_closure=calculate_non_reflexive_transitive_tau_closure(l,false);
263 for(std::vector < transition >::const_iterator i=original_transitions.begin(); i!=original_transitions.end(); ++i)
264 {
265 if (!l.is_tau(l.apply_hidden_label_map(i->label())))
266 {
267 std::set<state_t>& new_from_states=backward_tau_closure[i->from()];
268 for(typename std::set<state_t>::const_iterator j=new_from_states.begin(); j!=new_from_states.end(); ++j)
269 {
270 new_transitions.insert(transition(*j,i->label(),i->to()));
271 }
272 }
273 }
274 l.clear_transitions();
275
276 // Add the newly generated transitions
277 for(std::set < transition >::const_iterator i=new_transitions.begin();
278 i!=new_transitions.end(); ++i)
279 {
280 l.add_transition(*i);
281 }
282
283 reachability_check(l, true); // Remove unreachable parts.
284}
285
286}
287}
288}
289#endif // _LIBLTS_TAUSTARREDUCE_H
const std::vector< CONTENT > & get_transitions() const
A class that contains a labelled transition system.
Definition lts.h:83
std::vector< STATE_LABEL_T >::size_type states_size_type
The sort that contains the indices of states.
Definition lts.h:100
std::vector< ACTION_LABEL_T >::size_type labels_size_type
The sort that represents the indices of labels.
Definition lts.h:104
A class containing triples, source label and target representing transitions.
Definition transition.h:47
@ unknown
Definition linearise.cpp:58
This file contains some utility functions to manipulate lts's.
std::size_t state_type
type used to store state (numbers and) counts
std::map< std::size_t, std::set< typename lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS >::states_size_type > > calculate_non_reflexive_transitive_tau_closure(lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS > &l, const bool forward)
This procedure calculates the transitive tau closure as a separate vector of transitions,...
std::size_t label_type
type used to store label numbers and counts
void remove_redundant_transitions(lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS > &l)
Removes each transition s-a->s' if also transitions s-a->-tau->s' or s-tau->-a->s' are present....
void reflexive_transitive_tau_closure(lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS > &l)
void tau_star_reduce(lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS > &l)
std::size_t to(const outgoing_pair_t &p)
Target state of a label state pair.
bool reachability_check(lts< SL, AL, BASE > &l, bool remove_unreachable=false)
Checks whether all states in this LTS are reachable from the initial state and remove unreachable sta...
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.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72