mCRL2
Loading...
Searching...
No Matches
liblts_lts.cpp
Go to the documentation of this file.
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//
10
11#include "mcrl2/lts/lts_lts.h"
12#include "mcrl2/lts/lts_io.h"
13
15
16#include <fstream>
17#include <optional>
18
19namespace mcrl2::lts
20{
21
24{
25 if (state.size()==0)
26 {
27 // The probabilistic state is represented as a singular state and is stored without probability;
28 stream << atermpp::aterm_int(1);
29 stream << atermpp::aterm_int(state.get());
30 }
31 else if (state.size()<=1)
32 {
33 // The probabilistic state is the single element in a vector and is stored without probability;
34 stream << atermpp::aterm_int(1);
35 stream << atermpp::aterm_int(state.get());
36 }
37 else
38 {
39 // The probabilistic state is stored as a sequence of state probability pairs.
40 stream << atermpp::aterm_int(state.size());
41
42 for(const auto& p : state)
43 {
44 // Push a (index, probability) pair into the list.
45 stream << atermpp::aterm_int(p.state());
46 stream << p.probability();
47 }
48 }
49
50 return stream;
51}
52
54{
56 stream >> index; // Read the number of states.
57
58 const std::size_t value=index.value();
59 assert(value>0);
60 if (value==1)
61 {
62 stream >> index;
63 state.set(index.value());
64 }
65 else
66 {
67 state.clear();
69
70 for (std::size_t i = 0; i < value; ++i)
71 {
72 stream >> index;
73 stream >> probability;
74
75 state.add(index.value(), probability);
76 }
77
78 state.shrink_to_fit();
79 }
80 return stream;
81}
82
83namespace detail
84{
85
86using namespace atermpp;
87
88// Special terms to indicate the type of the following structure.
89
91{
92 static const atermpp::aterm_appl plain_mark(atermpp::function_symbol("transition", 0));
93 return plain_mark;
94}
95
97{
98 static atermpp::aterm_appl probabilistic_mark(atermpp::function_symbol("probabilistic_transition", 0));
99 return probabilistic_mark;
100}
101
103{
104 static const atermpp::aterm_appl initial_state_mark(atermpp::function_symbol("initial_state", 0));
105 return initial_state_mark;
106}
107
109{
110 static const atermpp::aterm_appl lts_mark(atermpp::function_symbol("labelled_transition_system", 0));
111 return lts_mark;
112}
113
114// Utility functions
115
117{
118 if (initial_state.size() > 1)
119 {
120 throw mcrl2::runtime_error("The initial state of the non probabilistic input lts is probabilistic.");
121 }
122
123 lts.set_initial_state(initial_state.get());
124}
125
127{
128 lts.set_initial_probabilistic_state(initial_state);
129}
130
131template <class LTS>
132static 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
140
141 atermpp::aterm marker;
142 stream >> marker;
143
144 if (marker != labelled_transition_system_mark())
145 {
146 throw mcrl2::runtime_error("Stream does not contain a labelled transition system (LTS).");
147 }
148
149 // Read the header of the lts.
151 data::variable_list parameters;
152 process::action_label_list action_labels;
153
154 stream >> spec;
155 stream >> parameters;
156 stream >> action_labels;
157
158 lts.set_data(spec);
159 lts.set_process_parameters(parameters);
160 lts.set_action_label_declarations(action_labels);
161
162 // An indexed set to keep indices for multi actions.
164 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 std::optional<probabilistic_lts_lts_t::probabilistic_state_t> initial_state;
168
169 // Ensure unique indices for the probabilistic states.
172
173 // Keep track of the number of states (derived from the transitions).
174 std::size_t number_of_states = 1;
175
176 aterm term;
178 action_label_lts action;
180
181 while (true)
182 {
183 stream.get(term);
184 if (!term.defined())
185 {
186 // The default constructed term indicates the end of the stream.
187 break;
188 }
189
190 if (term == transition_mark())
191 {
192 stream >> from;
193 stream >> action;
194 stream >> to;
195
196 const auto [index, inserted] = multi_actions.insert(action);
197
198 std::size_t target_index = to.value();
199 if constexpr (std::is_same<LTS, probabilistic_lts_lts_t>::value)
200 {
202
203 // For probabilistic lts it is necessary to add the state first (and use the returned index).
204 bool state_inserted;
205 std::tie(target_index, state_inserted) = probabilistic_states.insert(lts_state);
206
207 if (state_inserted)
208 {
209 std::size_t actual_index = lts.add_probabilistic_state(lts_state);
210 utilities::mcrl2_unused(actual_index);
211 assert(actual_index == target_index);
212 }
213 }
214
215 // Add the transition and update the number of states.
216 lts.add_transition(transition(from.value(), index, target_index));
217 number_of_states = std::max(number_of_states, std::max(from.value() + 1, to.value() + 1));
218
219 if (inserted)
220 {
221 std::size_t actual_index = lts.add_action(action);
222 utilities::mcrl2_unused(actual_index);
223 assert(actual_index == index);
224 }
225
226 }
227 else if(term == probabilistic_transition_mark())
228 {
229 if constexpr (std::is_same<LTS, probabilistic_lts_lts_t>::value)
230 {
232
233 stream >> from;
234 stream >> action;
235 stream >> to;
236
237 const auto [index, inserted] = multi_actions.insert(action);
238
239 // Compute the index of the probabilistic state.
240 const auto [to_index, state_inserted] = probabilistic_states.insert(to);
241
242 if (state_inserted)
243 {
244 std::size_t actual_index = lts.add_probabilistic_state(to);
245 utilities::mcrl2_unused(actual_index);
246 assert(actual_index == to_index);
247 }
248
249 lts.add_transition(transition(from.value(), index, to_index));
250
251 // Update the number of states
252 number_of_states = std::max(number_of_states, std::max(from.value() + 1, to_index + 1));
253
254 if (inserted)
255 {
256 std::size_t actual_index = lts.add_action(action);
257 utilities::mcrl2_unused(actual_index);
258 assert(actual_index == index);
259 }
260 }
261 else
262 {
263 throw mcrl2::runtime_error("Attempting to read a probabilistic LTS as a regular LTS.");
264 }
265 }
266 else if (term.type_is_list())
267 {
268 // Lists always represent state labels, only need to add the indices.
269 lts.add_state(reinterpret_cast<const state_label_lts&>(term));
270 }
271 else if (term == initial_state_mark())
272 {
273 // Read the initial state.
275 stream >> state;
276 initial_state = state;
277 }
278 else
279 {
280 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 if (initial_state)
286 {
287 // If the lts has no state labels, we need to add empty states labels.
288 lts.set_num_states(number_of_states, lts.has_state_info());
289
290 set_initial_state(lts, initial_state.value());
291 }
292 else
293 {
294 throw mcrl2::runtime_error("Missing initial state in labelled transition system (LTS) stream.");
295 }
296}
297
298template <class LTS_TRANSITION_SYSTEM>
299static 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 std::ifstream fstream;
306 if (!filename.empty())
307 {
308 fstream.open(filename, std::ifstream::in | std::ifstream::binary);
309 if (fstream.fail())
310 {
311 if (filename.empty())
312 {
313 throw mcrl2::runtime_error("Fail to open standard input to read an lts.");
314 }
315 else
316 {
317 throw mcrl2::runtime_error("Fail to open file " + filename + " to read an lts.");
318 }
319 }
320 }
321
322 try
323 {
324 atermpp::binary_aterm_istream stream(filename.empty() ? std::cin : fstream);
325 stream >> lts;
326 }
327 catch (const std::exception& ex)
328 {
329 mCRL2log(log::error) << ex.what() << "\n";
330 if (filename.empty())
331 {
332 throw mcrl2::runtime_error("Fail to correctly read an lts from standard input.");
333 }
334 else
335 {
336 throw mcrl2::runtime_error("Fail to correctly read an lts from the file " + filename + ".");
337 }
338 }
339}
340
342{
343 stream << detail::initial_state_mark();
344 stream << lts.initial_probabilistic_state();
345}
346
348{
349 stream << detail::initial_state_mark();
351}
352
353template <class LTS>
354static 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 write_lts_header(stream,
362 lts.data(),
363 lts.process_parameters(),
364 lts.action_label_declarations());
365
366 for (const transition& trans : lts.get_transitions())
367 {
369
370 if constexpr (std::is_same<LTS, probabilistic_lts_lts_t>::value)
371 {
372 write_transition(stream, trans.from(), label, lts.probabilistic_state(trans.to()));
373 }
374 else
375 {
376 write_transition(stream, trans.from(), label, trans.to());
377 }
378 }
379
380 if (lts.has_state_info())
381 {
382 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 stream << lts.state_label(i);
386 }
387 }
388
389 // Write the initial state.
390 write_initial_state(stream, lts);
391}
392
393template <class LTS_TRANSITION_SYSTEM>
394static 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 bool to_stdout = filename.empty() || filename == "-";
401 std::ofstream fstream;
402 if (!to_stdout)
403 {
404 fstream.open(filename, std::ofstream::out | std::ofstream::binary);
405 if (fstream.fail())
406 {
407 throw mcrl2::runtime_error("Fail to open file " + filename + " for writing.");
408 }
409 }
410
411 try
412 {
413 atermpp::binary_aterm_ostream stream(to_stdout ? std::cout : fstream);
414 stream << lts;
415 }
416 catch (const std::exception& ex)
417 {
418 mCRL2log(log::error) << ex.what() << "\n";
419 throw mcrl2::runtime_error("Fail to write lts correctly to the file " + filename + ".");
420 }
421}
422
423} // namespace detail
424
425// Implementation of public functions.
426
428{
429 read_lts(stream, lts);
430 return stream;
431}
432
434{
435 read_lts(stream, lts);
436 return stream;
437}
438
440{
441 detail::write_lts(stream, lts);
442 return stream;
443}
444
446{
447 detail::write_lts(stream, lts);
448 return stream;
449}
450
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).
458
459 // Write the header of the lts.
461 stream << data_spec;
462 stream << parameters;
463 stream << action_labels;
464}
465
466void write_transition(atermpp::aterm_ostream& stream, std::size_t from, const lps::multi_action& label, std::size_t to)
467{
468 stream << detail::transition_mark();
469 stream << atermpp::aterm_int(from);
470 stream << label;
471 stream << atermpp::aterm_int(to);
472}
473
475{
476 if (to.size() <= 1)
477 {
478 // Actually a non probabilistic transition.
479 write_transition(stream, from, label, to.get());
480 }
481 else
482 {
484 stream << atermpp::aterm_int(from);
485 stream << label;
486 stream << to;
487 }
488}
489
491{
492 // During reading we assume that state labels are the only aterm_list.
493 stream << label;
494}
495
496void write_initial_state(atermpp::aterm_ostream& stream, std::size_t index)
497{
498 stream << detail::initial_state_mark();
500}
501
502void probabilistic_lts_lts_t::save(const std::string& filename) const
503{
504 mCRL2log(log::verbose) << "Starting to save a probabilistic lts to the file " << filename << ".\n";
505 detail::write_to_lts(*this, filename);
506}
507
508void lts_lts_t::save(std::string const& filename) const
509{
510 mCRL2log(log::verbose) << "Starting to save an lts to the file " << filename << ".\n";
511 detail::write_to_lts(*this, filename);
512}
513
514void probabilistic_lts_lts_t::load(const std::string& filename)
515{
516 mCRL2log(log::verbose) << "Starting to load a probabilistic lts from the file " << filename << ".\n";
517 detail::read_from_lts(*this, filename);
518}
519
520void lts_lts_t::load(const std::string& filename)
521{
522 mCRL2log(log::verbose) << "Starting to load an lts from the file " << filename << ".\n";
523 detail::read_from_lts(*this, filename);
524}
525
526} // namespace mcrl2::lts
An integer term stores a single std::size_t value. It carries no arguments.
Definition aterm_int.h:25
std::size_t value() const noexcept
Provide the value stored in an aterm.
Definition aterm_int.h:53
The interface for a class that reads aterm from a stream. The default constructed term aterm() indica...
Definition aterm_io.h:59
virtual void get(aterm &t)=0
Reads an aterm from this stream.
The interface for a class that writes aterm to a stream. Every written term is retrieved by the corre...
Definition aterm_io.h:48
A helper class to restore the state of the aterm_{i,o}stream objects upon destruction....
Definition aterm_io.h:84
The aterm base class that provides protection of the underlying shared terms.
Definition aterm.h:186
Reads terms from a stream in the steamable binary aterm format.
Writes terms in a streamable binary aterm format to an output stream.
Read-only balanced binary tree of terms.
size_type size() const
Returns the size of the term_balanced_tree.
bool type_is_list() const noexcept
Dynamic check whether the term is an aterm_list.
Definition aterm.h:76
bool defined() const
Returns true if this term is not equal to the term assigned by the default constructor of aterms,...
Definition aterm.h:147
\brief A timed multi-action
This class contains labels for probabilistic transistions, consisting of a numerator and a denumerato...
A class containing the values for action labels for the .lts format.
Definition lts_lts.h:137
This class contains labelled transition systems in .lts format.
Definition lts_lts.h:374
void save(const std::string &filename) const
Save the labelled transition system to file.
void load(const std::string &filename)
Load the labelled transition system from file.
A class that contains a labelled transition system.
Definition lts.h:83
states_size_type num_state_labels() const
Gets the number of state labels of this LTS.
Definition lts.h:271
void add_transition(const transition &t)
Add a transition to the lts.
Definition lts.h:544
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
ACTION_LABEL_T action_label(const labels_size_type action) const
Gets the label of an action.
Definition lts.h:470
bool has_state_info() const
Checks whether this LTS has state values associated with its states.
Definition lts.h:636
void set_initial_state(const states_size_type state)
Sets the initial state number of this LTS.
Definition lts.h:334
labels_size_type apply_hidden_label_map(const labels_size_type action) const
If the action label is registered hidden, it returns tau, otherwise the original label.
Definition lts.h:438
STATE_LABEL_T state_label(const states_size_type state) const
Gets the label of a state.
Definition lts.h:450
states_size_type add_state(const STATE_LABEL_T &label=STATE_LABEL_T())
Adds a state to this LTS.
Definition lts.h:347
const std::vector< transition > & get_transitions() const
Gets a const reference to the vector of transitions of the current lts.
Definition lts.h:526
states_size_type initial_state() const
Gets the initial state number of this LTS.
Definition lts.h:326
labels_size_type add_action(const ACTION_LABEL_T &label)
Adds an action with a label to this LTS.
Definition lts.h:361
This class contains probabilistic labelled transition systems in .lts format.
Definition lts_lts.h:402
void load(const std::string &filename)
Load the labelled transition system from file.
void save(const std::string &filename) const
Save the labelled transition system to file.
std::size_t size() const
Gets the number of probabilistic states in the vector representation of this state....
STATE get() const
Get a probabilistic state if is is simple, i.e., consists of a single state.
This class contains state labels for an labelled transition system in .lts format.
Definition lts_lts.h:40
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
A set that assigns each element an unique index.
Definition indexed_set.h:33
std::pair< size_type, bool > insert(const key_type &key, std::size_t thread_index=0)
Insert a key in the indexed set and return its index.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
This include file contains routines to read and write labelled transitions from and to files and from...
This file contains a class that contains labelled transition systems in lts (mcrl2) format.
The main namespace for the aterm++ library.
Definition algorithm.h:21
atermpp::aterm_appl add_index_impl(const atermpp::aterm_appl &x)
Definition io.h:39
atermpp::aterm_appl remove_index_impl(const atermpp::aterm_appl &x)
Definition io.h:28
atermpp::aterm_istream & operator>>(atermpp::aterm_istream &stream, data_specification &spec)
Reads a data specification from a stream.
Definition data_io.cpp:66
std::ostream & operator<<(std::ostream &out, const abstraction &x)
Definition abstraction.h:94
@ verbose
Definition logger.h:35
atermpp::term_balanced_tree< data::data_expression > state
Definition state.h:24
static const atermpp::aterm_appl & labelled_transition_system_mark()
static void set_initial_state(lts_lts_t &lts, const probabilistic_lts_lts_t::probabilistic_state_t &initial_state)
static void write_to_lts(const LTS_TRANSITION_SYSTEM &lts, const std::string &filename)
static const atermpp::aterm_appl & transition_mark()
static void write_lts(atermpp::aterm_ostream &stream, const LTS &lts)
static const atermpp::aterm_appl & initial_state_mark()
static void read_from_lts(LTS_TRANSITION_SYSTEM &lts, const std::string &filename)
static void read_lts(atermpp::aterm_istream &stream, LTS &lts)
static const atermpp::aterm_appl & probabilistic_transition_mark()
The main LTS namespace.
std::size_t to(const outgoing_pair_t &p)
Target state of a label state pair.
void write_lts_header(atermpp::aterm_ostream &stream, const data::data_specification &data, const data::variable_list &parameters, const process::action_label_list &action_labels)
Writes the start of an LTS stream.
void write_initial_state(atermpp::aterm_ostream &stream, std::size_t index)
Write the initial state to the LTS stream.
void write_state_label(atermpp::aterm_ostream &stream, const state_label_lts &label)
Write a state label to the LTS stream.
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.
void write_transition(atermpp::aterm_ostream &stream, std::size_t from, const lps::multi_action &label, std::size_t to)
Write a transition to the LTS stream.
void mcrl2_unused(T &&...)
Function that can be used to silence unused parameter warnings.
Definition unused.h:20