Line data    Source code

       1             : // Author(s): Maurice Laveaux
       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/utilities/platform.h"
      11             : 
      12             : #ifdef MCRL2_ENABLE_SYLVAN
      13             : 
      14             : #include "mcrl2/lps/symbolic_lts_io.h"
      15             : 
      16             : #include "mcrl2/atermpp/aterm_io.h"
      17             : #include "mcrl2/atermpp/aterm_io_binary.h"
      18             : #include "mcrl2/data/detail/io.h"
      19             : #include "mcrl2/data/data_io.h"
      20             : #include "mcrl2/symbolic/ldd_stream.h"
      21             : 
      22             : using namespace mcrl2;
      23             : 
      24             : namespace mcrl2::lps
      25             : {
      26             : 
      27           0 : static atermpp::aterm symbolic_labelled_transition_system_mark()
      28             : {
      29           0 :   return atermpp::aterm_appl(atermpp::function_symbol("symbolic_labelled_transition_system", 0));
      30             : }
      31             : 
      32           0 : std::ostream& operator<<(std::ostream& stream, const symbolic_lts& lts)
      33             : {
      34           0 :   std::shared_ptr<utilities::obitstream> bitstream = std::make_shared<utilities::obitstream>(stream);
      35             : 
      36           0 :   atermpp::binary_aterm_ostream aterm_stream(bitstream);
      37           0 :   symbolic::binary_ldd_ostream ldd_stream(bitstream);
      38             : 
      39             :   // We set the transformer for all other elements (transitions, state labels and the initial state).
      40           0 :   aterm_stream << data::detail::remove_index_impl;
      41             : 
      42           0 :   aterm_stream << symbolic_labelled_transition_system_mark();
      43           0 :   aterm_stream << lts.data_spec;
      44           0 :   aterm_stream << lts.process_parameters;
      45             : 
      46           0 :   ldd_stream << lts.initial_state;
      47           0 :   ldd_stream << lts.states;
      48             : 
      49             :   // Write the mapping from indices to terms.
      50           0 :   for (const auto& index : lts.data_index)
      51             :   {
      52           0 :     bitstream->write_integer(index.size());
      53             : 
      54           0 :     for (const auto& term : index)
      55             :     {
      56           0 :       aterm_stream << term;
      57             :     }
      58             :   }
      59             : 
      60             :   // Write the action label indices.
      61           0 :   bitstream->write_integer(lts.action_index.size());
      62           0 :   for (const auto& term : lts.action_index)
      63             :   {
      64           0 :     aterm_stream << term;
      65             :   }
      66             : 
      67             :   // Write the transition group information: read and write dependencies and the local transition relation.
      68           0 :   bitstream->write_integer(lts.summand_groups.size());
      69           0 :   for (const auto& group : lts.summand_groups)
      70             :   {
      71           0 :     bitstream->write_integer(group.read_parameters.size());
      72           0 :     for (const auto& parameter : group.read_parameters)
      73             :     {
      74           0 :       aterm_stream << parameter;
      75             :     }
      76             : 
      77           0 :     bitstream->write_integer(group.write_parameters.size());
      78           0 :     for (const auto& parameter : group.write_parameters)
      79             :     {
      80           0 :       aterm_stream << parameter;
      81             :     }
      82           0 :     ldd_stream << group.L;
      83             :   }
      84             : 
      85           0 :   return stream;
      86           0 : }
      87             : 
      88           0 : std::istream& operator>>(std::istream& stream, symbolic_lts& lts)
      89             : {
      90           0 :   std::shared_ptr<utilities::ibitstream> bitstream = std::make_shared<utilities::ibitstream>(stream);
      91             : 
      92           0 :   atermpp::binary_aterm_istream aterm_stream(bitstream);
      93           0 :   symbolic::binary_ldd_istream ldd_stream(bitstream);
      94             : 
      95             :   // We set the transformer for all other elements (transitions, state labels and the initial state).
      96           0 :   aterm_stream >> data::detail::add_index_impl;
      97             : 
      98           0 :   atermpp::aterm marker;
      99           0 :   aterm_stream >> marker;
     100             : 
     101           0 :   if (marker != symbolic_labelled_transition_system_mark())
     102             :   {
     103           0 :     throw mcrl2::runtime_error("Stream does not contain a symbolic labelled transition system (SLTS).");
     104             :   }
     105             : 
     106           0 :   aterm_stream >> lts.data_spec;
     107           0 :   aterm_stream >> lts.process_parameters;
     108           0 :   ldd_stream >> lts.initial_state;
     109           0 :   ldd_stream >> lts.states;
     110             : 
     111             :   // For every process parameter read the data index.
     112           0 :   lts.data_index.clear();
     113           0 :   for (const data::variable& parameter : lts.process_parameters)
     114             :   {
     115           0 :     lts.data_index.push_back(parameter.sort());
     116             : 
     117           0 :     std::size_t number_of_entries = bitstream->read_integer();
     118           0 :     for (std::size_t i = 0; i < number_of_entries; ++i)
     119             :     {
     120           0 :       data::data_expression value;
     121           0 :       aterm_stream >> value;
     122             : 
     123           0 :       auto [result, inserted] = lts.data_index.back().insert(value);
     124           0 :       assert(i == result); utilities::mcrl2_unused(result);
     125           0 :       assert(inserted); utilities::mcrl2_unused(inserted);
     126           0 :     }
     127             :   }
     128             : 
     129           0 :   std::size_t number_of_action_labels = bitstream->read_integer();
     130           0 :   lts.action_index.clear();
     131             : 
     132           0 :   for (std::size_t i = 0; i < number_of_action_labels; ++i)
     133             :   {
     134           0 :     lps::multi_action value;
     135           0 :     aterm_stream >> value;
     136             : 
     137           0 :     auto [result, inserted] = lts.action_index.insert(value);
     138           0 :     assert(i == result); utilities::mcrl2_unused(result);
     139           0 :     assert(inserted); utilities::mcrl2_unused(inserted);
     140           0 :   }
     141             : 
     142           0 :   std::size_t number_of_groups = bitstream->read_integer();
     143           0 :   lts.summand_groups.clear();
     144             : 
     145           0 :   for (std::size_t i = 0; i < number_of_groups; ++i)
     146             :   {
     147           0 :     std::size_t number_of_read = bitstream->read_integer();
     148           0 :     data::variable_vector read_parameters = std::vector<data::variable>(number_of_read);
     149             : 
     150           0 :     for (auto& parameter : read_parameters)
     151             :     {
     152           0 :       aterm_stream >> parameter;
     153             :     }
     154             : 
     155           0 :     std::size_t number_of_write = bitstream->read_integer();
     156           0 :     data::variable_vector write_parameters = std::vector<data::variable>(number_of_write);
     157             : 
     158           0 :     for (auto& parameter : write_parameters)
     159             :     {
     160           0 :       aterm_stream >> parameter;
     161             :     }
     162             : 
     163           0 :     lts.summand_groups.emplace_back(lts.process_parameters, read_parameters, write_parameters);
     164           0 :     ldd_stream >> lts.summand_groups.back().L;
     165           0 :   }
     166             : 
     167           0 :   return stream;
     168           0 : }
     169             : 
     170             : } // namespace mcrl2::lps
     171             : 
     172             : #endif // MCRL2_ENABLE_SYLVAN