Include file:
#include "mcrl2/lps/stochastic_specification.h"
check_well_typedness
(const stochastic_specification &x)complete_data_specification
(stochastic_specification &spec)Adds all sorts that appear in the process of l to the data specification of l.
Parameters:
spec A linear process specification
find_all_variables
(const lps::stochastic_specification &x)find_free_variables
(const lps::stochastic_specification &x)find_function_symbols
(const lps::stochastic_specification &x)find_identifiers
(const lps::stochastic_specification &x)find_sort_expressions
(const lps::stochastic_specification &x)mcrl2::lps::
operator!=
(const stochastic_specification &spec1, const stochastic_specification &spec2)Inequality operator.
mcrl2::lps::
operator<<
(std::ostream &out, const stochastic_specification &x)Outputs the object to a stream.
Parameters:
out An output stream
x Object x
Returns: The output stream
mcrl2::lps::
operator==
(const stochastic_specification &spec1, const stochastic_specification &spec2)pp
(const stochastic_specification &x)pp_with_summand_numbers
(const stochastic_specification &x)mcrl2::lps::
remove_stochastic_operators
(const stochastic_specification &spec)Converts a stochastic specification to a specification. Throws an exception if non-empty distributions are encountered.