10#ifndef MCRL2_LPS_STOCHASTIC_SPECIFICATION_H
11#define MCRL2_LPS_STOCHASTIC_SPECIFICATION_H
20class stochastic_specification;
28std::set<core::identifier_string>
find_identifiers(
const lps::stochastic_specification& x);
32void normalize_sorts(stochastic_specification& x,
const data::sort_specification& sortspec);
73std::string
pp(
const stochastic_specification& x);
96 return !(spec1 == spec2);
123 "Transformation of this stochastic lps to a plain lps fails.");
135 if (s.distribution().is_defined())
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.");;
142 proc.action_summands() = v;
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....
A stochastic process initializer.
const stochastic_distribution & distribution() const
Linear process specification.
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()
Constructor.
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.
void find_function_symbols(const T &x, OutputIterator o)
std::string pp_with_summand_numbers(const specification &x)
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)
std::string pp(const action_summand &x)
void find_sort_expressions(const T &x, OutputIterator o)
atermpp::aterm specification_to_aterm(const specification_base< LinearProcess, InitialProcessExpression > &spec)
Conversion to aterm.
std::ostream & operator<<(std::ostream &out, const action_summand &x)
lps::multi_action normalize_sorts(const multi_action &x, const data::sort_specification &sortspec)
std::set< data::variable > find_free_variables(const lps::deadlock &x)
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)
std::vector< action_summand > action_summand_vector
\brief vector of action_summands
std::set< data::variable > find_all_variables(const lps::deadlock &x)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
add your file description here.