No Matches
Go to the documentation of this file.
1// Author(s): Muck van Weerdenburg, Jan Friso Groote
2// Copyright: see the accompanying file COPYING or copy at
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
19#ifndef MCRL2_LTS_LTS_IO_H
20#define MCRL2_LTS_LTS_IO_H
22#include "mcrl2/lps/io.h"
27namespace mcrl2::lts
36namespace detail
45lts_type guess_format(std::string const& s, const bool be_verbose=true);
57lts_type parse_format(std::string const& s);
63std::string string_for_type(const lts_type type);
69std::string extension_for_type(const lts_type type);
75std::string mime_type_for_type(const lts_type type);
79const std::set<lts_type>& supported_lts_formats();
89std::string supported_lts_formats_text(lts_type default_format = lts_none, const std::set<lts_type>& supported = supported_lts_formats());
97std::string supported_lts_formats_text(const std::set<lts_type>& supported);
105std::string lts_extensions_as_string(const std::string& sep = ",", const std::set<lts_type>& supported = supported_lts_formats());
112std::string lts_extensions_as_string(const std::set<lts_type>& supported);
115inline void read_lps_context(const std::string& data_file,
117 process::action_label_list& action_labels,
118 data::variable_list& process_parameters)
121 load_lps(spec, data_file);
122 data =;
123 action_labels = spec.action_labels();
124 process_parameters = spec.process().process_parameters();
127inline void read_data_context(const std::string& data_file,
129 process::action_label_list& action_labels)
131 // Add "init delta;" to the file to make the input a proper data specification.
132 // "init delta;" must appear at the front, such that a second init clause will be
133 // reported as wrong.
134 const std::string input="init delta; " + utilities::read_text(data_file);
138 action_labels=procspec.action_labels();
141inline void read_mcrl2_context(const std::string& data_file,
143 process::action_label_list& action_labels)
147 data =;
148 action_labels = procspec.action_labels();
151// converts an arbitrary lts to lts_lts_t
152template <class LTS_TYPE_IN, class LTS_TYPE_OUT>
153inline void convert_to_lts_lts(LTS_TYPE_IN& src,
154 LTS_TYPE_OUT& dest,
155 const data_file_type_t extra_data_file_type,
156 const std::string& extra_data_file_name)
158 std::string data_file;
160 process::action_label_list action_labels;
161 data::variable_list process_parameters;
162 bool extra_data_is_defined=true;
163 switch (extra_data_file_type)
164 {
165 case data_e:
166 {
167 read_data_context(extra_data_file_name,data,action_labels);
168 break;
169 }
170 case lps_e:
171 {
172 read_lps_context(extra_data_file_name,data,action_labels,process_parameters);
173 break;
174 }
175 case mcrl2_e:
176 {
177 read_mcrl2_context(extra_data_file_name,data,action_labels);
178 break;
179 }
180 default:
181 {
182 extra_data_is_defined = false;
183 mCRL2log(log::info) << "No data and action label specification is provided. Only the standard data types and no action labels can be used." << std::endl; break;
184 }
185 }
186 lts_convert(src, dest, data, action_labels, process_parameters, extra_data_is_defined);
188} // namespace detail
201template <class LTS_TYPE>
202inline void load_lts(LTS_TYPE& result,
203 const std::string& infilename,
204 lts_type type,
205 const data_file_type_t extra_data_file_type=none_e,
206 const std::string& extra_data_file_name="")
208 switch (type)
209 {
210 case lts_lts:
212 {
213 if (extra_data_file_type != none_e)
214 {
215 mCRL2log(log::warning) << "The lts file comes with a data specification. Ignoring the extra data and action label specification provided." << std::endl;
216 }
217 result.load(infilename);
218 break;
219 }
220 case lts_none:
221 mCRL2log(log::warning) << "Cannot determine type of input. Assuming .aut.\n";
222 [[fallthrough]]; // For the default (lts_none) load as aut file.
223 case lts_aut:
225 {
227 l.load(infilename);
228 convert_to_lts_lts(l, result,extra_data_file_type,extra_data_file_name);
229 break;
230 }
231 case lts_fsm:
233 {
235 l.load(infilename);
236 convert_to_lts_lts(l, result,extra_data_file_type,extra_data_file_name);
237 break;
238 }
239 case lts_dot:
240 {
241 throw mcrl2::runtime_error("Reading of .dot files is not supported anymore.");
242 }
243 }
253inline void load_lts_as_fsm_file(const std::string& path, lts_fsm_t& l)
255 const lts_type intype = mcrl2::lts::detail::guess_format(path);
256 switch (intype)
257 {
258 case lts_lts:
260 {
261 lts_lts_t l1;
262 l1.load(path);
264 return;
265 }
266 case lts_none:
267 mCRL2log(log::warning) << "Cannot determine type of input. Assuming .aut.\n";
268 [[fallthrough]]; // For the default (lts_none) load as aut file.
269 case lts_aut:
271 {
272 lts_aut_t l1;
273 l1.load(path);
275 return;
276 }
277 case lts_fsm:
279 {
280 l.load(path);
281 return;
282 }
283 case lts_dot:
284 {
285 throw mcrl2::runtime_error("Reading of dot files is not supported.");
286 }
287 }
290// Proper interface.
294atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, probabilistic_lts_lts_t& lts);
297atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const lts_lts_t& lts);
298atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const probabilistic_lts_lts_t& lts);
300// Streaming an LTS to disk:
301// write_lts_header(data_spec, parameters, action_labels)
303// In any order:
304// Write transitions (to, label, from), where 'to' and 'from' are indices and 'label' the multi_action, as necessary.
305// Write state labels (state_label_lts) in their order such that writing the i-th state label belongs to state with index i.
306// Write the initial state.
310 const data::data_specification& data,
311 const data::variable_list& parameters,
312 const process::action_label_list& action_labels);
315void write_transition(atermpp::aterm_ostream& stream, std::size_t from, const lps::multi_action& label, std::size_t to);
319void write_state_label(atermpp::aterm_ostream& stream, const state_label_lts& label);
322void write_initial_state(atermpp::aterm_ostream& stream, std::size_t index);
324} // namespace mcrl2::lts
326#endif // MCRL2_LTS_LTS_IO_H
The interface for a class that reads aterm from a stream. The default constructed term aterm() indica...
Definition aterm_io.h:59
The interface for a class that writes aterm to a stream. Every written term is retrieved by the corre...
Definition aterm_io.h:48
const data::variable_list & process_parameters() const
Returns the sequence of process parameters.
\brief A timed multi-action
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 simple labelled transition format with only strings as action labels.
Definition lts_aut.h:70
void load(const std::string &filename)
Load the labelled transition system from a file.
The class lts_fsm_t contains labelled transition systems in .fsm format.
Definition lts_fsm.h:248
void load(const std::string &filename)
Save the labelled transition system to file.
This class contains labelled transition systems in .lts format.
Definition lts_lts.h:374
void load(const std::string &filename)
Load the labelled transition system from file.
A simple labelled transition format with only strings as action labels.
Definition lts_aut.h:103
void load(const std::string &filename)
Load the labelled transition system from a file.
The class lts_fsm_t contains labelled transition systems in .fsm format.
Definition lts_fsm.h:276
void load(const std::string &filename)
Save the labelled transition system to file.
Process specification consisting of a data specification, action labels, a sequence of process equati...
const data::data_specification & data() const
Returns the data specification.
const process::action_label_list & action_labels() const
Returns the action label specification.
Standard exception class for reporting runtime errors.
Definition exception.h:27
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
IO routines for linear process specifications.
This file contains lts_convert routines that translate different lts formats into each other.
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
@ warning
Definition logger.h:32
void read_mcrl2_context(const std::string &data_file, data::data_specification &data, process::action_label_list &action_labels)
Definition lts_io.h:141
void read_lps_context(const std::string &data_file, data::data_specification &data, process::action_label_list &action_labels, data::variable_list &process_parameters)
Definition lts_io.h:115
void read_data_context(const std::string &data_file, data::data_specification &data, process::action_label_list &action_labels)
Definition lts_io.h:127
void lts_convert(const lts< STATE_LABEL1, ACTION_LABEL1, LTS_BASE1 > &lts_in, lts< STATE_LABEL2, ACTION_LABEL2, LTS_BASE2 > &lts_out)
lts_type guess_format(std::string const &s, const bool be_verbose=true)
Determines the LTS format from a filename by its extension.
Definition liblts.cpp:26
void convert_to_lts_lts(LTS_TYPE_IN &src, LTS_TYPE_OUT &dest, const data_file_type_t extra_data_file_type, const std::string &extra_data_file_name)
Definition lts_io.h:153
The main LTS namespace.
void load_lts(LTS_TYPE &result, const std::string &infilename, lts_type type, const data_file_type_t extra_data_file_type=none_e, const std::string &extra_data_file_name="")
Loads an lts of the indicated type, transforms it to an lts of the form lts_lts_t using the additiona...
Definition lts_io.h:202
The enumerated type lts_type contains an index for every type type of labelled transition system that...
Definition lts_type.h:37
@ lts_fsm_probabilistic
Definition lts_type.h:45
@ lts_lts_probabilistic
Definition lts_type.h:43
@ lts_aut_probabilistic
Definition lts_type.h:44
void load_lts_as_fsm_file(const std::string &path, lts_fsm_t &l)
Read a labelled transition system and return it in fsm format.
Definition lts_io.h:253
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.
Type for data files that contain extra information for an lts in .aut or .fsm format....
Definition lts_io.h:33
@ mcrl2_e
Definition lts_io.h:33
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.
process_specification parse_process_specification(std::istream &in)
Parses a process specification from an input stream.
Definition parse.h:43
std::string read_text(const std::string &filename, bool warn=false)
Read text from a file.