LCOV - code coverage report
Current view: top level - pbes/source - io.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 72 79 91.1 %
Date: 2020-02-28 00:44:21 Functions: 10 10 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): anonymous, Thomas Neele
       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             : 
      10             : #include "mcrl2/core/load_aterm.h"
      11             : #include "mcrl2/data/data_io.h"
      12             : #include "mcrl2/pbes/algorithms.h"
      13             : #include "mcrl2/pbes/detail/io.h"
      14             : #include "mcrl2/pbes/io.h"
      15             : #include "mcrl2/pbes/parse.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace pbes_system
      21             : {
      22             : 
      23          27 : const std::vector<utilities::file_format>& pbes_file_formats()
      24             : {
      25          27 :   static std::vector<utilities::file_format> result;
      26          27 :   if (result.empty())
      27             :   {
      28           3 :     result.push_back(utilities::file_format("pbes", "PBES in internal format", false));
      29           3 :     result.back().add_extension("pbes");
      30           3 :     result.push_back(utilities::file_format("text", "PBES in textual (mCRL2) format", true));
      31           3 :     result.back().add_extension("txt");
      32             :   }
      33          27 :   return result;
      34             : }
      35             : 
      36             : 
      37             : /// \brief Save a PBES in the format specified.
      38             : /// \param pbes The PBES to be stored
      39             : /// \param stream The stream to which the output is saved.
      40             : /// \param format Determines the format in which the result is written. If unspecified, or
      41             : ///        pbes_file_unknown is specified, then a default format is chosen.
      42           4 : void save_pbes(const pbes& pbes,
      43             :                std::ostream& stream,
      44             :                utilities::file_format format)
      45             : {
      46           4 :   if (format == utilities::file_format())
      47             :   {
      48           1 :     format = pbes_format_internal();
      49             :   }
      50           4 :   mCRL2log(log::verbose) << "Saving result in " << format.shortname() << " format..." << std::endl;
      51           4 :   if (format == pbes_format_internal())
      52             :   {
      53           3 :     pbes.save(stream, true);
      54             :   }
      55             :   else
      56           1 :   if (format == pbes_format_text())
      57             :   {
      58           1 :     stream << pp(pbes);
      59             :   }
      60             :   else
      61             :   {
      62           0 :     throw mcrl2::runtime_error("Trying to save PBES in non-PBES format (" + format.shortname() + ")");
      63             :   }
      64           4 : }
      65             : 
      66             : /// \brief Load a PBES from file.
      67             : /// \param pbes The PBES to which the result is loaded.
      68             : /// \param stream The stream from which to load the PBES.
      69             : /// \param format The format that should be assumed for the file in infilename. If unspecified, or
      70             : ///        pbes_file_unknown is specified, then a default format is chosen.
      71             : /// \param source The source from which the stream originates. Used for error messages.
      72           6 : void load_pbes(pbes& pbes, std::istream& stream, utilities::file_format format, const std::string& source)
      73             : {
      74           6 :   if (format == utilities::file_format())
      75             :   {
      76           2 :     format = pbes_format_internal();
      77             :   }
      78           6 :   mCRL2log(log::verbose) << "Loading PBES in " << format.shortname() << " format..." << std::endl;
      79           6 :   if (format == pbes_format_internal())
      80             :   {
      81           5 :     pbes.load(stream, true, source);
      82             :   }
      83             :   else
      84           1 :   if (format == pbes_format_text())
      85             :   {
      86           1 :     stream >> pbes;
      87             :   }
      88             :   else
      89             :   {
      90           0 :     throw mcrl2::runtime_error("Trying to load PBES from non-PBES format (" + format.shortname() + ")");
      91             :   }
      92           5 : }
      93             : 
      94             : /// \brief save_pbes Saves a PBES to a file.
      95             : /// \param pbes The PBES to save.
      96             : /// \param filename The file to save the PBES in.
      97             : /// \param format The format in which to save the PBES.
      98             : /// \param welltypedness_check If set to false, skips checking whether pbes is well typed before
      99             : ///                            saving it to file.
     100             : ///
     101             : /// The format of the file in infilename is guessed if format is not given or if it is equal to
     102             : /// utilities::file_format().
     103           4 : void save_pbes(const pbes& pbes, const std::string& filename,
     104             :                utilities::file_format format,
     105             :                bool welltypedness_check)
     106             : {
     107           4 :   if (welltypedness_check)
     108             :   {
     109           4 :     assert(pbes.is_well_typed());
     110             :   }
     111           4 :   if (format == utilities::file_format())
     112             :   {
     113           2 :     format = guess_format(filename);
     114             :   }
     115             : 
     116           4 :   if (filename.empty())
     117             :   {
     118           0 :     save_pbes(pbes, std::cout, format);
     119             :   }
     120             :   else
     121             :   {
     122           8 :     std::ofstream filestream(filename,(format.text_format()?std::ios_base::out: std::ios_base::binary));
     123           4 :     if (!filestream.good())
     124             :     {
     125           0 :       throw mcrl2::runtime_error("Could not open file " + filename);
     126             :     }
     127           4 :     save_pbes(pbes, filestream, format);
     128             :   }
     129           4 : }
     130             : 
     131             : /// \brief Load pbes from file.
     132             : /// \param pbes The pbes to which the result is loaded.
     133             : /// \param filename The file from which to load the PBES.
     134             : /// \param format The format in which the PBES is stored in the file.
     135             : ///
     136             : /// The format of the file in infilename is guessed if format is not given or if it is equal to
     137             : /// utilities::file_format().
     138           7 : void load_pbes(pbes& pbes,
     139             :                const std::string& filename,
     140             :                utilities::file_format format)
     141             : {
     142           7 :   if (format == utilities::file_format())
     143             :   {
     144           5 :     format = guess_format(filename);
     145             :   }
     146           7 :  if (filename.empty())
     147             :   {
     148           0 :     load_pbes(pbes, std::cin, format);
     149             :   }
     150             :   else
     151             :   {
     152          14 :     std::ifstream filestream(filename,(format.text_format()?std::ios_base::in: std::ios_base::binary));
     153           7 :     if (!filestream.good())
     154             :     {
     155           1 :       throw mcrl2::runtime_error("Could not open file " + filename);
     156             :     }
     157           7 :     load_pbes(pbes, filestream, format, core::detail::file_source(filename));
     158             :   }
     159           5 : }
     160             : 
     161             : /// \brief Reads the parameterized boolean equation system from a stream.
     162             : /// \param stream The stream to read from.
     163             : /// \param binary An indicator whether the stream is binary or textual.
     164             : /// \param source The source from which the stream originates. Used for error messages.
     165           5 : void pbes::load(std::istream& stream, bool binary, const std::string& source)
     166             : {
     167          10 :   atermpp::aterm t = core::load_aterm(stream, binary, "PBES", source, pbes_system::detail::add_index_impl);
     168             : 
     169           4 :   if (!t.type_is_appl() || !core::detail::check_rule_PBES(atermpp::down_cast<atermpp::aterm_appl>(t)))
     170             :   {
     171           0 :     throw mcrl2::runtime_error("The loaded ATerm is not a PBES.");
     172             :   }
     173             : 
     174           4 :   init_term(atermpp::down_cast<atermpp::aterm_appl>(t));
     175           4 :   m_data.declare_data_specification_to_be_type_checked();
     176             : 
     177             :   // Add all the sorts that are used in the specification
     178             :   // to the data specification. This is important for those
     179             :   // sorts that are built in, because these are not explicitly
     180             :   // declared.
     181           4 :   complete_data_specification(*this);
     182             : 
     183             :   // The well typedness check is only done in debug mode, since for large
     184             :   // PBESs it takes too much time
     185           4 :   assert(is_well_typed());
     186           4 : }
     187             : 
     188             : /// \brief Writes the pbes to a stream.
     189             : /// \param stream The stream to which the pbes is written.
     190             : /// \param binary If binary is true the pbes is saved in compressed binary format.
     191             : /// Otherwise an ascii representation is saved. In general the binary format is
     192             : /// much more compact than the ascii representation.
     193           3 : void pbes::save(std::ostream& stream, bool binary) const
     194             : {
     195           3 :   if (binary)
     196             :   {
     197           3 :     atermpp::binary_aterm_ostream(stream) << pbes_system::detail::remove_index_impl << pbes_to_aterm(*this);
     198             :   }
     199             :   else
     200             :   {
     201           0 :     atermpp::text_aterm_ostream(stream) << pbes_system::detail::remove_index_impl << pbes_to_aterm(*this);
     202             :   }
     203           3 : }
     204             : 
     205             : /// \brief Conversion to atermappl.
     206             : /// \return The PBES converted to aterm format.
     207         186 : atermpp::aterm_appl pbes_to_aterm(const pbes& p)
     208             : {
     209             :   atermpp::aterm_appl global_variables = atermpp::aterm_appl(core::detail::function_symbol_GlobVarSpec(),
     210         372 :                                                              data::variable_list(p.global_variables().begin(),
     211         558 :                                                                                  p.global_variables().end()));
     212             : 
     213         372 :   atermpp::aterm_list eqn_list;
     214         186 :   const std::vector<pbes_equation>& eqn = p.equations();
     215         764 :   for (auto i = eqn.rbegin(); i != eqn.rend(); ++i)
     216             :   {
     217        1156 :     atermpp::aterm a = pbes_equation_to_aterm(*i);
     218         578 :     eqn_list.push_front(a);
     219             :   }
     220         372 :   atermpp::aterm_appl equations = atermpp::aterm_appl(core::detail::function_symbol_PBEqnSpec(), eqn_list);
     221         372 :   atermpp::aterm_appl initial_state = atermpp::aterm_appl(core::detail::function_symbol_PBInit(), p.initial_state());
     222         186 :   atermpp::aterm_appl result;
     223             : 
     224         186 :   result = atermpp::aterm_appl(core::detail::function_symbol_PBES(),
     225         372 :              data::detail::data_specification_to_aterm(p.data()),
     226             :              global_variables,
     227             :              equations,
     228             :              initial_state);
     229             : 
     230         372 :   return result;
     231             : }
     232             : 
     233             : } // namespace pbes_system
     234             : 
     235         126 : } // namespace mcrl2

Generated by: LCOV version 1.13