mcrl2::lps Namespace Reference

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

Namespaces
namespace	anonymous_namespace{lps_summand_group.h}
namespace	detail
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
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
	Action rename specification. 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	cf_edge
struct	cf_graph
struct	cf_vertex
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	counting_iterator
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	dataspec_prune_rewriter
	A rewriter that removes unused data specifications. 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	lps_parvalues_algorithm
struct	lps_statistics_t
	Data structure to store the statistics about summands in a linear process. More...
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...
struct	projection_cache_equality
struct	projection_cache_hash
struct	projection_cache_key
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	update_active_cfg_vertices_timer
struct	update_active_cfg_vertices_timer_reporter
struct	variable_builder
	\brief Builder class More...
struct	variable_traverser
	\brief Traverser class More...

Typedefs
using	action_summand_list = atermpp::term_list< action_summand >
	\brief list of action_summands
using	action_summand_vector = std::vector< action_summand >
	\brief vector of action_summands
using	deadlock_list = atermpp::term_list< deadlock >
	\brief list of deadlocks
using	deadlock_vector = std::vector< deadlock >
	\brief vector of deadlocks
using	deadlock_summand_list = atermpp::term_list< deadlock_summand >
	\brief list of deadlock_summands
using	deadlock_summand_vector = std::vector< deadlock_summand >
	\brief vector of deadlock_summands
using	edge_label_map = std::unordered_map< const cf_edge *, std::set< std::size_t > >
using	projected_transition = std::pair< multi_action, state >
using	summand_cache_map = 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 >
using	projection_cache_map = atermpp::utilities::unordered_map< lps::state, std::vector< projected_transition >, projection_cache_hash, projection_cache_equality, std::allocator< std::pair< lps::state, std::vector< projected_transition > > >, true >
using	multi_action_list = atermpp::term_list< multi_action >
	\brief list of multi_actions
using	multi_action_vector = std::vector< multi_action >
	\brief vector of multi_actions
using	process_initializer_list = atermpp::term_list< process_initializer >
	\brief list of process_initializers
using	process_initializer_vector = std::vector< process_initializer >
	\brief vector of process_initializers
using	state = atermpp::term_balanced_tree< data::data_expression >
using	stochastic_action_summand_list = atermpp::term_list< stochastic_action_summand >
	\brief list of stochastic_action_summands
using	stochastic_action_summand_vector = std::vector< stochastic_action_summand >
	\brief vector of stochastic_action_summands
using	stochastic_distribution_list = atermpp::term_list< stochastic_distribution >
	\brief list of stochastic_distributions
using	stochastic_distribution_vector = std::vector< stochastic_distribution >
	\brief vector of stochastic_distributions
using	stochastic_process_initializer_list = atermpp::term_list< stochastic_process_initializer >
	\brief list of stochastic_process_initializers
using	stochastic_process_initializer_vector = std::vector< stochastic_process_initializer >
	\brief vector of stochastic_process_initializers

Enumerations
enum class	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 class	t_lin_method { lmStack , lmRegular , lmRegular2 }
	The available linearisation methods. More...
enum class	lps_rewriter_type { simplify , quantifier_one_point , condition_one_point , prune_dataspec }
	An enumerated type for the available lps rewriters. More...

Functions
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.
mcrl2::lps::stochastic_specification	linearise (const mcrl2::process::process_specification &type_checked_spec, const mcrl2::lps::t_lin_options &lin_options=t_lin_options())
	Linearises a process specification.
mcrl2::lps::stochastic_specification	linearise (const std::string &text, const mcrl2::lps::t_lin_options &lin_options=t_lin_options())
	Linearises a process specification from a textual specification.
std::string	log_allow_block_application (const lps_statistics_t &lps_statistics_before, const lps_statistics_t &lps_statistics_after, const bool is_allow, const std::size_t num_allowed_multiactions, const std::size_t num_blocked_actions, const bool apply_delta_elimination, const bool ignore_time, size_t indent=0)
bool	allow_ (const detail::allow_list_cache &allow_cache, const process::action_list &multi_action, const process::action &termination_action)
	Determine if multi_action is allowed by an allow expression in allow_list.
template<typename Container >
bool	encap (const Container &blocked_actions, const process::action_list &multiaction)
	Calculate if any of the actions in multiaction is blocked by encap_list.
bool	encap (const process::action_name_multiset_list &encaplist, const process::action_list &multiaction)
	Calculate if any of the actions in multiaction is blocked by encap_list.
void	allowblockcomposition (const process::action_name_multiset_list &allowlist1, const bool is_allow, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process::action &termination_action, bool ignore_time, bool nodeltaelimination)
void	communicationcomposition (const process::communication_expression_list &communications, const process::action_name_multiset_list &allowlist, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process::action &terminationAction, const bool nosumelm, const bool nodeltaelimination, const bool ignore_time, const std::function< data::data_expression(const data::data_expression &)> &RewriteTerm)
std::string	log_hide_application (const lps_statistics_t &lps_statistics_before, const lps_statistics_t &lps_statistics_after, const std::size_t num_hidden_actions, size_t indent=0)
process::action_list	hide_ (const core::identifier_string_list &hidelist, const process::action_list &multiaction)
multi_action	hide_ (const core::identifier_string_list &hidelist, const multi_action &label)
stochastic_action_summand	hide_ (const core::identifier_string_list &hidelist, const stochastic_action_summand &summand)
void	hidecomposition (const core::identifier_string_list &hidelist, stochastic_action_summand_vector &action_summands)
std::string	log_rename_application (const lps_statistics_t &lps_statistics_before, const lps_statistics_t &lps_statistics_after, const std::size_t num_rename_expressions, size_t indent=0)
process::action	rename (const process::rename_expression_list &renamings, const process::action &action)
	Apply renamings to a single action.
process::action_list	rename (const process::rename_expression_list &renamings, const process::action_list &actions)
multi_action	rename (const process::rename_expression_list &renamings, const multi_action &multi_action)
stochastic_action_summand	rename (const process::rename_expression_list &renamings, const stochastic_action_summand &summand)
void	rename (const process::rename_expression_list &renamings, lps::stochastic_action_summand_vector &action_summands)
std::string	print (const lps_statistics_t &stats, std::size_t indent=0)
	Print statistics of lps as indented block in YAML format.
lps_statistics_t	get_statistics (const stochastic_action_summand_vector &action_summands)
lps_statistics_t	get_statistics (const stochastic_action_summand_vector &action_summands, const deadlock_summand_vector &deadlock_summands)
	Get statistics for action and deadlock summands.
process::action_list	sort_actions (const process::action_list &actions)
bool	implies_condition (const data::data_expression &c1, const data::data_expression &c2)
bool	subsumes (const stochastic_action_summand &as, const deadlock_summand &ds)
bool	subsumes (const deadlock_summand &ds1, const deadlock_summand &ds2)
	Determine if delta summand ds1 subsumes delta summand ds2.
