Line data Source code
1 : // Author(s): anonymous 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/pbes/io.h 10 : /// \brief IO routines for boolean equation systems. 11 : 12 : #ifndef MCRL2_PBES_IO_H 13 : #define MCRL2_PBES_IO_H 14 : 15 : #include "mcrl2/pbes/pbes.h" 16 : #include "mcrl2/utilities/file_utility.h" 17 : 18 : namespace mcrl2 19 : { 20 : 21 : namespace pbes_system 22 : { 23 : 24 : void save_bes_pgsolver(const pbes& bes, std::ostream& stream, bool maxpg = true); 25 : 26 : const std::vector<utilities::file_format>& pbes_file_formats(); 27 : 28 : inline 29 : bool is_pbes_file_format(const utilities::file_format& format) 30 : { 31 : for (const utilities::file_format& i: pbes_file_formats()) 32 : { 33 : if (i == format) 34 : { 35 : return true; 36 : } 37 : } 38 : return false; 39 : } 40 : 41 : inline 42 15 : const utilities::file_format& pbes_format_internal() { return pbes_file_formats()[0]; } 43 : inline 44 4 : const utilities::file_format& pbes_format_text() { return pbes_file_formats()[1]; } 45 : inline 46 2 : const utilities::file_format& pbes_format_internal_bes() { return pbes_file_formats()[2]; } 47 : inline 48 1 : const utilities::file_format& pbes_format_pgsolver() { return pbes_file_formats()[3]; } 49 : 50 : inline 51 7 : const utilities::file_format guess_format(const std::string& filename) 52 : { 53 23 : for (const utilities::file_format& it : pbes_file_formats()) 54 : { 55 19 : if (it.matches(filename)) 56 : { 57 3 : return it; 58 : } 59 : } 60 4 : return utilities::file_format(); 61 : } 62 : 63 : /// \brief Save a PBES in the format specified. 64 : /// \param pbes The PBES to be stored 65 : /// \param stream The stream to which the output is saved. 66 : /// \param format Determines the format in which the result is written. If unspecified, or 67 : /// pbes_file_unknown is specified, then a default format is chosen. 68 : void save_pbes(const pbes& pbes, 69 : std::ostream& stream, 70 : utilities::file_format format = utilities::file_format()); 71 : 72 : /// \brief Load a PBES from file. 73 : /// \param pbes The PBES to which the result is loaded. 74 : /// \param stream The stream from which to load the PBES. 75 : /// \param format The format that should be assumed for the file in infilename. If unspecified, or 76 : /// pbes_file_unknown is specified, then a default format is chosen. 77 : /// \param source The source from which the stream originates. Used for error messages. 78 : void load_pbes(pbes& pbes, std::istream& stream, utilities::file_format format, const std::string& source = ""); 79 : 80 : /// \brief save_pbes Saves a PBES to a file. 81 : /// \param pbes The PBES to save. 82 : /// \param filename The file to save the PBES in. 83 : /// \param format The format in which to save the PBES. 84 : /// \param welltypedness_check If set to false, skips checking whether pbes is well typed before 85 : /// saving it to file. 86 : /// 87 : /// The format of the file in infilename is guessed if format is not given or if it is equal to 88 : /// utilities::file_format(). 89 : void save_pbes(const pbes& pbes, const std::string& filename, 90 : utilities::file_format format = utilities::file_format(), 91 : bool welltypedness_check = true); 92 : 93 : /// \brief Load pbes from file. 94 : /// \param pbes The pbes to which the result is loaded. 95 : /// \param filename The file from which to load the PBES. 96 : /// \param format The format in which the PBES is stored in the file. 97 : /// 98 : /// The format of the file in infilename is guessed if format is not given or if it is equal to 99 : /// utilities::file_format(). 100 : void load_pbes(pbes& pbes, 101 : const std::string& filename, 102 : utilities::file_format format = utilities::file_format()); 103 : 104 : } // namespace pbes_system 105 : 106 : } // namespace mcrl2 107 : 108 : #endif // MCRL2_PBES_IO_H