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_process_initializer.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_STOCHASTIC_PROCESS_INITIALIZER_H
      13             : #define MCRL2_LPS_STOCHASTIC_PROCESS_INITIALIZER_H
      14             : 
      15             : #include "mcrl2/lps/process_initializer.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace lps {
      20             : 
      21             : /// \brief A stochastic process initializer
      22             : class stochastic_process_initializer: public process_initializer
      23             : {
      24             :   typedef process_initializer super;
      25             : 
      26             :   public:
      27             :     /// \brief Default constructor.
      28       16255 :     stochastic_process_initializer()
      29       16255 :       : super(core::detail::default_values::LinearProcessInit)
      30       16255 :     {}
      31             : 
      32             :     /// \brief Constructor.
      33             :     /// \param term A term
      34             :     explicit stochastic_process_initializer(const atermpp::aterm& term)
      35             :       : super(term, false)
      36             :     {
      37             :       assert(core::detail::check_term_LinearProcessInit(*this));
      38             :     }
      39             : 
      40             :     /// \brief Constructor.
      41        2600 :     stochastic_process_initializer(const data::data_expression_list& expressions, const stochastic_distribution& distribution)
      42        2600 :       : super(atermpp::aterm_appl(core::detail::function_symbol_LinearProcessInit(), expressions, distribution), false)
      43        2600 :     {}
      44             : 
      45        6850 :     const stochastic_distribution& distribution() const
      46             :     {
      47        6850 :       return atermpp::down_cast<stochastic_distribution>((*this)[1]);
      48             :     }
      49             : };
      50             : 
      51             : template <class... ARGUMENTS>
      52         750 : inline void make_stochastic_process_initializer(atermpp::aterm_appl& t, ARGUMENTS... args)
      53             : {
      54         750 :   make_term_appl(t, core::detail::function_symbol_LinearProcessInit(), args...);
      55         750 : }
      56             : 
      57             : 
      58             : //--- start generated class stochastic_process_initializer ---//
      59             : /// \\brief list of stochastic_process_initializers
      60             : typedef atermpp::term_list<stochastic_process_initializer> stochastic_process_initializer_list;
      61             : 
      62             : /// \\brief vector of stochastic_process_initializers
      63             : typedef std::vector<stochastic_process_initializer>    stochastic_process_initializer_vector;
      64             : 
      65             : /// \\brief Test for a stochastic_process_initializer expression
      66             : /// \\param x A term
      67             : /// \\return True if \\a x is a stochastic_process_initializer expression
      68             : inline
      69             : bool is_stochastic_process_initializer(const atermpp::aterm_appl& x)
      70             : {
      71             :   return x.function() == core::detail::function_symbols::LinearProcessInit;
      72             : }
      73             : 
      74             : // prototype declaration
      75             : std::string pp(const stochastic_process_initializer& x);
      76             : 
      77             : /// \\brief Outputs the object to a stream
      78             : /// \\param out An output stream
      79             : /// \\param x Object x
      80             : /// \\return The output stream
      81             : inline
      82             : std::ostream& operator<<(std::ostream& out, const stochastic_process_initializer& x)
      83             : {
      84             :   return out << lps::pp(x);
      85             : }
      86             : 
      87             : /// \\brief swap overload
      88             : inline void swap(stochastic_process_initializer& t1, stochastic_process_initializer& t2)
      89             : {
      90             :   t1.swap(t2);
      91             : }
      92             : //--- end generated class stochastic_process_initializer ---//
      93             : 
      94             : // template function overloads
      95             : std::set<data::variable> find_free_variables(const lps::stochastic_process_initializer& x);
      96             : 
      97             : } // namespace lps
      98             : 
      99             : } // namespace mcrl2
     100             : 
     101             : #endif // MCRL2_LPS_STOCHASTIC_PROCESS_INITIALIZER_H