void	insert_timed_delta_summand (const stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const deadlock_summand &s, const bool ignore_time)
bool	occursinterm (const data::data_expression &t, const data::variable &var)
template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables_capture_avoiding_with_an_identifier_generator (T &x, Substitution &sigma, IdentifierGenerator &id_generator)
template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator > requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables_capture_avoiding_with_an_identifier_generator (const T &x, Substitution &sigma, IdentifierGenerator &id_generator)
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::string	pp (const lps::action_summand &x, bool arg0)
std::string	pp (const lps::deadlock &x, bool arg0)
std::string	pp (const lps::deadlock_summand &x, bool arg0)
std::string	pp (const lps::linear_process &x, bool arg0)
std::string	pp (const lps::multi_action &x, bool arg0)
std::string	pp (const lps::process_initializer &x, bool arg0)
std::string	pp (const lps::specification &x, bool arg0)
std::string	pp (const lps::stochastic_action_summand &x, bool arg0)
std::string	pp (const lps::stochastic_distribution &x, bool arg0)
std::string	pp (const lps::stochastic_linear_process &x, bool arg0)
std::string	pp (const lps::stochastic_process_initializer &x, bool arg0)
std::string	pp (const lps::stochastic_specification &x, bool arg0)
lps::multi_action	normalize_sorts (const lps::multi_action &x, const data::sort_specification &sortspec)
void	normalize_sorts (lps::specification &x, const data::sort_specification &)
void	normalize_sorts (lps::stochastic_specification &x, const data::sort_specification &)
lps::multi_action	translate_user_notation (const lps::multi_action &x)
std::set< data::sort_expression >	find_sort_expressions (const lps::specification &x)
std::set< data::sort_expression >	find_sort_expressions (const lps::stochastic_specification &x)
std::set< data::variable >	find_all_variables (const lps::linear_process &x)
std::set< data::variable >	find_all_variables (const lps::stochastic_linear_process &x)
std::set< data::variable >	find_all_variables (const lps::specification &x)
std::set< data::variable >	find_all_variables (const lps::stochastic_specification &x)
std::set< data::variable >	find_all_variables (const lps::deadlock &x)
std::set< data::variable >	find_all_variables (const multi_action &x)
	Returns all variables inside a multi-action.
std::set< data::variable >	find_free_variables (const lps::linear_process &x)
std::set< data::variable >	find_free_variables (const lps::stochastic_linear_process &x)
std::set< data::variable >	find_free_variables (const lps::specification &x)
std::set< data::variable >	find_free_variables (const lps::stochastic_specification &x)
std::set< data::variable >	find_free_variables (const lps::deadlock &x)
std::set< data::variable >	find_free_variables (const lps::multi_action &x)
std::set< data::variable >	find_free_variables (const lps::process_initializer &x)
std::set< data::variable >	find_free_variables (const lps::stochastic_process_initializer &x)
std::set< data::function_symbol >	find_function_symbols (const lps::specification &x)
std::set< data::function_symbol >	find_function_symbols (const lps::stochastic_specification &x)
std::set< core::identifier_string >	find_identifiers (const lps::specification &x)
std::set< core::identifier_string >	find_identifiers (const lps::stochastic_specification &x)
std::set< process::action_label >	find_action_labels (const lps::linear_process &x)
std::set< process::action_label >	find_action_labels (const lps::process_initializer &x)
std::set< process::action_label >	find_action_labels (const lps::specification &x)
std::set< process::action_label >	find_action_labels (const lps::stochastic_specification &x)
std::string	pp_extended (const lps::stochastic_specification &x, const std::string &process_name, bool precedence_aware=true)
std::string	pp_extended (const specification &x, const std::string &process_name, bool precedence_aware, bool summand_numbers)
std::string	pp_extended (const stochastic_specification &x, const std::string &process_name, bool precedence_aware, bool summand_numbers)
bool	check_well_typedness (const linear_process &x)
bool	check_well_typedness (const stochastic_linear_process &x)
bool	check_well_typedness (const specification &x)
bool	check_well_typedness (const stochastic_specification &x)
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	normalize_sorts (T &x, const data::sort_specification &sortspec)
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	normalize_sorts (const T &x, const data::sort_specification &sortspec)
template<typename T >
std::string	pp (const T &x, bool precedence_aware=true)
	Returns a string representation of the object x.
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	translate_user_notation (T &x)
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	translate_user_notation (const T &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)
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, lps::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.
void	complete_data_specification (stochastic_specification &spec)
	Adds all sorts that appear in the process of l to the data specification of l.
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.
specification	remove_stochastic_operators (const stochastic_specification &spec)
	Converts a stochastic specification to a specification. Throws an exception if non-empty distributions are encountered.
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	is_specification (const atermpp::aterm &x)
	Test for a specification expression.
std::ostream &	operator<< (std::ostream &out, const specification &x)
bool	operator== (const specification &spec1, const specification &spec2)
	Equality operator.
