mCRL2
Loading...
Searching...
No Matches
stochastic_linear_process.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_LPS_STOCHASTIC_LINEAR_PROCESS_H
13#define MCRL2_LPS_STOCHASTIC_LINEAR_PROCESS_H
14
18
19namespace mcrl2 {
20
21namespace lps {
22
23namespace detail {
24
25template <>
26inline
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
37inline
39{
41 for (const action_summand& s: action_summands)
42 {
43 result.push_back(stochastic_action_summand(s));
44 }
45 return result;
46}
47
48} // namespace detail
49
51class stochastic_linear_process: public linear_process_base<stochastic_action_summand>
52{
54
55 public:
58 { }
59
61 stochastic_linear_process(const atermpp::aterm& t, bool stochastic_distributions_allowed = true)
62 : super(t, stochastic_distributions_allowed)
63 { }
64
69 )
71 { }
72
75 : super(other.process_parameters(), other.deadlock_summands(), detail::convert_action_summands(other.action_summands()))
76 { }
77};
78
79//--- start generated class stochastic_linear_process ---//
80// prototype declaration
81std::string pp(const stochastic_linear_process& x);
82
87inline
88std::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
95std::set<data::variable> find_all_variables(const lps::stochastic_linear_process& x);
96std::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
LPS summand containing a multi-action.
const std::vector< stochastic_action_summand > & action_summands() const
Returns the sequence of action summands.
const deadlock_summand_vector & deadlock_summands() const
Returns the sequence of deadlock summands.
const data::variable_list & process_parameters() const
Returns the sequence of process parameters.
\brief A timed multi-action
LPS summand containing a multi-action.
\brief A stochastic distribution
stochastic_linear_process(const atermpp::aterm &t, bool stochastic_distributions_allowed=true)
Constructor.
stochastic_linear_process(const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const stochastic_action_summand_vector &action_summands)
Constructor.
linear_process_base< stochastic_action_summand > super
stochastic_linear_process(const linear_process &other)
Constructor.
The class linear_process.
stochastic_action_summand_vector convert_action_summands(const action_summand_vector &action_summands)
stochastic_action_summand make_action_summand< stochastic_action_summand >(const data::variable_list &summation_variables, const data::data_expression &condition, const multi_action &a, const data::assignment_list &assignments, const stochastic_distribution &distribution)
std::vector< stochastic_action_summand > stochastic_action_summand_vector
\brief vector of stochastic_action_summands
std::string pp(const action_summand &x)
Definition lps.cpp:26
std::vector< deadlock_summand > deadlock_summand_vector
\brief vector of deadlock_summands
std::ostream & operator<<(std::ostream &out, const action_summand &x)
std::set< data::variable > find_free_variables(const lps::deadlock &x)
Definition lps.cpp:54
std::vector< action_summand > action_summand_vector
\brief vector of action_summands
std::set< data::variable > find_all_variables(const lps::deadlock &x)
Definition lps.cpp:48
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
add your file description here.
add your file description here.