stochastic_specification.h File Reference

Go to the source code of this file.

Classes
class	mcrl2::lps::stochastic_specification
	Linear process specification. More...

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::lps
	The main namespace for the LPS library.

Functions
void	mcrl2::lps::complete_data_specification (stochastic_specification &spec)
	Adds all sorts that appear in the process of l to the data specification of l.
std::set< data::sort_expression >	mcrl2::lps::find_sort_expressions (const lps::stochastic_specification &x)
std::set< data::variable >	mcrl2::lps::find_all_variables (const lps::stochastic_specification &x)
std::set< data::variable >	mcrl2::lps::find_free_variables (const lps::stochastic_specification &x)
std::set< data::function_symbol >	mcrl2::lps::find_function_symbols (const lps::stochastic_specification &x)
std::set< core::identifier_string >	mcrl2::lps::find_identifiers (const lps::stochastic_specification &x)
bool	mcrl2::lps::check_well_typedness (const stochastic_specification &x)
void	mcrl2::lps::normalize_sorts (stochastic_specification &x, const data::sort_specification &sortspec)
std::string	mcrl2::lps::pp (const stochastic_specification &x)
std::ostream &	mcrl2::lps::operator<< (std::ostream &out, const stochastic_specification &x)
bool	mcrl2::lps::operator== (const stochastic_specification &spec1, const stochastic_specification &spec2)
bool	mcrl2::lps::operator!= (const stochastic_specification &spec1, const stochastic_specification &spec2)
	Inequality operator.
std::string	mcrl2::lps::pp_with_summand_numbers (const stochastic_specification &x)
specification	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.