bool	operator!= (const specification &spec1, const specification &spec2)
	Inequality operator.
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 > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	insert_case_functions (T &x, const lpsparunfold::case_func_replacement &cfv, data::set_identifier_generator &id_generator)
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	insert_case_functions (T &x, const lpsparunfold::case_func_replacement &cfv)
template<typename T , typename Substitution > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_sort_expressions (T &x, const Substitution &sigma, bool innermost)
template<typename T , typename Substitution > requires std::is_base_of_v<atermpp::aterm, T>
T	replace_sort_expressions (const T &x, const Substitution &sigma, bool innermost)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_data_expressions (T &x, const Substitution &sigma, bool innermost)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_data_expressions (const T &x, const Substitution &sigma, bool innermost)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables (T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables (const T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_all_variables (T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_all_variables (const T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_free_variables (T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_free_variables (const T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution, typename VariableContainer > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_free_variables (T &x, const Substitution &sigma, const VariableContainer &bound_variables)
template<typename T , data::IsSubstitution Substitution, typename VariableContainer > requires std::is_base_of_v<atermpp::aterm, T>
T	replace_free_variables (const T &x, const Substitution &sigma, const VariableContainer &bound_variables)
template<data::IsSubstitution Substitution>
void	replace_process_parameters (specification &spec, Substitution sigma)
	Applies a substitution to the process parameters of the specification spec.
void	replace_summand_variables (specification &spec, data::mutable_map_substitution<> &sigma)
	Applies a substitution to the process parameters of the specification spec.
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)
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::ostream &	operator<< (std::ostream &out, const action_summand &x)
void	swap (action_summand &t1, action_summand &t2) noexcept
	\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)
std::ostream &	operator<< (std::ostream &out, const deadlock &x)
void	swap (deadlock &t1, deadlock &t2) noexcept
	\brief swap overload
std::ostream &	operator<< (std::ostream &out, const deadlock_summand &x)
void	swap (deadlock_summand &t1, deadlock_summand &t2) noexcept
	\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)
bool	cfg_mentions_summand (const cf_graph &G, std::size_t s)
void	initialize_control_flow_bitsets (cf_graph &G, const edge_label_map &edge_labels, std::size_t number_of_summands)
void	print_edge_label_map (const edge_label_map &m)
std::vector< cf_graph >	extract_local_control_flow_graphs (const pbes_system::detail::lpsstategraph_algorithm &algorithm)
std::vector< cf_graph >	compute_control_flow_graphs (lps::specification &lpsspec, const pbes_system::pbesstategraph_options &stategraph_options, bool compute_marking=false)
template<typename Bitset >
void	print_bitset (std::ostream &os, const Bitset &bs)
void	print_graph (const cf_graph &G)
bool	cfg_allows_summand (std::size_t summand, const data::mutable_indexed_substitution<> &sigma, const std::vector< data::variable > &process_parameters, const std::vector< cf_graph > &cfgs)
template<typename Container >
void	update_active_cfg_vertices (const data::mutable_indexed_substitution<> &sigma, const std::vector< data::variable > &process_parameters, const std::vector< cf_graph > &cfgs, Container &active_cfg_vertices)
template<typename Container = boost::container::small_vector<std::size_t, 64>>
Container	compute_active_cfg_vertices (const data::mutable_indexed_substitution<> &sigma, const std::vector< data::variable > &process_parameters, const std::vector< cf_graph > &cfgs)
template<typename Container >
bool	cfg_allows_summand (std::size_t summand, const std::vector< cf_graph > &cfgs, const Container &active_cfg_vertices)
template<typename State >
void	report_cfg_error (std::size_t summand, const State &state, const std::vector< cf_graph > &cfgs)
std::ostream &	operator<< (std::ostream &out, const explorer_options &options)
template<typename Specification >
std::map< data::variable, std::size_t >	compute_process_parameter_index (const Specification &lpsspec)
	Assigns a unique index to every parameter of the process.
template<typename Specification >
std::pair< std::vector< std::vector< std::size_t > >, std::vector< std::vector< std::size_t > > >	compute_read_write_patterns_separated (const Specification &lpsspec)
std::set< data::function_symbol >	add_real_operators (std::set< data::function_symbol > s)
template<typename Specification >
data::rewriter	construct_rewriter (const Specification &lpsspec, data::rewrite_strategy rewrite_strategy, bool remove_unused_rewrite_rules)
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)
template<typename T , typename OutputIterator >
void	find_all_variables (const T &x, OutputIterator o)
	Writes all variables that occur in an object to an output iterator.
template<typename T >
std::set< data::variable >	find_all_variables (const T &x)
	Returns all variables that occur in an object.
template<typename T , typename OutputIterator >
void	find_free_variables (const T &x, OutputIterator o)
	Writes all free variables that occur in an object to an output iterator.
template<typename T , typename OutputIterator , typename VariableContainer >
void	find_free_variables_with_bound (const T &x, OutputIterator o, const VariableContainer &bound)
	Writes all free variables that occur in an object to an output iterator.
template<typename T >
std::set< data::variable >	find_free_variables (const T &x)
	Returns all free variables that occur in an object.
template<typename T , typename VariableContainer >
std::set< data::variable >	find_free_variables_with_bound (const T &x, VariableContainer const &bound)
	Returns all free variables that occur in an object.
template<typename T , typename OutputIterator >
void	find_identifiers (const T &x, OutputIterator o)
	Writes all identifiers that occur in an object to an output iterator.
template<typename T >
std::set< core::identifier_string >	find_identifiers (const T &x)
	Returns all identifiers that occur in an object.
template<typename T , typename OutputIterator >
void	find_sort_expressions (const T &x, OutputIterator o)
	Writes all sort expressions that occur in an object to an output iterator.
template<typename T >
std::set< data::sort_expression >	find_sort_expressions (const T &x)
	Returns all sort expressions that occur in an object.
template<typename T , typename OutputIterator >
void	find_function_symbols (const T &x, OutputIterator o)
	Writes all function symbols that occur in an object to an output iterator.
template<typename T >
std::set< data::function_symbol >	find_function_symbols (const T &x)
	Returns all function symbols that occur in an object.
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<class OutputIterator >
void	find_all_variables (const multi_action &x, OutputIterator o)
	Returns all variables inside a multi-action.
template<typename Node , typename GenerateSuccessors >
Node	find_representative (Node &u0, GenerateSuccessors generate_successors)
	Search for a unique representative in a graph.
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	if_rewrite (T &x)
	Applies the if rewriter to all embedded data expressions in an object x.
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	if_rewrite (const T &x)
	Applies the if rewriter to all embedded data expressions in an object x.
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.
template<typename ActionSummand >
atermpp::aterm	linear_process_to_aterm (const linear_process_base< ActionSummand > &p)
	Conversion to aterm.
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::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)
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)
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)
std::ostream &	operator<< (std::ostream &out, const multi_action &x)
void	swap (multi_action &t1, multi_action &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_multi_action (atermpp::aterm &t, const ARGUMENTS &... args)
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 > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	one_point_rule_rewrite (T &x)
	Applies the one point rule rewriter to all embedded data expressions in an object x.
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	one_point_rule_rewrite (const T &x)
	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 action 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.
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::ostream &	operator<< (std::ostream &out, const process_initializer &x)
void	swap (process_initializer &t1, process_initializer &t2) noexcept
	\brief swap overload
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 , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables_capture_avoiding (T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables_capture_avoiding (T &x, Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma)
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 > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_constants_by_variables (T &x, const data::rewriter &r, data::mutable_indexed_substitution<> &sigma)
	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 > requires (std::is_base_of_v<atermpp::aterm, T>)
T	replace_constants_by_variables (const T &x, const data::rewriter &r, data::mutable_indexed_substitution<> &sigma)
	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 > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	rewrite (T &x, Rewriter R)
template<typename T , typename Rewriter > requires std::is_base_of_v<atermpp::aterm, T>
T	rewrite (const T &x, Rewriter R)
template<typename T , typename Rewriter , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	rewrite (T &x, Rewriter R, const Substitution &sigma)
template<typename T , typename Rewriter , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	rewrite (const T &x, Rewriter R, const Substitution &sigma)
template<typename T , typename DataRewriter > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	one_point_condition_rewrite (T &x, const DataRewriter &R)
	Applies the one point condition rewriter to all embedded data expressions in an object x.
template<typename T , typename DataRewriter > requires (std::is_base_of_v<atermpp::aterm, T>)
T	one_point_condition_rewrite (const T &x, const DataRewriter &R)
	Applies the one point condition rewriter to all embedded data expressions in an object x.
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::ostream &	operator<< (std::ostream &out, const stochastic_action_summand &x)
void	swap (stochastic_action_summand &t1, stochastic_action_summand &t2) noexcept
	\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::ostream &	operator<< (std::ostream &out, const stochastic_distribution &x)
void	swap (stochastic_distribution &t1, stochastic_distribution &t2) noexcept
	\brief swap overload
std::ostream &	operator<< (std::ostream &out, const 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::ostream &	operator<< (std::ostream &out, const stochastic_process_initializer &x)
void	swap (stochastic_process_initializer &t1, stochastic_process_initializer &t2) noexcept
	\brief swap overload
std::set< data::sort_expression >	finite_sorts (const data::data_specification &s)
	Return a set with all finite sorts in data specification s.
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.

Variables
update_active_cfg_vertices_timer_reporter	update_active_cfg_vertices_timer_reporter_instance

Detailed Description

The main namespace for the LPS library.

Typedef Documentation

action_summand_list

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

\brief list of action_summands

Definition at line 113 of file action_summand.h.

action_summand_vector

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

\brief vector of action_summands

Definition at line 116 of file action_summand.h.

deadlock_list

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

\brief list of deadlocks

Definition at line 86 of file deadlock.h.

deadlock_summand_list

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

\brief list of deadlock_summands

Definition at line 78 of file deadlock_summand.h.

deadlock_summand_vector

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

\brief vector of deadlock_summands

Definition at line 81 of file deadlock_summand.h.

deadlock_vector

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

\brief vector of deadlocks

Definition at line 89 of file deadlock.h.

edge_label_map

using mcrl2::lps::edge_label_map = typedef std::unordered_map<const cf_edge*, std::set<std::size_t> >

Definition at line 54 of file explorer_control_flow.h.

multi_action_list

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

\brief list of multi_actions

Definition at line 89 of file multi_action.h.

multi_action_vector

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

\brief vector of multi_actions

Definition at line 92 of file multi_action.h.

process_initializer_list

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

\brief list of process_initializers

Definition at line 74 of file process_initializer.h.

process_initializer_vector

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

\brief vector of process_initializers

Definition at line 77 of file process_initializer.h.

projected_transition

using mcrl2::lps::projected_transition = typedef std::pair<multi_action, state>

Definition at line 100 of file explorer_projections.h.

projection_cache_map

using mcrl2::lps::projection_cache_map = typedef atermpp::utilities::unordered_map<lps::state, std::vector<projected_transition>, projection_cache_hash, projection_cache_equality, std::allocator<std::pair<lps::state, std::vector<projected_transition> >>, true>

Definition at line 172 of file explorer_utilities.h.

state

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

Definition at line 21 of file state.h.

stochastic_action_summand_list

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

\brief list of stochastic_action_summands

Definition at line 70 of file stochastic_action_summand.h.

stochastic_action_summand_vector

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

\brief vector of stochastic_action_summands

Definition at line 73 of file stochastic_action_summand.h.

stochastic_distribution_list

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

\brief list of stochastic_distributions

Definition at line 76 of file stochastic_distribution.h.

stochastic_distribution_vector

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

\brief vector of stochastic_distributions

Definition at line 79 of file stochastic_distribution.h.

stochastic_process_initializer_list

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

\brief list of stochastic_process_initializers

Definition at line 58 of file stochastic_process_initializer.h.

stochastic_process_initializer_vector

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

\brief vector of stochastic_process_initializers

Definition at line 61 of file stochastic_process_initializer.h.

summand_cache_map

using mcrl2::lps::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>

Definition at line 165 of file explorer_utilities.h.

Enumeration Type Documentation

caching

enum class mcrl2::lps::caching

strong

Enumerator
none
local
global

Definition at line 49 of file explorer_utilities.h.

exploration_strategy

enum class mcrl2::lps::exploration_strategy

strong

Enumerator
es_none
es_breadth
es_depth
es_random
es_value_prioritized
es_value_random_prioritized
es_highway

Definition at line 19 of file exploration_strategy.h.

lps_rewriter_type

enum class mcrl2::lps::lps_rewriter_type

strong

An enumerated type for the available lps rewriters.

Enumerator
simplify
quantifier_one_point
condition_one_point
prune_dataspec

Definition at line 22 of file lps_rewriter_type.h.

t_lin_method

enum class mcrl2::lps::t_lin_method

strong

The available linearisation methods.

Enumerator
lmStack
lmRegular
lmRegular2

Definition at line 21 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 414 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 781 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 244 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 250 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 169 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 115 of file stochastic_action_summand.h.

add_real_operators()

std::set< data::function_symbol > mcrl2::lps::add_real_operators ( std::set< data::function_symbol >  s )

inline

Definition at line 26 of file explorer_utilities.h.

allow_()

bool mcrl2::lps::allow_ ( const detail::allow_list_cache &  allow_cache, const process::action_list &  multi_action, const process::action &  termination_action  )

inline

Determine if multi_action is allowed by an allow expression in allow_list.

Calculates if the names of the action in multi_action match with an expression in allow_list. If multi_action is the termination action, or multi_action is the empty multiaction, the result is also true.

Definition at line 105 of file linearise_allow_block.h.

allowblockcomposition()

void mcrl2::lps::allowblockcomposition ( const process::action_name_multiset_list &  allowlist1, const bool  is_allow, stochastic_action_summand_vector &  action_summands, deadlock_summand_vector &  deadlock_summands, const process::action &  termination_action, bool  ignore_time, bool  nodeltaelimination  )

inline

Calculate the application of the allow or block operator over the action summands.

Parameters

allowlist1	the allowset. If is_allow is false, the list has length 1, and its only element contains the blocked actions.
is_allow	determines if we calculate the allow or the block operator
action_summands	the summands over which to compute the operator
deadlock_summands	the deadlock summands tha may be extended.
termination_action	the termination action generated by the linearizer. This action is always allowed.
ignore_time	if true, and nodeltaelimination is false, a true->delta summand is added that subsumes all other deadlock summands
nodeltaaelimination	do not eliminate deadlock summands.

Cache the list of allowed actions, to avoid linear searches in the allow list.

Definition at line 185 of file linearise_allow_block.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 759 of file lpsparunfoldlib.h.

cfg_allows_summand() [1/2]

bool mcrl2::lps::cfg_allows_summand ( std::size_t  summand, const data::mutable_indexed_substitution<> &  sigma, const std::vector< data::variable > &  process_parameters, const std::vector< cf_graph > &  cfgs  )

inline

Definition at line 332 of file explorer_control_flow.h.

cfg_allows_summand() [2/2]

template<typename Container >

bool mcrl2::lps::cfg_allows_summand	(	std::size_t	summand,
		const std::vector< cf_graph > &	cfgs,
		const Container &	active_cfg_vertices
	)

Definition at line 420 of file explorer_control_flow.h.

cfg_mentions_summand()

bool mcrl2::lps::cfg_mentions_summand ( const cf_graph &  G, std::size_t  s  )

inline

Definition at line 57 of file explorer_control_flow.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 66 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 88 of file stochastic_state.h.

check_well_typedness() [1/5]

bool mcrl2::lps::check_well_typedness

(

const linear_process &

x

)

Definition at line 108 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 118 of file lps.cpp.

check_well_typedness() [4/5]

bool mcrl2::lps::check_well_typedness

(

const stochastic_linear_process &

x

)

Definition at line 113 of file lps.cpp.

check_well_typedness() [5/5]

bool mcrl2::lps::check_well_typedness

(

const stochastic_specification &

x

)

Definition at line 123 of file lps.cpp.

communicationcomposition()

void mcrl2::lps::communicationcomposition ( const process::communication_expression_list &  communications, const process::action_name_multiset_list &  allowlist, const bool  is_allow, const bool  is_block, stochastic_action_summand_vector &  action_summands, deadlock_summand_vector &  deadlock_summands, const process::action &  terminationAction, const bool  nosumelm, const bool  nodeltaelimination, const bool  ignore_time, const std::function< data::data_expression(const data::data_expression &)> &  RewriteTerm  )

inline

Definition at line 906 of file linearise_communication.h.

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 252 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 101 of file stochastic_specification.h.

compute_active_cfg_vertices()

template<typename Container = boost::container::small_vector<std::size_t, 64>>

Container mcrl2::lps::compute_active_cfg_vertices	(	const data::mutable_indexed_substitution<> &	sigma,
		const std::vector< data::variable > &	process_parameters,
		const std::vector< cf_graph > &	cfgs
	)

Definition at line 410 of file explorer_control_flow.h.

compute_control_flow_graphs()

std::vector< cf_graph > mcrl2::lps::compute_control_flow_graphs ( lps::specification &  lpsspec, const pbes_system::pbesstategraph_options &  stategraph_options, bool  compute_marking = false  )

inline

Definition at line 236 of file explorer_control_flow.h.

compute_process_parameter_index()

template<typename Specification >

std::map< data::variable, std::size_t > mcrl2::lps::compute_process_parameter_index

(

const Specification &

lpsspec

)

Assigns a unique index to every parameter of the process.

Definition at line 24 of file explorer_projections.h.

compute_read_write_patterns_separated()

template<typename Specification >

std::pair< std::vector< std::vector< std::size_t > >, std::vector< std::vector< std::size_t > > > mcrl2::lps::compute_read_write_patterns_separated

(

const Specification &

lpsspec

)

Definition at line 37 of file explorer_projections.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 269 of file constelm.h.

construct_rewriter()

template<typename Specification >

data::rewriter mcrl2::lps::construct_rewriter	(	const Specification &	lpsspec,
		data::rewrite_strategy	rewrite_strategy,
		bool	remove_unused_rewrite_rules
	)

Definition at line 35 of file explorer_utilities.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 106 of file deadlock_summand.h.

description() [1/3]

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

inline

Definition at line 103 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 74 of file lps_rewriter_type.h.

description() [3/3]

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

inline

Definition at line 44 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.

encap() [1/2]

template<typename Container >

bool mcrl2::lps::encap	(	const Container &	blocked_actions,
		const process::action_list &	multiaction
	)

Calculate if any of the actions in multiaction is blocked by encap_list.

Parameters

blocked_actions	is a list of action names that are blocked.
multi_action	contains a multiaction a1(d1)|...|an(dn)

Returns

Definition at line 127 of file linearise_allow_block.h.

encap() [2/2]

bool mcrl2::lps::encap ( const process::action_name_multiset_list &  encaplist, const process::action_list &  multiaction  )

inline

Calculate if any of the actions in multiaction is blocked by encap_list.

Parameters

encap_list	is a list of action_name_multisets of size 1. Its single element contains all the blocked actions.
multi_action	contains a multiaction a1(d1)|...|an(dn)

Returns

Definition at line 165 of file linearise_allow_block.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 290 of file multi_action.h.

extract_local_control_flow_graphs()

std::vector< cf_graph > mcrl2::lps::extract_local_control_flow_graphs ( const pbes_system::detail::lpsstategraph_algorithm &  algorithm )

inline

Definition at line 137 of file explorer_control_flow.h.

find_action_labels() [1/6]

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

(

const lps::linear_process &

x

)

Definition at line 65 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 66 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 67 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 68 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 172 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 163 of file find.h.

find_all_variables() [1/9]

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

(

const lps::deadlock &

x

)

Definition at line 51 of file lps.cpp.

find_all_variables() [2/9]

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

(

const lps::linear_process &

x

)

Definition at line 47 of file lps.cpp.

find_all_variables() [3/9]

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

(

const lps::specification &

x

)

Definition at line 49 of file lps.cpp.

find_all_variables() [4/9]

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

(

const lps::stochastic_linear_process &

x

)

Definition at line 48 of file lps.cpp.

find_all_variables() [5/9]

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

(

const lps::stochastic_specification &

x

)

Definition at line 50 of file lps.cpp.

find_all_variables() [6/9]

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

(

const lps::multi_action &

x

)

Returns all variables inside a multi-action.

Parameters

x	A multi-action from which variables are.

Definition at line 52 of file lps.cpp.

find_all_variables() [7/9]

template<class OutputIterator >

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

Returns all variables inside a multi-action.

Parameters

x	A multi-action from which variables are.
o	The output to which the variables are added.

Definition at line 183 of file find.h.

find_all_variables() [8/9]

template<typename T >

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

(

const T &

x

)

Returns all variables that occur in an object.

Parameters

[in]

x

an object containing variables

Returns

All variables that occur in the object x

Definition at line 36 of file find.h.

find_all_variables() [9/9]

template<typename T , typename OutputIterator >

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

Writes all variables that occur in an object to an output iterator.

Parameters

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

Definition at line 27 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 57 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 53 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 58 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 59 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 55 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 54 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 60 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 56 of file lps.cpp.

find_free_variables() [9/10]

template<typename T >

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

(

const T &

x

)

Returns all free variables that occur in an object.

Parameters

[in]

x

an object containing variables

Returns

All free variables that occur in the object x

Definition at line 66 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
	)

Writes all free variables that occur in an object to an output iterator.

Parameters

[in]	x	an object containing variables
[in,out]	o	an output iterator to which all variables occurring in x are added.

Definition at line 47 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
	)

Writes all free variables that occur in an object to an output iterator.

Parameters

[in]	x	an object containing variables
[in,out]	o	an output iterator to which all variables occurring in x are written.
[in]	bound	a container of variables

Definition at line 57 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
	)

