Line data Source code
1 : // Author(s): Sjoerd Cranen; simplified 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 mcrl2/lps/io.h 10 : /// \brief IO routines for linear process specifications. 11 : 12 : #ifndef MCRL2_LPS_IO_H 13 : #define MCRL2_LPS_IO_H 14 : 15 : #include "mcrl2/atermpp/aterm_io_binary.h" 16 : #include "mcrl2/lps/specification.h" 17 : #include "mcrl2/lps/stochastic_specification.h" 18 : 19 : #include <fstream> 20 : 21 : namespace mcrl2 22 : { 23 : 24 : namespace lps 25 : { 26 : 27 : /// \brief Writes LPS to the stream. 28 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const specification& spec); 29 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const stochastic_specification& spec); 30 : 31 : /// \brief Reads LPS from the stream. 32 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, specification& spec); 33 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, stochastic_specification& spec); 34 : 35 : /// \brief Save an LPS in the format specified. 36 : /// \param spec The LPS to be stored 37 : /// \param stream The stream to which the output is written. 38 : /// \param target A string indicating the target stream, used to print information. 39 : /// utilities::file_format::unknown() is specified, then a default format is chosen. 40 : /// 41 : template <typename Specification> 42 3 : void save_lps(const Specification& spec, std::ostream& stream, const std::string& target = "") 43 : { 44 3 : mCRL2log(log::verbose) << "Saving LPS" << (target.empty()?"":" to " + target) << ".\n"; 45 3 : atermpp::binary_aterm_ostream(stream) << spec; 46 3 : } 47 : 48 : /// \brief Load LPS from file. 49 : /// \param spec The LPS to which the result is loaded. 50 : /// \param stream The stream from which to load the LPS (it is assumed to have been opened in the 51 : /// right mode). 52 : /// \param source The source from which the stream originates. Used for error messages. 53 : template <typename Specification> 54 5 : void load_lps(Specification& spec, std::istream& stream, const std::string& source = "") 55 : { 56 5 : mCRL2log(log::verbose) << "Loading LPS" << (source.empty()?"":" from " + source) << ".\n"; 57 5 : atermpp::binary_aterm_istream(stream) >> spec; 58 5 : } 59 : 60 : /// \brief Saves an LPS to a file. 61 : /// \param spec The LPS to save. 62 : /// \param filename The file to save the LPS in. If empty, the file is written to stdout. 63 : template <typename Specification> 64 3 : void save_lps(const Specification& spec, const std::string& filename) 65 : { 66 3 : if (filename.empty() || filename == "-") 67 : { 68 0 : save_lps(spec, std::cout, "standard output"); 69 0 : return; 70 : } 71 : 72 3 : std::ofstream ofs(filename, std::ios_base::binary); 73 3 : if (!ofs.good()) 74 : { 75 0 : throw mcrl2::runtime_error("Could not open file " + filename + "."); 76 : } 77 3 : save_lps(spec, ofs, filename); 78 3 : } 79 : 80 : /// \brief Load LPS from file. 81 : /// \param spec The LPS to which the result is loaded. 82 : /// \param filename The file from which to load the LPS. If empty, the file is read from stdin. 83 : 84 : template <typename Specification> 85 5 : void load_lps(Specification& spec, const std::string& filename) 86 : { 87 5 : if (filename.empty() || filename == "-") 88 : { 89 0 : load_lps(spec, std::cin, "standard input"); 90 0 : return; 91 : } 92 : 93 5 : std::ifstream ifs(filename, std::ios_base::binary); 94 5 : if (!ifs.good()) 95 : { 96 0 : throw mcrl2::runtime_error("Could not open file " + filename + "."); 97 : } 98 5 : load_lps(spec, ifs, filename); 99 5 : } 100 : 101 : } // namespace lps 102 : 103 : } // namespace mcrl2 104 : 105 : #endif // MCRL2_LPS_IO_H