Include file:
#include "mcrl2/lps/specification.h"
The class specification.
mcrl2::lps::
check_well_typedness
(const Object &o)¶complete_data_specification
(specification &spec)¶Adds all sorts that appear in the process of l to the data specification of l.
Parameters:
complete_data_specification
(stochastic_specification &spec)¶Adds all sorts that appear in the process of l to the data specification of l.
Parameters:
mcrl2::lps::
is_specification
(const atermpp::aterm_appl &x)¶Test for a specification expression.
Parameters:
Returns: True if x is a specification expression
mcrl2::lps::
operator!=
(const specification &spec1, const specification &spec2)¶Inequality operator.
mcrl2::lps::
operator!=
(const stochastic_specification &spec1, const stochastic_specification &spec2)¶Inequality operator.
mcrl2::lps::
operator<<
(std::ostream &out, const specification &x)¶brief Outputs the object to a stream param out An output stream param x Object x return The output stream
mcrl2::lps::
operator<<
(std::ostream &out, const stochastic_specification &x)¶brief Outputs the object to a stream param out An output stream param x Object x return The output stream
mcrl2::lps::
operator==
(const specification &spec1, const specification &spec2)¶Equality operator.
mcrl2::lps::
operator==
(const stochastic_specification &spec1, const stochastic_specification &spec2)¶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.
specification_to_aterm
(const specification_base<LinearProcess, InitialProcessExpression> &spec)¶Conversion to aterm_appl.
Returns: The specification converted to aterm format.