Returns all free variables that occur in an object.

Parameters

[in]	x	an object containing variables
[in]	bound	a container of variables

Returns

All free variables that occur in the object x

Definition at line 78 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 61 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 62 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

)

Returns all function symbols that occur in an object.

Parameters

[in]

x

an object containing function symbols

Returns

All function symbols that occur in the object x

Definition at line 138 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
	)

Writes all function symbols that occur in an object to an output iterator.

Parameters

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

Definition at line 129 of file find.h.

find_identifiers() [1/4]

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

(

const lps::specification &

x

)

Definition at line 63 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 64 of file lps.cpp.

find_identifiers() [3/4]

template<typename T >

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

(

const T &

x

)

Returns all identifiers that occur in an object.

Parameters

[in]

x

an object containing identifiers

Returns

All identifiers that occur in the object x

Definition at line 98 of file find.h.

find_identifiers() [4/4]

template<typename T , typename OutputIterator >

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

Writes all identifiers that occur in an object to an output iterator.

Parameters

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

Definition at line 89 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 31 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 45 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 46 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

)

Returns all sort expressions that occur in an object.

Parameters

[in]

x

an object containing sort expressions

Returns

All sort expressions that occur in the object x

Definition at line 118 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
	)

Writes all sort expressions that occur in an object to an output iterator.

