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             : /// \file mcrl2/lps/stochastic_linear_process.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_STOCHASTIC_LINEAR_PROCESS_H
      13             : #define MCRL2_LPS_STOCHASTIC_LINEAR_PROCESS_H
      14             : 
      15             : #include "mcrl2/lps/linear_process.h"
      16             : #include "mcrl2/lps/stochastic_action_summand.h"
      17             : #include "mcrl2/lps/stochastic_process_initializer.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace lps {
      22             : 
      23             : namespace detail {
      24             : 
      25             : template <>
      26             : inline
      27             : stochastic_action_summand make_action_summand<stochastic_action_summand>(const data::variable_list& summation_variables,
      28             :                                                                          const data::data_expression& condition,
      29             :                                                                          const multi_action& a,
      30             :                                                                          const data::assignment_list& assignments,
      31             :                                                                          const stochastic_distribution& distribution
      32             :                                                                         )
      33             : {
      34             :   return stochastic_action_summand(summation_variables, condition, a, assignments, distribution);
      35             : }
      36             : 
      37             : inline
      38         279 : stochastic_action_summand_vector convert_action_summands(const action_summand_vector& action_summands)
      39             : {
      40         279 :   stochastic_action_summand_vector result;
      41        1319 :   for (const action_summand& s: action_summands)
      42             :   {
      43        1040 :     result.push_back(stochastic_action_summand(s));
      44             :   }
      45         279 :   return result;
      46           0 : }
      47             : 
      48             : } // namespace detail
      49             : 
      50             : /// \brief linear process.
      51             : class stochastic_linear_process: public linear_process_base<stochastic_action_summand>
      52             : {
      53             :   typedef linear_process_base<stochastic_action_summand> super;
      54             : 
      55             :   public:
      56             :     /// \brief Constructor.
      57       14751 :     stochastic_linear_process()
      58       14751 :     { }
      59             : 
      60             :     /// \brief Constructor.
      61             :     stochastic_linear_process(const atermpp::aterm_appl& t, bool stochastic_distributions_allowed = true)
      62             :       : super(t, stochastic_distributions_allowed)
      63             :     { }
      64             : 
      65             :     /// \brief Constructor.
      66        1612 :     stochastic_linear_process(const data::variable_list& process_parameters,
      67             :                               const deadlock_summand_vector& deadlock_summands,
      68             :                               const stochastic_action_summand_vector& action_summands
      69             :                              )
      70        1612 :       : super(process_parameters, deadlock_summands, action_summands)
      71        1612 :     { }
      72             : 
      73             :     /// \brief Constructor.
      74         279 :     explicit stochastic_linear_process(const linear_process& other)
      75         279 :       : super(other.process_parameters(), other.deadlock_summands(), detail::convert_action_summands(other.action_summands()))
      76         279 :     { }
      77             : };
      78             : 
      79             : //--- start generated class stochastic_linear_process ---//
      80             : // prototype declaration
      81             : std::string pp(const stochastic_linear_process& x);
      82             : 
      83             : /// \\brief Outputs the object to a stream
      84             : /// \\param out An output stream
      85             : /// \\param x Object x
      86             : /// \\return The output stream
      87             : inline
      88             : std::ostream& operator<<(std::ostream& out, const stochastic_linear_process& x)
      89             : {
      90             :   return out << lps::pp(x);
      91             : }
      92             : //--- end generated class stochastic_linear_process ---//
      93             : 
      94             : // template function overloads
      95             : std::set<data::variable> find_all_variables(const lps::stochastic_linear_process& x);
      96             : std::set<data::variable> find_free_variables(const lps::stochastic_linear_process& x);
      97             : 
      98             : } // namespace lps
      99             : 
     100             : } // namespace mcrl2
     101             : 
     102             : #endif // MCRL2_LPS_STOCHASTIC_LINEAR_PROCESS_H