mCRL2
Loading...
Searching...
No Matches
stochastic_lts_builder.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
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//
11
12#ifndef MCRL2_LTS_STOCHASTIC_LTS_BUILDER_H
13#define MCRL2_LTS_STOCHASTIC_LTS_BUILDER_H
14
16
17namespace mcrl2 {
18
19namespace lts {
20
22{
24 // All LTS classes use integers to represent actions in transitions. A mapping from actions to integers
25 // is needed to avoid duplicates.
27
29 {
31 m_actions.emplace(std::make_pair(tau, m_actions.size()));
32 }
33
34 std::size_t add_action(const lps::multi_action& a)
35 {
36 auto i = m_actions.find(a);
37 if (i == m_actions.end())
38 {
39 i = m_actions.emplace(std::make_pair(a, m_actions.size())).first;
40 }
41 return i->second;
42 }
43
44 // Set the initial (stochastic) state of the LTS
45 virtual void set_initial_state(const std::list<std::size_t>& targets, const std::vector<data::data_expression>& probabilities) = 0;
46
47 // Add a transition to the LTS
48 virtual void add_transition(std::size_t from, const lps::multi_action& a, const std::list<std::size_t>& targets, const std::vector<data::data_expression>& probabilities, const std::size_t number_of_threads = 1) = 0;
49
50 // Add actions and states to the LTS
51 virtual void finalize(const indexed_set_for_states_type& state_map, bool timed) = 0;
52
53 // Save the LTS to a file
54 virtual void save(const std::string& filename) = 0;
55
56 virtual ~stochastic_lts_builder() = default;
57};
58
60{
61 public:
62 void set_initial_state(const std::list<std::size_t>& /* to */, const std::vector<data::data_expression>& /* probabilities */) override
63 {}
64
65 void add_transition(std::size_t /* from */, const lps::multi_action& /* a */, const std::list<std::size_t>& /* targets */, const std::vector<data::data_expression>& /* probabilities */, const std::size_t /* number_of_threads */) override
66 {}
67
68 void finalize(const indexed_set_for_states_type& /* state_map */, bool /* timed */) override
69 {}
70
71 void save(const std::string& /* filename */) override
72 {}
73};
74
76{
77 protected:
79 {
80 std::list<std::size_t> targets;
81 std::vector<data::data_expression> probabilities;
82
83 stochastic_state() = default;
84
85 stochastic_state(std::list<std::size_t> targets_, std::vector<data::data_expression> probabilities_)
86 : targets(std::move(targets_)), probabilities(std::move(probabilities_))
87 {}
88
89 void save_to_aut(std::ostream& out) const
90 {
91 auto j = targets.begin();
92 out << *j++;
93 if (targets.size() > 1)
94 {
95 for (auto i = probabilities.begin(); j != targets.end(); ++i, ++j)
96 {
97 out << " " << lps::print_probability(*i) << " " << *j;
98 }
99 }
100 }
101 };
102
104 {
105 std::size_t from;
106 std::size_t label;
107 std::size_t to;
108
109 transition(std::size_t from_, std::size_t label_, std::size_t to_)
110 : from(from_), label(label_), to(to_)
111 {}
112
113 bool operator<(const transition& other) const
114 {
115 return std::tie(from, label, to) < std::tie(other.from, other.label, other.to);
116 }
117 };
118
119 std::vector<stochastic_state> m_stochastic_states;
120 std::vector<transition> m_transitions;
121 std::size_t m_number_of_states = 0;
123
124 public:
126
127 // Set the initial (stochastic) state of the LTS
128 void set_initial_state(const std::list<std::size_t>& targets, const std::vector<data::data_expression>& probabilities) override
129 {
130 m_stochastic_states.emplace_back(targets, probabilities);
131 }
132
133 // Add a transition to the LTS
134 void add_transition(std::size_t from, const lps::multi_action& a, const std::list<std::size_t>& targets, const std::vector<data::data_expression>& probabilities, const std::size_t number_of_threads) override
135 {
137 std::size_t to = m_stochastic_states.size();
138 std::size_t label = add_action(a);
139 m_stochastic_states.emplace_back(targets, probabilities);
140 m_transitions.emplace_back(from, label, to);
142 }
143
144 // Add actions and states to the LTS
145 void finalize(const indexed_set_for_states_type& state_map, bool /* timed */) override
146 {
147 m_number_of_states = state_map.size();
148 }
149
150 void save(std::ostream& out) const
151 {
152 std::vector<lps::multi_action> actions{ m_actions.size() };
153 for (const auto& p: m_actions)
154 {
155 actions[p.second] = p.first;
156 }
157
158 out << "des (";
159 m_stochastic_states[0].save_to_aut(out);
160 out << "," << m_transitions.size() << "," << m_number_of_states << ")" << "\n";
161
162 for (const transition& t: m_transitions)
163 {
164 out << "(" << t.from << ",\"" << lps::pp(actions[t.label]) << "\",";
165 m_stochastic_states[t.to].save_to_aut(out);
166 out << ")" << "\n";
167 }
168 }
169
170 // Save the LTS to a file
171 void save(const std::string& filename) override
172 {
173 if (filename.empty())
174 {
175 save(std::cout);
176 }
177 else
178 {
179 std::ofstream out(filename.c_str());
180 if (!out.is_open())
181 {
182 throw mcrl2::runtime_error("cannot create .aut file '" + filename + ".");
183 }
184 save(out);
185 out.close();
186 }
187 }
188};
189
191{
192 protected:
197
198 public:
200 const data::data_specification& dataspec,
201 const process::action_label_list& action_labels,
202 const data::variable_list& process_parameters,
203 bool discard_state_labels = false
204 )
205 : m_discard_state_labels(discard_state_labels)
206 {
207 m_lts.set_data(dataspec);
208 m_lts.set_process_parameters(process_parameters);
209 m_lts.set_action_label_declarations(action_labels);
210 }
211
213 make_probabilistic_state(const std::list<std::size_t>& targets, const std::vector<data::data_expression>& probabilities)
214 {
216 assert(targets.size()>0);
217 if (targets.size()==1)
218 {
219 result.set(targets.front());
220 }
221 else
222 {
223 std::list<std::size_t>::const_iterator ti = targets.begin();
224 std::vector<data::data_expression>::const_iterator pi = probabilities.begin();
225 for (; ti != targets.end(); ++pi, ++ti)
226 {
227 result.add(*ti, lps::probabilistic_data_expression(*pi));
228 }
229 }
230 return result;
231 }
232
233 // Set the initial (stochastic) state of the LTS
234 void set_initial_state(const std::list<std::size_t>& targets, const std::vector<data::data_expression>& probabilities) override
235 {
236 m_initial_state = make_probabilistic_state(targets, probabilities);
237 }
238
239 // Add a transition to the LTS
240 void add_transition(std::size_t from, const lps::multi_action& a, const std::list<std::size_t>& targets, const std::vector<data::data_expression>& probabilities, const std::size_t number_of_threads) override
241 {
243 auto s1 = make_probabilistic_state(targets, probabilities);
244 std::size_t label = add_action(a);
245 std::size_t to = m_lts.add_probabilistic_state(s1);
248
249 }
250
251 // Add actions and states to the LTS
252 void finalize(const indexed_set_for_states_type& state_map, bool timed) override
253 {
254 // add actions
256 for (const auto& p: m_actions)
257 {
258 m_lts.set_action_label(p.second, action_label_lts(lps::multi_action(p.first.actions(), p.first.time())));
259 }
260
261 // add state labels
263 {
264 std::size_t n = state_map.size();
265 std::vector<state_label_lts> state_labels(n);
266 for (std::size_t i = 0; i < n; i++)
267 {
268 if (timed)
269 {
270 state_labels[i] = state_label_lts(remove_time_stamp(state_map[i]));
271 }
272 else
273 {
274 state_labels[i] = state_label_lts(state_map[i]);
275 }
276 }
277 m_lts.state_labels() = std::move(state_labels);
278 }
279
280 m_lts.set_num_states(state_map.size(), true);
281 m_lts.set_initial_probabilistic_state(m_initial_state); // This can't be done at the start :-(
282 }
283
284 // Save the LTS to a file
285 void save(const std::string& filename) override
286 {
287 m_lts.save(filename);
288 }
289};
290
292{
293 public:
295 stochastic_lts_fsm_builder(const data::data_specification& dataspec, const process::action_label_list& action_labels, const data::variable_list& process_parameters)
296 : super(dataspec, action_labels, process_parameters)
297 { }
298
299 void save(const std::string& filename) override
300 {
303 fsm.save(filename);
304 }
305};
306
307inline
308std::unique_ptr<stochastic_lts_builder> create_stochastic_lts_builder(const lps::stochastic_specification& lpsspec, const lps::explorer_options& options, lts_type output_format)
309{
310 switch (output_format)
311 {
312 case lts_aut: return std::make_unique<stochastic_lts_aut_builder>();
313 case lts_lts: return std::make_unique<stochastic_lts_lts_builder>(lpsspec.data(), lpsspec.action_labels(), lpsspec.process().process_parameters(), options.discard_lts_state_labels);
314 case lts_fsm: return std::make_unique<stochastic_lts_fsm_builder>(lpsspec.data(), lpsspec.action_labels(), lpsspec.process().process_parameters());
315 default: return std::make_unique<stochastic_lts_none_builder>();
316 }
317}
318
319} // namespace lts
320
321} // namespace mcrl2
322
323#endif // MCRL2_LTS_STOCHASTIC_LTS_BUILDER_H
A set that assigns each element an unique index, and protects its internal terms en masse.
Definition indexed_set.h:30
A list of aterm objects.
Definition aterm_list.h:23
const data::variable_list & process_parameters() const
Returns the sequence of process parameters.
\brief A timed multi-action
This class contains labels for probabilistic transistions, consisting of a numerator and a denumerato...
const process::action_label_list & action_labels() const
Returns a sequence of action labels. This sequence contains all action labels occurring in the specif...
const LinearProcess & process() const
Returns the linear process of the specification.
const data::data_specification & data() const
Returns the data specification.
A class containing the values for action labels for the .lts format.
Definition lts_lts.h:137
void add_transition(const transition &t)
Add a transition to the lts.
Definition lts.h:544
void set_num_action_labels(const labels_size_type n)
Sets the number of action labels of this LTS.
Definition lts.h:310
void set_num_states(const states_size_type n, const bool has_state_labels=true)
Sets the number of states of this LTS.
Definition lts.h:280
std::vector< STATE_LABEL_T > & state_labels()
Provides the state labels of an LTS.
Definition lts.h:253
void set_action_label(const labels_size_type action, const ACTION_LABEL_T &label)
Sets the label of an action.
Definition lts.h:402
The class lts_fsm_t contains labelled transition systems in .fsm format.
Definition lts_fsm.h:276
void save(const std::string &filename) const
Save the labelled transition system to file.
This class contains probabilistic labelled transition systems in .lts format.
Definition lts_lts.h:402
void save(const std::string &filename) const
Save the labelled transition system to file.
void set_initial_probabilistic_state(const PROBABILISTIC_STATE_T &state)
Sets the probabilistic initial state number of this LTS.
states_size_type add_probabilistic_state(const PROBABILISTIC_STATE_T &s)
Adds a probabilistic state to this LTS.
A class that contains a probabilistic state.
void set(const STATE &s)
Set this probabilistic state to a single state with probability one.
void add(const STATE &s, const PROBABILITY &p)
Add a state with a probability to the probabilistic state.
This class contains state labels for an labelled transition system in .lts format.
Definition lts_lts.h:40
void save(const std::string &filename) override
void finalize(const indexed_set_for_states_type &state_map, bool) override
void add_transition(std::size_t from, const lps::multi_action &a, const std::list< std::size_t > &targets, const std::vector< data::data_expression > &probabilities, const std::size_t number_of_threads) override
std::vector< stochastic_state > m_stochastic_states
void set_initial_state(const std::list< std::size_t > &targets, const std::vector< data::data_expression > &probabilities) override
void save(const std::string &filename) override
stochastic_lts_fsm_builder(const data::data_specification &dataspec, const process::action_label_list &action_labels, const data::variable_list &process_parameters)
void save(const std::string &filename) override
probabilistic_state< std::size_t, lps::probabilistic_data_expression > m_initial_state
static probabilistic_state< std::size_t, lps::probabilistic_data_expression > make_probabilistic_state(const std::list< std::size_t > &targets, const std::vector< data::data_expression > &probabilities)
stochastic_lts_lts_builder(const data::data_specification &dataspec, const process::action_label_list &action_labels, const data::variable_list &process_parameters, bool discard_state_labels=false)
void add_transition(std::size_t from, const lps::multi_action &a, const std::list< std::size_t > &targets, const std::vector< data::data_expression > &probabilities, const std::size_t number_of_threads) override
void set_initial_state(const std::list< std::size_t > &targets, const std::vector< data::data_expression > &probabilities) override
void finalize(const indexed_set_for_states_type &state_map, bool timed) override
void save(const std::string &) override
void set_initial_state(const std::list< std::size_t > &, const std::vector< data::data_expression > &) override
void finalize(const indexed_set_for_states_type &, bool) override
void add_transition(std::size_t, const lps::multi_action &, const std::list< std::size_t > &, const std::vector< data::data_expression > &, const std::size_t) override
A class containing triples, source label and target representing transitions.
Definition transition.h:43
Standard exception class for reporting runtime errors.
Definition exception.h:27
size_type size(std::size_t thread_index=0) const
The number of elements in the indexed set.
A class for a map of keys to values in T based using the simple hash table set implementation.
add your file description here.
const data::data_expression & undefined_real()
Returns a data expression of type Real that corresponds to 'undefined'.
Definition undefined.h:62
std::string pp(const action_summand &x)
Definition lps.cpp:26
std::string print_probability(const data::data_expression &x)
void lts_convert(const lts< STATE_LABEL1, ACTION_LABEL1, LTS_BASE1 > &lts_in, lts< STATE_LABEL2, ACTION_LABEL2, LTS_BASE2 > &lts_out)
lts_type
The enumerated type lts_type contains an index for every type type of labelled transition system that...
Definition lts_type.h:37
std::size_t to(const outgoing_pair_t &p)
Target state of a label state pair.
std::unique_ptr< stochastic_lts_builder > create_stochastic_lts_builder(const lps::stochastic_specification &lpsspec, const lps::explorer_options &options, lts_type output_format)
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.
lps::state remove_time_stamp(const lps::state &s)
Removes the last element from state s.
Definition lts_builder.h:25
static constexpr bool GlobalThreadSafe
Enables thread safety for the whole toolset.
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.
stochastic_state(std::list< std::size_t > targets_, std::vector< data::data_expression > probabilities_)
transition(std::size_t from_, std::size_t label_, std::size_t to_)
utilities::unordered_map_large< lps::multi_action, std::size_t > m_actions
virtual ~stochastic_lts_builder()=default
virtual void save(const std::string &filename)=0
virtual void set_initial_state(const std::list< std::size_t > &targets, const std::vector< data::data_expression > &probabilities)=0
atermpp::indexed_set< lps::state, mcrl2::utilities::detail::GlobalThreadSafe > indexed_set_for_states_type
std::size_t add_action(const lps::multi_action &a)
virtual void add_transition(std::size_t from, const lps::multi_action &a, const std::list< std::size_t > &targets, const std::vector< data::data_expression > &probabilities, const std::size_t number_of_threads=1)=0
virtual void finalize(const indexed_set_for_states_type &state_map, bool timed)=0