Parameters

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

Definition at line 109 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 26 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 42 of file ltsmin.h.

get_statistics() [1/2]

lps_statistics_t mcrl2::lps::get_statistics ( const stochastic_action_summand_vector &  action_summands )

inline

Utility function to calculate the number of summands and the sizes of multiactions in those summands for printing statistics

Definition at line 55 of file linearise_utility.h.

get_statistics() [2/2]

lps_statistics_t mcrl2::lps::get_statistics ( const stochastic_action_summand_vector &  action_summands, const deadlock_summand_vector &  deadlock_summands  )

inline

Get statistics for action and deadlock summands.

Definition at line 73 of file linearise_utility.h.

has_ctau_action()

template<typename Specification >

bool mcrl2::lps::has_ctau_action

(

const Specification &

lpsspec

)

Definition at line 195 of file confluence.h.

hide_() [1/3]

multi_action mcrl2::lps::hide_ ( const core::identifier_string_list &  hidelist, const multi_action &  label  )

inline

Definition at line 58 of file linearise_hide.h.

hide_() [2/3]

process::action_list mcrl2::lps::hide_ ( const core::identifier_string_list &  hidelist, const process::action_list &  multiaction  )

inline

Definition at line 46 of file linearise_hide.h.

hide_() [3/3]

stochastic_action_summand mcrl2::lps::hide_ ( const core::identifier_string_list &  hidelist, const stochastic_action_summand &  summand  )

