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/lps/io.h"
      11             : 
      12             : #include "mcrl2/lps/stochastic_specification.h"
      13             : #include "mcrl2/lps/specification.h"
      14             : 
      15             : namespace mcrl2::lps
      16             : {
      17             : 
      18           8 : atermpp::aterm linear_process_specification_marker()
      19             : {
      20           8 :   return atermpp::aterm_appl(atermpp::function_symbol("linear_process_specification", 0));
      21             : }
      22             : 
      23          12 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const multi_action& action)
      24             : {
      25          12 :   stream << action.actions();
      26          12 :   stream << action.time();
      27          12 :   return stream;
      28             : }
      29             : 
      30          23 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, multi_action& action)
      31             : {
      32          23 :   process::action_list actions;
      33          23 :   data::data_expression time;
      34             : 
      35          23 :   stream >> actions;
      36          23 :   stream >> time;
      37             : 
      38          23 :   action = multi_action(actions, time);
      39          23 :   return stream;
      40          23 : }
      41             : 
      42           1 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const deadlock_summand& summand)
      43             : {
      44           1 :   stream << summand.summation_variables();
      45           1 :   stream << summand.condition();
      46           1 :   stream << summand.deadlock().time();
      47           1 :   return stream;
      48             : }
      49             : 
      50           2 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, deadlock_summand& summand)
      51             : {
      52           2 :   data::variable_list summation_variables;
      53           2 :   data::data_expression condition;
      54           2 :   data::data_expression time;
      55             : 
      56           2 :   stream >> summation_variables;
      57           2 :   stream >> condition;
      58           2 :   stream >> time;
      59             : 
      60           2 :   summand = deadlock_summand(summation_variables, condition, lps::deadlock(time));
      61           2 :   return stream;
      62           2 : }
      63             : 
      64          12 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const stochastic_action_summand& summand)
      65             : {
      66          12 :   stream << summand.distribution();
      67          12 :   stream << summand.summation_variables();
      68          12 :   stream << summand.condition();
      69          12 :   stream << summand.multi_action();
      70          12 :   stream << summand.assignments();
      71          12 :   return stream;
      72             : }
      73             : 
      74          23 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, stochastic_action_summand& summand)
      75             : {
      76          23 :   stochastic_distribution distribution;
      77          23 :   data::variable_list summation_variables;
      78          23 :   data::data_expression condition;
      79          46 :   lps::multi_action multi_action;
      80          23 :   data::assignment_list assignments;
      81             : 
      82          23 :   stream >> distribution;
      83          23 :   stream >> summation_variables;
      84          23 :   stream >> condition;
      85          23 :   stream >> multi_action;
      86          23 :   stream >> assignments;
      87             : 
      88          46 :   summand = stochastic_action_summand(summation_variables,
      89             :     condition,
      90             :     multi_action,
      91             :     assignments,
      92          23 :     distribution);
      93          23 :   return stream;
      94          23 : }
      95             : 
      96             : template <typename ActionSummand>
      97           3 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const linear_process_base<ActionSummand>& lps)
      98             : {
      99           3 :   stream << lps.process_parameters();
     100           3 :   stream << lps.action_summands();
     101           3 :   stream << lps.deadlock_summands();
     102             : 
     103           3 :   return stream;
     104             : }
     105             : 
     106             : template <typename ActionSummand>
     107           5 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, linear_process_base<ActionSummand>& lps)
     108             : {
     109           5 :   data::variable_list process_parameters;
     110           5 :   deadlock_summand_vector deadlock_summands;
     111           5 :   std::vector<ActionSummand> action_summands;
     112             : 
     113           5 :   stream >> process_parameters;
     114           5 :   stream >> action_summands;
     115           5 :   stream >> deadlock_summands;
     116             : 
     117           5 :   lps = linear_process_base<ActionSummand>(process_parameters, deadlock_summands, action_summands);
     118           5 :   return stream;
     119           5 : }
     120             : 
     121             : static
     122           3 : void write_spec(atermpp::aterm_ostream& stream, const stochastic_specification& spec)
     123             : {
     124           3 :   atermpp::aterm_stream_state state(stream);
     125           3 :   stream << data::detail::remove_index_impl;
     126             : 
     127           3 :   stream << linear_process_specification_marker();
     128           3 :   stream << spec.data();
     129           3 :   stream << spec.action_labels();
     130           3 :   stream << spec.global_variables();
     131           3 :   stream << spec.process();
     132           3 :   stream << spec.initial_process();
     133           3 : }
     134             : 
     135             : static
     136           5 : void read_spec(atermpp::aterm_istream& stream, stochastic_specification& spec)
     137             : {
     138           5 :   atermpp::aterm_stream_state state(stream);
     139           5 :   stream >> data::detail::add_index_impl;
     140             : 
     141             :   try
     142             :   {
     143           5 :     atermpp::aterm marker;
     144           5 :     stream >> marker;
     145             : 
     146           5 :     if (marker != linear_process_specification_marker())
     147             :     {
     148           0 :       throw mcrl2::runtime_error("Stream does not contain a linear process specification (LPS).");
     149             :     }
     150             : 
     151           5 :     data::data_specification data;
     152           5 :     process::action_label_list action_labels;
     153           5 :     std::set<data::variable> global_variables;
     154           5 :     stochastic_linear_process process;
     155           5 :     stochastic_process_initializer initial_process;
     156             : 
     157           5 :     stream >> data;
     158           5 :     stream >> action_labels;
     159           5 :     stream >> global_variables;
     160           5 :     stream >> process;
     161           5 :     stream >> initial_process;
     162           5 :     spec = stochastic_specification(data, action_labels, global_variables, process, initial_process);
     163           5 :   }
     164           0 :   catch (std::exception& ex)
     165             :   {
     166           0 :     mCRL2log(log::error) << ex.what() << "\n";
     167           0 :     throw mcrl2::runtime_error(std::string("Error reading linear process specification (LPS)."));
     168           0 :   }
     169           5 : }
     170             : 
     171           3 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const specification& spec)
     172             : {
     173           3 :   write_spec(stream, stochastic_specification(spec));
     174           3 :   return stream;
     175             : }
     176             : 
     177           0 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const stochastic_specification& spec)
     178             : {
     179           0 :   write_spec(stream, spec);
     180           0 :   return stream;
     181             : }
     182             : 
     183           5 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, lps::specification& spec)
     184             : {
     185           5 :   stochastic_specification stochastic_spec;
     186           5 :   read_spec(stream, stochastic_spec);
     187           5 :   spec = remove_stochastic_operators(stochastic_spec);
     188           5 :   return stream;
     189           5 : }
     190             : 
     191           0 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, lps::stochastic_specification& spec)
     192             : {
     193           0 :   read_spec(stream, spec);
     194           0 :   return stream;
     195             : }
     196             : 
     197             : } // namespace mcrl2::lps