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/lts_builder.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_LTS_BUILDER_H
13 : #define MCRL2_LTS_BUILDER_H
14 :
15 : #include "mcrl2/lps/explorer.h"
16 : #include "mcrl2/lts/detail/lts_convert.h"
17 : #include "mcrl2/lts/lts_io.h"
18 :
19 : namespace mcrl2 {
20 :
21 : namespace lts {
22 :
23 : /// \brief Removes the last element from state s
24 : inline
25 12 : lps::state remove_time_stamp(const lps::state& s)
26 : {
27 24 : return lps::state(s.begin(), s.size() - 1);
28 : }
29 :
30 : struct lts_builder
31 : {
32 : typedef atermpp::indexed_set<lps::state, mcrl2::utilities::detail::GlobalThreadSafe> indexed_set_for_states_type;
33 : // All LTS classes use integers to represent actions in transitions. A mapping from actions to integers
34 : // is needed to avoid duplicates.
35 : utilities::unordered_map_large<lps::multi_action, std::size_t> m_actions;
36 :
37 174 : lts_builder()
38 174 : {
39 348 : lps::multi_action tau(process::action_list(), data::undefined_real());
40 174 : m_actions.emplace(std::make_pair(tau, m_actions.size()));
41 174 : }
42 :
43 2346 : std::size_t add_action(const lps::multi_action& a)
44 : {
45 2346 : lps::multi_action sorted_multi_action(a.sort_actions());
46 2346 : auto i = m_actions.find(sorted_multi_action);
47 2346 : if (i == m_actions.end())
48 : {
49 1320 : i = m_actions.emplace(std::make_pair(sorted_multi_action, m_actions.size())).first;
50 : }
51 4692 : return i->second;
52 2346 : }
53 :
54 : // Add a transition to the LTS
55 : virtual void add_transition(std::size_t from, const lps::multi_action& a, std::size_t to, const std::size_t number_of_threads = 0) = 0;
56 :
57 : // Add actions and states to the LTS
58 : virtual void finalize(const indexed_set_for_states_type& state_map, bool timed) = 0;
59 :
60 : // Save the LTS to a file
61 : virtual void save(const std::string& filename) = 0;
62 :
63 174 : virtual ~lts_builder() = default;
64 : };
65 :
66 : class lts_none_builder: public lts_builder
67 : {
68 : public:
69 0 : void add_transition(std::size_t /* from */, const lps::multi_action& /* a */, std::size_t /* to */, const std::size_t /* number_of_threads */) override
70 0 : {}
71 :
72 0 : void finalize(const indexed_set_for_states_type& /* state_map */, bool /* timed */) override
73 0 : {}
74 :
75 0 : void save(const std::string& /* filename */) override
76 0 : {}
77 : };
78 :
79 : class lts_aut_builder: public lts_builder
80 : {
81 : protected:
82 : lts_aut_t m_lts;
83 : std::mutex m_exclusive_transition_access;
84 :
85 : public:
86 66 : lts_aut_builder() = default;
87 :
88 814 : void add_transition(std::size_t from, const lps::multi_action& a, std::size_t to, const std::size_t number_of_threads) override
89 : {
90 814 : if (mcrl2::utilities::detail::GlobalThreadSafe && number_of_threads>1) m_exclusive_transition_access.lock();
91 814 : std::size_t label = add_action(a);
92 814 : m_lts.add_transition(transition(from, label, to));
93 814 : if (mcrl2::utilities::detail::GlobalThreadSafe && number_of_threads>1) m_exclusive_transition_access.unlock();
94 814 : }
95 :
96 : // Add actions and states to the LTS
97 66 : void finalize(const indexed_set_for_states_type& state_map, bool /* timed */) override
98 : {
99 : // add actions
100 66 : m_lts.set_num_action_labels(m_actions.size());
101 588 : for (const auto& p: m_actions)
102 : {
103 522 : m_lts.set_action_label(p.second, action_label_string(lps::pp(p.first)));
104 : }
105 :
106 66 : m_lts.set_num_states(state_map.size());
107 66 : }
108 :
109 66 : void save(const std::string& filename) override
110 : {
111 66 : m_lts.save(filename);
112 66 : }
113 : };
114 :
115 : // Write transitions immediately to disk, and add the AUT header later.
116 : class lts_aut_disk_builder: public lts_builder
117 : {
118 : protected:
119 : std::ofstream out;
120 : std::size_t m_transition_count = 0;
121 : std::mutex m_exclusive_transition_access;
122 :
123 : public:
124 0 : explicit lts_aut_disk_builder(const std::string& filename)
125 0 : {
126 0 : mCRL2log(log::verbose) << "writing state space in AUT format to '" << filename << "'." << std::endl;
127 0 : out.open(filename.c_str());
128 0 : if (!out.is_open())
129 : {
130 0 : throw mcrl2::runtime_error("cannot open '" + filename + "' for writing");
131 : }
132 0 : out << "des \n"; // write a dummy header that will be overwritten
133 0 : }
134 :
135 0 : void add_transition(std::size_t from, const lps::multi_action& a, std::size_t to, const std::size_t number_of_threads) override
136 : {
137 0 : if (mcrl2::utilities::detail::GlobalThreadSafe && number_of_threads>1) m_exclusive_transition_access.lock();
138 0 : m_transition_count++;
139 0 : out << "(" << from << ",\"" << lps::pp(a) << "\"," << to << ")\n";
140 0 : if (mcrl2::utilities::detail::GlobalThreadSafe && number_of_threads>1) m_exclusive_transition_access.unlock();
141 0 : }
142 :
143 : // Add actions and states to the LTS
144 0 : void finalize(const indexed_set_for_states_type& state_map, bool /* timed */) override
145 : {
146 0 : assert(!out.fail());
147 0 : out.flush();
148 0 : out.seekp(0);
149 0 : if (out.fail())
150 : {
151 0 : throw mcrl2::runtime_error("seeking is not supported by the output stream");
152 : }
153 0 : out << "des (0," << m_transition_count << "," << state_map.size() << ")";
154 0 : out.close();
155 0 : }
156 :
157 0 : void save(const std::string& /* filename */) override
158 0 : { }
159 : };
160 :
161 : class lts_lts_builder: public lts_builder
162 : {
163 : protected:
164 : lts_lts_t m_lts;
165 : bool m_discard_state_labels = false;
166 : std::mutex m_exclusive_transition_access;
167 :
168 : public:
169 108 : lts_lts_builder(
170 : const data::data_specification& dataspec,
171 : const process::action_label_list& action_labels,
172 : const data::variable_list& process_parameters,
173 : bool discard_state_labels = false
174 : )
175 108 : : m_discard_state_labels(discard_state_labels)
176 : {
177 108 : m_lts.set_data(dataspec);
178 108 : m_lts.set_process_parameters(process_parameters);
179 108 : m_lts.set_action_label_declarations(action_labels);
180 108 : }
181 :
182 1532 : void add_transition(std::size_t from, const lps::multi_action& a, std::size_t to, const std::size_t number_of_threads) override
183 : {
184 1532 : if (mcrl2::utilities::detail::GlobalThreadSafe && number_of_threads>1) m_exclusive_transition_access.lock();
185 1532 : std::size_t label = add_action(a);
186 1532 : m_lts.add_transition(transition(from, label, to));
187 1532 : if (mcrl2::utilities::detail::GlobalThreadSafe && number_of_threads>1) m_exclusive_transition_access.unlock();
188 1532 : }
189 :
190 : // Add actions and states to the LTS
191 108 : void finalize(const indexed_set_for_states_type& state_map, bool timed) override
192 : {
193 : // add actions
194 108 : m_lts.set_num_action_labels(m_actions.size());
195 1080 : for (const auto& p: m_actions)
196 : {
197 972 : m_lts.set_action_label(p.second, action_label_lts(lps::multi_action(p.first.actions(), p.first.time())));
198 : }
199 :
200 : // add state labels
201 108 : if (!m_discard_state_labels)
202 : {
203 108 : std::size_t n = state_map.size();
204 108 : std::vector<state_label_lts> state_labels(n);
205 860 : for (std::size_t i = 0; i < n; i++)
206 : {
207 752 : if (timed)
208 : {
209 12 : state_labels[i] = state_label_lts(remove_time_stamp(state_map[i]));
210 : }
211 : else
212 : {
213 740 : state_labels[i] = state_label_lts(state_map[i]);
214 : }
215 : }
216 108 : m_lts.state_labels() = std::move(state_labels);
217 108 : }
218 :
219 108 : m_lts.set_num_states(state_map.size(), true);
220 108 : m_lts.set_initial_state(0);
221 108 : }
222 :
223 54 : void save(const std::string& filename) override
224 : {
225 54 : m_lts.save(filename);
226 54 : }
227 : };
228 :
229 : class lts_lts_disk_builder: public lts_builder
230 : {
231 : protected:
232 : std::fstream fstream;
233 : std::unique_ptr<atermpp::binary_aterm_ostream> stream;
234 : bool m_discard_state_labels = false;
235 : std::mutex m_exclusive_transition_access;
236 :
237 : public:
238 0 : lts_lts_disk_builder(
239 : const std::string& filename,
240 : const data::data_specification& dataspec,
241 : const process::action_label_list& action_labels,
242 : const data::variable_list& process_parameters,
243 : bool discard_state_labels = false
244 : )
245 0 : : m_discard_state_labels(discard_state_labels)
246 : {
247 0 : bool to_stdout = filename.empty() || filename == "-";
248 0 : if (!to_stdout)
249 : {
250 0 : fstream.open(filename, std::ofstream::out | std::ofstream::binary);
251 0 : if (fstream.fail())
252 : {
253 0 : throw mcrl2::runtime_error("Fail to open file " + filename + " for writing.");
254 : }
255 :
256 0 : mCRL2log(log::verbose) << "writing state space in LTS format to '" << filename << "'." << std::endl;
257 : }
258 0 : stream = std::make_unique<atermpp::binary_aterm_ostream>(to_stdout ? std::cout : fstream);
259 :
260 0 : mcrl2::lts::write_lts_header(*stream, dataspec, process_parameters, action_labels);
261 0 : }
262 :
263 0 : void add_transition(std::size_t from, const lps::multi_action& a, std::size_t to, const std::size_t number_of_threads) override
264 : {
265 0 : if (mcrl2::utilities::detail::GlobalThreadSafe && number_of_threads>1) m_exclusive_transition_access.lock();
266 0 : write_transition(*stream, from, a, to);
267 0 : if (mcrl2::utilities::detail::GlobalThreadSafe && number_of_threads>1) m_exclusive_transition_access.unlock();
268 0 : }
269 :
270 : // Add actions and states to the LTS
271 0 : void finalize(const indexed_set_for_states_type& state_map, bool timed) override
272 : {
273 0 : if (!m_discard_state_labels)
274 : {
275 : // Write the state labels in the order of their indices.
276 0 : for (std::size_t i = 0; i < state_map.size(); i++)
277 : {
278 0 : if (is_aterm_balanced_tree(state_map[i])) // in a parallel context not all positions may be filled.
279 : {
280 0 : if (timed)
281 : {
282 0 : write_state_label(*stream, state_label_lts(remove_time_stamp(state_map[i])));
283 : }
284 : else
285 : {
286 0 : write_state_label(*stream, state_label_lts(state_map[i]));
287 : }
288 : }
289 : }
290 : }
291 :
292 : // Write the initial state.
293 0 : write_initial_state(*stream, 0);
294 0 : }
295 :
296 0 : void save(const std::string&) override {}
297 : };
298 :
299 : class lts_dot_builder: public lts_lts_builder
300 : {
301 : public:
302 : typedef lts_lts_builder super;
303 0 : lts_dot_builder(const data::data_specification& dataspec, const process::action_label_list& action_labels, const data::variable_list& process_parameters)
304 0 : : super(dataspec, action_labels, process_parameters)
305 0 : { }
306 :
307 0 : void save(const std::string& filename) override
308 : {
309 0 : lts_dot_t dot;
310 0 : detail::lts_convert(m_lts, dot);
311 0 : dot.save(filename);
312 0 : }
313 : };
314 :
315 : class lts_fsm_builder: public lts_lts_builder
316 : {
317 : public:
318 : typedef lts_lts_builder super;
319 54 : lts_fsm_builder(const data::data_specification& dataspec, const process::action_label_list& action_labels, const data::variable_list& process_parameters)
320 54 : : super(dataspec, action_labels, process_parameters)
321 54 : { }
322 :
323 54 : void save(const std::string& filename) override
324 : {
325 54 : lts_fsm_t fsm;
326 54 : detail::lts_convert(m_lts, fsm);
327 54 : fsm.save(filename);
328 54 : }
329 : };
330 :
331 : inline
332 174 : std::unique_ptr<lts_builder> create_lts_builder(const lps::specification& lpsspec, const lps::explorer_options& options, lts_type output_format, const std::string& output_filename = "")
333 : {
334 174 : switch (output_format)
335 : {
336 66 : case lts_aut:
337 : {
338 66 : if (options.save_at_end)
339 : {
340 66 : return std::make_unique<lts_aut_builder>();
341 : }
342 : else
343 : {
344 0 : return std::make_unique<lts_aut_disk_builder>(output_filename);
345 : }
346 : }
347 0 : case lts_dot: return std::make_unique<lts_dot_builder>(lpsspec.data(), lpsspec.action_labels(), lpsspec.process().process_parameters());
348 54 : case lts_fsm: return std::make_unique<lts_fsm_builder>(lpsspec.data(), lpsspec.action_labels(), lpsspec.process().process_parameters());
349 54 : case lts_lts:
350 : {
351 54 : if (options.save_at_end)
352 : {
353 54 : return std::make_unique<lts_lts_builder>(lpsspec.data(), lpsspec.action_labels(), lpsspec.process().process_parameters(), options.discard_lts_state_labels);
354 : }
355 : else
356 : {
357 0 : return std::make_unique<lts_lts_disk_builder>(output_filename, lpsspec.data(), lpsspec.action_labels(), lpsspec.process().process_parameters(), options.discard_lts_state_labels);
358 : }
359 : }
360 0 : default: return std::make_unique<lts_none_builder>();
361 : }
362 : }
363 :
364 : } // namespace lts
365 :
366 : } // namespace mcrl2
367 :
368 : #endif // MCRL2_LTS_BUILDER_H
|