inline

Definition at line 64 of file linearise_hide.h.

hidecomposition()

void mcrl2::lps::hidecomposition ( const core::identifier_string_list &  hidelist, stochastic_action_summand_vector &  action_summands  )

inline

Definition at line 75 of file linearise_hide.h.

if_rewrite() [1/2]

template<typename T >
requires (std::is_base_of_v<atermpp::aterm, T>)

T mcrl2::lps::if_rewrite

(

const T &

x

)

Applies the if rewriter to all embedded data expressions in an object x.

Parameters

x	an object containing data expressions

Returns

the rewrite result

Definition at line 55 of file if_rewrite.h.

if_rewrite() [2/2]

template<typename T >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::if_rewrite

(

T &

x

)

Applies the if 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.

implies_condition()

bool mcrl2::lps::implies_condition ( const data::data_expression &  c1, const data::data_expression &  c2  )

inline

Definition at line 89 of file linearise_utility.h.

initial_distribution() [1/2]

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

inline

Definition at line 84 of file explorer_utilities.h.

initial_distribution() [2/2]

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

inline

Definition at line 91 of file explorer_utilities.h.

initialize_control_flow_bitsets()

void mcrl2::lps::initialize_control_flow_bitsets ( cf_graph &  G, const edge_label_map &  edge_labels, std::size_t  number_of_summands  )

inline

Definition at line 70 of file explorer_control_flow.h.

insert_case_functions() [1/2]

template<typename T >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::insert_case_functions	(	T &	x,
		const lpsparunfold::case_func_replacement &	cfv
	)

Definition at line 776 of file lpsparunfoldlib.h.

insert_case_functions() [2/2]

template<typename T >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::insert_case_functions	(	T &	x,
		const lpsparunfold::case_func_replacement &	cfv,
		data::set_identifier_generator &	id_generator
	)

Definition at line 767 of file lpsparunfoldlib.h.

insert_timed_delta_summand()

void mcrl2::lps::insert_timed_delta_summand ( const stochastic_action_summand_vector &  action_summands, deadlock_summand_vector &  deadlock_summands, const deadlock_summand &  s, const bool  ignore_time  )

inline

Definition at line 169 of file linearise_utility.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 261 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 98 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 83 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 41 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 45 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 85 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 67 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 222 of file linear_process.h.

linearise() [1/2]

