Line data Source code
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 : //
9 : /// \file mcrl2/lts/stochastic_stochastic_lts_builder.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_LTS_STOCHASTIC_LTS_BUILDER_H
13 : #define MCRL2_LTS_STOCHASTIC_LTS_BUILDER_H
14 :
15 : #include "mcrl2/lts/lts_builder.h"
16 :
17 : namespace mcrl2 {
18 :
19 : namespace lts {
20 :
21 : struct stochastic_lts_builder
22 : {
23 : typedef atermpp::indexed_set<lps::state, mcrl2::utilities::detail::GlobalThreadSafe> indexed_set_for_states_type;
24 : // All LTS classes use integers to represent actions in transitions. A mapping from actions to integers
25 : // is needed to avoid duplicates.
26 : utilities::unordered_map_large<lps::multi_action, std::size_t> m_actions;
27 :
28 18 : stochastic_lts_builder()
29 18 : {
30 36 : lps::multi_action tau(process::action_list(), data::undefined_real());
31 18 : m_actions.emplace(std::make_pair(tau, m_actions.size()));
32 18 : }
33 :
34 190 : std::size_t add_action(const lps::multi_action& a)
35 : {
36 190 : auto i = m_actions.find(a);
37 190 : if (i == m_actions.end())
38 : {
39 66 : i = m_actions.emplace(std::make_pair(a, m_actions.size())).first;
40 : }
41 190 : 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 18 : virtual ~stochastic_lts_builder() = default;
57 : };
58 :
59 : class stochastic_lts_none_builder: public stochastic_lts_builder
60 : {
61 : public:
62 0 : void set_initial_state(const std::list<std::size_t>& /* to */, const std::vector<data::data_expression>& /* probabilities */) override
63 0 : {}
64 :
65 0 : 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 0 : {}
67 :
68 0 : void finalize(const indexed_set_for_states_type& /* state_map */, bool /* timed */) override
69 0 : {}
70 :
71 0 : void save(const std::string& /* filename */) override
72 0 : {}
73 : };
74 :
75 : class stochastic_lts_aut_builder: public stochastic_lts_builder
76 : {
77 : protected:
78 : struct stochastic_state
79 : {
80 : std::list<std::size_t> targets;
81 : std::vector<data::data_expression> probabilities;
82 :
83 : stochastic_state() = default;
84 :
85 92 : stochastic_state(std::list<std::size_t> targets_, std::vector<data::data_expression> probabilities_)
86 92 : : targets(std::move(targets_)), probabilities(std::move(probabilities_))
87 92 : {}
88 :
89 92 : void save_to_aut(std::ostream& out) const
90 : {
91 92 : auto j = targets.begin();
92 92 : out << *j++;
93 92 : if (targets.size() > 1)
94 : {
95 168 : for (auto i = probabilities.begin(); j != targets.end(); ++i, ++j)
96 : {
97 84 : out << " " << lps::print_probability(*i) << " " << *j;
98 : }
99 : }
100 92 : }
101 : };
102 :
103 : struct transition
104 : {
105 : std::size_t from;
106 : std::size_t label;
107 : std::size_t to;
108 :
109 82 : transition(std::size_t from_, std::size_t label_, std::size_t to_)
110 82 : : from(from_), label(label_), to(to_)
111 82 : {}
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;
122 : std::mutex m_exclusive_transition_access;
123 :
124 : public:
125 10 : stochastic_lts_aut_builder() = default;
126 :
127 : // Set the initial (stochastic) state of the LTS
128 10 : void set_initial_state(const std::list<std::size_t>& targets, const std::vector<data::data_expression>& probabilities) override
129 : {
130 10 : m_stochastic_states.emplace_back(targets, probabilities);
131 10 : }
132 :
133 : // Add a transition to the LTS
134 82 : 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 : {
136 82 : if (mcrl2::utilities::detail::GlobalThreadSafe && number_of_threads>1) m_exclusive_transition_access.lock();
137 82 : std::size_t to = m_stochastic_states.size();
138 82 : std::size_t label = add_action(a);
139 82 : m_stochastic_states.emplace_back(targets, probabilities);
140 82 : m_transitions.emplace_back(from, label, to);
141 82 : if (mcrl2::utilities::detail::GlobalThreadSafe && number_of_threads>1) m_exclusive_transition_access.unlock();
142 82 : }
143 :
144 : // Add actions and states to the LTS
145 10 : void finalize(const indexed_set_for_states_type& state_map, bool /* timed */) override
146 : {
147 10 : m_number_of_states = state_map.size();
148 10 : }
149 :
150 10 : void save(std::ostream& out) const
151 : {
152 10 : std::vector<lps::multi_action> actions{ m_actions.size() };
153 50 : for (const auto& p: m_actions)
154 : {
155 40 : actions[p.second] = p.first;
156 : }
157 :
158 10 : out << "des (";
159 10 : m_stochastic_states[0].save_to_aut(out);
160 10 : out << "," << m_transitions.size() << "," << m_number_of_states << ")" << "\n";
161 :
162 92 : for (const transition& t: m_transitions)
163 : {
164 82 : out << "(" << t.from << ",\"" << lps::pp(actions[t.label]) << "\",";
165 82 : m_stochastic_states[t.to].save_to_aut(out);
166 82 : out << ")" << "\n";
167 : }
168 10 : }
169 :
170 : // Save the LTS to a file
171 10 : void save(const std::string& filename) override
172 : {
173 10 : if (filename.empty())
174 : {
175 0 : save(std::cout);
176 : }
177 : else
178 : {
179 10 : std::ofstream out(filename.c_str());
180 10 : if (!out.is_open())
181 : {
182 0 : throw mcrl2::runtime_error("cannot create .aut file '" + filename + ".");
183 : }
184 10 : save(out);
185 10 : out.close();
186 10 : }
187 10 : }
188 : };
189 :
190 : class stochastic_lts_lts_builder: public stochastic_lts_builder
191 : {
192 : protected:
193 : probabilistic_lts_lts_t m_lts;
194 : bool m_discard_state_labels = false;
195 : probabilistic_state<std::size_t, lps::probabilistic_data_expression> m_initial_state;
196 : std::mutex m_exclusive_transition_access;
197 :
198 : public:
199 8 : stochastic_lts_lts_builder(
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 8 : : m_discard_state_labels(discard_state_labels)
206 : {
207 8 : m_lts.set_data(dataspec);
208 8 : m_lts.set_process_parameters(process_parameters);
209 8 : m_lts.set_action_label_declarations(action_labels);
210 8 : }
211 :
212 : static probabilistic_state<std::size_t, lps::probabilistic_data_expression>
213 116 : make_probabilistic_state(const std::list<std::size_t>& targets, const std::vector<data::data_expression>& probabilities)
214 : {
215 116 : probabilistic_state<std::size_t, lps::probabilistic_data_expression> result;
216 116 : assert(targets.size()>0);
217 116 : if (targets.size()==1)
218 : {
219 4 : result.set(targets.front());
220 : }
221 : else
222 : {
223 112 : std::list<std::size_t>::const_iterator ti = targets.begin();
224 112 : std::vector<data::data_expression>::const_iterator pi = probabilities.begin();
225 336 : for (; ti != targets.end(); ++pi, ++ti)
226 : {
227 224 : result.add(*ti, lps::probabilistic_data_expression(*pi));
228 : }
229 : }
230 116 : return result;
231 0 : }
232 :
233 : // Set the initial (stochastic) state of the LTS
234 8 : void set_initial_state(const std::list<std::size_t>& targets, const std::vector<data::data_expression>& probabilities) override
235 : {
236 8 : m_initial_state = make_probabilistic_state(targets, probabilities);
237 8 : }
238 :
239 : // Add a transition to the LTS
240 108 : 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 : {
242 108 : if (mcrl2::utilities::detail::GlobalThreadSafe && number_of_threads>1) m_exclusive_transition_access.lock();
243 108 : auto s1 = make_probabilistic_state(targets, probabilities);
244 108 : std::size_t label = add_action(a);
245 108 : std::size_t to = m_lts.add_probabilistic_state(s1);
246 108 : m_lts.add_transition(transition(from, label, to));
247 108 : if (mcrl2::utilities::detail::GlobalThreadSafe && number_of_threads>1) m_exclusive_transition_access.unlock();
248 :
249 108 : }
250 :
251 : // Add actions and states to the LTS
252 8 : void finalize(const indexed_set_for_states_type& state_map, bool timed) override
253 : {
254 : // add actions
255 8 : m_lts.set_num_action_labels(m_actions.size());
256 52 : for (const auto& p: m_actions)
257 : {
258 44 : 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
262 8 : if (!m_discard_state_labels)
263 : {
264 8 : std::size_t n = state_map.size();
265 8 : std::vector<state_label_lts> state_labels(n);
266 120 : for (std::size_t i = 0; i < n; i++)
267 : {
268 112 : if (timed)
269 : {
270 0 : state_labels[i] = state_label_lts(remove_time_stamp(state_map[i]));
271 : }
272 : else
273 : {
274 112 : state_labels[i] = state_label_lts(state_map[i]);
275 : }
276 : }
277 8 : m_lts.state_labels() = std::move(state_labels);
278 8 : }
279 :
280 8 : m_lts.set_num_states(state_map.size(), true);
281 8 : m_lts.set_initial_probabilistic_state(m_initial_state); // This can't be done at the start :-(
282 8 : }
283 :
284 : // Save the LTS to a file
285 4 : void save(const std::string& filename) override
286 : {
287 4 : m_lts.save(filename);
288 4 : }
289 : };
290 :
291 : class stochastic_lts_fsm_builder: public stochastic_lts_lts_builder
292 : {
293 : public:
294 : typedef stochastic_lts_lts_builder super;
295 4 : stochastic_lts_fsm_builder(const data::data_specification& dataspec, const process::action_label_list& action_labels, const data::variable_list& process_parameters)
296 4 : : super(dataspec, action_labels, process_parameters)
297 4 : { }
298 :
299 4 : void save(const std::string& filename) override
300 : {
301 4 : probabilistic_lts_fsm_t fsm;
302 4 : detail::lts_convert(m_lts, fsm);
303 4 : fsm.save(filename);
304 4 : }
305 : };
306 :
307 : inline
308 18 : std::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 18 : switch (output_format)
311 : {
312 10 : case lts_aut: return std::make_unique<stochastic_lts_aut_builder>();
313 4 : 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 4 : case lts_fsm: return std::make_unique<stochastic_lts_fsm_builder>(lpsspec.data(), lpsspec.action_labels(), lpsspec.process().process_parameters());
315 0 : 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
|
