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/process_initializer.h
      10             : /// \brief The class process_initializer.
      11             : 
      12             : #ifndef MCRL2_LPS_PROCESS_INITIALIZER_H
      13             : #define MCRL2_LPS_PROCESS_INITIALIZER_H
      14             : 
      15             : #include "mcrl2/data/print.h"
      16             : #include "mcrl2/data/replace.h"
      17             : #include "mcrl2/data/substitutions/assignment_sequence_substitution.h"
      18             : #include "mcrl2/lps/stochastic_distribution.h"
      19             : #include "mcrl2/process/action_label.h"
      20             : 
      21             : namespace mcrl2
      22             : {
      23             : 
      24             : namespace lps
      25             : {
      26             : 
      27             : /// \brief A process initializer
      28             : class process_initializer: public atermpp::aterm_appl
      29             : {
      30             :   public:
      31             :     /// \brief Default constructor.
      32         887 :     process_initializer()
      33         887 :       : atermpp::aterm_appl(core::detail::default_values::LinearProcessInit)
      34         887 :     {}
      35             : 
      36             :     /// \brief Constructor.
      37             :     /// \param term A term.
      38             :     /// \param check_distribution Check whether the initial state is plain or a state distribution.
      39       18855 :     explicit process_initializer(const atermpp::aterm& term, bool check_distribution = true)
      40       18855 :       : atermpp::aterm_appl(atermpp::down_cast<atermpp::aterm_appl>(term))
      41             :     {
      42       18855 :       assert(core::detail::check_term_LinearProcessInit(*this));
      43       18855 :       const lps::stochastic_distribution& dist = atermpp::down_cast<lps::stochastic_distribution>(atermpp::down_cast<atermpp::aterm_appl>(term)[1]);
      44       18855 :       if (check_distribution && dist.is_defined())
      45             :       {
      46           0 :         throw mcrl2::runtime_error("initial state with non-empty stochastic distribution encountered");
      47             :       }
      48       18855 :     }
      49             : 
      50             :     /// \brief Constructor.
      51         573 :     explicit process_initializer(const data::data_expression_list& expressions)
      52         573 :       : atermpp::aterm_appl(core::detail::function_symbol_LinearProcessInit(), expressions, stochastic_distribution())
      53         573 :     {}
      54             : 
      55             :     /// Move semantics
      56        2383 :     process_initializer(const process_initializer&) noexcept = default;
      57             :     process_initializer(process_initializer&&) noexcept = default;
      58        1541 :     process_initializer& operator=(const process_initializer&) noexcept = default;
      59        1795 :     process_initializer& operator=(process_initializer&&) noexcept = default;
      60             : 
      61       11364 :     data::data_expression_list expressions() const
      62             :     {
      63       11364 :       return atermpp::down_cast<data::data_expression_list>((*this)[0]);
      64             :     }
      65             : };
      66             : 
      67             : 
      68             : template <class EXPRESSION_LIST>
      69         242 : inline void make_process_initializer(atermpp::aterm_appl& t, EXPRESSION_LIST args)
      70             : {
      71         242 :   make_term_appl(t, core::detail::function_symbol_LinearProcessInit(), args, stochastic_distribution());
      72         242 : }
      73             : 
      74             : 
      75             : //--- start generated class process_initializer ---//
      76             : /// \\brief list of process_initializers
      77             : typedef atermpp::term_list<process_initializer> process_initializer_list;
      78             : 
      79             : /// \\brief vector of process_initializers
      80             : typedef std::vector<process_initializer>    process_initializer_vector;
      81             : 
      82             : /// \\brief Test for a process_initializer expression
      83             : /// \\param x A term
      84             : /// \\return True if \\a x is a process_initializer expression
      85             : inline
      86             : bool is_process_initializer(const atermpp::aterm_appl& x)
      87             : {
      88             :   return x.function() == core::detail::function_symbols::LinearProcessInit;
      89             : }
      90             : 
      91             : // prototype declaration
      92             : std::string pp(const process_initializer& x);
      93             : 
      94             : /// \\brief Outputs the object to a stream
      95             : /// \\param out An output stream
      96             : /// \\param x Object x
      97             : /// \\return The output stream
      98             : inline
      99             : std::ostream& operator<<(std::ostream& out, const process_initializer& x)
     100             : {
     101             :   return out << lps::pp(x);
     102             : }
     103             : 
     104             : /// \\brief swap overload
     105             : inline void swap(process_initializer& t1, process_initializer& t2)
     106             : {
     107             :   t1.swap(t2);
     108             : }
     109             : //--- end generated class process_initializer ---//
     110             : 
     111             : // template function overloads
     112             : std::set<data::variable> find_free_variables(const lps::process_initializer& x);
     113             : std::set<process::action_label> find_action_labels(const lps::process_initializer& x);
     114             : 
     115             : } // namespace lps
     116             : 
     117             : } // namespace mcrl2
     118             : 
     119             : #endif // MCRL2_LPS_PROCESS_INITIALIZER_H