mcrl2::lps::stochastic_specification mcrl2::lps::linearise	(	const mcrl2::process::process_specification &	type_checked_spec,
		const 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 10051 of file linearise.cpp.

linearise() [2/2]

mcrl2::lps::stochastic_specification mcrl2::lps::linearise ( const std::string &  text, const 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 58 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 92 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 51 of file io.h.

log_allow_block_application()

std::string mcrl2::lps::log_allow_block_application ( const lps_statistics_t &  lps_statistics_before, const lps_statistics_t &  lps_statistics_after, const bool  is_allow, const std::size_t  num_allowed_multiactions, const std::size_t  num_blocked_actions, const bool  apply_delta_elimination, const bool  ignore_time, size_t  indent = 0  )

inline

Definition at line 27 of file linearise_allow_block.h.

log_hide_application()

std::string mcrl2::lps::log_hide_application ( const lps_statistics_t &  lps_statistics_before, const lps_statistics_t &  lps_statistics_after, const std::size_t  num_hidden_actions, size_t  indent = 0  )

inline

Definition at line 25 of file linearise_hide.h.

log_rename_application()

std::string mcrl2::lps::log_rename_application ( const lps_statistics_t &  lps_statistics_before, const lps_statistics_t &  lps_statistics_after, const std::size_t  num_rename_expressions, size_t  indent = 0  )

inline

Definition at line 24 of file linearise_rename.h.

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 65 of file explorer_utilities.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 127 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 66 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 33 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 24 of file state.h.

make_stochastic_distribution()

template<class... ARGUMENTS>

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

inline

\brief The function 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 70 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 50 of file stochastic_process_initializer.h.

normalize_sorts() [1/5]

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

Definition at line 41 of file lps.cpp.

normalize_sorts() [2/5]

template<typename T >
requires (std::is_base_of_v<atermpp::aterm, T>)

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

Definition at line 31 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 42 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 43 of file lps.cpp.

normalize_sorts() [5/5]

template<typename T >
requires (!std::is_base_of_v<atermpp::aterm, T>)

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

Definition at line 23 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 327 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 24 of file binary.h.

occursinterm()

bool mcrl2::lps::occursinterm ( const data::data_expression &  t, const data::variable &  var  )

inline

Definition at line 216 of file linearise_utility.h.

one_point_condition_rewrite() [1/2]

template<typename T , typename DataRewriter >
requires (std::is_base_of_v<atermpp::aterm, T>)

T mcrl2::lps::one_point_condition_rewrite	(	const T &	x,
		const DataRewriter &	R
	)

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 178 of file one_point_condition_rewrite.h.

one_point_condition_rewrite() [2/2]

template<typename T , typename DataRewriter >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::one_point_condition_rewrite	(	T &	x,
		const DataRewriter &	R
	)

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 166 of file one_point_condition_rewrite.h.

one_point_rule_rewrite() [1/2]

template<typename T >
requires (std::is_base_of_v<atermpp::aterm, T>)

T mcrl2::lps::one_point_rule_rewrite

(

const T &

x

)

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 >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::one_point_rule_rewrite

(

T &

x

)

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 45 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 244 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 91 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 140 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 97 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 52 of file explorer_utilities.h.

operator<<() [8/25]

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

inline

Definition at line 97 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 111 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 98 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 126 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 99 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 91 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 276 of file explorer_utilities.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 251 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 111 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 546 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 96 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 205 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 83 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 98 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 86 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 80 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 77 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 159 of file action_summand.h.

operator==() [2/4]

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

inline

Equality operator.

Definition at line 237 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 108 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 84 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,
		lps::stochastic_specification &	spec
	)

Definition at line 191 of file lps_io.cpp.

operator>>() [4/9]

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

Definition at line 30 of file lps_io.cpp.

operator>>() [5/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>>() [6/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>>() [7/9]

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

inline

Definition at line 81 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 95 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 81 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 22 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 220 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 208 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 action 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 107 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 91 of file parse.h.

parse_exploration_strategy()

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

inline

Definition at line 29 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 59 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 149 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 125 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 194 of file parse.h.

parse_lps() [2/2]

template<typename Specification >

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

Definition at line 156 of file parse.h.

parse_lps< specification >()

template<>

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

inline

Definition at line 163 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 180 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 67 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 80 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 39 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 53 of file parse.h.

pp() [1/15]

std::string mcrl2::lps::pp	(	const lps::action_summand &	x,
		bool	arg0 = true
	)

Definition at line 29 of file lps.cpp.

pp() [2/15]

std::string mcrl2::lps::pp	(	const lps::deadlock &	x,
		bool	arg0 = true
	)

Definition at line 30 of file lps.cpp.

pp() [3/15]

std::string mcrl2::lps::pp	(	const lps::deadlock_summand &	x,
		bool	arg0 = true
	)

Definition at line 31 of file lps.cpp.

pp() [4/15]

std::string mcrl2::lps::pp	(	const lps::linear_process &	x,
		bool	arg0 = true
	)

Definition at line 32 of file lps.cpp.

pp() [5/15]

std::string mcrl2::lps::pp	(	const lps::multi_action &	x,
		bool	arg0 = true
	)

Definition at line 33 of file lps.cpp.

pp() [6/15]

std::string mcrl2::lps::pp	(	const lps::process_initializer &	x,
		bool	arg0 = true
	)

Definition at line 34 of file lps.cpp.

pp() [7/15]

std::string mcrl2::lps::pp	(	const lps::specification &	x,
		bool	arg0 = true
	)

Definition at line 35 of file lps.cpp.

pp() [8/15]

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

inline

Definition at line 44 of file state.h.

pp() [9/15]

std::string mcrl2::lps::pp	(	const lps::stochastic_action_summand &	x,
		bool	arg0 = true
	)

Definition at line 36 of file lps.cpp.

pp() [10/15]

std::string mcrl2::lps::pp	(	const lps::stochastic_distribution &	x,
		bool	arg0 = true
	)

Definition at line 37 of file lps.cpp.

pp() [11/15]

std::string mcrl2::lps::pp	(	const lps::stochastic_linear_process &	x,
		bool	arg0 = true
	)

Definition at line 38 of file lps.cpp.

pp() [12/15]

std::string mcrl2::lps::pp	(	const lps::stochastic_process_initializer &	x,
		bool	arg0 = true
	)

Definition at line 39 of file lps.cpp.

pp() [13/15]

std::string mcrl2::lps::pp	(	const lps::stochastic_specification &	x,
		bool	arg0 = true
	)

Definition at line 40 of file lps.cpp.

pp() [14/15]

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

inline

Definition at line 538 of file probabilistic_data_expression.h.

pp() [15/15]

template<typename T >

std::string mcrl2::lps::pp	(	const T &	x,
		bool	precedence_aware = true
	)

Returns a string representation of the object x.

Definition at line 332 of file print.h.

pp_extended() [1/3]

std::string mcrl2::lps::pp_extended	(	const lps::stochastic_specification &	x,
		const std::string &	process_name,
		bool	precedence_aware = true
	)

Definition at line 79 of file lps.cpp.

pp_extended() [2/3]

std::string mcrl2::lps::pp_extended	(	const specification &	x,
		const std::string &	process_name,
		bool	precedence_aware,
		bool	summand_numbers
	)

Definition at line 88 of file lps.cpp.

pp_extended() [3/3]

std::string mcrl2::lps::pp_extended	(	const stochastic_specification &	x,
		const std::string &	process_name,
		bool	precedence_aware,
		bool	summand_numbers
	)

Definition at line 98 of file lps.cpp.

print()

std::string mcrl2::lps::print ( const lps_statistics_t &  stats, std::size_t  indent = 0  )

inline

Print statistics of lps as indented block in YAML format.

Definition at line 36 of file linearise_utility.h.

print_bitset()

template<typename Bitset >

void mcrl2::lps::print_bitset	(	std::ostream &	os,
		const Bitset &	bs
	)

Definition at line 264 of file explorer_control_flow.h.

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_edge_label_map()

void mcrl2::lps::print_edge_label_map ( const edge_label_map &  m )

inline

Definition at line 111 of file explorer_control_flow.h.

print_exploration_strategy()

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

inline

Definition at line 59 of file exploration_strategy.h.

print_graph()

void mcrl2::lps::print_graph ( const cf_graph &  G )

inline

Definition at line 284 of file explorer_control_flow.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 32 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 55 of file lps_rewriter_type.h.

print_probability()

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

inline

Definition at line 59 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 187 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 226 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 244 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 208 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 110 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 196 of file remove.h.

rename() [1/5]

multi_action mcrl2::lps::rename ( const process::rename_expression_list &  renamings, const multi_action &  multi_action  )

inline

Definition at line 77 of file linearise_rename.h.

rename() [2/5]

process::action mcrl2::lps::rename ( const process::rename_expression_list &  renamings, const process::action &  action  )

inline

Apply renamings to a single action.

Definition at line 45 of file linearise_rename.h.

rename() [3/5]

process::action_list mcrl2::lps::rename ( const process::rename_expression_list &  renamings, const process::action_list &  actions  )

inline

Apply renamings to a list of actions.

Note that the result is not sorted.

Definition at line 63 of file linearise_rename.h.

rename() [4/5]

stochastic_action_summand mcrl2::lps::rename ( const process::rename_expression_list &  renamings, const stochastic_action_summand &  summand  )

inline

Definition at line 84 of file linearise_rename.h.

rename() [5/5]

void mcrl2::lps::rename ( const process::rename_expression_list &  renamings, lps::stochastic_action_summand_vector &  action_summands  )

inline

Definition at line 96 of file linearise_rename.h.

replace_all_variables() [1/2]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::lps::replace_all_variables	(	const T &	x,
		const Substitution &	sigma
	)

Definition at line 103 of file replace.h.

replace_all_variables() [2/2]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::replace_all_variables	(	T &	x,
		const Substitution &	sigma
	)

Definition at line 94 of file replace.h.

replace_constants_by_variables() [1/2]

template<typename T >
requires (std::is_base_of_v<atermpp::aterm, T>)

T mcrl2::lps::replace_constants_by_variables	(	const T &	x,
		const data::rewriter &	r,
		data::mutable_indexed_substitution<> &	sigma
	)

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 54 of file replace_constants_by_variables.h.

replace_constants_by_variables() [2/2]

template<typename T >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::replace_constants_by_variables	(	T &	x,
		const data::rewriter &	r,
		data::mutable_indexed_substitution<> &	sigma
	)

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_data_expressions() [1/2]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::lps::replace_data_expressions	(	const T &	x,
		const Substitution &	sigma,
		bool	innermost
	)

Definition at line 60 of file replace.h.

replace_data_expressions() [2/2]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::replace_data_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost
	)

Definition at line 50 of file replace.h.

replace_free_variables() [1/4]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::lps::replace_free_variables	(	const T &	x,
		const Substitution &	sigma
	)

\brief Applies the substitution sigma to x. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 128 of file replace.h.

replace_free_variables() [2/4]

template<typename T , data::IsSubstitution Substitution, typename VariableContainer >
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::lps::replace_free_variables	(	const T &	x,
		const Substitution &	sigma,
		const VariableContainer &	bound_variables
	)

\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 155 of file replace.h.

replace_free_variables() [3/4]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::replace_free_variables	(	T &	x,
		const Substitution &	sigma
	)

\brief Applies the substitution sigma to x. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 116 of file replace.h.

replace_free_variables() [4/4]

template<typename T , data::IsSubstitution Substitution, typename VariableContainer >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::replace_free_variables	(	T &	x,
		const Substitution &	sigma,
		const VariableContainer &	bound_variables
	)

\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 142 of file replace.h.

replace_process_parameters()

template<data::IsSubstitution Substitution>

void mcrl2::lps::replace_process_parameters	(	specification &	spec,
		Substitution	sigma
	)

Applies a substitution to the process parameters of the specification spec.

Definition at line 265 of file replace.h.

replace_sort_expressions() [1/2]

template<typename T , typename Substitution >
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::lps::replace_sort_expressions	(	const T &	x,
		const Substitution &	sigma,
		bool	innermost
	)

Definition at line 38 of file replace.h.

replace_sort_expressions() [2/2]

template<typename T , typename Substitution >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::replace_sort_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost
	)

Definition at line 28 of file replace.h.

replace_summand_variables()

void mcrl2::lps::replace_summand_variables ( specification &  spec, data::mutable_map_substitution<> &  sigma  )

inline

Applies a substitution to the process parameters of the specification spec.

Definition at line 272 of file replace.h.

replace_variables() [1/2]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::lps::replace_variables	(	const T &	x,
		const Substitution &	sigma
	)

Definition at line 82 of file replace.h.

replace_variables() [2/2]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::replace_variables	(	T &	x,
		const Substitution &	sigma
	)

Definition at line 73 of file replace.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 276 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 258 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [3/6]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::lps::replace_variables_capture_avoiding	(	const T &	x,
		Substitution &	sigma
	)

\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 236 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [4/6]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::lps::replace_variables_capture_avoiding	(	const T &	x,
		Substitution &	sigma,
		data::set_identifier_generator &	id_generator
	)

\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 202 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [5/6]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::replace_variables_capture_avoiding	(	T &	x,
		Substitution &	sigma
	)

\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 218 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [6/6]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::replace_variables_capture_avoiding	(	T &	x,
		Substitution &	sigma,
		data::set_identifier_generator &	id_generator
	)

\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 187 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [1/2]

template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator >
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::lps::replace_variables_capture_avoiding_with_an_identifier_generator	(	const T &	x,
		Substitution &	sigma,
		IdentifierGenerator &	id_generator
	)

\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 160 of file replace_capture_avoiding_with_an_identifier_generator.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [2/2]

template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::replace_variables_capture_avoiding_with_an_identifier_generator	(	T &	x,
		Substitution &	sigma,
		IdentifierGenerator &	id_generator
	)

\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 141 of file replace_capture_avoiding_with_an_identifier_generator.h.

report_cfg_error()

template<typename State >

void mcrl2::lps::report_cfg_error	(	std::size_t	summand,
		const State &	state,
		const std::vector< cf_graph > &	cfgs
	)

Definition at line 442 of file explorer_control_flow.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 140 of file resolve_name_clashes.h.

rewrite() [1/4]

template<typename T , typename Rewriter >
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::lps::rewrite	(	const T &	x,
		Rewriter	R
	)

\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 38 of file rewrite.h.

rewrite() [2/4]

template<typename T , typename Rewriter , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::lps::rewrite	(	const T &	x,
		Rewriter	R,
		const Substitution &	sigma
	)

\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 68 of file rewrite.h.

rewrite() [3/4]

template<typename T , typename Rewriter >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::rewrite	(	T &	x,
		Rewriter	R
	)

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

Definition at line 25 of file rewrite.h.

rewrite() [4/4]

template<typename T , typename Rewriter , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::rewrite	(	T &	x,
		Rewriter	R,
		const Substitution &	sigma
	)

\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 53 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 71 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 39 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 151 of file find.h.

sort_actions()

process::action_list mcrl2::lps::sort_actions ( const process::action_list &  actions )

inline

Definition at line 83 of file linearise_utility.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 224 of file specification.h.

subsumes() [1/2]

bool mcrl2::lps::subsumes ( const deadlock_summand &  ds1, const deadlock_summand &  ds2  )

inline

Determine if delta summand ds1 subsumes delta summand ds2.

Definition at line 161 of file linearise_utility.h.

subsumes() [2/2]

bool mcrl2::lps::subsumes ( const stochastic_action_summand &  as, const deadlock_summand &  ds  )

inline

Determine if action summand as subsumes delta summand ds.

The action summand subsumes the deadlock summand if its condition is implied by that of the deadlock summand, and either the action summand is not timed, or the timestamp of the deadlock summand and the action summand coincide.

Definition at line 153 of file linearise_utility.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 112 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 136 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 124 of file sumelm.h.

summand_distribution() [1/3]

template<>

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

inline

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 78 of file explorer_utilities.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  )

