Line data Source code
1 : // Author(s): Muck van Weerdenburg; completely rewritten by 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 : //
9 : /// \file liblts_lts.cpp
10 :
11 : #include "mcrl2/lts/lts_lts.h"
12 : #include "mcrl2/lts/lts_io.h"
13 :
14 : #include "mcrl2/atermpp/standard_containers/indexed_set.h"
15 :
16 : #include <fstream>
17 : #include <optional>
18 :
19 : namespace mcrl2::lts
20 : {
21 :
22 : /// \brief Converts a probabilistic state into an aterm that encodes it.
23 115 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const probabilistic_lts_lts_t::probabilistic_state_t& state)
24 : {
25 115 : if (state.size()==0)
26 : {
27 : // The probabilistic state is represented as a singular state and is stored without probability;
28 59 : stream << atermpp::aterm_int(1);
29 59 : stream << atermpp::aterm_int(state.get());
30 : }
31 56 : else if (state.size()<=1)
32 : {
33 : // The probabilistic state is the single element in a vector and is stored without probability;
34 0 : stream << atermpp::aterm_int(1);
35 0 : stream << atermpp::aterm_int(state.get());
36 : }
37 : else
38 : {
39 : // The probabilistic state is stored as a sequence of state probability pairs.
40 56 : stream << atermpp::aterm_int(state.size());
41 :
42 168 : for(const auto& p : state)
43 : {
44 : // Push a (index, probability) pair into the list.
45 112 : stream << atermpp::aterm_int(p.state());
46 112 : stream << p.probability();
47 : }
48 : }
49 :
50 115 : return stream;
51 : }
52 :
53 115 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, probabilistic_lts_lts_t::probabilistic_state_t& state)
54 : {
55 115 : atermpp::aterm_int index;
56 115 : stream >> index; // Read the number of states.
57 :
58 115 : const std::size_t value=index.value();
59 115 : assert(value>0);
60 115 : if (value==1)
61 : {
62 59 : stream >> index;
63 59 : state.set(index.value());
64 : }
65 : else
66 : {
67 56 : state.clear();
68 56 : lps::probabilistic_data_expression probability;
69 :
70 168 : for (std::size_t i = 0; i < value; ++i)
71 : {
72 112 : stream >> index;
73 112 : stream >> probability;
74 :
75 112 : state.add(index.value(), probability);
76 : }
77 :
78 56 : state.shrink_to_fit();
79 56 : }
80 115 : return stream;
81 115 : }
82 :
83 : namespace detail
84 : {
85 :
86 : using namespace atermpp;
87 :
88 : // Special terms to indicate the type of the following structure.
89 :
90 2101 : static const atermpp::aterm_appl& transition_mark()
91 : {
92 2101 : static const atermpp::aterm_appl plain_mark(atermpp::function_symbol("transition", 0));
93 2101 : return plain_mark;
94 : }
95 :
96 605 : static const atermpp::aterm_appl& probabilistic_transition_mark()
97 : {
98 605 : static atermpp::aterm_appl probabilistic_mark(atermpp::function_symbol("probabilistic_transition", 0));
99 605 : return probabilistic_mark;
100 : }
101 :
102 126 : static const atermpp::aterm_appl& initial_state_mark()
103 : {
104 126 : static const atermpp::aterm_appl initial_state_mark(atermpp::function_symbol("initial_state", 0));
105 126 : return initial_state_mark;
106 : }
107 :
108 126 : static const atermpp::aterm_appl& labelled_transition_system_mark()
109 : {
110 126 : static const atermpp::aterm_appl lts_mark(atermpp::function_symbol("labelled_transition_system", 0));
111 126 : return lts_mark;
112 : }
113 :
114 : // Utility functions
115 :
116 59 : static void set_initial_state(lts_lts_t& lts, const probabilistic_lts_lts_t::probabilistic_state_t& initial_state)
117 : {
118 59 : if (initial_state.size() > 1)
119 : {
120 0 : throw mcrl2::runtime_error("The initial state of the non probabilistic input lts is probabilistic.");
121 : }
122 :
123 59 : lts.set_initial_state(initial_state.get());
124 59 : }
125 :
126 4 : static void set_initial_state(probabilistic_lts_lts_t& lts, const probabilistic_lts_lts_t::probabilistic_state_t& initial_state)
127 : {
128 4 : lts.set_initial_probabilistic_state(initial_state);
129 4 : }
130 :
131 : template <class LTS>
132 63 : static void read_lts(atermpp::aterm_istream& stream, LTS& lts)
133 : {
134 : static_assert(std::is_same<LTS,probabilistic_lts_lts_t>::value ||
135 : std::is_same<LTS,lts_lts_t>::value,
136 : "Function read_lts can only be applied to a (probabilistic) lts. ");
137 :
138 63 : atermpp::aterm_stream_state state(stream);
139 63 : stream >> data::detail::add_index_impl;
140 :
141 63 : atermpp::aterm marker;
142 63 : stream >> marker;
143 :
144 63 : if (marker != labelled_transition_system_mark())
145 : {
146 0 : throw mcrl2::runtime_error("Stream does not contain a labelled transition system (LTS).");
147 : }
148 :
149 : // Read the header of the lts.
150 63 : data::data_specification spec;
151 63 : data::variable_list parameters;
152 63 : process::action_label_list action_labels;
153 :
154 63 : stream >> spec;
155 63 : stream >> parameters;
156 63 : stream >> action_labels;
157 :
158 63 : lts.set_data(spec);
159 63 : lts.set_process_parameters(parameters);
160 63 : lts.set_action_label_declarations(action_labels);
161 :
162 : // An indexed set to keep indices for multi actions.
163 63 : mcrl2::utilities::indexed_set<action_label_lts> multi_actions;
164 63 : multi_actions.insert(action_label_lts::tau_action()); // This action list represents 'tau'.
165 :
166 : // The initial state is stored and set as last.
167 63 : std::optional<probabilistic_lts_lts_t::probabilistic_state_t> initial_state;
168 :
169 : // Ensure unique indices for the probabilistic states.
170 : mcrl2::utilities::indexed_set<
171 63 : probabilistic_lts_lts_t::probabilistic_state_t> probabilistic_states;
172 :
173 : // Keep track of the number of states (derived from the transitions).
174 63 : std::size_t number_of_states = 1;
175 :
176 63 : aterm term;
177 63 : aterm_int from;
178 63 : action_label_lts action;
179 63 : aterm_int to;
180 :
181 1327 : while (true)
182 : {
183 1390 : stream.get(term);
184 1390 : if (!term.defined())
185 : {
186 : // The default constructed term indicates the end of the stream.
187 63 : break;
188 : }
189 :
190 1327 : if (term == transition_mark())
191 : {
192 774 : stream >> from;
193 774 : stream >> action;
194 774 : stream >> to;
195 :
196 774 : const auto [index, inserted] = multi_actions.insert(action);
197 :
198 774 : std::size_t target_index = to.value();
199 : if constexpr (std::is_same<LTS, probabilistic_lts_lts_t>::value)
200 : {
201 2 : probabilistic_lts_lts_t::probabilistic_state_t lts_state(to.value());
202 :
203 : // For probabilistic lts it is necessary to add the state first (and use the returned index).
204 : bool state_inserted;
205 2 : std::tie(target_index, state_inserted) = probabilistic_states.insert(lts_state);
206 :
207 2 : if (state_inserted)
208 : {
209 2 : std::size_t actual_index = lts.add_probabilistic_state(lts_state);
210 2 : utilities::mcrl2_unused(actual_index);
211 2 : assert(actual_index == target_index);
212 : }
213 2 : }
214 :
215 : // Add the transition and update the number of states.
216 774 : lts.add_transition(transition(from.value(), index, target_index));
217 774 : number_of_states = std::max(number_of_states, std::max(from.value() + 1, to.value() + 1));
218 :
219 774 : if (inserted)
220 : {
221 440 : std::size_t actual_index = lts.add_action(action);
222 440 : utilities::mcrl2_unused(actual_index);
223 440 : assert(actual_index == index);
224 : }
225 :
226 : }
227 553 : else if(term == probabilistic_transition_mark())
228 : {
229 : if constexpr (std::is_same<LTS, probabilistic_lts_lts_t>::value)
230 : {
231 52 : probabilistic_lts_lts_t::probabilistic_state_t to;
232 :
233 52 : stream >> from;
234 52 : stream >> action;
235 52 : stream >> to;
236 :
237 52 : const auto [index, inserted] = multi_actions.insert(action);
238 :
239 : // Compute the index of the probabilistic state.
240 52 : const auto [to_index, state_inserted] = probabilistic_states.insert(to);
241 :
242 52 : if (state_inserted)
243 : {
244 24 : std::size_t actual_index = lts.add_probabilistic_state(to);
245 24 : utilities::mcrl2_unused(actual_index);
246 24 : assert(actual_index == to_index);
247 : }
248 :
249 52 : lts.add_transition(transition(from.value(), index, to_index));
250 :
251 : // Update the number of states
252 52 : number_of_states = std::max(number_of_states, std::max(from.value() + 1, to_index + 1));
253 :
254 52 : if (inserted)
255 : {
256 16 : std::size_t actual_index = lts.add_action(action);
257 16 : utilities::mcrl2_unused(actual_index);
258 16 : assert(actual_index == index);
259 : }
260 52 : }
261 : else
262 : {
263 0 : throw mcrl2::runtime_error("Attempting to read a probabilistic LTS as a regular LTS.");
264 : }
265 : }
266 501 : else if (term.type_is_list())
267 : {
268 : // Lists always represent state labels, only need to add the indices.
269 438 : lts.add_state(reinterpret_cast<const state_label_lts&>(term));
270 : }
271 63 : else if (term == initial_state_mark())
272 : {
273 : // Read the initial state.
274 63 : probabilistic_lts_lts_t::probabilistic_state_t state;
275 63 : stream >> state;
276 63 : initial_state = state;
277 63 : }
278 : else
279 : {
280 0 : throw mcrl2::runtime_error("Unknown mark in labelled transition system (LTS) stream.");
281 : }
282 : }
283 :
284 : // The initial state can only be set after the states are known.
285 63 : if (initial_state)
286 : {
287 : // If the lts has no state labels, we need to add empty states labels.
288 63 : lts.set_num_states(number_of_states, lts.has_state_info());
289 :
290 63 : set_initial_state(lts, initial_state.value());
291 : }
292 : else
293 : {
294 0 : throw mcrl2::runtime_error("Missing initial state in labelled transition system (LTS) stream.");
295 : }
296 63 : }
297 :
298 : template <class LTS_TRANSITION_SYSTEM>
299 63 : static void read_from_lts(LTS_TRANSITION_SYSTEM& lts, const std::string& filename)
300 : {
301 : static_assert(std::is_same<LTS_TRANSITION_SYSTEM,probabilistic_lts_lts_t>::value ||
302 : std::is_same<LTS_TRANSITION_SYSTEM,lts_lts_t>::value,
303 : "Function read_from_lts can only be applied to a (probabilistic) lts. ");
304 :
305 63 : std::ifstream fstream;
306 63 : if (!filename.empty())
307 : {
308 63 : fstream.open(filename, std::ifstream::in | std::ifstream::binary);
309 63 : if (fstream.fail())
310 : {
311 0 : if (filename.empty())
312 : {
313 0 : throw mcrl2::runtime_error("Fail to open standard input to read an lts.");
314 : }
315 : else
316 : {
317 0 : throw mcrl2::runtime_error("Fail to open file " + filename + " to read an lts.");
318 : }
319 : }
320 : }
321 :
322 : try
323 : {
324 63 : atermpp::binary_aterm_istream stream(filename.empty() ? std::cin : fstream);
325 63 : stream >> lts;
326 63 : }
327 0 : catch (const std::exception& ex)
328 : {
329 0 : mCRL2log(log::error) << ex.what() << "\n";
330 0 : if (filename.empty())
331 : {
332 0 : throw mcrl2::runtime_error("Fail to correctly read an lts from standard input.");
333 : }
334 : else
335 : {
336 0 : throw mcrl2::runtime_error("Fail to correctly read an lts from the file " + filename + ".");
337 : }
338 : }
339 63 : }
340 :
341 4 : void write_initial_state(atermpp::aterm_ostream& stream, const probabilistic_lts_lts_t& lts)
342 : {
343 4 : stream << detail::initial_state_mark();
344 4 : stream << lts.initial_probabilistic_state();
345 4 : }
346 :
347 59 : void write_initial_state(atermpp::aterm_ostream& stream, const lts_lts_t& lts)
348 : {
349 59 : stream << detail::initial_state_mark();
350 59 : stream << probabilistic_lts_lts_t::probabilistic_state_t(lts.initial_state());
351 59 : }
352 :
353 : template <class LTS>
354 63 : static void write_lts(atermpp::aterm_ostream& stream, const LTS& lts)
355 : {
356 : static_assert(std::is_same<LTS,probabilistic_lts_lts_t>::value ||
357 : std::is_same<LTS,lts_lts_t>::value,
358 : "Function write_lts can only be applied to a (probabilistic) lts. ");
359 :
360 : // Write the process related information.
361 63 : write_lts_header(stream,
362 : lts.data(),
363 : lts.process_parameters(),
364 : lts.action_label_declarations());
365 :
366 889 : for (const transition& trans : lts.get_transitions())
367 : {
368 826 : lts_lts_t::action_label_t label = lts.action_label(lts.apply_hidden_label_map(trans.label()));
369 :
370 : if constexpr (std::is_same<LTS, probabilistic_lts_lts_t>::value)
371 : {
372 54 : write_transition(stream, trans.from(), label, lts.probabilistic_state(trans.to()));
373 : }
374 : else
375 : {
376 772 : write_transition(stream, trans.from(), label, trans.to());
377 : }
378 : }
379 :
380 63 : if (lts.has_state_info())
381 : {
382 499 : for (std::size_t i = 0; i < lts.num_state_labels(); ++i)
383 : {
384 : // Write state labels as such, we assume that all list terms without headers are state labels.
385 438 : stream << lts.state_label(i);
386 : }
387 : }
388 :
389 : // Write the initial state.
390 63 : write_initial_state(stream, lts);
391 63 : }
392 :
393 : template <class LTS_TRANSITION_SYSTEM>
394 63 : static void write_to_lts(const LTS_TRANSITION_SYSTEM& lts, const std::string& filename)
395 : {
396 : static_assert(std::is_same<LTS_TRANSITION_SYSTEM,probabilistic_lts_lts_t>::value ||
397 : std::is_same<LTS_TRANSITION_SYSTEM,lts_lts_t>::value,
398 : "Function write_to_lts can only be applied to a (probabilistic) lts. ");
399 :
400 63 : bool to_stdout = filename.empty() || filename == "-";
401 63 : std::ofstream fstream;
402 63 : if (!to_stdout)
403 : {
404 63 : fstream.open(filename, std::ofstream::out | std::ofstream::binary);
405 63 : if (fstream.fail())
406 : {
407 0 : throw mcrl2::runtime_error("Fail to open file " + filename + " for writing.");
408 : }
409 : }
410 :
411 : try
412 : {
413 63 : atermpp::binary_aterm_ostream stream(to_stdout ? std::cout : fstream);
414 63 : stream << lts;
415 63 : }
416 0 : catch (const std::exception& ex)
417 : {
418 0 : mCRL2log(log::error) << ex.what() << "\n";
419 0 : throw mcrl2::runtime_error("Fail to write lts correctly to the file " + filename + ".");
420 : }
421 63 : }
422 :
423 : } // namespace detail
424 :
425 : // Implementation of public functions.
426 :
427 59 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, lts_lts_t& lts)
428 : {
429 59 : read_lts(stream, lts);
430 59 : return stream;
431 : }
432 :
433 4 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, probabilistic_lts_lts_t& lts)
434 : {
435 4 : read_lts(stream, lts);
436 4 : return stream;
437 : }
438 :
439 59 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const lts_lts_t& lts)
440 : {
441 59 : detail::write_lts(stream, lts);
442 59 : return stream;
443 : }
444 :
445 4 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const probabilistic_lts_lts_t& lts)
446 : {
447 4 : detail::write_lts(stream, lts);
448 4 : return stream;
449 : }
450 :
451 63 : void write_lts_header(atermpp::aterm_ostream& stream,
452 : const data::data_specification& data_spec,
453 : const data::variable_list& parameters,
454 : const process::action_label_list& action_labels)
455 : {
456 : // We set the transformer for all other elements (transitions, state labels and the initial state).
457 63 : stream << data::detail::remove_index_impl;
458 :
459 : // Write the header of the lts.
460 63 : stream << detail::labelled_transition_system_mark();
461 63 : stream << data_spec;
462 63 : stream << parameters;
463 63 : stream << action_labels;
464 63 : }
465 :
466 774 : void write_transition(atermpp::aterm_ostream& stream, std::size_t from, const lps::multi_action& label, std::size_t to)
467 : {
468 774 : stream << detail::transition_mark();
469 774 : stream << atermpp::aterm_int(from);
470 774 : stream << label;
471 774 : stream << atermpp::aterm_int(to);
472 774 : }
473 :
474 54 : void write_transition(atermpp::aterm_ostream& stream, std::size_t from, const lps::multi_action& label, const probabilistic_lts_lts_t::probabilistic_state_t& to)
475 : {
476 54 : if (to.size() <= 1)
477 : {
478 : // Actually a non probabilistic transition.
479 2 : write_transition(stream, from, label, to.get());
480 : }
481 : else
482 : {
483 52 : stream << detail::probabilistic_transition_mark();
484 52 : stream << atermpp::aterm_int(from);
485 52 : stream << label;
486 52 : stream << to;
487 : }
488 54 : }
489 :
490 0 : void write_state_label(atermpp::aterm_ostream& stream, const state_label_lts& label)
491 : {
492 : // During reading we assume that state labels are the only aterm_list.
493 0 : stream << label;
494 0 : }
495 :
496 0 : void write_initial_state(atermpp::aterm_ostream& stream, std::size_t index)
497 : {
498 0 : stream << detail::initial_state_mark();
499 0 : stream << probabilistic_lts_lts_t::probabilistic_state_t(index);
500 0 : }
501 :
502 4 : void probabilistic_lts_lts_t::save(const std::string& filename) const
503 : {
504 4 : mCRL2log(log::verbose) << "Starting to save a probabilistic lts to the file " << filename << ".\n";
505 4 : detail::write_to_lts(*this, filename);
506 4 : }
507 :
508 59 : void lts_lts_t::save(std::string const& filename) const
509 : {
510 59 : mCRL2log(log::verbose) << "Starting to save an lts to the file " << filename << ".\n";
511 59 : detail::write_to_lts(*this, filename);
512 59 : }
513 :
514 4 : void probabilistic_lts_lts_t::load(const std::string& filename)
515 : {
516 4 : mCRL2log(log::verbose) << "Starting to load a probabilistic lts from the file " << filename << ".\n";
517 4 : detail::read_from_lts(*this, filename);
518 4 : }
519 :
520 59 : void lts_lts_t::load(const std::string& filename)
521 : {
522 59 : mCRL2log(log::verbose) << "Starting to load an lts from the file " << filename << ".\n";
523 59 : detail::read_from_lts(*this, filename);
524 59 : }
525 :
526 : } // namespace mcrl2::lts
|
