Line data    Source code

       1             : // Author(s): Wieger Wesselink
       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             : #ifndef MCRL2_LPS_STOCHASTIC_SPECIFICATION_H
      11             : #define MCRL2_LPS_STOCHASTIC_SPECIFICATION_H
      12             : 
      13             : #include "mcrl2/lps/specification.h"
      14             : #include "mcrl2/lps/stochastic_linear_process.h"
      15             : 
      16             : namespace mcrl2 {
      17             : 
      18             : namespace lps {
      19             : 
      20             : class stochastic_specification;
      21             : void complete_data_specification(stochastic_specification& spec);
      22             : 
      23             : // template function overloads
      24             : std::set<data::sort_expression> find_sort_expressions(const lps::stochastic_specification& x);
      25             : std::set<data::variable> find_all_variables(const lps::stochastic_specification& x);
      26             : std::set<data::variable> find_free_variables(const lps::stochastic_specification& x);
      27             : std::set<data::function_symbol> find_function_symbols(const lps::stochastic_specification& x);
      28             : std::set<core::identifier_string> find_identifiers(const lps::stochastic_specification& x);
      29             : 
      30             : // template function overloads
      31             : bool check_well_typedness(const stochastic_specification& x);
      32             : void normalize_sorts(stochastic_specification& x, const data::sort_specification& sortspec);
      33             : 
      34             : /// \brief Linear process specification.
      35             : class stochastic_specification: public specification_base<stochastic_linear_process, stochastic_process_initializer>
      36             : {
      37             :   protected:
      38             :     typedef specification_base<stochastic_linear_process, stochastic_process_initializer> super;
      39             : 
      40             :   public:
      41             :     /// \brief Constructor.
      42       14744 :     stochastic_specification()
      43       14744 :     { }
      44             : 
      45             :     /// \brief Constructor.
      46             :     /// \param data A data specification
      47             :     /// \param action_labels A sequence of action labels
      48             :     /// \param global_variables A set of global variables
      49             :     /// \param lps A linear process
      50             :     /// \param initial_process A process initializer
      51        1619 :     stochastic_specification(const data::data_specification& data,
      52             :                              const process::action_label_list& action_labels,
      53             :                              const std::set<data::variable>& global_variables,
      54             :                              const stochastic_linear_process& lps,
      55             :                              const stochastic_process_initializer& initial_process)
      56        1619 :       : super(data, action_labels, global_variables, lps, initial_process)
      57             :     {
      58        1619 :       complete_data_specification(*this);
      59        1619 :     }
      60             : 
      61             :     /// \brief Constructor. This constructor is explicit as implicit conversions of this kind is a source of bugs.
      62         279 :     explicit stochastic_specification(const specification& other)
      63         279 :       : super(other.data(), 
      64             :         other.action_labels(), 
      65             :         other.global_variables(), 
      66         558 :         stochastic_linear_process(other.process()),
      67         837 :         stochastic_process_initializer(other.initial_process().expressions(),stochastic_distribution()))
      68         279 :     { } 
      69             : };
      70             : 
      71             : //--- start generated class stochastic_specification ---//
      72             : // prototype declaration
      73             : std::string pp(const stochastic_specification& x);
      74             : 
      75             : /// \\brief Outputs the object to a stream
      76             : /// \\param out An output stream
      77             : /// \\param x Object x
      78             : /// \\return The output stream
      79             : inline
      80           1 : std::ostream& operator<<(std::ostream& out, const stochastic_specification& x)
      81             : {
      82           1 :   return out << lps::pp(x);
      83             : }
      84             : //--- end generated class stochastic_specification ---//
      85             : 
      86             : inline
      87          48 : bool operator==(const stochastic_specification& spec1, const stochastic_specification& spec2)
      88             : {
      89          48 :   return specification_to_aterm(spec1) == specification_to_aterm(spec2);
      90             : }
      91             : 
      92             : /// \brief Inequality operator
      93             : inline
      94          48 : bool operator!=(const stochastic_specification& spec1, const stochastic_specification& spec2)
      95             : {
      96          48 :   return !(spec1 == spec2);
      97             : }
      98             : 
      99             : std::string pp_with_summand_numbers(const stochastic_specification& x);
     100             : 
     101             : /// \brief Adds all sorts that appear in the process of l to the data specification of l.
     102             : /// \param spec A linear process specification
     103             : inline
     104        2506 : void complete_data_specification(stochastic_specification& spec)
     105             : {
     106        2506 :   std::set<data::sort_expression> s = lps::find_sort_expressions(spec);
     107        2506 :   spec.data().add_context_sorts(s);
     108        2506 : }
     109             : 
     110             : /// \brief Converts a stochastic specification to a specification. Throws an exception if
     111             : /// non-empty distributions are encountered.
     112             : inline
     113         398 : specification remove_stochastic_operators(const stochastic_specification& spec)
     114             : {
     115         398 :   specification result;
     116         398 :   result.data() = spec.data();
     117         398 :   result.action_labels() = spec.action_labels();
     118         398 :   result.global_variables() = spec.global_variables();
     119             : 
     120         398 :   if (spec.initial_process().distribution().is_defined())
     121             :   {
     122           0 :     throw mcrl2::runtime_error("The initial state has a non-empty stochastic distribution " + pp(spec.initial_process().distribution()) + ".\n" + 
     123           0 :                                "Transformation of this stochastic lps to a plain lps fails.");
     124             :   }
     125         398 :   result.initial_process() = process_initializer(spec.initial_process().expressions());
     126             : 
     127         398 :   linear_process& proc = result.process();
     128         398 :   proc.process_parameters() = spec.process().process_parameters();
     129         398 :   proc.deadlock_summands() = spec.process().deadlock_summands();
     130             : 
     131         398 :   action_summand_vector v;
     132             : 
     133        1654 :   for (const stochastic_action_summand& s: spec.process().action_summands())
     134             :   {
     135        1256 :     if (s.distribution().is_defined())
     136             :     {
     137           0 :       throw mcrl2::runtime_error("There is an action summand that has a non-empty stochastic distribution " + pp(s.distribution()) + ".\n" + 
     138           0 :                                  "Transformation of this stochastic lps to a plain lps fails.");;
     139             :     }
     140        1256 :     v.push_back(s);
     141             :   }
     142         398 :   proc.action_summands() = v;
     143         796 :   return result;
     144         398 : }
     145             : 
     146             : } // namespace lps
     147             : 
     148             : } // namespace mcrl2
     149             : 
     150             : #endif // MCRL2_LPS_STOCHASTIC_SPECIFICATION_H