inlinenoexcept

\brief swap overload

Definition at line 132 of file action_summand.h.

swap() [2/8]

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

inlinenoexcept

\brief swap overload

Definition at line 105 of file deadlock.h.

swap() [3/8]

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

inlinenoexcept

\brief swap overload

Definition at line 97 of file deadlock_summand.h.

swap() [4/8]

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

inlinenoexcept

\brief swap overload

Definition at line 117 of file multi_action.h.

swap() [5/8]

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

inlinenoexcept

\brief swap overload

Definition at line 102 of file process_initializer.h.

swap() [6/8]

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

inlinenoexcept

\brief swap overload

Definition at line 89 of file stochastic_action_summand.h.

swap() [7/8]

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

inlinenoexcept

\brief swap overload

Definition at line 104 of file stochastic_distribution.h.

swap() [8/8]

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

inlinenoexcept

\brief swap overload

Definition at line 86 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 44 of file lps.cpp.

translate_user_notation() [2/3]

template<typename T >
requires (std::is_base_of_v<atermpp::aterm, T>)

T mcrl2::lps::translate_user_notation

(

const T &

x

)

Definition at line 30 of file translate_user_notation.h.

translate_user_notation() [3/3]

template<typename T >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::lps::translate_user_notation

(

T &

x

)

Definition at line 23 of file translate_user_notation.h.

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 154 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 125 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 141 of file typecheck.h.

update_active_cfg_vertices()

template<typename Container >

void mcrl2::lps::update_active_cfg_vertices	(	const data::mutable_indexed_substitution<> &	sigma,
		const std::vector< data::variable > &	process_parameters,
		const std::vector< cf_graph > &	cfgs,
		Container &	active_cfg_vertices
	)

Definition at line 395 of file explorer_control_flow.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.

Variable Documentation

update_active_cfg_vertices_timer_reporter_instance

update_active_cfg_vertices_timer_reporter mcrl2::lps::update_active_cfg_vertices_timer_reporter_instance

inline

Definition at line 392 of file explorer_control_flow.h.