mCRL2
Loading...
Searching...
No Matches
stochastic_specification.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//
9
10#ifndef MCRL2_LPS_STOCHASTIC_SPECIFICATION_H
11#define MCRL2_LPS_STOCHASTIC_SPECIFICATION_H
12
15
16namespace mcrl2 {
17
18namespace lps {
19
20class stochastic_specification;
21void complete_data_specification(stochastic_specification& spec);
22
23// template function overloads
24std::set<data::sort_expression> find_sort_expressions(const lps::stochastic_specification& x);
25std::set<data::variable> find_all_variables(const lps::stochastic_specification& x);
26std::set<data::variable> find_free_variables(const lps::stochastic_specification& x);
27std::set<data::function_symbol> find_function_symbols(const lps::stochastic_specification& x);
28std::set<core::identifier_string> find_identifiers(const lps::stochastic_specification& x);
29
30// template function overloads
31bool check_well_typedness(const stochastic_specification& x);
32void normalize_sorts(stochastic_specification& x, const data::sort_specification& sortspec);
33
35class stochastic_specification: public specification_base<stochastic_linear_process, stochastic_process_initializer>
36{
37 protected:
39
40 public:
43 { }
44
53 const std::set<data::variable>& global_variables,
57 {
59 }
60
63 : super(other.data(),
64 other.action_labels(),
65 other.global_variables(),
68 { }
69};
70
71//--- start generated class stochastic_specification ---//
72// prototype declaration
73std::string pp(const stochastic_specification& x);
74
79inline
80std::ostream& operator<<(std::ostream& out, const stochastic_specification& x)
81{
82 return out << lps::pp(x);
83}
84//--- end generated class stochastic_specification ---//
85
86inline
88{
89 return specification_to_aterm(spec1) == specification_to_aterm(spec2);
90}
91
93inline
95{
96 return !(spec1 == spec2);
97}
98
99std::string pp_with_summand_numbers(const stochastic_specification& x);
100
103inline
105{
106 std::set<data::sort_expression> s = lps::find_sort_expressions(spec);
107 spec.data().add_context_sorts(s);
108}
109
112inline
114{
115 specification result;
116 result.data() = spec.data();
117 result.action_labels() = spec.action_labels();
118 result.global_variables() = spec.global_variables();
119
121 {
122 throw mcrl2::runtime_error("The initial state has a non-empty stochastic distribution " + pp(spec.initial_process().distribution()) + ".\n" +
123 "Transformation of this stochastic lps to a plain lps fails.");
124 }
126
127 linear_process& proc = result.process();
128 proc.process_parameters() = spec.process().process_parameters();
129 proc.deadlock_summands() = spec.process().deadlock_summands();
130
132
133 for (const stochastic_action_summand& s: spec.process().action_summands())
134 {
135 if (s.distribution().is_defined())
136 {
137 throw mcrl2::runtime_error("There is an action summand that has a non-empty stochastic distribution " + pp(s.distribution()) + ".\n" +
138 "Transformation of this stochastic lps to a plain lps fails.");;
139 }
140 v.push_back(s);
141 }
142 proc.action_summands() = v;
143 return result;
144}
145
146} // namespace lps
147
148} // namespace mcrl2
149
150#endif // MCRL2_LPS_STOCHASTIC_SPECIFICATION_H
void add_context_sorts(const Container &c, typename atermpp::enable_if_container< Container >::type *=nullptr)
Adds the sorts in c to the context sorts.
const std::vector< ActionSummand > & 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.
data::data_expression_list expressions() const
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the LPS.
const process::action_label_list & action_labels() const
Returns a sequence of action labels. This sequence contains all action labels occurring in the specif...
const stochastic_process_initializer & initial_process() const
Returns the initial process.
const stochastic_linear_process & process() const
Returns the linear process of the specification.
const data::data_specification & data() const
Returns the data specification.
Linear process specification.
LPS summand containing a multi-action.
\brief A stochastic distribution
bool is_defined() const
Returns true if the distribution is defined, i.e. it contains a valid distribution....
const stochastic_distribution & distribution() const
stochastic_specification(const specification &other)
Constructor. This constructor is explicit as implicit conversions of this kind is a source of bugs.
specification_base< stochastic_linear_process, stochastic_process_initializer > super
stochastic_specification(const data::data_specification &data, const process::action_label_list &action_labels, const std::set< data::variable > &global_variables, const stochastic_linear_process &lps, const stochastic_process_initializer &initial_process)
Constructor.
Standard exception class for reporting runtime errors.
Definition exception.h:27
@ proc
Definition linearise.cpp:78
void find_function_symbols(const T &x, OutputIterator o)
Definition find.h:138
atermpp::aterm_appl specification_to_aterm(const specification_base< LinearProcess, InitialProcessExpression > &spec)
Conversion to aterm_appl.
std::string pp_with_summand_numbers(const specification &x)
Definition lps.cpp:74
void complete_data_specification(specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
bool check_well_typedness(const linear_process &x)
Definition lps.cpp:92
std::string pp(const action_summand &x)
Definition lps.cpp:26
void find_sort_expressions(const T &x, OutputIterator o)
Definition find.h:117
std::ostream & operator<<(std::ostream &out, const action_summand &x)
lps::multi_action normalize_sorts(const multi_action &x, const data::sort_specification &sortspec)
Definition lps.cpp:38
std::set< data::variable > find_free_variables(const lps::deadlock &x)
Definition lps.cpp:54
bool operator!=(const specification &spec1, const specification &spec2)
Inequality operator.
specification remove_stochastic_operators(const stochastic_specification &spec)
Converts a stochastic specification to a specification. Throws an exception if non-empty distribution...
bool operator==(const action_summand &x, const action_summand &y)
Equality operator of action summands.
void find_identifiers(const T &x, OutputIterator o)
Definition find.h:96
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
The class specification.
add your file description here.