11#ifndef _LIBLTS_TAUSTARREDUCE_H
12#define _LIBLTS_TAUSTARREDUCE_H
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 > >
45 typedef std::map < state_t,std::set < state_t > > map_from_states_to_states;
46 map_from_states_to_states resulting_tau_transitions;
49 for(std::vector < mcrl2::lts::transition>::const_iterator i=l.get_transitions().begin(); i!=l.get_transitions().end(); ++i)
51 if (l.is_tau(l.apply_hidden_label_map(i->label())))
55 resulting_tau_transitions[i->from()].insert(i->to());
59 resulting_tau_transitions[i->to()].insert(i->from());
64 bool new_state_added=
true;
65 while (new_state_added)
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)
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++)
75 new_outgoing_states.insert(resulting_tau_transitions[*j].begin(),
76 resulting_tau_transitions[*j].end());
78 if (i->second.size()<new_outgoing_states.size())
80 i->second=new_outgoing_states;
86 return resulting_tau_transitions;
90template <
class STATE_LABEL_T,
class ACTION_LABEL_T,
class LTS_BASE_CLASS >
95 const std::vector < transition >& original_transitions=l.get_transitions();
96 std::set < transition> new_transitions;
101 for(
const transition& t: original_transitions)
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)
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)
111 new_transitions.insert(
transition(*j_from,t.label(),*j_to));
114 for(
typename std::set<state_t>::const_iterator j_to=new_to_states.begin(); j_to!=new_to_states.end(); ++j_to)
116 new_transitions.insert(
transition(t.from(),t.label(),*j_to));
120 l.clear_transitions();
122 for(state_t i=0; i<l.num_states(); ++i)
124 new_transitions.insert(
transition(i,l.tau_label_index(),i));
128 for(std::set < transition >::const_iterator i=new_transitions.begin();
129 i!=new_transitions.end(); ++i)
131 l.add_transition(*i);
138template <
class STATE_LABEL_T,
class ACTION_LABEL_T,
class LTS_BASE_CLASS >
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;
162 states_reachable_in_one_visible_action.clear();
163 states_reachable_in_one_hidden_action.clear();
168 for(
size_t j_=outgoing_transitions.
lowerbound(from_); j_<outgoing_transitions.
upperbound(from_); ++j_)
171 if (l.is_tau(l.apply_hidden_label_map(
label(j))))
173 states_reachable_in_one_hidden_action.insert(
to(j));
175 else if (label_==
label(j))
177 assert(!l.is_tau(l.apply_hidden_label_map(label_)));
178 states_reachable_in_one_visible_action.insert(
to(j));
186 for(
const state_type& middle: states_reachable_in_one_hidden_action)
191 for(
size_t j_=outgoing_transitions.
lowerbound(middle); j_<outgoing_transitions.
upperbound(middle); ++j_)
194 if (l.is_tau(l.apply_hidden_label_map(label_)))
196 if (l.is_tau(l.apply_hidden_label_map(
label(j))) &&
to(j)==to_)
204 if (
label(j)==label_ &&
to(j)==to_)
214 if (!found && !l.is_tau(l.apply_hidden_label_map(label_)))
216 for(
const state_type& middle: states_reachable_in_one_visible_action)
220 for(
size_t j_=outgoing_transitions.
lowerbound(middle); j_<outgoing_transitions.
upperbound(middle); ++j_)
223 if (l.is_tau(l.apply_hidden_label_map(
label(j))) &&
to(j)==to_)
236 l.add_transition(
transition(from_, label_, to_));
244template <
class STATE_LABEL_T,
class ACTION_LABEL_T,
class LTS_BASE_CLASS >
249 std::vector < transition >& original_transitions=l.get_transitions();
250 std::set < transition> new_transitions;
253 for(std::vector < transition >::const_iterator i=original_transitions.begin(); i!=original_transitions.end(); ++i)
255 if (!l.is_tau(l.apply_hidden_label_map(i->label())))
257 new_transitions.insert(*i);
263 for(std::vector < transition >::const_iterator i=original_transitions.begin(); i!=original_transitions.end(); ++i)
265 if (!l.is_tau(l.apply_hidden_label_map(i->label())))
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)
270 new_transitions.insert(
transition(*j,i->label(),i->to()));
274 l.clear_transitions();
277 for(std::set < transition >::const_iterator i=new_transitions.begin();
278 i!=new_transitions.end(); ++i)
280 l.add_transition(*i);
size_t upperbound(const state_type s) const
size_t lowerbound(const state_type s) const
const std::vector< CONTENT > & get_transitions() const
A class that contains a labelled transition system.
std::vector< STATE_LABEL_T >::size_type states_size_type
The sort that contains the indices of states.
std::vector< ACTION_LABEL_T >::size_type labels_size_type
The sort that represents the indices of labels.
A class containing triples, source label and target representing transitions.
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...