mcrl2::lps Namespace Reference

The main namespace for the LPS library. More...

Namespaces
namespace	detail
namespace	tools

Classes
struct	abortable
class	action_label_data_type
	Models the mapping of mCRL2 action labels to integers. More...
struct	action_label_traverser
	\brief Traverser class More...
class	action_rename_rule
	Action rename rule. More...
class	action_rename_specification
	Read-only singly linked list of action rename rules. More...
class	action_rename_type_checker
class	action_summand
	LPS summand containing a multi-action. More...
struct	add_data_expressions
struct	add_data_variable_binding
	Maintains a multiset of bound data variables during traversal. More...
struct	add_data_variable_builder_binding
struct	add_data_variable_traverser_binding
struct	add_sort_expressions
struct	add_traverser_action_labels
struct	add_traverser_data_expressions
struct	add_traverser_identifier_strings
struct	add_traverser_sort_expressions
struct	add_traverser_variables
struct	add_variables
class	binary_algorithm
	Algorithm class that can be used to apply the binary algorithm. More...
class	breadth_first_todo_set
struct	commutative_confluence_condition
	Function object that computes the condition for commutative confluence. More...
class	confluence_checker
struct	confluence_summand
class	constelm_algorithm
	Algorithm class for elimination of constant parameters. More...
struct	data_expression_builder
	\brief Builder class More...
struct	data_expression_traverser
	\brief Traverser class More...
struct	data_rewriter
	A rewriter that applies a data rewriter to data expressions in a term. More...
class	deadlock
	Represents a deadlock. More...
class	deadlock_summand
	LPS summand containing a deadlock. More...
class	decluster_algorithm
class	depth_first_todo_set
class	explorer
struct	explorer_options
struct	explorer_summand
class	highway_todo_set
struct	identifier_string_traverser
	\brief Traverser class More...
class	invelm_algorithm
class	linear_process
	linear process. More...
class	linear_process_base
class	lpsparunfold
class	multi_action
	\brief A timed multi-action More...
class	multi_action_type_checker
class	parelm_algorithm
	Algorithm class for elimination of unused parameters from a linear process specification. More...
struct	parunfold_replacement
class	pins
class	pins_data_type
	Models a pins data type. A pins data type maintains a mapping between known values of a data type and integers. More...
class	probabilistic_data_expression
	This class contains labels for probabilistic transistions, consisting of a numerator and a denumerator. More...
class	process_initializer
	A process initializer. More...
class	simulation
	Simulation process. More...
struct	sort_expression_builder
	\brief Builder class More...
struct	sort_expression_traverser
	\brief Traverser class More...
class	specification
	Linear process specification. More...
class	specification_base
struct	square_confluence_condition
	Function object that computes the condition for square confluence. More...
class	state_data_type
	Models the mapping of mCRL2 state values to integers. More...
class	state_probability_pair
class	stochastic_action_summand
	LPS summand containing a multi-action. More...
class	stochastic_distribution
	\brief A stochastic distribution More...
class	stochastic_linear_process
	linear process. More...
class	stochastic_process_initializer
	A stochastic process initializer. More...
class	stochastic_specification
	Linear process specification. More...
struct	stochastic_state
struct	stream_printer
	Prints the object x to a stream. More...
class	sumelm_algorithm
	Class implementing the sum elimination lemma. More...
class	suminst_algorithm
class	summand_base
	Base class for LPS summands. More...
struct	t_lin_options
	Options for linearisation. More...
class	todo_set
struct	triangular_confluence_condition
	Function object that computes the condition for triangular confluence. More...
struct	trivial_confluence_condition
	Function object that computes the condition for triangular confluence. More...
struct	unfold_cache_element
	Element in the cache that keeps track of the information for a single unfolded sort, say s. More...
class	untime_algorithm
struct	variable_builder
	\brief Builder class More...
struct	variable_traverser
	\brief Traverser class More...

Typedefs
typedef atermpp::term_list< action_summand >	action_summand_list
	\brief list of action_summands
typedef std::vector< action_summand >	action_summand_vector
	\brief vector of action_summands
typedef atermpp::term_list< deadlock >	deadlock_list
	\brief list of deadlocks
typedef std::vector< deadlock >	deadlock_vector
	\brief vector of deadlocks
typedef atermpp::term_list< deadlock_summand >	deadlock_summand_list
	\brief list of deadlock_summands
typedef std::vector< deadlock_summand >	deadlock_summand_vector
	\brief vector of deadlock_summands
typedef atermpp::utilities::unordered_map< atermpp::aterm, atermpp::term_list< data::data_expression_list >, detail::cache_hash, detail::cache_equality, std::allocator< std::pair< atermpp::aterm, atermpp::term_list< data::data_expression_list > > >, true >	summand_cache_map
typedef atermpp::term_list< multi_action >	multi_action_list
	\brief list of multi_actions
typedef std::vector< multi_action >	multi_action_vector
	\brief vector of multi_actions
typedef atermpp::term_list< process_initializer >	process_initializer_list
	\brief list of process_initializers
typedef std::vector< process_initializer >	process_initializer_vector
	\brief vector of process_initializers
typedef atermpp::term_balanced_tree< data::data_expression >	state
typedef atermpp::term_list< stochastic_action_summand >	stochastic_action_summand_list
	\brief list of stochastic_action_summands
typedef std::vector< stochastic_action_summand >	stochastic_action_summand_vector
	\brief vector of stochastic_action_summands
typedef atermpp::term_list< stochastic_distribution >	stochastic_distribution_list
	\brief list of stochastic_distributions
typedef std::vector< stochastic_distribution >	stochastic_distribution_vector
	\brief vector of stochastic_distributions
typedef atermpp::term_list< stochastic_process_initializer >	stochastic_process_initializer_list
	\brief list of stochastic_process_initializers
typedef std::vector< stochastic_process_initializer >	stochastic_process_initializer_vector
	\brief vector of stochastic_process_initializers

Enumerations
enum	exploration_strategy {   es_none , es_breadth , es_depth , es_random ,   es_value_prioritized , es_value_random_prioritized , es_highway }
enum class	caching { none , local , global }
enum	t_lin_method { lmStack , lmRegular , lmRegular2 }
	The available linearisation methods. More...
enum	lps_rewriter_type { simplify , quantifier_one_point , condition_one_point }
	An enumerated type for the available lps rewriters. More...

Functions
atermpp::aterm	action_rename_rule_to_aterm (const action_rename_rule &rule)
atermpp::aterm	action_rename_specification_to_aterm (const action_rename_specification &spec)
lps::stochastic_specification	action_rename (const action_rename_specification &action_rename_spec, const lps::stochastic_specification &lps_old_spec, const data::rewriter &rewr, const bool enable_rewriting)
	Rename the actions in a linear specification using a given action_rename_spec.
stochastic_specification	action_rename (const std::regex &matching_regex, const std::string &replacing_fmt, const stochastic_specification &lps_old_spec)
	Rename actions in given specification based on a regular expression and a string that specifies how the replacement should be formatted.
std::string	pp (const action_summand &x)
std::ostream &	operator<< (std::ostream &out, const action_summand &x)
void	swap (action_summand &t1, action_summand &t2)
	\brief swap overload
bool	operator< (const action_summand &x, const action_summand &y)
	Comparison operator for action summands.
bool	operator== (const action_summand &x, const action_summand &y)
	Equality operator of action summands.
atermpp::aterm	action_summand_to_aterm (const action_summand &s)
	Conversion to aterm.
std::size_t	nr_of_booleans_for_elements (std::size_t n)
template<typename Summand >
const stochastic_distribution &	summand_distribution (const Summand &)
template<>
const stochastic_distribution &	summand_distribution (const lps::stochastic_action_summand &summand)
std::set< data::variable >	used_read_variables (const action_summand &summand)
std::set< data::variable >	changed_variables (const action_summand &summand)
data::assignment_list	make_assignment_list (const data::variable_list &variables, const data::data_expression_list &expressions)
std::string	print_confluence_summand (const confluence_summand &summand, const data::variable_list &process_parameters)
bool	disjoint (const confluence_summand &summand1, const confluence_summand &summand2)
	Indicates whether or not two summands are disjoint.
process::action_label	make_ctau_act_id ()
	Creates an identifier for the ctau action.
process::action	make_ctau_action ()
	Creates the ctau action.
template<typename Specification >
bool	has_ctau_action (const Specification &lpsspec)
template<typename DataRewriter , typename Specification >
void	constelm (Specification &spec, const DataRewriter &R, bool instantiate_global_variables=false)
	Removes zero or more constant parameters from the specification spec.
std::string	pp (const deadlock &x)
std::ostream &	operator<< (std::ostream &out, const deadlock &x)
void	swap (deadlock &t1, deadlock &t2)
	\brief swap overload
std::set< data::variable >	find_all_variables (const lps::deadlock &x)
std::set< data::variable >	find_free_variables (const lps::deadlock &x)
std::string	pp (const deadlock_summand &x)
std::ostream &	operator<< (std::ostream &out, const deadlock_summand &x)
void	swap (deadlock_summand &t1, deadlock_summand &t2)
	\brief swap overload
atermpp::aterm	deadlock_summand_to_aterm (const deadlock_summand &s)
	Conversion to atermappl.
exploration_strategy	parse_exploration_strategy (const std::string &s)
std::string	print_exploration_strategy (const exploration_strategy es)
std::istream &	operator>> (std::istream &is, exploration_strategy &strat)
std::ostream &	operator<< (std::ostream &os, const exploration_strategy strat)
std::string	description (const exploration_strategy strat)
std::ostream &	operator<< (std::ostream &os, caching c)
std::vector< data::data_expression >	make_data_expression_vector (const data::data_expression_list &v)
template<>
const stochastic_distribution &	summand_distribution (const lps::stochastic_action_summand &summand)
const stochastic_distribution &	initial_distribution (const lps::specification &)
const stochastic_distribution &	initial_distribution (const lps::stochastic_specification &lpsspec)
std::ostream &	operator<< (std::ostream &out, const explorer_summand &summand)
std::ostream &	operator<< (std::ostream &out, const explorer_options &options)
template<typename T , typename OutputIterator >
void	find_all_variables (const T &x, OutputIterator o)
template<typename T >
std::set< data::variable >	find_all_variables (const T &x)
template<typename T , typename OutputIterator >
void	find_free_variables (const T &x, OutputIterator o)
template<typename T , typename OutputIterator , typename VariableContainer >
void	find_free_variables_with_bound (const T &x, OutputIterator o, const VariableContainer &bound)
template<typename T >
std::set< data::variable >	find_free_variables (const T &x)
template<typename T , typename VariableContainer >
std::set< data::variable >	find_free_variables_with_bound (const T &x, VariableContainer const &bound)
template<typename T , typename OutputIterator >
void	find_identifiers (const T &x, OutputIterator o)
template<typename T >
std::set< core::identifier_string >	find_identifiers (const T &x)
template<typename T , typename OutputIterator >
void	find_sort_expressions (const T &x, OutputIterator o)
template<typename T >
std::set< data::sort_expression >	find_sort_expressions (const T &x)
template<typename T , typename OutputIterator >
void	find_function_symbols (const T &x, OutputIterator o)
template<typename T >
std::set< data::function_symbol >	find_function_symbols (const T &x)
template<typename T >
bool	search_free_variable (const T &x, const data::variable &v)
	Returns true if the term has a given free variable as subterm.
template<typename T , typename OutputIterator >
void	find_action_labels (const T &x, OutputIterator o)
	Returns all action labels that occur in an object.
template<typename T >
std::set< process::action_label >	find_action_labels (const T &x)
	Returns all action labels that occur in an object.
template<typename Node , typename GenerateSuccessors >
Node	find_representative (Node &u0, GenerateSuccessors generate_successors)
	Search for a unique representative in a graph.
