LCOV - code coverage report
Current view: top level - pbes/source - io.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 127 160 79.4 %
Date: 2024-03-08 02:52:28 Functions: 13 15 86.7 %
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/atermpp/aterm_io_binary.h"
      11             : #include "mcrl2/core/load_aterm.h"
      12             : #include "mcrl2/data/data_io.h"
      13             : #include "mcrl2/pbes/algorithms.h"
      14             : #include "mcrl2/pbes/detail/pbes_io.h"
      15             : #include "mcrl2/pbes/io.h"
      16             : #include "mcrl2/pbes/join.h"
      17             : #include "mcrl2/pbes/parse.h"
      18             : #include "mcrl2/pbes/normal_forms.h"
      19             : 
      20             : namespace mcrl2
      21             : {
      22             : 
      23             : namespace pbes_system
      24             : {
      25             : 
      26          29 : const std::vector<utilities::file_format>& pbes_file_formats()
      27             : {
      28          29 :   static std::vector<utilities::file_format> result;
      29          29 :   if (result.empty())
      30             :   {
      31           2 :     result.push_back(utilities::file_format("pbes", "PBES in internal format", false));
      32           2 :     result.back().add_extension("pbes");
      33           2 :     result.push_back(utilities::file_format("text", "PBES in textual (mCRL2) format", true));
      34           2 :     result.back().add_extension("txt");
      35           2 :     result.push_back(utilities::file_format("bes", "BES in internal format", false));
      36           2 :     result.back().add_extension("bes");
      37           2 :     result.push_back(utilities::file_format("pgsolver", "BES in PGSolver format", true));
      38           2 :     result.back().add_extension("gm");
      39           2 :     result.back().add_extension("pg");
      40             :   }
      41          29 :   return result;
      42             : }
      43             : 
      44             : /// \brief Save a PBES in the format specified.
      45             : /// \param pbes The PBES to be stored
      46             : /// \param stream The stream to which the output is saved.
      47             : /// \param format Determines the format in which the result is written. If unspecified, or
      48             : ///        pbes_file_unknown is specified, then a default format is chosen.
      49           4 : void save_pbes(const pbes& pbes,
      50             :                std::ostream& stream,
      51             :                utilities::file_format format)
      52             : {
      53           4 :   if (format == utilities::file_format())
      54             :   {
      55           1 :     format = pbes_format_internal();
      56             :   }
      57           4 :   mCRL2log(log::verbose) << "Saving result in " << format.shortname() << " format..." << std::endl;
      58           4 :   if (format == pbes_format_internal() || (format == pbes_format_internal_bes() && pbes_system::algorithms::is_bes(pbes)))
      59             :   {
      60           3 :     atermpp::binary_aterm_ostream(stream) << pbes;
      61             :   }
      62           1 :   else if (format == pbes_format_pgsolver() && pbes_system::algorithms::is_bes(pbes))
      63             :   {
      64           0 :     save_bes_pgsolver(pbes, stream);
      65             :   }
      66           1 :   else if (format == pbes_format_text())
      67             :   {
      68           1 :     stream << pp(pbes);
      69             :   }
      70             :   else
      71             :   {
      72           0 :     throw mcrl2::runtime_error("Trying to save PBES in non-PBES format (" + format.shortname() + ")");
      73             :   }
      74           4 : }
      75             : 
      76             : /// \brief Load a PBES from file.
      77             : /// \param pbes The PBES to which the result is loaded.
      78             : /// \param stream The stream from which to load the PBES.
      79             : /// \param format The format that should be assumed for the file in infilename. If unspecified, or
      80             : ///        pbes_file_unknown is specified, then a default format is chosen.
      81             : /// \param source The source from which the stream originates. Used for error messages.
      82           6 : void load_pbes(pbes& pbes, std::istream& stream, utilities::file_format format, const std::string& /*source*/)
      83             : {
      84           6 :   if (format == utilities::file_format())
      85             :   {
      86           2 :     format = pbes_format_internal();
      87             :   }
      88           6 :   mCRL2log(log::verbose) << "Loading PBES in " << format.shortname() << " format..." << std::endl;
      89           6 :   if (format == pbes_format_internal() || format == pbes_format_internal_bes())
      90             :   {
      91           5 :     atermpp::binary_aterm_istream(stream) >> pbes;
      92             :   }
      93             :   else
      94           1 :   if (format == pbes_format_text())
      95             :   {
      96           1 :     stream >> pbes;
      97             :   }
      98             :   else
      99             :   {
     100           0 :     throw mcrl2::runtime_error("Trying to load PBES from non-PBES format (" + format.shortname() + ")");
     101             :   }
     102           5 : }
     103             : 
     104             : /// \brief save_pbes Saves a PBES to a file.
     105             : /// \param pbes The PBES to save.
     106             : /// \param filename The file to save the PBES in.
     107             : /// \param format The format in which to save the PBES.
     108             : /// \param welltypedness_check If set to false, skips checking whether pbes is well typed before
     109             : ///                            saving it to file.
     110             : ///
     111             : /// The format of the file in infilename is guessed if format is not given or if it is equal to
     112             : /// utilities::file_format().
     113           4 : void save_pbes(const pbes& pbes, const std::string& filename,
     114             :                utilities::file_format format,
     115             :                bool welltypedness_check)
     116             : {
     117           4 :   if (welltypedness_check)
     118             :   {
     119           4 :     assert(pbes.is_well_typed());
     120             :   }
     121           4 :   if (format == utilities::file_format())
     122             :   {
     123           2 :     format = guess_format(filename);
     124             :   }
     125             : 
     126           4 :   if (filename.empty())
     127             :   {
     128           0 :     save_pbes(pbes, std::cout, format);
     129             :   }
     130             :   else
     131             :   {
     132           4 :     std::ofstream filestream(filename,(format.text_format()?std::ios_base::out: std::ios_base::binary));
     133           4 :     if (!filestream.good())
     134             :     {
     135           0 :       throw mcrl2::runtime_error("Could not open file " + filename);
     136             :     }
     137           4 :     save_pbes(pbes, filestream, format);
     138           4 :   }
     139           4 : }
     140             : 
     141             : /// \brief Load pbes from file.
     142             : /// \param pbes The pbes to which the result is loaded.
     143             : /// \param filename The file from which to load the PBES.
     144             : /// \param format The format in which the PBES is stored in the file.
     145             : ///
     146             : /// The format of the file in infilename is guessed if format is not given or if it is equal to
     147             : /// utilities::file_format().
     148           7 : void load_pbes(pbes& pbes,
     149             :                const std::string& filename,
     150             :                utilities::file_format format)
     151             : {
     152           7 :   if (format == utilities::file_format())
     153             :   {
     154           5 :     format = guess_format(filename);
     155             :   }
     156           7 :   if (filename.empty())
     157             :   {
     158           0 :     load_pbes(pbes, std::cin, format);
     159             :   }
     160             :   else
     161             :   {
     162           7 :     std::ifstream filestream(filename,(format.text_format()?std::ios_base::in: std::ios_base::binary));
     163           7 :     if (!filestream.good())
     164             :     {
     165           1 :       throw mcrl2::runtime_error("Could not open file " + filename);
     166             :     }
     167           8 :     load_pbes(pbes, filestream, format, core::detail::file_source(filename));
     168           7 :   }
     169           5 : }
     170             : 
     171             : // transforms DataVarId to DataVarIdNoIndex
     172             : // transforms OpId to OpIdNoIndex
     173             : // transforms PropVarInst to PropVarInstNoIndex
     174         352 : static atermpp::aterm_appl remove_index_impl(const atermpp::aterm_appl& x)
     175             : {
     176         352 :   if (x.function() == core::detail::function_symbol_OpId())
     177             :   {
     178          54 :     return atermpp::aterm_appl(core::detail::function_symbol_OpIdNoIndex(), x.begin(), --x.end());
     179             :   }
     180         325 :   return x;
     181             : }
     182             : 
     183             : // transforms DataVarIdNoIndex to DataVarId (obsolete)
     184             : // transforms OpIdNoIndex to OpId
     185             : // transforms PropVarInstNoIndex to PropVarInst (obsolete)
     186         306 : static atermpp::aterm_appl add_index_impl(const atermpp::aterm_appl& x)
     187             : {
     188         306 :   if (x.function() == core::detail::function_symbol_DataVarIdNoIndex())
     189             :   {
     190           0 :     const data::variable& y = reinterpret_cast<const data::variable&>(x);
     191           0 :     return data::variable(y.name(), y.sort());
     192             :   }
     193         306 :   else if (x.function() == core::detail::function_symbol_OpIdNoIndex())    // This should be removed in due time. Say 2025.
     194             :   {
     195          24 :     const data::function_symbol& y = reinterpret_cast<const data::function_symbol&>(x);
     196          24 :     return data::function_symbol(y.name(), y.sort());
     197             :   }
     198         282 :   else if (x.function() == core::detail::function_symbol_PropVarInstNoIndex())    // This should be removed in due time. Say 2025. 
     199             :   {
     200           0 :     const pbes_system::propositional_variable_instantiation& y = reinterpret_cast<const pbes_system::propositional_variable_instantiation&>(x);
     201           0 :     return pbes_system::propositional_variable_instantiation(y.name(), y.parameters());
     202             :   }
     203         282 :   return x;
     204             : }
     205             : 
     206           6 : inline atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const pbes_equation& equation)
     207             : {
     208           6 :   stream << equation.symbol();
     209           6 :   stream << equation.variable();
     210           6 :   stream << equation.formula();
     211           6 :   return stream;
     212             : }
     213             : 
     214           9 : inline atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, pbes_equation& equation)
     215             : {
     216           9 :   fixpoint_symbol symbol;
     217           9 :   propositional_variable var;
     218           9 :   pbes_expression expression;
     219             : 
     220           9 :   stream >> symbol;
     221           9 :   stream >> var;
     222           9 :   stream >> expression;
     223             : 
     224           9 :   equation = pbes_equation(symbol, var, expression);
     225             : 
     226           9 :   return stream;
     227           9 : }
     228             : 
     229           7 : atermpp::aterm pbes_marker()
     230             : {
     231           7 :   return atermpp::aterm_appl(atermpp::function_symbol("parameterised_boolean_equation_system", 0));
     232             : }
     233             : 
     234           3 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const pbes& pbes)
     235             : {
     236           3 :   atermpp::aterm_stream_state state(stream);
     237           3 :   stream << remove_index_impl;
     238             : 
     239           3 :   stream << pbes_marker();
     240           3 :   stream << pbes.data();
     241           3 :   stream << pbes.global_variables();
     242           3 :   stream << pbes.equations();
     243           3 :   stream << pbes.initial_state();
     244           3 :   return stream;
     245           3 : }
     246             : 
     247           4 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, pbes& pbes)
     248             : {
     249           4 :   atermpp::aterm_stream_state state(stream);
     250           4 :   stream >> add_index_impl;
     251             : 
     252             :   try
     253             :   {
     254           4 :     atermpp::aterm marker;
     255           4 :     stream >> marker;
     256             : 
     257           4 :     if (marker != pbes_marker())
     258             :     {
     259           0 :       throw mcrl2::runtime_error("Stream does not contain a parameterised boolean equation system (PBES).");
     260             :     }
     261             : 
     262           4 :     data::data_specification data;
     263           4 :     std::set<data::variable> global_variables;
     264           4 :     std::vector<pbes_equation> equations;
     265           4 :     propositional_variable_instantiation initial_state;
     266             : 
     267           4 :     stream >> data;
     268           4 :     stream >> global_variables;
     269           4 :     stream >> equations;
     270           4 :     stream >> initial_state;
     271             : 
     272           4 :     pbes = pbes_system::pbes(data, global_variables, equations, initial_state);
     273             : 
     274             :     // Add all the sorts that are used in the specification
     275             :     // to the data specification. This is important for those
     276             :     // sorts that are built in, because these are not explicitly
     277             :     // declared.
     278           4 :     complete_data_specification(pbes);
     279           4 :   }
     280           0 :   catch (std::exception& ex)
     281             :   {
     282           0 :     mCRL2log(log::error) << ex.what() << "\n";
     283           0 :     throw mcrl2::runtime_error(std::string("Error reading parameterised boolean equation system (PBES)."));
     284           0 :   }
     285             : 
     286           4 :   return stream;
     287           4 : }
     288             : 
     289             : namespace detail
     290             : {
     291             : 
     292           0 : pbes load_pbes(const std::string& filename)
     293             : {
     294           0 :   pbes result;
     295           0 :   if (filename.empty())
     296             :   {
     297           0 :     atermpp::binary_aterm_istream(std::cin) >> result;
     298             :   }
     299             :   else
     300             :   {
     301           0 :     std::ifstream from(filename, std::ifstream::in | std::ifstream::binary);
     302           0 :     atermpp::binary_aterm_istream(from) >> result;
     303           0 :   }
     304           0 :   return result;
     305           0 : }
     306             : 
     307           0 : void save_pbes(const pbes& pbesspec, const std::string& filename)
     308             : {
     309           0 :   if (filename.empty())
     310             :   {
     311           0 :     atermpp::binary_aterm_ostream(std::cout) << pbesspec;
     312             :   }
     313             :   else
     314             :   {
     315           0 :     std::ofstream to(filename, std::ofstream::out | std::ofstream::binary);
     316           0 :     if (!to.good())
     317             :     {
     318           0 :       throw mcrl2::runtime_error("Could not write to filename " + filename);
     319             :     }
     320           0 :     atermpp::binary_aterm_ostream(to) << pbesspec;
     321           0 :   }
     322           0 : }
     323             : 
     324             : } // namespace detail
     325             : 
     326             : /// \brief Conversion to atermappl.
     327             : /// \return The PBES converted to aterm format.
     328         195 : atermpp::aterm_appl pbes_to_aterm(const pbes& p)
     329             : {
     330             :   atermpp::aterm_appl global_variables = atermpp::aterm_appl(core::detail::function_symbol_GlobVarSpec(),
     331         195 :                                                              data::variable_list(p.global_variables().begin(),
     332         390 :                                                                                  p.global_variables().end()));
     333             : 
     334         195 :   atermpp::aterm_list eqn_list;
     335         195 :   const std::vector<pbes_equation>& eqn = p.equations();
     336         784 :   for (auto i = eqn.rbegin(); i != eqn.rend(); ++i)
     337             :   {
     338         589 :     atermpp::aterm a = pbes_equation_to_aterm(*i);
     339         589 :     eqn_list.push_front(a);
     340         589 :   }
     341         195 :   atermpp::aterm_appl equations = atermpp::aterm_appl(core::detail::function_symbol_PBEqnSpec(), eqn_list);
     342         195 :   atermpp::aterm_appl initial_state = atermpp::aterm_appl(core::detail::function_symbol_PBInit(), p.initial_state());
     343         195 :   atermpp::aterm_appl result;
     344             : 
     345         390 :   result = atermpp::aterm_appl(core::detail::function_symbol_PBES(),
     346         390 :              data::detail::data_specification_to_aterm(p.data()),
     347             :              global_variables,
     348             :              equations,
     349         195 :              initial_state);
     350             : 
     351         390 :   return result;
     352         195 : }
     353             : 
     354             : } // namespace pbes_system
     355             : 
     356             : } // namespace mcrl2

Generated by: LCOV version 1.14