template<typename T >
void	if_rewrite (T &x, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Applies the one point rule rewriter to all embedded data expressions in an object x.
template<typename T >
T	if_rewrite (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Applies the one point rule rewriter to all embedded data expressions in an object x.
atermpp::aterm_ostream &	operator<< (atermpp::aterm_ostream &stream, const specification &spec)
	Writes LPS to the stream.
atermpp::aterm_ostream &	operator<< (atermpp::aterm_ostream &stream, const stochastic_specification &spec)
atermpp::aterm_istream &	operator>> (atermpp::aterm_istream &stream, specification &spec)
	Reads LPS from the stream.
atermpp::aterm_istream &	operator>> (atermpp::aterm_istream &stream, stochastic_specification &spec)
template<typename Specification >
void	save_lps (const Specification &spec, std::ostream &stream, const std::string &target="")
	Save an LPS in the format specified.
template<typename Specification >
void	load_lps (Specification &spec, std::istream &stream, const std::string &source="")
	Load LPS from file.
template<typename Specification >
void	save_lps (const Specification &spec, const std::string &filename)
	Saves an LPS to a file.
template<typename Specification >
void	load_lps (Specification &spec, const std::string &filename)
	Load LPS from file.
template<typename T >
bool	is_stochastic (const T &x)
	Returns true if the LPS object x contains a stochastic distribution in one of its attributes.
bool	check_well_typedness (const linear_process &x)
bool	check_well_typedness (const stochastic_linear_process &x)
template<typename ActionSummand >
atermpp::aterm	linear_process_to_aterm (const linear_process_base< ActionSummand > &p)
	Conversion to aterm.
std::string	pp (const linear_process &x)
std::ostream &	operator<< (std::ostream &out, const linear_process &x)
bool	is_linear_process (const atermpp::aterm &x)
	Test for a linear_process expression.
std::set< data::variable >	find_all_variables (const lps::linear_process &x)
std::set< data::variable >	find_free_variables (const lps::linear_process &x)
std::set< process::action_label >	find_action_labels (const lps::linear_process &x)
std::string	print_lin_method (const t_lin_method lin_method)
	String representation of a linearisation method.
std::string	description (const t_lin_method lin_method)
t_lin_method	parse_lin_method (const std::string &s)
	Parse a linearisation method.
std::istream &	operator>> (std::istream &is, t_lin_method &l)
std::ostream &	operator<< (std::ostream &os, const t_lin_method l)
mcrl2::lps::stochastic_specification	linearise (const mcrl2::process::process_specification &type_checked_spec, mcrl2::lps::t_lin_options lin_options=t_lin_options())
	Linearises a process specification.
mcrl2::lps::stochastic_specification	linearise (const std::string &text, mcrl2::lps::t_lin_options lin_options=t_lin_options())
	Linearises a process specification from a textual specification.
lps_rewriter_type	parse_lps_rewriter_type (const std::string &type)
	Parses a lps rewriter type.
std::string	print_lps_rewriter_type (const lps_rewriter_type type)
	Prints a lps rewriter type.
std::string	description (const lps_rewriter_type type)
	Returns a description of a lps rewriter.
std::istream &	operator>> (std::istream &is, lps_rewriter_type &t)
	Stream operator for rewriter type.
std::ostream &	operator<< (std::ostream &os, const lps_rewriter_type t)
template<template< class > class Builder, template< template< class > class, class, class > class Binder>
parunfold_replacement< Builder, Binder >	apply_parunfold_replacement_builder (const lpsparunfold::case_func_replacement &case_funcs, data::set_identifier_generator &id_generator)
template<typename T >
void	insert_case_functions (T &x, const lpsparunfold::case_func_replacement &cfv, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T >
void	insert_case_functions (T &x, const lpsparunfold::case_func_replacement &cfv, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
std::vector< std::string >	generate_values (const data::data_specification &dataspec, const data::sort_expression &s, std::size_t max_size=1000)
	Generates possible values of the data type (at most max_size).
bool	is_multi_action (const atermpp::aterm &x)
template<class... ARGUMENTS>
void	make_multi_action (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const multi_action &x)
std::ostream &	operator<< (std::ostream &out, const multi_action &x)
void	swap (multi_action &t1, multi_action &t2)
	\brief swap overload
lps::multi_action	normalize_sorts (const multi_action &x, const data::sort_specification &sortspec)
lps::multi_action	translate_user_notation (const lps::multi_action &x)
std::set< data::variable >	find_all_variables (const lps::multi_action &x)
std::set< data::variable >	find_free_variables (const lps::multi_action &x)
data::data_expression	equal_multi_actions (const multi_action &a, const multi_action &b)
	Returns a data expression that expresses under which conditions the multi actions a and b are equal. The multi actions may contain free variables.
data::data_expression	not_equal_multi_actions (const multi_action &a, const multi_action &b)
	Returns a pbes expression that expresses under which conditions the multi actions a and b are not equal. The multi actions may contain free variables.
template<typename T >
void	normalize_sorts (T &x, const data::sort_specification &sortspec, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T >
T	normalize_sorts (const T &x, const data::sort_specification &sortspec, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0)
template<typename T >
void	one_point_rule_rewrite (T &x, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Applies the one point rule rewriter to all embedded data expressions in an object x.
template<typename T >
T	one_point_rule_rewrite (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Applies the one point rule rewriter to all embedded data expressions in an object x.
template<typename Specification >
void	order_summand_variables (Specification &lpsspec)
	Order summand variables to make enumeration over these variables more efficient.
template<typename Specification >
void	parelm (Specification &spec, bool variant1=true)
	Removes unused parameters from a linear process specification.
multi_action	parse_multi_action (std::stringstream &in, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
	Parses a multi_action from an input stream.
multi_action	parse_multi_action (std::stringstream &in, multi_action_type_checker &typechecker, const data::data_specification &data_spec=data::detail::default_specification())
	Parses a multi_action from an input stream.
multi_action	parse_multi_action (const std::string &text, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
	Parses a multi_action from a string.
multi_action	parse_multi_action (const std::string &text, multi_action_type_checker &typechecker, const data::data_specification &data_spec=data::detail::default_specification())
	Parses a multi_action from a string.
action_rename_specification	parse_action_rename_specification (std::istream &in, const lps::stochastic_specification &spec)
	Parses a process specification from an input stream.
action_rename_specification	parse_action_rename_specification (const std::string &spec_string, const lps::stochastic_specification &spec)
	Parses an action rename specification. Parses an acion rename specification. If the action rename specification contains data types that are not present in the data specification of spec they are added to it.
specification	parse_linear_process_specification (std::istream &spec_stream)
	Parses a linear process specification from an input stream.
specification	parse_linear_process_specification (const std::string &text)
	Parses a linear process specification from a string.
template<typename Specification >
void	parse_lps (std::istream &, Specification &)
template<>
void	parse_lps< specification > (std::istream &from, specification &result)
template<>
void	parse_lps< stochastic_specification > (std::istream &from, stochastic_specification &result)
	Parses a stochastic linear process specification from an input stream.
template<typename Specification >
void	parse_lps (const std::string &text, Specification &result)
process::action	parse_action (const std::string &text, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
	Parses an action from a string.
template<typename T >
std::string	pp (const T &x)
	Returns a string representation of the object x.
std::string	pp (const probabilistic_data_expression &l)
std::ostream &	operator<< (std::ostream &out, const probabilistic_data_expression &x)
	Pretty print to an outstream.
template<class EXPRESSION_LIST >
void	make_process_initializer (atermpp::aterm &t, EXPRESSION_LIST args)
bool	is_process_initializer (const atermpp::aterm &x)
std::string	pp (const process_initializer &x)
std::ostream &	operator<< (std::ostream &out, const process_initializer &x)
void	swap (process_initializer &t1, process_initializer &t2)
	\brief swap overload
std::set< data::variable >	find_free_variables (const lps::process_initializer &x)
std::set< process::action_label >	find_action_labels (const lps::process_initializer &x)
template<typename Object >
void	remove_parameters (Object &x, const std::set< data::variable > &to_be_removed)
	Rewrites an LPS data type.
template<typename Specification >
void	remove_trivial_summands (Specification &spec)
	Removes summands with condition equal to false from a linear process specification.
template<typename Specification >
void	remove_singleton_sorts (Specification &spec)
	Removes parameters with a singleton sort from a linear process specification.
data::assignment_list	remove_redundant_assignments (const data::assignment_list &assignments, const data::variable_list &do_not_remove)
	Removes assignments of the form x := x from v for variables x that are not contained in do_not_remove.
template<typename Specification >
void	remove_redundant_assignments (Specification &lpsspec)
	Removes redundant assignments of the form x = x from an LPS specification.
template<typename T , typename Substitution >
void	replace_variables_capture_avoiding (T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
void	replace_variables_capture_avoiding (T &x, Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename Substitution >
stochastic_distribution	replace_variables_capture_avoiding (const stochastic_distribution &x, data::data_expression_list &pars, Substitution &sigma, data::set_identifier_generator &id_generator)
template<typename Substitution >
stochastic_distribution	replace_variables_capture_avoiding (const stochastic_distribution &x, data::data_expression_list &pars, Substitution &sigma)
template<typename T , typename Substitution , typename IdentifierGenerator >
void	replace_variables_capture_avoiding_with_an_identifier_generator (T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution , typename IdentifierGenerator >
T	replace_variables_capture_avoiding_with_an_identifier_generator (const T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T >
void	replace_constants_by_variables (T &x, const data::rewriter &r, data::mutable_indexed_substitution<> &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times.
template<typename T >
T	replace_constants_by_variables (const T &x, const data::rewriter &r, data::mutable_indexed_substitution<> &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times.
template<typename Specification >
void	resolve_summand_variable_name_clashes (Specification &spec)
	Renames summand variables such that there are no name clashes between summand variables and process parameters.
template<typename T , typename Rewriter >
void	rewrite (T &x, Rewriter R, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Rewriter >
T	rewrite (const T &x, Rewriter R, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Rewriter , typename Substitution >
void	rewrite (T &x, Rewriter R, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Rewriter , typename Substitution >
T	rewrite (const T &x, Rewriter R, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename DataRewriter >
void	one_point_condition_rewrite (T &x, const DataRewriter &R, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Applies the one point condition rewriter to all embedded data expressions in an object x.
template<typename T , typename DataRewriter >
T	one_point_condition_rewrite (const T &x, const DataRewriter &R, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Applies the one point condition rewriter to all embedded data expressions in an object x.
template<typename Object >
bool	check_well_typedness (const Object &o)
template<typename LinearProcess , typename InitialProcessExpression >
atermpp::aterm	specification_to_aterm (const specification_base< LinearProcess, InitialProcessExpression > &spec)
	Conversion to aterm.
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 specification &x)
void	normalize_sorts (lps::specification &x, const data::sort_specification &sortspec)
bool	is_specification (const atermpp::aterm &x)
	Test for a specification expression.
std::string	pp (const specification &x)
std::ostream &	operator<< (std::ostream &out, const specification &x)
std::string	pp_with_summand_numbers (const specification &x)
std::set< data::sort_expression >	find_sort_expressions (const lps::specification &x)
std::set< data::variable >	find_all_variables (const lps::specification &x)
std::set< data::variable >	find_free_variables (const lps::specification &x)
std::set< data::function_symbol >	find_function_symbols (const lps::specification &x)
std::set< core::identifier_string >	find_identifiers (const lps::specification &x)
std::set< process::action_label >	find_action_labels (const lps::specification &x)
bool	operator== (const specification &spec1, const specification &spec2)
	Equality operator.
bool	operator!= (const specification &spec1, const specification &spec2)
	Inequality operator.
template<class ForwardTraversalIterator , class Transformer >
void	make_state (state &result, ForwardTraversalIterator p, const std::size_t size, Transformer transformer)
template<class ForwardTraversalIterator >
void	make_state (state &result, ForwardTraversalIterator p, const std::size_t size)
std::string	pp (const lps::state &x)
std::string	pp (const stochastic_action_summand &x)
std::ostream &	operator<< (std::ostream &out, const stochastic_action_summand &x)
void	swap (stochastic_action_summand &t1, stochastic_action_summand &t2)
	\brief swap overload
bool	operator< (const stochastic_action_summand &x, const stochastic_action_summand &y)
	Comparison operator for action summands.
bool	operator== (const stochastic_action_summand &x, const stochastic_action_summand &y)
	Equality operator of stochastic action summands.
atermpp::aterm	action_summand_to_aterm (const stochastic_action_summand &s)
	Conversion to aterm.
template<class... ARGUMENTS>
void	make_stochastic_distribution (atermpp::aterm &t, const ARGUMENTS &... args)
bool	is_stochastic_distribution (const atermpp::aterm &x)
std::string	pp (const stochastic_distribution &x)
std::ostream &	operator<< (std::ostream &out, const stochastic_distribution &x)
void	swap (stochastic_distribution &t1, stochastic_distribution &t2)
	\brief swap overload
std::string	pp (const stochastic_linear_process &x)
std::ostream &	operator<< (std::ostream &out, const stochastic_linear_process &x)
std::set< data::variable >	find_all_variables (const lps::stochastic_linear_process &x)
std::set< data::variable >	find_free_variables (const lps::stochastic_linear_process &x)
template<class... ARGUMENTS>
void	make_stochastic_process_initializer (atermpp::aterm &t, ARGUMENTS... args)
bool	is_stochastic_process_initializer (const atermpp::aterm &x)
std::string	pp (const stochastic_process_initializer &x)
std::ostream &	operator<< (std::ostream &out, const stochastic_process_initializer &x)
void	swap (stochastic_process_initializer &t1, stochastic_process_initializer &t2)
	\brief swap overload
std::set< data::variable >	find_free_variables (const lps::stochastic_process_initializer &x)
void	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 >	find_sort_expressions (const lps::stochastic_specification &x)
std::set< data::variable >	find_all_variables (const lps::stochastic_specification &x)
std::set< data::variable >	find_free_variables (const lps::stochastic_specification &x)
std::set< data::function_symbol >	find_function_symbols (const lps::stochastic_specification &x)
std::set< core::identifier_string >	find_identifiers (const lps::stochastic_specification &x)
bool	check_well_typedness (const stochastic_specification &x)
void	normalize_sorts (stochastic_specification &x, const data::sort_specification &sortspec)
std::string	pp (const stochastic_specification &x)
std::ostream &	operator<< (std::ostream &out, const stochastic_specification &x)
bool	operator== (const stochastic_specification &spec1, const stochastic_specification &spec2)
bool	operator!= (const stochastic_specification &spec1, const stochastic_specification &spec2)
	Inequality operator.
std::string	pp_with_summand_numbers (const stochastic_specification &x)
specification	remove_stochastic_operators (const stochastic_specification &spec)
	Converts a stochastic specification to a specification. Throws an exception if non-empty distributions are encountered.
std::string	print_probability (const data::data_expression &x)
void	check_probability (const data::data_expression &x, const data::rewriter &rewr)
void	check_stochastic_state (const stochastic_state &s, const data::rewriter &rewr)
bool	sumelm (action_summand &s)
	Apply the sum elimination lemma to summand s.
bool	sumelm (stochastic_action_summand &s)
	Apply the sum elimination lemma to summand s.
bool	sumelm (deadlock_summand &s)
	Apply the sum elimination lemma to summand s.
std::set< data::sort_expression >	finite_sorts (const data::data_specification &s)
	Return a set with all finite sorts in data specification s.
void	lpsbinary (const std::string &input_filename, const std::string &output_filename, const std::string &parameter_selection)
void	lpsconstelm (const std::string &input_filename, const std::string &output_filename, data::rewriter::strategy rewrite_strategy, bool instantiate_free_variables, bool ignore_conditions, bool remove_trivial_summands, bool remove_singleton_sorts)
void	lpsinfo (const std::string &input_filename, const std::string &input_file_message)
bool	lpsinvelm (const std::string &input_filename, const std::string &output_filename, const std::string &invariant_filename, const std::string &dot_file_name, data::rewriter::strategy rewrite_strategy, data::detail::smt_solver_type solver_type, const bool no_check, const bool no_elimination, const bool simplify_all, const bool all_violations, const bool counter_example, const bool path_eliminator, const bool apply_induction, const int time_limit)
void	lpsparelm (const std::string &input_filename, const std::string &output_filename)
void	lpspp (const std::string &input_filename, const std::string &output_filename, bool print_summand_numbers, core::print_format_type format)
void	lpsrewr (const std::string &input_filename, const std::string &output_filename, const data::rewriter::strategy rewrite_strategy, const lps::lps_rewriter_type rewriter_type)
void	lpssumelm (const std::string &input_filename, const std::string &output_filename, const bool decluster)
void	lpssuminst (const std::string &input_filename, const std::string &output_filename, const data::rewriter::strategy rewrite_strategy, const std::string &sorts_string, const bool finite_sorts_only, const bool tau_summands_only)
void	lpsuntime (const std::string &input_filename, const std::string &output_filename, const bool add_invariants, const bool apply_fourier_motzkin, const data::rewriter::strategy rewrite_strategy)
void	txt2lps (const std::string &input_filename, const std::string &output_filename)
template<typename T >
void	translate_user_notation (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T >
T	translate_user_notation (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0)
multi_action	typecheck_multi_action (process::untyped_multi_action &mult_act, const data::data_specification &data_spec, const process::action_label_list &action_decls)
	Type check a multi action Throws an exception if something went wrong.
multi_action	typecheck_multi_action (process::untyped_multi_action &mult_act, multi_action_type_checker &typechecker)
	Type check a multi action Throws an exception if something went wrong.
action_rename_specification	typecheck_action_rename_specification (const action_rename_specification &arspec, const lps::stochastic_specification &lpsspec)
	Type checks an action rename specification.
std::set< process::action_label >	find_action_labels (const lps::stochastic_specification &x)
atermpp::aterm	linear_process_specification_marker ()
atermpp::aterm_ostream &	operator<< (atermpp::aterm_ostream &stream, const multi_action &action)
atermpp::aterm_istream &	operator>> (atermpp::aterm_istream &stream, multi_action &action)
atermpp::aterm_ostream &	operator<< (atermpp::aterm_ostream &stream, const deadlock_summand &summand)
atermpp::aterm_istream &	operator>> (atermpp::aterm_istream &stream, deadlock_summand &summand)
atermpp::aterm_ostream &	operator<< (atermpp::aterm_ostream &stream, const stochastic_action_summand &summand)
atermpp::aterm_istream &	operator>> (atermpp::aterm_istream &stream, stochastic_action_summand &summand)
template<typename ActionSummand >
atermpp::aterm_ostream &	operator<< (atermpp::aterm_ostream &stream, const linear_process_base< ActionSummand > &lps)
template<typename ActionSummand >
atermpp::aterm_istream &	operator>> (atermpp::aterm_istream &stream, linear_process_base< ActionSummand > &lps)
static void	write_spec (atermpp::aterm_ostream &stream, const stochastic_specification &spec)
static void	read_spec (atermpp::aterm_istream &stream, stochastic_specification &spec)

Detailed Description

The main namespace for the LPS library.

Typedef Documentation

action_summand_list

typedef atermpp::term_list<action_summand> mcrl2::lps::action_summand_list

\brief list of action_summands

Definition at line 116 of file action_summand.h.

action_summand_vector

typedef std::vector<action_summand> mcrl2::lps::action_summand_vector

\brief vector of action_summands

Definition at line 119 of file action_summand.h.

deadlock_list

typedef atermpp::term_list<deadlock> mcrl2::lps::deadlock_list

\brief list of deadlocks

Definition at line 89 of file deadlock.h.

deadlock_summand_list

typedef atermpp::term_list<deadlock_summand> mcrl2::lps::deadlock_summand_list

\brief list of deadlock_summands

Definition at line 81 of file deadlock_summand.h.

deadlock_summand_vector

typedef std::vector<deadlock_summand> mcrl2::lps::deadlock_summand_vector

\brief vector of deadlock_summands

Definition at line 84 of file deadlock_summand.h.

deadlock_vector

typedef std::vector<deadlock> mcrl2::lps::deadlock_vector

\brief vector of deadlocks

Definition at line 92 of file deadlock.h.

multi_action_list

typedef atermpp::term_list<multi_action> mcrl2::lps::multi_action_list

\brief list of multi_actions

Definition at line 109 of file multi_action.h.

multi_action_vector

typedef std::vector<multi_action> mcrl2::lps::multi_action_vector

\brief vector of multi_actions

Definition at line 112 of file multi_action.h.

process_initializer_list

typedef atermpp::term_list<process_initializer> mcrl2::lps::process_initializer_list

\brief list of process_initializers

Definition at line 77 of file process_initializer.h.

process_initializer_vector

typedef std::vector<process_initializer> mcrl2::lps::process_initializer_vector

\brief vector of process_initializers

Definition at line 80 of file process_initializer.h.

state

typedef atermpp::term_balanced_tree<data::data_expression> mcrl2::lps::state

Definition at line 24 of file state.h.

stochastic_action_summand_list

typedef atermpp::term_list<stochastic_action_summand> mcrl2::lps::stochastic_action_summand_list

\brief list of stochastic_action_summands

Definition at line 73 of file stochastic_action_summand.h.

stochastic_action_summand_vector

typedef std::vector<stochastic_action_summand> mcrl2::lps::stochastic_action_summand_vector

\brief vector of stochastic_action_summands

Definition at line 76 of file stochastic_action_summand.h.

stochastic_distribution_list

typedef atermpp::term_list<stochastic_distribution> mcrl2::lps::stochastic_distribution_list

\brief list of stochastic_distributions

Definition at line 78 of file stochastic_distribution.h.

stochastic_distribution_vector

typedef std::vector<stochastic_distribution> mcrl2::lps::stochastic_distribution_vector

\brief vector of stochastic_distributions

Definition at line 81 of file stochastic_distribution.h.

stochastic_process_initializer_list

typedef atermpp::term_list<stochastic_process_initializer> mcrl2::lps::stochastic_process_initializer_list

\brief list of stochastic_process_initializers

Definition at line 60 of file stochastic_process_initializer.h.

stochastic_process_initializer_vector

typedef std::vector<stochastic_process_initializer> mcrl2::lps::stochastic_process_initializer_vector

\brief vector of stochastic_process_initializers

Definition at line 63 of file stochastic_process_initializer.h.

summand_cache_map

typedef atermpp::utilities::unordered_map<atermpp::aterm, atermpp::term_list<data::data_expression_list>, detail::cache_hash, detail::cache_equality, std::allocator< std::pair<atermpp::aterm, atermpp::term_list<data::data_expression_list> > >, true > mcrl2::lps::summand_cache_map

Definition at line 345 of file explorer.h.

Enumeration Type Documentation

caching

enum class mcrl2::lps::caching

strong

Enumerator
none
local
global

Definition at line 39 of file explorer.h.

exploration_strategy

enum mcrl2::lps::exploration_strategy

Enumerator
es_none
es_breadth
es_depth
es_random
es_value_prioritized
es_value_random_prioritized
es_highway

Definition at line 21 of file exploration_strategy.h.

lps_rewriter_type

enum mcrl2::lps::lps_rewriter_type

An enumerated type for the available lps rewriters.

Enumerator
simplify
quantifier_one_point
condition_one_point

Definition at line 23 of file lps_rewriter_type.h.

t_lin_method

enum mcrl2::lps::t_lin_method

The available linearisation methods.

Enumerator
lmStack
lmRegular
lmRegular2

Definition at line 24 of file linearisation_method.h.

Function Documentation

action_rename() [1/2]

lps::stochastic_specification mcrl2::lps::action_rename ( const action_rename_specification &  action_rename_spec, const lps::stochastic_specification &  lps_old_spec, const data::rewriter &  rewr, const bool  enable_rewriting  )

inline

Rename the actions in a linear specification using a given action_rename_spec.

The actions in a linear specification are renamed according to a given action rename specification. Note that the rules are applied in the order they appear in the specification. This yield quite elaborate conditions in the resulting lps, as a latter rule can only be applied if an earlier rule is not applicable. Note also that there is always a default summand, where the action is not renamed. Using sum elimination and rewriting a substantial reduction of the conditions that are generated can be obtained, often allowing many summands to be removed.

Parameters

action_rename_spec	The action_rename_specification to be used.
lps_old_spec	The input linear specification.
rewr	A data rewriter.

Returns

The lps_old_spec where all actions have been renamed according to action_rename_spec.

Definition at line 428 of file action_rename.h.

action_rename() [2/2]

stochastic_specification mcrl2::lps::action_rename ( const std::regex &  matching_regex, const std::string &  replacing_fmt, const stochastic_specification &  lps_old_spec  )

inline

Rename actions in given specification based on a regular expression and a string that specifies how the replacement should be formatted.

Definition at line 787 of file action_rename.h.

action_rename_rule_to_aterm()

atermpp::aterm mcrl2::lps::action_rename_rule_to_aterm ( const action_rename_rule &  rule )

inline

Definition at line 253 of file action_rename.h.

action_rename_specification_to_aterm()

atermpp::aterm mcrl2::lps::action_rename_specification_to_aterm ( const action_rename_specification &  spec )

inline

Definition at line 259 of file action_rename.h.

action_summand_to_aterm() [1/2]

atermpp::aterm mcrl2::lps::action_summand_to_aterm ( const action_summand &  s )

inline

Conversion to aterm.

Definition at line 172 of file action_summand.h.

action_summand_to_aterm() [2/2]

atermpp::aterm mcrl2::lps::action_summand_to_aterm ( const stochastic_action_summand &  s )

inline

Conversion to aterm.

Definition at line 118 of file stochastic_action_summand.h.

apply_parunfold_replacement_builder()

template<template< class > class Builder, template< template< class > class, class, class > class Binder>

parunfold_replacement< Builder, Binder > mcrl2::lps::apply_parunfold_replacement_builder	(	const lpsparunfold::case_func_replacement &	case_funcs,
		data::set_identifier_generator &	id_generator
	)

Definition at line 753 of file lpsparunfoldlib.h.

changed_variables()

std::set< data::variable > mcrl2::lps::changed_variables ( const action_summand &  summand )

inline

Definition at line 101 of file confluence.h.

check_probability()

void mcrl2::lps::check_probability ( const data::data_expression &  x, const data::rewriter &  rewr  )

inline

Definition at line 81 of file stochastic_state.h.

check_stochastic_state()

void mcrl2::lps::check_stochastic_state ( const stochastic_state &  s, const data::rewriter &  rewr  )

inline

Definition at line 103 of file stochastic_state.h.

check_well_typedness() [1/5]

bool mcrl2::lps::check_well_typedness

(

const linear_process &

x

)

Definition at line 92 of file lps.cpp.

check_well_typedness() [2/5]

template<typename Object >

bool mcrl2::lps::check_well_typedness

(

const Object &

o

)

check_well_typedness() [3/5]

bool mcrl2::lps::check_well_typedness

(

const specification &

x

)

Definition at line 102 of file lps.cpp.

check_well_typedness() [4/5]

bool mcrl2::lps::check_well_typedness

(

const stochastic_linear_process &

x

)

Definition at line 97 of file lps.cpp.

check_well_typedness() [5/5]

bool mcrl2::lps::check_well_typedness

(

const stochastic_specification &

x

)

Definition at line 107 of file lps.cpp.

complete_data_specification() [1/2]

void mcrl2::lps::complete_data_specification ( specification &  spec )

inline

Adds all sorts that appear in the process of l to the data specification of l.

Parameters

spec	A linear process specification

Definition at line 256 of file specification.h.

complete_data_specification() [2/2]

void mcrl2::lps::complete_data_specification ( stochastic_specification &  spec )

inline

Adds all sorts that appear in the process of l to the data specification of l.

Parameters

spec	A linear process specification

Definition at line 104 of file stochastic_specification.h.

constelm()

template<typename DataRewriter , typename Specification >

void mcrl2::lps::constelm	(	Specification &	spec,
		const DataRewriter &	R,
		bool	instantiate_global_variables = false
	)

Removes zero or more constant parameters from the specification spec.

Parameters

spec	A linear process specification
R	A data rewriter
instantiate_global_variables	If true, free variables may be instantiated as a side effect of the algorithm

Definition at line 271 of file constelm.h.

deadlock_summand_to_aterm()

atermpp::aterm mcrl2::lps::deadlock_summand_to_aterm ( const deadlock_summand &  s )

inline

Conversion to atermappl.

Returns

The deadlock summand converted to aterm format.

Definition at line 109 of file deadlock_summand.h.

description() [1/3]

std::string mcrl2::lps::description ( const exploration_strategy  strat )

inline

Definition at line 105 of file exploration_strategy.h.

description() [2/3]

std::string mcrl2::lps::description ( const lps_rewriter_type  type )

inline

Returns a description of a lps rewriter.

Definition at line 68 of file lps_rewriter_type.h.

description() [3/3]

std::string mcrl2::lps::description ( const t_lin_method  lin_method )

inline

Definition at line 42 of file linearisation_method.h.

disjoint()

bool mcrl2::lps::disjoint ( const confluence_summand &  summand1, const confluence_summand &  summand2  )

inline

Indicates whether or not two summands are disjoint.

Definition at line 172 of file confluence.h.

equal_multi_actions()

data::data_expression mcrl2::lps::equal_multi_actions ( const multi_action &  a, const multi_action &  b  )

inline

Returns a data expression that expresses under which conditions the multi actions a and b are equal. The multi actions may contain free variables.

Parameters

a	A sequence of actions
b	A sequence of actions

Returns

Necessary conditions for the equality of a and b

Definition at line 311 of file multi_action.h.

find_action_labels() [1/6]

std::set< process::action_label > mcrl2::lps::find_action_labels

(

const lps::linear_process &

x

)

Definition at line 62 of file lps.cpp.

find_action_labels() [2/6]

std::set< process::action_label > mcrl2::lps::find_action_labels

(

const lps::process_initializer &

x

)

Definition at line 63 of file lps.cpp.

find_action_labels() [3/6]

std::set< process::action_label > mcrl2::lps::find_action_labels

(

const lps::specification &

x

)

Definition at line 64 of file lps.cpp.

find_action_labels() [4/6]

std::set< process::action_label > mcrl2::lps::find_action_labels

(

const lps::stochastic_specification &

x

)

Definition at line 65 of file lps.cpp.

find_action_labels() [5/6]

template<typename T >

std::set< process::action_label > mcrl2::lps::find_action_labels

(

const T &

x

)

Returns all action labels that occur in an object.

Parameters

[in]

x

an object containing action labels

Returns

All action labels that occur in the object x

Definition at line 181 of file find.h.

find_action_labels() [6/6]

template<typename T , typename OutputIterator >

void mcrl2::lps::find_action_labels	(	const T &	x,
		OutputIterator	o
	)

Returns all action labels that occur in an object.

Parameters

[in]	x	an object containing action labels
[in,out]	o	an output iterator to which all action labels occurring in x are written.

Returns

All action labels that occur in the term x

Definition at line 172 of file find.h.

find_all_variables() [1/8]

std::set< data::variable > mcrl2::lps::find_all_variables

(

const lps::deadlock &

x

)

Definition at line 48 of file lps.cpp.

find_all_variables() [2/8]

std::set< data::variable > mcrl2::lps::find_all_variables

(

const lps::linear_process &

x

)

Definition at line 44 of file lps.cpp.

find_all_variables() [3/8]

std::set< data::variable > mcrl2::lps::find_all_variables

(

const lps::multi_action &

x

)

Definition at line 49 of file lps.cpp.

find_all_variables() [4/8]

std::set< data::variable > mcrl2::lps::find_all_variables

(

const lps::specification &

x

)

Definition at line 46 of file lps.cpp.

find_all_variables() [5/8]

std::set< data::variable > mcrl2::lps::find_all_variables

(

const lps::stochastic_linear_process &

x

)

Definition at line 45 of file lps.cpp.

find_all_variables() [6/8]

std::set< data::variable > mcrl2::lps::find_all_variables

(

const lps::stochastic_specification &

x

)

Definition at line 47 of file lps.cpp.

find_all_variables() [7/8]

template<typename T >

std::set< data::variable > mcrl2::lps::find_all_variables

(

const T &

x

)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \return All variables that occur in the object x

Definition at line 40 of file find.h.

find_all_variables() [8/8]

template<typename T , typename OutputIterator >

void mcrl2::lps::find_all_variables	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are written. \return All variables that occur in the term x

Definition at line 31 of file find.h.

find_free_variables() [1/10]

std::set< data::variable > mcrl2::lps::find_free_variables

(

const lps::deadlock &

x

)

Definition at line 54 of file lps.cpp.

find_free_variables() [2/10]

std::set< data::variable > mcrl2::lps::find_free_variables

(

const lps::linear_process &

x

)

Definition at line 50 of file lps.cpp.

find_free_variables() [3/10]

std::set< data::variable > mcrl2::lps::find_free_variables

(

const lps::multi_action &

x

)

Definition at line 55 of file lps.cpp.

find_free_variables() [4/10]

std::set< data::variable > mcrl2::lps::find_free_variables

(

const lps::process_initializer &

x

)

Definition at line 56 of file lps.cpp.

find_free_variables() [5/10]

std::set< data::variable > mcrl2::lps::find_free_variables

(

const lps::specification &

x

)

Definition at line 52 of file lps.cpp.

find_free_variables() [6/10]

std::set< data::variable > mcrl2::lps::find_free_variables

(

const lps::stochastic_linear_process &

x

)

Definition at line 51 of file lps.cpp.

find_free_variables() [7/10]

std::set< data::variable > mcrl2::lps::find_free_variables

(

const lps::stochastic_process_initializer &

x

)

Definition at line 57 of file lps.cpp.

find_free_variables() [8/10]

std::set< data::variable > mcrl2::lps::find_free_variables

(

const lps::stochastic_specification &

x

)

Definition at line 53 of file lps.cpp.

find_free_variables() [9/10]

template<typename T >

std::set< data::variable > mcrl2::lps::find_free_variables

(

const T &

x

)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \return All free variables that occur in the object x

Definition at line 72 of file find.h.

find_free_variables() [10/10]

template<typename T , typename OutputIterator >

void mcrl2::lps::find_free_variables	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are added. \return All free variables that occur in the object x

Definition at line 52 of file find.h.

find_free_variables_with_bound() [1/2]

template<typename T , typename OutputIterator , typename VariableContainer >

void mcrl2::lps::find_free_variables_with_bound	(	const T &	x,
		OutputIterator	o,
		const VariableContainer &	bound
	)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are written. \param[in] bound a container of variables \return All free variables that occur in the object x

Definition at line 63 of file find.h.

find_free_variables_with_bound() [2/2]

template<typename T , typename VariableContainer >

std::set< data::variable > mcrl2::lps::find_free_variables_with_bound	(	const T &	x,
		VariableContainer const &	bound
	)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in] bound a bound a container of variables \return All free variables that occur in the object x

Definition at line 84 of file find.h.

find_function_symbols() [1/4]

std::set< data::function_symbol > mcrl2::lps::find_function_symbols

(

const lps::specification &

x

)

Definition at line 58 of file lps.cpp.

find_function_symbols() [2/4]

std::set< data::function_symbol > mcrl2::lps::find_function_symbols

(

const lps::stochastic_specification &

x

)

Definition at line 59 of file lps.cpp.

find_function_symbols() [3/4]

template<typename T >

std::set< data::function_symbol > mcrl2::lps::find_function_symbols

(

const T &

x

)

\brief Returns all function symbols that occur in an object \param[in] x an object containing function symbols \return All function symbols that occur in the object x

Definition at line 147 of file find.h.

find_function_symbols() [4/4]

template<typename T , typename OutputIterator >

void mcrl2::lps::find_function_symbols	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all function symbols that occur in an object \param[in] x an object containing function symbols \param[in,out] o an output iterator to which all function symbols occurring in x are written. \return All function symbols that occur in the term x

Definition at line 138 of file find.h.

find_identifiers() [1/4]

std::set< core::identifier_string > mcrl2::lps::find_identifiers

(

const lps::specification &

x

)

Definition at line 60 of file lps.cpp.

find_identifiers() [2/4]

std::set< core::identifier_string > mcrl2::lps::find_identifiers

(

const lps::stochastic_specification &

x

)

Definition at line 61 of file lps.cpp.

find_identifiers() [3/4]

template<typename T >

std::set< core::identifier_string > mcrl2::lps::find_identifiers

(

const T &

x

)

\brief Returns all identifiers that occur in an object \param[in] x an object containing identifiers \return All identifiers that occur in the object x

Definition at line 105 of file find.h.

find_identifiers() [4/4]

template<typename T , typename OutputIterator >

void mcrl2::lps::find_identifiers	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all identifiers that occur in an object \param[in] x an object containing identifiers \param[in,out] o an output iterator to which all identifiers occurring in x are written. \return All identifiers that occur in the term x

Definition at line 96 of file find.h.

find_representative()

template<typename Node , typename GenerateSuccessors >

Node mcrl2::lps::find_representative	(	Node &	u0,
		GenerateSuccessors	generate_successors
	)

Search for a unique representative in a graph.

Parameters

u0	The root of the graph.
generate_successors	A function that generates successors of a node.

This function is based on an iterative version of Tarjan's strongly connected components algorithm. It returns the smallest node of the first SCC that is detected. The first SCC is a TSCC, meaning that it has no outgoing edges. In a confluent tau graph there is only one TSCC, so this should guarantee a unique representative. N.B. The implementation is based on https://llbit.se/?p=3379

Definition at line 32 of file find_representative.h.

find_sort_expressions() [1/4]

std::set< data::sort_expression > mcrl2::lps::find_sort_expressions

(

const lps::specification &

x

)

Definition at line 42 of file lps.cpp.

find_sort_expressions() [2/4]

std::set< data::sort_expression > mcrl2::lps::find_sort_expressions

(

const lps::stochastic_specification &

x

)

Definition at line 43 of file lps.cpp.

find_sort_expressions() [3/4]

template<typename T >

std::set< data::sort_expression > mcrl2::lps::find_sort_expressions

(

const T &

x

)

\brief Returns all sort expressions that occur in an object \param[in] x an object containing sort expressions \return All sort expressions that occur in the object x

Definition at line 126 of file find.h.

find_sort_expressions() [4/4]

template<typename T , typename OutputIterator >

void mcrl2::lps::find_sort_expressions	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all sort expressions that occur in an object \param[in] x an object containing sort expressions \param[in,out] o an output iterator to which all sort expressions occurring in x are written. \return All sort expressions that occur in the term x

Definition at line 117 of file find.h.

finite_sorts()

std::set< data::sort_expression > mcrl2::lps::finite_sorts ( const data::data_specification &  s )

inline

Return a set with all finite sorts in data specification s.

Definition at line 28 of file suminst.h.

generate_values()

std::vector< std::string > mcrl2::lps::generate_values ( const data::data_specification &  dataspec, const data::sort_expression &  s, std::size_t  max_size = 1000  )

inline

Generates possible values of the data type (at most max_size).

Definition at line 41 of file ltsmin.h.

has_ctau_action()

template<typename Specification >

bool mcrl2::lps::has_ctau_action

(

const Specification &

lpsspec

)

Definition at line 195 of file confluence.h.

if_rewrite() [1/2]

template<typename T >

T mcrl2::lps::if_rewrite	(	const T &	x,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Applies the one point rule rewriter to all embedded data expressions in an object x.

Parameters

x	an object containing data expressions

Returns

the rewrite result

Definition at line 54 of file if_rewrite.h.

if_rewrite() [2/2]

template<typename T >

void mcrl2::lps::if_rewrite	(	T &	x,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Applies the one point rule rewriter to all embedded data expressions in an object x.

Parameters

x	an object containing data expressions

Definition at line 44 of file if_rewrite.h.

initial_distribution() [1/2]

const stochastic_distribution & mcrl2::lps::initial_distribution ( const lps::specification &  )

inline

Definition at line 257 of file explorer.h.

initial_distribution() [2/2]

const stochastic_distribution & mcrl2::lps::initial_distribution ( const lps::stochastic_specification &  lpsspec )

inline

Definition at line 264 of file explorer.h.

insert_case_functions() [1/2]

template<typename T >

void mcrl2::lps::insert_case_functions	(	T &	x,
		const lpsparunfold::case_func_replacement &	cfv,
		data::set_identifier_generator &	id_generator,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Definition at line 760 of file lpsparunfoldlib.h.

insert_case_functions() [2/2]

template<typename T >

void mcrl2::lps::insert_case_functions	(	T &	x,
		const lpsparunfold::case_func_replacement &	cfv,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Definition at line 770 of file lpsparunfoldlib.h.

is_linear_process()

bool mcrl2::lps::is_linear_process ( const atermpp::aterm &  x )

inline

Test for a linear_process expression.

Parameters

x

A term

Returns

True if x is a linear process expression

Definition at line 266 of file linear_process.h.

is_multi_action()

bool mcrl2::lps::is_multi_action ( const atermpp::aterm &  x )

inline

\brief Test for a multi_action expression \param x A term \return True if \a x is a multi_action expression

Definition at line 118 of file multi_action.h.

is_process_initializer()

bool mcrl2::lps::is_process_initializer ( const atermpp::aterm &  x )

inline

\brief Test for a process_initializer expression \param x A term \return True if \a x is a process_initializer expression

Definition at line 86 of file process_initializer.h.

is_specification()

bool mcrl2::lps::is_specification ( const atermpp::aterm &  x )

inline

Test for a specification expression.

Parameters

x

A term

Returns

True if x is a specification expression

Definition at line 44 of file specification.h.

is_stochastic()

template<typename T >

bool mcrl2::lps::is_stochastic

(

const T &

x

)

Returns true if the LPS object x contains a stochastic distribution in one of its attributes.

Definition at line 50 of file is_stochastic.h.

is_stochastic_distribution()

bool mcrl2::lps::is_stochastic_distribution ( const atermpp::aterm &  x )

inline

\brief Test for a stochastic_distribution expression \param x A term \return True if \a x is a stochastic_distribution expression

Definition at line 87 of file stochastic_distribution.h.

is_stochastic_process_initializer()

bool mcrl2::lps::is_stochastic_process_initializer ( const atermpp::aterm &  x )

inline

\brief Test for a stochastic_process_initializer expression \param x A term \return True if \a x is a stochastic_process_initializer expression

Definition at line 69 of file stochastic_process_initializer.h.

linear_process_specification_marker()

atermpp::aterm mcrl2::lps::linear_process_specification_marker

(

)

Definition at line 18 of file lps_io.cpp.

linear_process_to_aterm()

template<typename ActionSummand >

atermpp::aterm mcrl2::lps::linear_process_to_aterm

(

const linear_process_base< ActionSummand > &

p

)

Conversion to aterm.

Returns

The action summand converted to aterm format.

Definition at line 227 of file linear_process.h.

linearise() [1/2]

mcrl2::lps::stochastic_specification mcrl2::lps::linearise	(	const mcrl2::process::process_specification &	type_checked_spec,
		mcrl2::lps::t_lin_options	lin_options = t_lin_options()
	)

Linearises a process specification.

Parameters

[in]	type_checked_spec	A process specification
[in]	lin_options	options that should be used during linearisation

Returns

An LPS equivalent to spec, which is linearised using lin_options

Exceptions

mcrl2::runtime_error

Linearisation failed

Definition at line 11262 of file linearise.cpp.

linearise() [2/2]

mcrl2::lps::stochastic_specification mcrl2::lps::linearise ( const std::string &  text, mcrl2::lps::t_lin_options  lin_options = t_lin_options()  )

inline

Linearises a process specification from a textual specification.

Parameters

[in]	text	A string containing a process specification
[in]	lin_options	options that should be used during linearisation

Returns

An LPS equivalent to the specification representing text, which is linearised using lin_options

Exceptions

mcrl2::runtime_error

Linearisation failed

Definition at line 79 of file linearise.h.

load_lps() [1/2]

template<typename Specification >

void mcrl2::lps::load_lps	(	Specification &	spec,
		const std::string &	filename
	)

Load LPS from file.

Parameters

spec	The LPS to which the result is loaded.
filename	The file from which to load the LPS. If empty, the file is read from stdin.

Definition at line 95 of file io.h.

load_lps() [2/2]

template<typename Specification >

void mcrl2::lps::load_lps	(	Specification &	spec,
		std::istream &	stream,
		const std::string &	source = ""
	)

Load LPS from file.

Parameters

spec	The LPS to which the result is loaded.
stream	The stream from which to load the LPS (it is assumed to have been opened in the right mode).
source	The source from which the stream originates. Used for error messages.

Definition at line 54 of file io.h.

lpsbinary()

void mcrl2::lps::lpsbinary	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const std::string &	parameter_selection
	)

Definition at line 31 of file tools.cpp.

lpsconstelm()

void mcrl2::lps::lpsconstelm	(	const std::string &	input_filename,
		const std::string &	output_filename,
		data::rewriter::strategy	rewrite_strategy,
		bool	instantiate_free_variables,
		bool	ignore_conditions,
		bool	remove_trivial_summands,
		bool	remove_singleton_sorts
	)

Definition at line 43 of file tools.cpp.

lpsinfo()

void mcrl2::lps::lpsinfo	(	const std::string &	input_filename,
		const std::string &	input_file_message
	)

Definition at line 75 of file tools.cpp.

lpsinvelm()

bool mcrl2::lps::lpsinvelm	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const std::string &	invariant_filename,
		const std::string &	dot_file_name,
		data::rewriter::strategy	rewrite_strategy,
		data::detail::smt_solver_type	solver_type,
		const bool	no_check,
		const bool	no_elimination,
		const bool	simplify_all,
		const bool	all_violations,
		const bool	counter_example,
		const bool	path_eliminator,
		const bool	apply_induction,
		const int	time_limit
	)

Definition at line 86 of file tools.cpp.

lpsparelm()

void mcrl2::lps::lpsparelm	(	const std::string &	input_filename,
		const std::string &	output_filename
	)

Definition at line 161 of file tools.cpp.

lpspp()

void mcrl2::lps::lpspp	(	const std::string &	input_filename,
		const std::string &	output_filename,
		bool	print_summand_numbers,
		core::print_format_type	format
	)

Definition at line 171 of file tools.cpp.

lpsrewr()

void mcrl2::lps::lpsrewr	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const data::rewriter::strategy	rewrite_strategy,
		const lps::lps_rewriter_type	rewriter_type
	)

Definition at line 213 of file tools.cpp.

lpssumelm()

void mcrl2::lps::lpssumelm	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const bool	decluster
	)

Definition at line 246 of file tools.cpp.

lpssuminst()

void mcrl2::lps::lpssuminst	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const data::rewriter::strategy	rewrite_strategy,
		const std::string &	sorts_string,
		const bool	finite_sorts_only,
		const bool	tau_summands_only
	)

Definition at line 259 of file tools.cpp.

lpsuntime()

void mcrl2::lps::lpsuntime	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const bool	add_invariants,
		const bool	apply_fourier_motzkin,
		const data::rewriter::strategy	rewrite_strategy
	)

Definition at line 296 of file tools.cpp.

make_assignment_list()

data::assignment_list mcrl2::lps::make_assignment_list ( const data::variable_list &  variables, const data::data_expression_list &  expressions  )

inline

Definition at line 113 of file confluence.h.

make_ctau_act_id()

process::action_label mcrl2::lps::make_ctau_act_id ( )

inline

Creates an identifier for the ctau action.

Definition at line 181 of file confluence.h.

make_ctau_action()

process::action mcrl2::lps::make_ctau_action ( )

inline

Creates the ctau action.

Definition at line 188 of file confluence.h.

make_data_expression_vector()

std::vector< data::data_expression > mcrl2::lps::make_data_expression_vector ( const data::data_expression_list &  v )

inline

Definition at line 55 of file explorer.h.

make_multi_action()

template<class... ARGUMENTS>

void mcrl2::lps::make_multi_action ( atermpp::aterm &  t, const ARGUMENTS &...  args  )

inline

\brief Make_multi_action constructs a new term into a given address. \

Parameters

t	The reference into which the new multi_action is constructed.

Definition at line 103 of file multi_action.h.

make_process_initializer()

template<class EXPRESSION_LIST >

void mcrl2::lps::make_process_initializer ( atermpp::aterm &  t, EXPRESSION_LIST  args  )

inline

Definition at line 69 of file process_initializer.h.

make_state() [1/2]

template<class ForwardTraversalIterator >

void mcrl2::lps::make_state	(	state &	result,
		ForwardTraversalIterator	p,
		const std::size_t	size
	)

Definition at line 37 of file state.h.

make_state() [2/2]

template<class ForwardTraversalIterator , class Transformer >

void mcrl2::lps::make_state	(	state &	result,
		ForwardTraversalIterator	p,
		const std::size_t	size,
		Transformer	transformer
	)

Definition at line 27 of file state.h.

make_stochastic_distribution()

template<class... ARGUMENTS>

void mcrl2::lps::make_stochastic_distribution ( atermpp::aterm &  t, const ARGUMENTS &...  args  )

inline

\brief Make_stochastic_distribution constructs a new term into a given address. \

Parameters

t	The reference into which the new stochastic_distribution is constructed.

Definition at line 72 of file stochastic_distribution.h.

make_stochastic_process_initializer()

template<class... ARGUMENTS>

void mcrl2::lps::make_stochastic_process_initializer ( atermpp::aterm &  t, ARGUMENTS...  args  )

inline

Definition at line 52 of file stochastic_process_initializer.h.

normalize_sorts() [1/5]

lps::multi_action mcrl2::lps::normalize_sorts	(	const multi_action &	x,
		const data::sort_specification &	sortspec
	)

Definition at line 38 of file lps.cpp.

normalize_sorts() [2/5]

template<typename T >

T mcrl2::lps::normalize_sorts	(	const T &	x,
		const data::sort_specification &	sortspec,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= 0
	)

Definition at line 34 of file normalize_sorts.h.

normalize_sorts() [3/5]

void mcrl2::lps::normalize_sorts	(	lps::specification &	x,
		const data::sort_specification &	sortspec
	)

Definition at line 39 of file lps.cpp.

normalize_sorts() [4/5]

void mcrl2::lps::normalize_sorts	(	lps::stochastic_specification &	x,
		const data::sort_specification &	sortspec
	)

Definition at line 40 of file lps.cpp.

normalize_sorts() [5/5]

template<typename T >

void mcrl2::lps::normalize_sorts	(	T &	x,
		const data::sort_specification &	sortspec,
		typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Definition at line 25 of file normalize_sorts.h.

not_equal_multi_actions()

data::data_expression mcrl2::lps::not_equal_multi_actions ( const multi_action &  a, const multi_action &  b  )

inline

Returns a pbes expression that expresses under which conditions the multi actions a and b are not equal. The multi actions may contain free variables.

Parameters

a	A sequence of actions
b	A sequence of actions

Returns

Necessary conditions for the inequality of a and b

Definition at line 359 of file multi_action.h.

nr_of_booleans_for_elements()

std::size_t mcrl2::lps::nr_of_booleans_for_elements ( std::size_t  n )

inline

Definition at line 27 of file binary.h.

one_point_condition_rewrite() [1/2]

template<typename T , typename DataRewriter >

T mcrl2::lps::one_point_condition_rewrite	(	const T &	x,
		const DataRewriter &	R,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Applies the one point condition rewriter to all embedded data expressions in an object x.

Parameters

x	an object containing data expressions

Returns

the rewrite result

Definition at line 175 of file one_point_condition_rewrite.h.

one_point_condition_rewrite() [2/2]

template<typename T , typename DataRewriter >

void mcrl2::lps::one_point_condition_rewrite	(	T &	x,
		const DataRewriter &	R,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Applies the one point condition rewriter to all embedded data expressions in an object x.

Parameters

x	an object containing data expressions

Definition at line 165 of file one_point_condition_rewrite.h.

one_point_rule_rewrite() [1/2]

template<typename T >

T mcrl2::lps::one_point_rule_rewrite	(	const T &	x,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Applies the one point rule rewriter to all embedded data expressions in an object x.

Parameters

x	an object containing data expressions

Returns

the rewrite result

Definition at line 56 of file one_point_rule_rewrite.h.

one_point_rule_rewrite() [2/2]

template<typename T >

void mcrl2::lps::one_point_rule_rewrite	(	T &	x,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Applies the one point rule rewriter to all embedded data expressions in an object x.

Parameters

x	an object containing data expressions

Definition at line 46 of file one_point_rule_rewrite.h.

operator!=() [1/2]

bool mcrl2::lps::operator!= ( const specification &  spec1, const specification &  spec2  )

inline

Inequality operator.

Definition at line 248 of file specification.h.

operator!=() [2/2]

bool mcrl2::lps::operator!= ( const stochastic_specification &  spec1, const stochastic_specification &  spec2  )

inline

Inequality operator.

Definition at line 94 of file stochastic_specification.h.

operator<() [1/2]

bool mcrl2::lps::operator< ( const action_summand &  x, const action_summand &  y  )

inline

Comparison operator for action summands.

Definition at line 143 of file action_summand.h.

operator<() [2/2]

bool mcrl2::lps::operator< ( const stochastic_action_summand &  x, const stochastic_action_summand &  y  )

inline

Comparison operator for action summands.

Definition at line 100 of file stochastic_action_summand.h.

operator<<() [1/25]

atermpp::aterm_ostream & mcrl2::lps::operator<<	(	atermpp::aterm_ostream &	stream,
		const deadlock_summand &	summand
	)

Definition at line 42 of file lps_io.cpp.

operator<<() [2/25]

template<typename ActionSummand >

atermpp::aterm_ostream & mcrl2::lps::operator<<	(	atermpp::aterm_ostream &	stream,
		const linear_process_base< ActionSummand > &	lps
	)

Definition at line 97 of file lps_io.cpp.

operator<<() [3/25]

atermpp::aterm_ostream & mcrl2::lps::operator<<	(	atermpp::aterm_ostream &	stream,
		const multi_action &	action
	)

Definition at line 23 of file lps_io.cpp.

operator<<() [4/25]

atermpp::aterm_ostream & mcrl2::lps::operator<<	(	atermpp::aterm_ostream &	stream,
		const specification &	spec
	)

Writes LPS to the stream.

Definition at line 171 of file lps_io.cpp.

operator<<() [5/25]

atermpp::aterm_ostream & mcrl2::lps::operator<<	(	atermpp::aterm_ostream &	stream,
		const stochastic_action_summand &	summand
	)

Definition at line 64 of file lps_io.cpp.

operator<<() [6/25]

atermpp::aterm_ostream & mcrl2::lps::operator<<	(	atermpp::aterm_ostream &	stream,
		const stochastic_specification &	spec
	)

Definition at line 177 of file lps_io.cpp.

operator<<() [7/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  os, caching  c  )

inline

Definition at line 42 of file explorer.h.

operator<<() [8/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  os, const exploration_strategy  strat  )

inline

Definition at line 99 of file exploration_strategy.h.

operator<<() [9/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  os, const lps_rewriter_type  t  )

inline

Definition at line 103 of file lps_rewriter_type.h.

operator<<() [10/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  os, const t_lin_method  l  )

inline

Definition at line 96 of file linearisation_method.h.

operator<<() [11/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const action_summand &  x  )

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 129 of file action_summand.h.

operator<<() [12/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const deadlock &  x  )

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 102 of file deadlock.h.

operator<<() [13/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const deadlock_summand &  x  )

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 94 of file deadlock_summand.h.

operator<<() [14/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const explorer_options &  options  )

inline

Definition at line 75 of file explorer_options.h.

operator<<() [15/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const explorer_summand &  summand  )

inline

Definition at line 430 of file explorer.h.

operator<<() [16/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const linear_process &  x  )

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 256 of file linear_process.h.

operator<<() [17/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const multi_action &  x  )

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 131 of file multi_action.h.

operator<<() [18/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const probabilistic_data_expression &  x  )

inline

Pretty print to an outstream.

Definition at line 547 of file probabilistic_data_expression.h.

operator<<() [19/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const process_initializer &  x  )

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 99 of file process_initializer.h.

operator<<() [20/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const specification &  x  )

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 209 of file specification.h.

operator<<() [21/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const stochastic_action_summand &  x  )

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 86 of file stochastic_action_summand.h.

operator<<() [22/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const stochastic_distribution &  x  )

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 100 of file stochastic_distribution.h.

operator<<() [23/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const stochastic_linear_process &  x  )

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 88 of file stochastic_linear_process.h.

operator<<() [24/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const stochastic_process_initializer &  x  )

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 82 of file stochastic_process_initializer.h.

operator<<() [25/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out, const stochastic_specification &  x  )

inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 80 of file stochastic_specification.h.

operator==() [1/4]

bool mcrl2::lps::operator== ( const action_summand &  x, const action_summand &  y  )

inline

Equality operator of action summands.

Definition at line 162 of file action_summand.h.

operator==() [2/4]

bool mcrl2::lps::operator== ( const specification &  spec1, const specification &  spec2  )

inline

Equality operator.

Definition at line 241 of file specification.h.

operator==() [3/4]

bool mcrl2::lps::operator== ( const stochastic_action_summand &  x, const stochastic_action_summand &  y  )

inline

Equality operator of stochastic action summands.

Definition at line 111 of file stochastic_action_summand.h.

operator==() [4/4]

bool mcrl2::lps::operator== ( const stochastic_specification &  spec1, const stochastic_specification &  spec2  )

inline

Definition at line 87 of file stochastic_specification.h.

operator>>() [1/9]

atermpp::aterm_istream & mcrl2::lps::operator>>	(	atermpp::aterm_istream &	stream,
		deadlock_summand &	summand
	)

Definition at line 50 of file lps_io.cpp.

operator>>() [2/9]

template<typename ActionSummand >

atermpp::aterm_istream & mcrl2::lps::operator>>	(	atermpp::aterm_istream &	stream,
		linear_process_base< ActionSummand > &	lps
	)

Definition at line 107 of file lps_io.cpp.

operator>>() [3/9]

atermpp::aterm_istream & mcrl2::lps::operator>>	(	atermpp::aterm_istream &	stream,
		multi_action &	action
	)

Definition at line 30 of file lps_io.cpp.

operator>>() [4/9]

atermpp::aterm_istream & mcrl2::lps::operator>>	(	atermpp::aterm_istream &	stream,
		lps::specification &	spec
	)

Reads LPS from the stream.

Definition at line 183 of file lps_io.cpp.

operator>>() [5/9]

atermpp::aterm_istream & mcrl2::lps::operator>>	(	atermpp::aterm_istream &	stream,
		stochastic_action_summand &	summand
	)

Definition at line 74 of file lps_io.cpp.

operator>>() [6/9]

atermpp::aterm_istream & mcrl2::lps::operator>>	(	atermpp::aterm_istream &	stream,
		lps::stochastic_specification &	spec
	)

Definition at line 191 of file lps_io.cpp.

operator>>() [7/9]

std::istream & mcrl2::lps::operator>> ( std::istream &  is, exploration_strategy &  strat  )

inline

Definition at line 83 of file exploration_strategy.h.

operator>>() [8/9]

std::istream & mcrl2::lps::operator>> ( std::istream &  is, lps_rewriter_type &  t  )

inline

Stream operator for rewriter type.

Parameters

is	An input stream
t	A rewriter type

Returns

The input stream

Definition at line 87 of file lps_rewriter_type.h.

operator>>() [9/9]

std::istream & mcrl2::lps::operator>> ( std::istream &  is, t_lin_method &  l  )

inline

Definition at line 79 of file linearisation_method.h.

order_summand_variables()

template<typename Specification >

void mcrl2::lps::order_summand_variables

(

Specification &

lpsspec

)

Order summand variables to make enumeration over these variables more efficient.

Definition at line 23 of file order_summand_variables.h.

parelm()

template<typename Specification >

void mcrl2::lps::parelm	(	Specification &	spec,
		bool	variant1 = true
	)

Removes unused parameters from a linear process specification.

Parameters

spec	A linear process specification
variant1	If true the default variant of parelm is used, otherwise an alternative implementation is chosen.

Definition at line 273 of file parelm.h.

parse_action()

process::action mcrl2::lps::parse_action ( const std::string &  text, const process::action_label_list &  action_decls, const data::data_specification &  data_spec = data::detail::default_specification()  )

inline

Parses an action from a string.

Parameters

	text	A string containing an action
	action_decls	An action declaration
[in]	data_spec	A data specification used for sort normalization

Returns

An action

Exceptions

mcrl2::runtime_error

when the input does not match the syntax of an action.

Definition at line 211 of file parse.h.

parse_action_rename_specification() [1/2]

action_rename_specification mcrl2::lps::parse_action_rename_specification ( const std::string &  spec_string, const lps::stochastic_specification &  spec  )

inline

Parses an action rename specification. Parses an acion rename specification. If the action rename specification contains data types that are not present in the data specification of spec they are added to it.

Parameters

spec_string	A string containing an action rename specification.
spec	A linear process specification

Returns

An action rename specification

Definition at line 110 of file parse.h.

parse_action_rename_specification() [2/2]

action_rename_specification mcrl2::lps::parse_action_rename_specification ( std::istream &  in, const lps::stochastic_specification &  spec  )

inline

Parses a process specification from an input stream.

Parameters

in	An input stream
spec	A linear process specification.

Returns

The parse result

Definition at line 94 of file parse.h.

parse_exploration_strategy()

exploration_strategy mcrl2::lps::parse_exploration_strategy ( const std::string &  s )

inline

Definition at line 31 of file exploration_strategy.h.

parse_lin_method()

t_lin_method mcrl2::lps::parse_lin_method ( const std::string &  s )

inline

Parse a linearisation method.

Parameters

[in]

s

A string

Returns

The linearisation method represented by s

Definition at line 57 of file linearisation_method.h.

parse_linear_process_specification() [1/2]

specification mcrl2::lps::parse_linear_process_specification ( const std::string &  text )

inline

Parses a linear process specification from a string.

Parameters

text	A string containing a linear process specification

Returns

The parsed specification

Exceptions

non_linear_process	if a non-linear sub-expression is encountered.
mcrl2::runtime_error	in the following cases: The number of equations is not equal to one The initial process is not a process instance, or it does not match with the equation A sequential process is found with a right hand side that is not a process instance, or it doesn't match the equation

Definition at line 152 of file parse.h.

parse_linear_process_specification() [2/2]

specification mcrl2::lps::parse_linear_process_specification ( std::istream &  spec_stream )

inline

Parses a linear process specification from an input stream.

Parameters

spec_stream

An input stream containing a linear process specification

Returns

The parsed specification

Exceptions

non_linear_process	if a non-linear sub-expression is encountered.
mcrl2::runtime_error	in the following cases: The number of equations is not equal to one The initial process is not a process instance, or it does not match with the equation A sequential process is found with a right hand side that is not a process instance, or it doesn't match the equation

Definition at line 128 of file parse.h.

parse_lps() [1/2]

template<typename Specification >

void mcrl2::lps::parse_lps	(	const std::string &	text,
		Specification &	result
	)

Definition at line 197 of file parse.h.

parse_lps() [2/2]

template<typename Specification >

void mcrl2::lps::parse_lps	(	std::istream &	,
		Specification &
	)

Definition at line 159 of file parse.h.

parse_lps< specification >()

template<>

void mcrl2::lps::parse_lps< specification > ( std::istream &  from, specification &  result  )

inline

Definition at line 166 of file parse.h.

parse_lps< stochastic_specification >()

template<>

void mcrl2::lps::parse_lps< stochastic_specification > ( std::istream &  from, stochastic_specification &  result  )

inline

Parses a stochastic linear process specification from an input stream.

Parameters

from	An input stream containing a linear process specification.
result	An output parameter in which the parsed stochastic process is put.

Returns

The parsed specification.

Exceptions

non_linear_process	if a non-linear sub-expression is encountered.
mcrl2::runtime_error	in the following cases: The number of equations is not equal to one. The initial process is not a process instance, or it does not match with the equation. A sequential process is found with a right hand side that is not a process instance, or it doesn't match the equation.

Definition at line 183 of file parse.h.

parse_lps_rewriter_type()

lps_rewriter_type mcrl2::lps::parse_lps_rewriter_type ( const std::string &  type )

inline

Parses a lps rewriter type.

Definition at line 32 of file lps_rewriter_type.h.

parse_multi_action() [1/4]

multi_action mcrl2::lps::parse_multi_action ( const std::string &  text, const process::action_label_list &  action_decls, const data::data_specification &  data_spec = data::detail::default_specification()  )

inline

Parses a multi_action from a string.

Parameters

	text	A string containing a multi_action
[in]	action_decls	A list of allowed action labels that is used for type checking.
[in]	data_spec	The data specification that is used for type checking.

Returns

The parsed multi_action

Exceptions

mcrl2::runtime_error

when the input does not match the syntax of a multi action.

Definition at line 70 of file parse.h.

parse_multi_action() [2/4]

multi_action mcrl2::lps::parse_multi_action ( const std::string &  text, multi_action_type_checker &  typechecker, const data::data_specification &  data_spec = data::detail::default_specification()  )

inline

Parses a multi_action from a string.

Parameters

	text	A string containing a multi_action
[in]	typechecker	Typechecker used to check the action.
[in]	data_spec	The data specification that is used for type checking.

Returns

The parsed multi_action

Exceptions

mcrl2::runtime_error

when the input does not match the syntax of a multi action.

Definition at line 83 of file parse.h.

parse_multi_action() [3/4]

multi_action mcrl2::lps::parse_multi_action ( std::stringstream &  in, const process::action_label_list &  action_decls, const data::data_specification &  data_spec = data::detail::default_specification()  )

inline

Parses a multi_action from an input stream.

Parameters

	in	An input stream containing a multi_action
[in]	action_decls	A list of allowed action labels that is used for type checking.
[in]	data_spec	The data specification that is used for type checking.

Returns

The parsed multi_action

Exceptions

mcrl2::runtime_error

when the input does not match the syntax of a multi action.

Definition at line 42 of file parse.h.

parse_multi_action() [4/4]

multi_action mcrl2::lps::parse_multi_action ( std::stringstream &  in, multi_action_type_checker &  typechecker, const data::data_specification &  data_spec = data::detail::default_specification()  )

inline

Parses a multi_action from an input stream.

Parameters

	in	An input stream containing a multi_action
[in]	typechecker	Typechecker used to check the action.
[in]	data_spec	The data specification that is used for type checking.

Returns

The parsed multi_action

Exceptions

mcrl2::runtime_error

when the input does not match the syntax of a multi action.

Definition at line 56 of file parse.h.

pp() [1/15]

std::string mcrl2::lps::pp

(

const action_summand &

x

)

Definition at line 26 of file lps.cpp.

pp() [2/15]

std::string mcrl2::lps::pp

(

const deadlock &

x

)

Definition at line 27 of file lps.cpp.

pp() [3/15]

std::string mcrl2::lps::pp

(

const deadlock_summand &

x

)

Definition at line 28 of file lps.cpp.

pp() [4/15]

std::string mcrl2::lps::pp

(

const linear_process &

x

)

Definition at line 29 of file lps.cpp.

pp() [5/15]

std::string mcrl2::lps::pp ( const lps::state &  x )

inline

Definition at line 49 of file state.h.

pp() [6/15]

std::string mcrl2::lps::pp

(

const multi_action &

x

)

Definition at line 30 of file lps.cpp.

pp() [7/15]

std::string mcrl2::lps::pp ( const probabilistic_data_expression &  l )

inline

Definition at line 539 of file probabilistic_data_expression.h.

pp() [8/15]

std::string mcrl2::lps::pp

(

const process_initializer &

x

)

Definition at line 31 of file lps.cpp.

pp() [9/15]

std::string mcrl2::lps::pp

(

const specification &

x

)

Definition at line 32 of file lps.cpp.

pp() [10/15]

std::string mcrl2::lps::pp

(

const stochastic_action_summand &

x

)

Definition at line 33 of file lps.cpp.

pp() [11/15]

std::string mcrl2::lps::pp

(

const stochastic_distribution &

x

)

Definition at line 34 of file lps.cpp.

pp() [12/15]

std::string mcrl2::lps::pp

(

const stochastic_linear_process &

x

)

Definition at line 35 of file lps.cpp.

pp() [13/15]

std::string mcrl2::lps::pp

(

const stochastic_process_initializer &

x

)

Definition at line 36 of file lps.cpp.

pp() [14/15]

std::string mcrl2::lps::pp

(

const stochastic_specification &

x

)

Definition at line 37 of file lps.cpp.

pp() [15/15]

template<typename T >

std::string mcrl2::lps::pp

(

const T &

x

)

Returns a string representation of the object x.

Definition at line 331 of file print.h.

pp_with_summand_numbers() [1/2]

std::string mcrl2::lps::pp_with_summand_numbers

(

const specification &

x

)

Definition at line 74 of file lps.cpp.

pp_with_summand_numbers() [2/2]

std::string mcrl2::lps::pp_with_summand_numbers

(

const stochastic_specification &

x

)

Definition at line 83 of file lps.cpp.

print_confluence_summand()

std::string mcrl2::lps::print_confluence_summand ( const confluence_summand &  summand, const data::variable_list &  process_parameters  )

inline

Definition at line 157 of file confluence.h.

print_exploration_strategy()

std::string mcrl2::lps::print_exploration_strategy ( const exploration_strategy  es )

inline

Definition at line 61 of file exploration_strategy.h.

print_lin_method()

std::string mcrl2::lps::print_lin_method ( const t_lin_method  lin_method )

inline

String representation of a linearisation method.

Parameters

[in]

lin_method

A linerisation method

Returns

String representation of lin_method

Definition at line 30 of file linearisation_method.h.

print_lps_rewriter_type()

std::string mcrl2::lps::print_lps_rewriter_type ( const lps_rewriter_type  type )

inline

Prints a lps rewriter type.

Definition at line 51 of file lps_rewriter_type.h.

print_probability()

std::string mcrl2::lps::print_probability ( const data::data_expression &  x )

inline

Definition at line 74 of file stochastic_state.h.

read_spec()

static void mcrl2::lps::read_spec ( atermpp::aterm_istream &  stream, stochastic_specification &  spec  )

static

Definition at line 136 of file lps_io.cpp.

remove_parameters()

template<typename Object >

void mcrl2::lps::remove_parameters	(	Object &	x,
		const std::set< data::variable > &	to_be_removed
	)

Rewrites an LPS data type.

Definition at line 190 of file remove.h.

remove_redundant_assignments() [1/2]

data::assignment_list mcrl2::lps::remove_redundant_assignments ( const data::assignment_list &  assignments, const data::variable_list &  do_not_remove  )

inline

Removes assignments of the form x := x from v for variables x that are not contained in do_not_remove.

Definition at line 229 of file remove.h.

remove_redundant_assignments() [2/2]

template<typename Specification >

void mcrl2::lps::remove_redundant_assignments

(

Specification &

lpsspec

)

Removes redundant assignments of the form x = x from an LPS specification.

Parameters

lpsspec

A linear process specification

Definition at line 247 of file remove.h.

remove_singleton_sorts()

template<typename Specification >

void mcrl2::lps::remove_singleton_sorts

(

Specification &

spec

)

Removes parameters with a singleton sort from a linear process specification.

Parameters

spec	A linear process specification

Definition at line 211 of file remove.h.

remove_stochastic_operators()

specification mcrl2::lps::remove_stochastic_operators ( const stochastic_specification &  spec )

inline

Converts a stochastic specification to a specification. Throws an exception if non-empty distributions are encountered.

Definition at line 113 of file stochastic_specification.h.

remove_trivial_summands()

template<typename Specification >

void mcrl2::lps::remove_trivial_summands

(

Specification &

spec

)

Removes summands with condition equal to false from a linear process specification.

Parameters

spec	A linear process specification

Definition at line 199 of file remove.h.

replace_constants_by_variables() [1/2]

template<typename T >

T mcrl2::lps::replace_constants_by_variables	(	const T &	x,
		const data::rewriter &	r,
		data::mutable_indexed_substitution<> &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times.

Definition at line 55 of file replace_constants_by_variables.h.

replace_constants_by_variables() [2/2]

template<typename T >

void mcrl2::lps::replace_constants_by_variables	(	T &	x,
		const data::rewriter &	r,
		data::mutable_indexed_substitution<> &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times.

Definition at line 41 of file replace_constants_by_variables.h.

replace_variables_capture_avoiding() [1/6]

template<typename Substitution >

stochastic_distribution mcrl2::lps::replace_variables_capture_avoiding	(	const stochastic_distribution &	x,
		data::data_expression_list &	pars,
		Substitution &	sigma
	)

\brief Applies sigma as a capture avoiding substitution to a stochastic_distribution and a list of parameters. \param x The object to which the substiution is applied. \param pars The parameters of which the variables are bound. This list is changed if necessary. \param sigma A substitution.

Definition at line 277 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [2/6]

template<typename Substitution >

stochastic_distribution mcrl2::lps::replace_variables_capture_avoiding	(	const stochastic_distribution &	x,
		data::data_expression_list &	pars,
		Substitution &	sigma,
		data::set_identifier_generator &	id_generator
	)

\brief Applies sigma as a capture avoiding substitution to x with x a distribution.. \details The capture avoiding substitution must also be applied to the expression to which the distribution is applied. \param x The object to which the substiution is applied. \param pars The parameter list to which the distribution is applied. \param sigma A substitution. \param id_generator An identifier generator that generates names that do not appear in x and sigma

Definition at line 259 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [3/6]

template<typename T , typename Substitution >

T mcrl2::lps::replace_variables_capture_avoiding	(	const T &	x,
		Substitution &	sigma,
		data::set_identifier_generator &	id_generator,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the substiution is applied. \param sigma A substitution. \param id_generator An identifier generator that generates names that do not appear in x and sigma

Definition at line 203 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [4/6]

template<typename T , typename Substitution >

T mcrl2::lps::replace_variables_capture_avoiding	(	const T &	x,
		Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the substiution is applied. \param sigma A substitution.

Definition at line 237 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [5/6]

template<typename T , typename Substitution >

void mcrl2::lps::replace_variables_capture_avoiding	(	T &	x,
		Substitution &	sigma,
		data::set_identifier_generator &	id_generator,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the subsitution is applied. \param sigma A substitution. \param id_generator An identifier generator that generates names that do not appear in x and sigma

Definition at line 188 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [6/6]

template<typename T , typename Substitution >

void mcrl2::lps::replace_variables_capture_avoiding	(	T &	x,
		Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the subsitution is applied. \param sigma A substitution.

Definition at line 219 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [1/2]

template<typename T , typename Substitution , typename IdentifierGenerator >

T mcrl2::lps::replace_variables_capture_avoiding_with_an_identifier_generator	(	const T &	x,
		Substitution &	sigma,
		IdentifierGenerator &	id_generator,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Applies sigma as a capture avoiding substitution to x using an identifier generator.. \details This substitution function is much faster than replace_variables_capture_avoiding, but it requires an identifier generator that generates strings for fresh variables. These strings must be unique in the sense that they have not been used for other variables. \param x The object to which the substiution is applied. \param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its right hand side. The class maintain_variables_in_rhs is useful for this purpose. \param id_generator A generator that generates unique strings, not yet used as variable names. \return The result is the term x to which sigma has been applied.

Definition at line 158 of file replace_capture_avoiding_with_an_identifier_generator.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [2/2]

template<typename T , typename Substitution , typename IdentifierGenerator >

void mcrl2::lps::replace_variables_capture_avoiding_with_an_identifier_generator	(	T &	x,
		Substitution &	sigma,
		IdentifierGenerator &	id_generator,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Applies sigma as a capture avoiding substitution to x using an identifier generator. \details This substitution function is much faster than replace_variables_capture_avoiding, but it requires an identifier generator that generates strings for fresh variables. These strings must be unique in the sense that they have not been used for other variables. \param x The object to which the subsitution is applied. \param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its right hand side. The class maintain_variables_in_rhs is useful for this purpose. \param id_generator A generator that generates unique strings, not yet used as variable names.

Definition at line 139 of file replace_capture_avoiding_with_an_identifier_generator.h.

resolve_summand_variable_name_clashes()

template<typename Specification >

void mcrl2::lps::resolve_summand_variable_name_clashes

(

Specification &

spec

)

Renames summand variables such that there are no name clashes between summand variables and process parameters.

Definition at line 136 of file resolve_name_clashes.h.

rewrite() [1/4]

template<typename T , typename Rewriter , typename Substitution >

T mcrl2::lps::rewrite	(	const T &	x,
		Rewriter	R,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly \param x an object containing expressions \param R a rewriter \param sigma a substitution \return the rewrite result

Definition at line 70 of file rewrite.h.

rewrite() [2/4]

template<typename T , typename Rewriter >

T mcrl2::lps::rewrite	(	const T &	x,
		Rewriter	R,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Rewrites all embedded expressions in an object x \param x an object containing expressions \param R a rewriter \return the rewrite result

Definition at line 40 of file rewrite.h.

rewrite() [3/4]

template<typename T , typename Rewriter , typename Substitution >

void mcrl2::lps::rewrite	(	T &	x,
		Rewriter	R,
		const Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly \param x an object containing expressions \param R a rewriter \param sigma a substitution

Definition at line 55 of file rewrite.h.

rewrite() [4/4]

template<typename T , typename Rewriter >

void mcrl2::lps::rewrite	(	T &	x,
		Rewriter	R,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Rewrites all embedded expressions in an object x \param x an object containing expressions \param R a rewriter

Definition at line 27 of file rewrite.h.

save_lps() [1/2]

template<typename Specification >

void mcrl2::lps::save_lps	(	const Specification &	spec,
		const std::string &	filename
	)

Saves an LPS to a file.

Parameters

spec	The LPS to save.
filename	The file to save the LPS in. If empty, the file is written to stdout.

Definition at line 74 of file io.h.

save_lps() [2/2]

template<typename Specification >

void mcrl2::lps::save_lps	(	const Specification &	spec,
		std::ostream &	stream,
		const std::string &	target = ""
	)

Save an LPS in the format specified.

Parameters

spec	The LPS to be stored
stream	The stream to which the output is written.
target	A string indicating the target stream, used to print information. utilities::file_format::unknown() is specified, then a default format is chosen.

Definition at line 42 of file io.h.

search_free_variable()

template<typename T >

bool mcrl2::lps::search_free_variable	(	const T &	x,
		const data::variable &	v
	)

Returns true if the term has a given free variable as subterm.

Parameters

[in]	x	an expression
[in]	v	a variable

Returns

True if v occurs free in x.

Definition at line 160 of file find.h.

specification_to_aterm()

template<typename LinearProcess , typename InitialProcessExpression >

atermpp::aterm mcrl2::lps::specification_to_aterm

(

const specification_base< LinearProcess, InitialProcessExpression > &

spec

)

Conversion to aterm.

Returns

The specification converted to aterm format.

Definition at line 228 of file specification.h.

sumelm() [1/3]

bool mcrl2::lps::sumelm ( action_summand &  s )

inline

Apply the sum elimination lemma to summand s.

Parameters

s	an action summand

Returns

true if any summation variables have been removed, or false otherwise.

Definition at line 114 of file sumelm.h.

sumelm() [2/3]

bool mcrl2::lps::sumelm ( deadlock_summand &  s )

inline

Apply the sum elimination lemma to summand s.

Parameters

s	a deadlock summand

Returns

true if any summation variables have been removed, or false otherwise.

Definition at line 138 of file sumelm.h.

sumelm() [3/3]

bool mcrl2::lps::sumelm ( stochastic_action_summand &  s )

inline

Apply the sum elimination lemma to summand s.

Parameters

s	a stochastic action summand

Returns

true if any summation variables have been removed, or false otherwise.

Definition at line 126 of file sumelm.h.

summand_distribution() [1/3]

template<>

const stochastic_distribution & mcrl2::lps::summand_distribution

(

const lps::stochastic_action_summand &

summand

)

Definition at line 79 of file confluence.h.

summand_distribution() [2/3]

template<>

const stochastic_distribution & mcrl2::lps::summand_distribution ( const lps::stochastic_action_summand &  summand )

inline

Definition at line 251 of file explorer.h.

summand_distribution() [3/3]

template<typename Summand >

const stochastic_distribution & mcrl2::lps::summand_distribution ( const Summand &  )

inline

Definition at line 71 of file confluence.h.

swap() [1/8]

void mcrl2::lps::swap ( action_summand &  t1, action_summand &  t2  )

inline

\brief swap overload

Definition at line 135 of file action_summand.h.

swap() [2/8]

void mcrl2::lps::swap ( deadlock &  t1, deadlock &  t2  )

inline

\brief swap overload

Definition at line 108 of file deadlock.h.

swap() [3/8]

void mcrl2::lps::swap ( deadlock_summand &  t1, deadlock_summand &  t2  )

inline

\brief swap overload

Definition at line 100 of file deadlock_summand.h.

swap() [4/8]

void mcrl2::lps::swap ( multi_action &  t1, multi_action &  t2  )

inline

\brief swap overload

Definition at line 137 of file multi_action.h.

swap() [5/8]

void mcrl2::lps::swap ( process_initializer &  t1, process_initializer &  t2  )

inline

\brief swap overload

Definition at line 105 of file process_initializer.h.

swap() [6/8]

void mcrl2::lps::swap ( stochastic_action_summand &  t1, stochastic_action_summand &  t2  )

inline

\brief swap overload

Definition at line 92 of file stochastic_action_summand.h.

swap() [7/8]

void mcrl2::lps::swap ( stochastic_distribution &  t1, stochastic_distribution &  t2  )

inline

\brief swap overload

Definition at line 106 of file stochastic_distribution.h.

swap() [8/8]

void mcrl2::lps::swap ( stochastic_process_initializer &  t1, stochastic_process_initializer &  t2  )

inline

\brief swap overload

Definition at line 88 of file stochastic_process_initializer.h.

translate_user_notation() [1/3]

lps::multi_action mcrl2::lps::translate_user_notation

(

const lps::multi_action &

x

)

Definition at line 41 of file lps.cpp.

translate_user_notation() [2/3]

template<typename T >

T mcrl2::lps::translate_user_notation	(	const T &	x,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= 0
	)

Definition at line 33 of file translate_user_notation.h.

translate_user_notation() [3/3]

template<typename T >

void mcrl2::lps::translate_user_notation	(	T &	x,
		typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Definition at line 25 of file translate_user_notation.h.

txt2lps()

void mcrl2::lps::txt2lps	(	const std::string &	input_filename,
		const std::string &	output_filename
	)

Definition at line 310 of file tools.cpp.

typecheck_action_rename_specification()

action_rename_specification mcrl2::lps::typecheck_action_rename_specification ( const action_rename_specification &  arspec, const lps::stochastic_specification &  lpsspec  )

inline

Type checks an action rename specification.

Parameters

arspec	An action rename specifition.
lpsspec	A linear process specification, used for the datatypes and action declarations.

Returns

A type checked rename specification.

Definition at line 157 of file typecheck.h.

typecheck_multi_action() [1/2]

multi_action mcrl2::lps::typecheck_multi_action ( process::untyped_multi_action &  mult_act, const data::data_specification &  data_spec, const process::action_label_list &  action_decls  )

inline

Type check a multi action Throws an exception if something went wrong.

Parameters

[in]	mult_act	A multi action that has not been type checked.
[in]	data_spec	A data specification to use as context.
[in]	action_decls	A list of action declarations to use as context.

Postcondition

mult_action is type checked and sorts have been added when necessary.

Definition at line 128 of file typecheck.h.

typecheck_multi_action() [2/2]

multi_action mcrl2::lps::typecheck_multi_action ( process::untyped_multi_action &  mult_act, multi_action_type_checker &  typechecker  )

inline

Type check a multi action Throws an exception if something went wrong.

Parameters

[in]	mult_act	A multi action that has not been type checked.
[in]	typechecker	Checker that will be used to check multi_act

Postcondition

mult_action is type checked and sorts have been added when necessary.

Definition at line 144 of file typecheck.h.

used_read_variables()

std::set< data::variable > mcrl2::lps::used_read_variables ( const action_summand &  summand )

inline

Definition at line 85 of file confluence.h.

write_spec()

static void mcrl2::lps::write_spec ( atermpp::aterm_ostream &  stream, const stochastic_specification &  spec  )

static

Definition at line 122 of file lps_io.cpp.