mcrl2::pbes_system Namespace Reference

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

Namespaces
namespace	accessors
	The namespace for accessor functions on pbes expressions.
namespace	algorithms
namespace	detail
namespace	tools

Classes
struct	absinthe_algorithm
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_pbes_expressions
struct	add_sort_expressions
struct	add_traverser_data_expressions
struct	add_traverser_identifier_strings
struct	add_traverser_pbes_expressions
struct	add_traverser_sort_expressions
struct	add_traverser_variables
struct	add_variables
class	and_
	\brief The and operator for pbes expressions More...
struct	approximate
	Approximation algorithm. More...
class	bisimulation_algorithm
	Base class for bisimulation algorithms. More...
class	bqnf_rewriter
	A rewriter that rewrites universal quantifiers over conjuncts in BQNF expressions to conjuncts over universal quantifiers. More...
class	branching_bisimulation_algorithm
	Algorithm class for branching bisimulation. More...
class	branching_simulation_equivalence_algorithm
	Algorithm class for branching simulation equivalence. More...
struct	compare_progress_measures_vertex
class	data2pbes_rewriter
	A rewriter that applies one point rule quantifier elimination to a PBES. More...
struct	data_expression_builder
	\brief Builder class More...
struct	data_expression_traverser
	\brief Traverser class More...
struct	data_rewriter
	A rewriter that applies a data rewriter to data expressions in a term. More...
struct	deque_vertex_set
struct	empty_parameter_selection
	Exception that is used to signal an empty parameter selection. More...
struct	enumerate_quantifiers_rewriter
	An attempt for improving the efficiency. More...
class	equation_index
	Maps variables to their corresponding equations in a boolean_equation_system or PBES. More...
class	exists
	\brief The existential quantification operator for pbes expressions More...
class	explorer
class	fixpoint_symbol
	\brief A fixpoint symbol More...
class	forall
	\brief The universal quantification operator for pbes expressions More...
class	gauss_elimination_algorithm
	Algorithm class for the Gauss elimination algorithm for solving systems of (P)BES equations. More...
struct	global_local_strategy
struct	global_strategy
struct	identifier_string_traverser
	\brief Traverser class More...
class	if_rewriter
class	imp
	\brief The implication operator for pbes expressions More...
struct	is_not_false
struct	is_not_true
struct	lazy_union
struct	local_strategy
class	lps2pbes_algorithm
	Algorithm for translating a state formula and a timed specification to a pbes. More...
class	lps_solve_structure_graph_algorithm
class	lts2pbes_algorithm
	Algorithm for translating a state formula and an untimed specification to a pbes. More...
class	lts_info
class	lts_solve_structure_graph_algorithm
class	lts_type
class	ltsmin_state
struct	no_strategy
struct	node_t
class	not_
	\brief The not operator for pbes expressions More...
class	one_point_rule_rewriter
	A rewriter that applies one point rule quantifier elimination to a PBES. More...
class	or_
	\brief The or operator for pbes expressions More...
class	parity_game_generator
	Class for generating a BES from a PBES. This BES can be interpreted as a graph corresponding to a parity game problem. The proposition variables of the BES correspond to the vertices of the graph. An interface to the graph is provided in which the vertices correspond to integer values. The values are in the range [0, 1, ..., n], i.e. there are no holes in the sequence. Each vertex is labeled with a priority value, which is the block nesting depth of the proposition variable in the BES. More...
class	partial_order_reduction_algorithm
class	pbes
	parameterized boolean equation system More...
class	pbes2data_rewriter
class	pbes_abstract_algorithm
	Algorithm class for the abstract algorithm. More...
class	pbes_constelm_algorithm
	Algorithm class for the constelm algorithm. More...
class	pbes_eqelm_algorithm
	Algorithm class for the eqelm algorithm. More...
class	pbes_equation
	pbes equation. More...
struct	pbes_equation_index
struct	pbes_equation_solver
	Solves an equation. More...
class	pbes_expression
	\brief A pbes expression More...
struct	pbes_expression_builder
	\brief Builder class More...
struct	pbes_expression_builder_base
	Builder class. More...
struct	pbes_expression_traverser
	\brief Traverser class More...
struct	pbes_expression_traverser_base
	Traversal class for pbes_expressions. Used as a base class for pbes_expression_traverser. More...
class	pbes_parelm_algorithm
	Algorithm class for the parelm algorithm. More...
struct	pbes_traits
	Traits class for pbes expressions. More...
class	pbes_type_checker
class	pbesinst_algorithm
	Algorithm class for the pbesinst instantiation algorithm. More...
class	pbesinst_alternative_lazy_algorithm
	An alternative lazy algorithm for instantiating a PBES, ported from bes_deprecated.h. More...
class	pbesinst_finite_algorithm
	Algorithm class for the finite pbesinst algorithm. More...
struct	pbesinst_finite_rename
	Function object for renaming a propositional variable instantiation. More...
class	pbesinst_lazy_algorithm
	A PBES instantiation algorithm that uses a lazy strategy. More...
class	pbesinst_lazy_todo
struct	pbesinst_rename
	Creates a unique name for a propositional variable instantiation. The propositional variable instantiation must be closed. Originally implemented by Alexander van Dam. More...
struct	pbesinst_rename_long
	Creates a unique name for a propositional variable instantiation. The propositional variable instantiation must be closed. Originally implemented by Alexander van Dam. More...
class	pbesinst_structure_graph_algorithm
	Variant of pbesinst that will compute a structure graph for a PBES. The result will be put in the structure graph that is passed in the constructor. More...
class	pbesinst_structure_graph_algorithm2
	Adds an optimization to pbesinst_structure_graph. More...
class	pbesinst_symbolic_algorithm
	Algorithm class for the symbolic_exploration instantiation algorithm. More...
class	pbespgsolve_algorithm
struct	pbespgsolve_options
struct	pbespor_options
struct	pbespor_pbes_composer
struct	pbessolve_options
struct	pbesstategraph_options
class	pfnf_rewriter
	A rewriter that brings PBES expressions into PFNF normal form. More...
struct	pfnf_stream_printer
	Prints the object x to a stream. More...
struct	pg_actions
struct	print_brief_traverser
	Visitor for printing the root node of a PBES. More...
struct	progress_measure
struct	progress_measures_vertex
	Vertex of the progress measures graph. More...
class	propositional_variable
	\brief A propositional variable declaration More...
class	propositional_variable_instantiation
	\brief A propositional variable instantiation More...
class	propositional_variable_substitution
	Substitution function for propositional variables. More...
class	quantifiers_inside_rewriter
	A rewriter that pushes quantifiers inside in a PBES expression. More...
class	simple_structure_graph
struct	simplify_data_rewriter
	A rewriter that simplifies boolean expressions in a term, and rewrites data expressions. More...
struct	simplify_quantifiers_data_rewriter
	A rewriter that simplifies boolean expressions and quantifiers, and rewrites data expressions. More...
struct	simplify_quantifiers_rewriter
	A rewriter that simplifies boolean expressions and quantifiers. More...
struct	simplify_rewriter
	A rewriter that simplifies boolean expressions in a term. More...
class	small_progress_measures_algorithm
	Algorithm class for the small progress measures algorithm. More...
class	solve_structure_graph_algorithm
struct	sort_expression_builder
	\brief Builder class More...
struct	sort_expression_traverser
	\brief Traverser class More...
class	srf_equation
class	srf_pbes
class	srf_summand
class	strategy_vector
struct	stream_printer
	Prints the object x to a stream. More...
class	strong_bisimulation_algorithm
	Algorithm class for strong bisimulation. More...
class	structure_graph
struct	summand_class
struct	summand_equivalence_key
struct	unify_parameters_replace_function
struct	untyped_pbes
struct	variable_builder
	\brief Builder class More...
struct	variable_traverser
	\brief Traverser class More...
struct	vertex_set
class	weak_bisimulation_algorithm
	Algorithm class for weak bisimulation. More...

Typedefs
typedef atermpp::term_list< fixpoint_symbol >	fixpoint_symbol_list
	\brief list of fixpoint_symbols
typedef std::vector< fixpoint_symbol >	fixpoint_symbol_vector
	\brief vector of fixpoint_symbols
typedef boost::dynamic_bitset	summand_set
typedef atermpp::term_list< pbes_equation >	pbes_equation_list
	\brief list of pbes_equations
typedef std::vector< pbes_equation >	pbes_equation_vector
	\brief vector of pbes_equations
typedef atermpp::term_list< pbes_expression >	pbes_expression_list
	\brief list of pbes_expressions
typedef std::vector< pbes_expression >	pbes_expression_vector
	\brief vector of pbes_expressions
typedef atermpp::term_list< propositional_variable_instantiation >	propositional_variable_instantiation_list
	\brief list of propositional_variable_instantiations
typedef std::vector< propositional_variable_instantiation >	propositional_variable_instantiation_vector
	\brief vector of propositional_variable_instantiations
typedef std::map< core::identifier_string, std::vector< std::size_t > >	pbesinst_index_map
	Data structure for storing the indices of the variables that should be expanded by the finite pbesinst algorithm.
typedef std::map< core::identifier_string, std::vector< data::variable > >	pbesinst_variable_map
	Data structure for storing the variables that should be expanded by the finite pbesinst algorithm.
typedef unsigned long long	identifier_t
typedef unsigned short	priority_t
typedef bool	owner_t
typedef atermpp::term_list< propositional_variable >	propositional_variable_list
	\brief list of propositional_variables
typedef std::vector< propositional_variable >	propositional_variable_vector
	\brief vector of propositional_variables
typedef std::map< core::identifier_string, std::size_t >	variable_map

Enumerations
enum	absinthe_strategy { absinthe_over , absinthe_under }
	The approximation strategies of the absinthe tool. More...
enum	bisimulation_type { strong_bisim , weak_bisim , branching_bisim , branching_sim }
	An enumerated type for the available bisimulation types. More...
enum	tribool { no , maybe , yes }
enum	pbes_rewriter_type {   simplify , quantifier_all , quantifier_finite , quantifier_inside ,   quantifier_one_point , prover , pfnf , ppg ,   bqnf_quantifier }
	An enumerated type for the available pbes rewriters. More...
enum	pbesinst_strategy { pbesinst_lazy_strategy , pbesinst_alternative_lazy_strategy , pbesinst_finite_strategy }
	pbesinst transformation strategies More...
enum	remove_level { none , some , all }
	BES variable remove level when generating a BES from a PBES. More...
enum	search_strategy { breadth_first , depth_first , breadth_first_short , depth_first_short }
	Search strategy when generating a BES from a PBES. More...
enum	solution_strategy_t { gauss , small_progr_measures }
enum	transformation_strategy { lazy , optimize , on_the_fly , on_the_fly_with_fixed_points }
	Strategies for the generation of a BES from a PBES. More...
enum	pbespg_solver_type { spm_solver , alternative_spm_solver , recursive_solver , priority_promotion }

Functions
template<typename Term >
std::string	print_term (const Term &x)
template<typename Term >
std::string	print_symbol (const Term &x)
absinthe_strategy	parse_absinthe_strategy (const std::string &strategy)
	Parses an absinthe strategy.
std::string	print_absinthe_strategy (const absinthe_strategy strategy)
	Prints an absinthe strategy.
std::istream &	operator>> (std::istream &is, absinthe_strategy &strategy)
std::ostream &	operator<< (std::ostream &os, const absinthe_strategy strategy)
std::string	description (const absinthe_strategy strategy)
	Prints an absinthe strategy.
void	anonymize (pbes &pbesspec)
pbes	branching_bisimulation (const lps::specification &model, const lps::specification &spec)
	Returns a pbes that expresses branching bisimulation between two specifications.
pbes	strong_bisimulation (const lps::specification &model, const lps::specification &spec)
	Returns a pbes that expresses strong bisimulation between two specifications.
pbes	weak_bisimulation (const lps::specification &model, const lps::specification &spec)
	Returns a pbes that expresses weak bisimulation between two specifications.
pbes	branching_simulation_equivalence (const lps::specification &model, const lps::specification &spec)
	Returns a pbes that expresses branching simulation equivalence between two specifications.
bisimulation_type	parse_bisimulation_type (const std::string &type)
	Returns the string corresponding to a bisimulation type.
std::string	print_bisimulation_type (const bisimulation_type t)
	Returns a description of a bisimulation type.
std::string	description (const bisimulation_type t)
	Returns a description of a bisimulation type.
std::istream &	operator>> (std::istream &is, bisimulation_type &t)
std::ostream &	operator<< (std::ostream &os, const bisimulation_type t)
pbes_expression	complement (const pbes_expression &x)
	Returns the complement of a pbes expression.
pbes_system::pbes	complps2pbes (const process::process_specification &procspec, const state_formulas::state_formula &)
void	constelm (pbes &p, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type, bool compute_conditions=false, bool remove_redundant_equations=true, bool check_quantifiers=true)
	Apply the constelm algorithm.
void	check_whether_argument_is_a_well_formed_bes (const pbes_expression &x)
	This function checks whether x is a well formed bes expression, without quantifiers and.
void	lpsstategraph (lps::specification &lpsspec, const pbesstategraph_options &options)
	Apply the stategraph algorithm.
void	lpsstategraph (const std::string &input_filename, const std::string &output_filename, const pbesstategraph_options &options)
std::pair< std::vector< pbes_expression >, data::data_specification >	parse_pbes_expressions (std::string text, const std::string &data_spec="")
	Parses a sequence of pbes expressions. The format of the text is as follows:
pbes_expression	parse_pbes_expression (const std::string &text, const std::string &var_decl="datavar\npredvar\n", const std::string &data_spec="")
	Parses a single pbes expression.
template<typename SubstitutionFunction >
pbes_expression	parse_pbes_expression (const std::string &expr, const std::string &subst, const pbes &p, SubstitutionFunction &sigma)
	Parses a pbes expression.
atermpp::aterm_ostream &	operator<< (atermpp::aterm_ostream &stream, const pbes &pbes)
	Writes the pbes to a stream.
atermpp::aterm_istream &	operator>> (atermpp::aterm_istream &stream, pbes &pbes)
	Reads a pbes from a stream.
template<typename T >
std::string	pfnf_pp (const T &x)
	Returns a PFNF string representation of the object x.
void	eqelm (pbes &p, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type, bool ignore_initial_state=false)
	Apply the eqelm algorithm.
template<typename T , typename OutputIterator >
void	find_all_variables (const T &x, OutputIterator o)
template<typename T >
std::set< data::variable >	find_all_variables (const T &x)
template<typename T , typename OutputIterator >
void	find_free_variables (const T &x, OutputIterator o)
template<typename T , typename OutputIterator , typename VariableContainer >
void	find_free_variables_with_bound (const T &x, OutputIterator o, const VariableContainer &bound)
template<typename T >
std::set< data::variable >	find_free_variables (const T &x)
template<typename T , typename VariableContainer >
std::set< data::variable >	find_free_variables_with_bound (const T &x, VariableContainer const &bound)
template<typename T , typename OutputIterator >
void	find_identifiers (const T &x, OutputIterator o)
template<typename T >
std::set< core::identifier_string >	find_identifiers (const T &x)
template<typename T , typename OutputIterator >
void	find_sort_expressions (const T &x, OutputIterator o)
template<typename T >
std::set< data::sort_expression >	find_sort_expressions (const T &x)
template<typename T , typename OutputIterator >
void	find_function_symbols (const T &x, OutputIterator o)
template<typename T >
std::set< data::function_symbol >	find_function_symbols (const T &x)
template<typename Container , typename OutputIterator >
void	find_propositional_variable_instantiations (Container const &container, OutputIterator o)
	Returns all data variables that occur in a range of expressions.
template<typename Container >
std::set< propositional_variable_instantiation >	find_propositional_variable_instantiations (Container const &container)
	Returns all data variables that occur in a range of expressions.
template<typename T >
bool	search_variable (const T &x, const data::variable &v)
	Returns true if the term has a given variable as subterm.
std::map< data::variable, std::set< data::data_expression > >	find_equalities (const pbes_expression &x)
std::map< data::variable, std::set< data::data_expression > >	find_inequalities (const pbes_expression &x)
std::string	pp (const fixpoint_symbol &x)
std::ostream &	operator<< (std::ostream &out, const fixpoint_symbol &x)
void	swap (fixpoint_symbol &t1, fixpoint_symbol &t2)
	\brief swap overload
void	save_bes_pgsolver (const pbes &bes, std::ostream &stream, bool maxpg=true)
const std::vector< utilities::file_format > &	pbes_file_formats ()
bool	is_pbes_file_format (const utilities::file_format &format)
const utilities::file_format &	pbes_format_internal ()
const utilities::file_format &	pbes_format_text ()
const utilities::file_format &	pbes_format_internal_bes ()
const utilities::file_format &	pbes_format_pgsolver ()
const utilities::file_format	guess_format (const std::string &filename)
void	save_pbes (const pbes &pbes, std::ostream &stream, utilities::file_format format=utilities::file_format())
	Save a PBES in the format specified.
void	load_pbes (pbes &pbes, std::istream &stream, utilities::file_format format, const std::string &source="")
	Load a PBES from file.
void	save_pbes (const pbes &pbes, const std::string &filename, utilities::file_format format=utilities::file_format(), bool welltypedness_check=true)
	save_pbes Saves a PBES to a file.
void	load_pbes (pbes &pbes, const std::string &filename, utilities::file_format format=utilities::file_format())
	Load pbes from file.
template<typename T >
bool	is_bes (const T &x)
	Returns true if a PBES object is in BES form.
bool	is_monotonous (pbes_expression f)
	Returns true if the pbes expression is monotonous.
bool	is_monotonous (const pbes_equation &e)
	Returns true if the pbes equation is monotonous.
bool	is_monotonous (const pbes &p)
	Returns true if the pbes is monotonous.
template<typename FwdIt >
pbes_expression	join_or (FwdIt first, FwdIt last)
	Returns or applied to the sequence of pbes expressions [first, last)
template<typename FwdIt >
pbes_expression	join_and (FwdIt first, FwdIt last)
	Returns and applied to the sequence of pbes expressions [first, last)
std::set< pbes_expression >	split_or (const pbes_expression &expr, bool split_data_expressions=false)
	Splits a disjunction into a sequence of operands Given a pbes expression of the form p1 || p2 || .... || pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main function symbol.
std::set< pbes_expression >	split_and (const pbes_expression &expr, bool split_data_expressions=false)
	Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 && p2 && .... && pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main function symbol.
template<typename FwdIt >
pbes_expression	optimized_join_or (FwdIt first, FwdIt last)
	Returns or applied to the sequence of pbes expressions [first, last)
template<typename FwdIt >
pbes_expression	optimized_join_and (FwdIt first, FwdIt last)
	Returns and applied to the sequence of pbes expressions [first, last)
pbes	lps2pbes (const lps::specification &lpsspec, const state_formulas::state_formula &formula, bool timed=false, bool structured=false, bool unoptimized=false, bool preprocess_modal_operators=false, bool generate_counter_example=false, bool check_only=false)
	Translates a linear process specification and a state formula to a PBES. If the solution of the PBES is true, the formula holds for the specification.
pbes	lps2pbes (const lps::specification &lpsspec, const state_formulas::state_formula_specification &formspec, bool timed=false, bool structured=false, bool unoptimized=false, bool preprocess_modal_operators=false, bool generate_counter_example=false, bool check_only=false)
	Translates a linear process specification and a state formula to a PBES. If the solution of the PBES is true, the formula holds for the specification.
pbes	lps2pbes (const std::string &spec_text, const std::string &formula_text, bool timed=false, bool structured=false, bool unoptimized=false, bool preprocess_modal_operators=false, bool generate_counter_example=false, bool check_only=false)
	Applies the lps2pbes algorithm.
pbes	lts2pbes (const lts::lts_lts_t &l, const state_formulas::state_formula_specification &formspec, bool preprocess_modal_operators=false, bool generate_counter_example=false)
	Translates an LTS and a modal formula into a PBES that represents the corresponding model checking problem.
void	make_standard_form (pbes &eqn, bool recursive_form=false)
	Transforms a PBES into standard form.
template<typename T >
bool	is_normalized (const T &x)
	Checks if a pbes expression is normalized.
template<typename T >
void	normalize (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	The function normalize brings (embedded) pbes expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.
template<typename T >
T	normalize (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	The function normalize brings (embedded) pbes expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.
template<typename T >
void	normalize_sorts (T &x, const data::sort_specification &sortspec, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T >
T	normalize_sorts (const T &x, const data::sort_specification &sortspec, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
void	parelm (pbes &p)
	Apply the parelm algorithm.
pbes	parse_pbes (std::istream &in)
std::istream &	operator>> (std::istream &from, pbes &result)
	Reads a PBES from an input stream.
pbes	parse_pbes (const std::string &text)
template<typename VariableContainer >
propositional_variable	parse_propositional_variable (const std::string &text, const VariableContainer &variables, const data::data_specification &dataspec=data::data_specification())
template<typename VariableContainer , typename PropositionalVariableContainer >
pbes_expression	parse_pbes_expression (const std::string &text, const data::data_specification &dataspec, const VariableContainer &variables, const PropositionalVariableContainer &propositional_variables, bool type_check=true, bool translate_user_notation=true, bool normalize_sorts=true)
	Parse a pbes expression. Throws an exception if something went wrong.
template<typename VariableContainer >
pbes_expression	parse_pbes_expression (const std::string &text, const pbes &pbesspec, const VariableContainer &variables, bool type_check=true, bool translate_user_notation=true, bool normalize_sorts=true)
	Parse a pbes expression. Throws an exception if something went wrong.
std::string	print_summand_set (const summand_set &s)
static bool	operator&& (tribool a, tribool b)
static bool	operator&& (const std::function< tribool()> &a, const std::function< tribool(bool)> &b)
void	complete_data_specification (pbes &p)
	Adds all sorts that appear in the PBES p to the data specification of p.
std::string	pp (const pbes &x)
void	normalize_sorts (pbes &x, const data::sort_specification &sortspec)
void	translate_user_notation (pbes_system::pbes &x)
std::set< data::sort_expression >	find_sort_expressions (const pbes_system::pbes &x)
std::set< data::variable >	find_all_variables (const pbes_system::pbes &x)
std::set< data::variable >	find_free_variables (const pbes_system::pbes &x)
std::set< data::function_symbol >	find_function_symbols (const pbes_system::pbes &x)
bool	is_well_typed_equation (const pbes_equation &eqn, const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const data::data_specification &data_spec)
bool	is_well_typed_pbes (const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const std::set< data::variable > &occurring_global_variables, const std::set< propositional_variable > &declared_variables, const std::set< propositional_variable_instantiation > &occ, const propositional_variable_instantiation &init, const data::data_specification &data_spec)
atermpp::aterm_appl	pbes_to_aterm (const pbes &p)
	Conversion to atermappl.
std::ostream &	operator<< (std::ostream &out, const pbes &x)
bool	operator== (const pbes &p1, const pbes &p2)
	Equality operator on PBESs.
atermpp::aterm_appl	pbes_equation_to_aterm (const pbes_equation &eqn)
	Conversion to atermaPpl.
bool	is_well_typed (const pbes_equation &eqn)
bool	has_propositional_variables (const pbes_expression &x)
std::string	pp (const pbes_equation &x)
std::ostream &	operator<< (std::ostream &out, const pbes_equation &x)
void	swap (pbes_equation &t1, pbes_equation &t2)
	\brief swap overload
bool	operator== (const pbes_equation &x, const pbes_equation &y)
bool	operator!= (const pbes_equation &x, const pbes_equation &y)
std::string	pp (const pbes_equation_vector &x)
void	normalize_sorts (pbes_equation_vector &x, const data::sort_specification &sortspec)
std::set< data::variable >	find_free_variables (const pbes_system::pbes_equation &x)
std::ostream &	operator<< (std::ostream &out, const pbes_equation_index &index)
bool	is_propositional_variable_instantiation (const atermpp::aterm_appl &x)
bool	is_not (const atermpp::aterm_appl &x)
bool	is_and (const atermpp::aterm_appl &x)
bool	is_or (const atermpp::aterm_appl &x)
bool	is_imp (const atermpp::aterm_appl &x)
bool	is_forall (const atermpp::aterm_appl &x)
bool	is_exists (const atermpp::aterm_appl &x)
bool	is_pbes_expression (const atermpp::aterm_appl &x)
std::string	pp (const pbes_expression &x)
std::ostream &	operator<< (std::ostream &out, const pbes_expression &x)
void	swap (pbes_expression &t1, pbes_expression &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_propositional_variable_instantiation (atermpp::aterm_appl &t, const ARGUMENTS &... args)
std::string	pp (const propositional_variable_instantiation &x)
std::ostream &	operator<< (std::ostream &out, const propositional_variable_instantiation &x)
void	swap (propositional_variable_instantiation &t1, propositional_variable_instantiation &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_not_ (atermpp::aterm_appl &t, const ARGUMENTS &... args)
std::string	pp (const not_ &x)
std::ostream &	operator<< (std::ostream &out, const not_ &x)
void	swap (not_ &t1, not_ &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_and_ (atermpp::aterm_appl &t, const ARGUMENTS &... args)
std::string	pp (const and_ &x)
std::ostream &	operator<< (std::ostream &out, const and_ &x)
void	swap (and_ &t1, and_ &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_or_ (atermpp::aterm_appl &t, const ARGUMENTS &... args)
std::string	pp (const or_ &x)
std::ostream &	operator<< (std::ostream &out, const or_ &x)
void	swap (or_ &t1, or_ &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_imp (atermpp::aterm_appl &t, const ARGUMENTS &... args)
std::string	pp (const imp &x)
std::ostream &	operator<< (std::ostream &out, const imp &x)
void	swap (imp &t1, imp &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_forall (atermpp::aterm_appl &t, const ARGUMENTS &... args)
std::string	pp (const forall &x)
std::ostream &	operator<< (std::ostream &out, const forall &x)
void	swap (forall &t1, forall &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_exists (atermpp::aterm_appl &t, const ARGUMENTS &... args)
std::string	pp (const exists &x)
std::ostream &	operator<< (std::ostream &out, const exists &x)
void	swap (exists &t1, exists &t2)
	\brief swap overload
std::string	pp (const pbes_expression_list &x)
std::string	pp (const pbes_expression_vector &x)
std::string	pp (const propositional_variable_instantiation_list &x)
std::string	pp (const propositional_variable_instantiation_vector &x)
std::set< pbes_system::propositional_variable_instantiation >	find_propositional_variable_instantiations (const pbes_system::pbes_expression &x)
std::set< core::identifier_string >	find_identifiers (const pbes_system::pbes_expression &x)
std::set< data::variable >	find_free_variables (const pbes_system::pbes_expression &x)
bool	search_variable (const pbes_system::pbes_expression &x, const data::variable &v)
pbes_system::pbes_expression	normalize_sorts (const pbes_system::pbes_expression &x, const data::sort_specification &sortspec)
pbes_system::pbes_expression	translate_user_notation (const pbes_system::pbes_expression &x)
const pbes_expression &	true_ ()
const pbes_expression &	false_ ()
bool	is_true (const pbes_expression &t)
	Test for the value true.
bool	is_false (const pbes_expression &t)
	Test for the value false.
bool	is_pbes_not (const pbes_expression &t)
	Returns true if the term t is a not expression.
bool	is_pbes_and (const pbes_expression &t)
	Returns true if the term t is an and expression.
bool	is_pbes_or (const pbes_expression &t)
	Returns true if the term t is an or expression.
bool	is_pbes_imp (const pbes_expression &t)
	Returns true if the term t is an imp expression.
bool	is_pbes_forall (const pbes_expression &t)
	Returns true if the term t is a universal quantification.
bool	is_pbes_exists (const pbes_expression &t)
	Returns true if the term t is an existential quantification.
bool	is_universal_not (const pbes_expression &t)
	Test for a conjunction.
bool	is_universal_and (const pbes_expression &t)
	Test for a conjunction.
bool	is_universal_or (const pbes_expression &t)
	Test for a disjunction.
bool	is_data (const pbes_expression &t)
	Returns true if the term t is a data expression.
pbes_expression	make_forall_ (const data::variable_list &l, const pbes_expression &p)
	Make a universal quantification. It checks for an empty variable list, which is not allowed.
pbes_expression	make_exists_ (const data::variable_list &l, const pbes_expression &p)
	Make an existential quantification. It checks for an empty variable list, which is not allowed.
void	optimized_not (pbes_expression &result, const pbes_expression &p)
	Make a negation.
void	optimized_and (pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
	Make a conjunction.
void	optimized_or (pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
	Make a disjunction.
void	optimized_imp (pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
	Make an implication.
void	optimized_forall (pbes_expression &result, const data::variable_list &l, const pbes_expression &p)
	Make a universal quantification If l is empty, p is returned.
void	optimized_exists (pbes_expression &result, const data::variable_list &l, const pbes_expression &p)
	Make an existential quantification If l is empty, p is returned.
bool	is_constant (const pbes_expression &x)
const data::variable_list &	quantifier_variables (const pbes_expression &x)
data::variable_list	free_variables (const pbes_expression &x)
template<typename T >
std::string	print_brief (const T &x)
	Returns a string representation of the root node of a PBES.
template<typename T >
bool	is_simple_expression (const T &x)
	Determines if an expression is a simple expression. An expression is simple if it is free of propositional variables.
bool	is_non_simple_disjunct (const pbes_expression &t)
	Test for a disjunction.
bool	is_non_simple_conjunct (const pbes_expression &t)
	Test for a conjunction.
std::vector< pbes_expression >	split_disjuncts (const pbes_expression &expr, bool split_simple_expr=false)
	Splits a disjunction into a sequence of operands. Given a pbes expression of the form p1 || p2 || .... || pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main function symbol.
std::vector< pbes_expression >	split_conjuncts (const pbes_expression &expr, bool split_simple_expr=false)
	Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 && p2 && .... && pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main function symbol.
template<typename Rewriter >
pbes_equation_solver< Rewriter >	make_pbes_equation_solver (const Rewriter &rewriter)
	Utility function for creating a pbes_equation_solver.
int	gauss_elimination (pbes &p)
	Solves a PBES equation system using Gauss elimination.
pbes_rewriter_type	parse_pbes_rewriter_type (const std::string &type)
	Parses a pbes rewriter type.
std::string	print_pbes_rewriter_type (const pbes_rewriter_type type)
	Prints a pbes rewriter type.
std::string	description (const pbes_rewriter_type type)
	Returns a description of a pbes rewriter.
std::istream &	operator>> (std::istream &is, pbes_rewriter_type &t)
	Stream operator for rewriter type.
std::ostream &	operator<< (std::ostream &os, const pbes_rewriter_type t)
bool	pbes_instantiation_test_algorithm_test (pbes &pbes_spec, const bool expected_outcome, const data::rewriter::strategy rewrite_strategy)
bool	alternative_lazy_algorithm_test (pbes &pbes_spec, const bool expected_outcome, const transformation_strategy trans_strat, const search_strategy search_strat, const data::rewriter::strategy rewrite_strategy)
bool	pbes2_bool_test (pbes &pbes_spec, const bool expected_outcome, data::rewriter::strategy rewrite_strategy=data::jitty)
void	make_pbesinst_substitution (const data::variable_list &v, const data::data_expression_list &e, data::rewriter::substitution_type &sigma)
	Creates a substitution function for the pbesinst rewriter.
bool	pbesinst_is_constant (const pbes_expression &x)
mcrl2::pbes_system::pbes_expression	pbes_expression_order_quantified_variables (const mcrl2::pbes_system::pbes_expression &p, const mcrl2::data::data_specification &data_spec)
void	pbesinst_finite (pbes &p, data::rewrite_strategy rewrite_strategy, const std::string &finite_parameter_selection)
std::ostream &	operator<< (std::ostream &out, const pbesinst_lazy_todo &todo)
pbesinst_strategy	parse_pbesinst_strategy (const std::string &s)
	Parse a pbesinst transformation strategy.
std::istream &	operator>> (std::istream &is, pbesinst_strategy &s)
std::string	print_pbesinst_strategy (const pbesinst_strategy strategy)
	Returns a string representation of a pbesinst transformation strategy.
std::ostream &	operator<< (std::ostream &os, const pbesinst_strategy strategy)
std::string	description (const pbesinst_strategy strategy)
	Returns a string representation of a pbesinst transformation strategy.
template<typename StructureGraph , typename VertexSet >
bool	includes_successors (const StructureGraph &G, typename StructureGraph::index_type u, const VertexSet &A)
template<typename StructureGraph >
deque_vertex_set	exclusive_predecessors (const StructureGraph &G, const vertex_set &A)
template<typename StructureGraph >
void	insert_predecessors (const StructureGraph &G, structure_graph::index_type u, const vertex_set &A, deque_vertex_set &todo)
template<typename StructureGraph , typename Strategy >
vertex_set	attr_default_generic (const StructureGraph &G, vertex_set A, std::size_t alpha, Strategy tau)
template<typename StructureGraph >
vertex_set	attr_default (const StructureGraph &G, vertex_set A, std::size_t alpha)
template<typename StructureGraph >
vertex_set	attr_default_no_strategy (const StructureGraph &G, vertex_set A, std::size_t alpha)
template<typename StructureGraph >
vertex_set	attr_default_with_tau (const StructureGraph &G, vertex_set A, std::size_t alpha, std::array< strategy_vector, 2 > &tau)
std::ostream &	operator<< (std::ostream &out, const pbessolve_options &options)
std::ostream &	operator<< (std::ostream &out, const vertex_set &V)
vertex_set	set_union (const vertex_set &V, const vertex_set &W)
template<typename VertexSet >
vertex_set	set_intersection (const VertexSet &V, const vertex_set &W)
vertex_set	set_minus (const vertex_set &V, const vertex_set &W)
std::ostream &	operator<< (std::ostream &out, const lazy_union &V)
bool	is_subset_of (const vertex_set &V, const vertex_set &W)
template<typename StructureGraph , typename VertexSet >
structure_graph::index_type	find_successor_in (const StructureGraph &G, structure_graph::index_type u, const VertexSet &A)
template<typename StructureGraph >
void	log_vertex_set (const StructureGraph &G, const vertex_set &V, const std::string &name)
std::ostream &	operator<< (std::ostream &out, const strategy_vector &tau_alpha)
std::string	print_strategy_vector (const vertex_set &S_alpha, const strategy_vector &tau_alpha)
template<typename StructureGraph >
std::set< structure_graph::index_type >	extract_minimal_structure_graph (StructureGraph &G, typename StructureGraph::index_type init, const vertex_set &S0, const vertex_set &S1)
template<typename StructureGraph >
std::set< structure_graph::index_type >	extract_minimal_structure_graph (StructureGraph &G, typename StructureGraph::index_type init, const vertex_set &S0, const vertex_set &S1, const strategy_vector &tau0, const strategy_vector &tau1)
template<typename StructureGraph >
std::set< structure_graph::index_type >	extract_minimal_structure_graph (StructureGraph &G, typename StructureGraph::index_type init, bool is_disjunctive)
pbes_expression	formula (std::set< identifier_t > const &v, const owner_t owner, const std::string &prefix="X")
void	parse_pgsolver_string (const std::string &text, pbes &result, bool maxpg=true)
	Reads a parity game from an input stream, and stores it as a BES.
void	parse_pgsolver (std::istream &from, pbes &result, bool maxpg=true)
	Reads a parity game from an input stream, and stores it as a BES.
void	parse_pgsolver (const std::string &filename, pbes &b, bool maxpg=true)
	Parse parity game in PGSolver format from filename, and store the resulting BES in b.
constexpr int	precedence (const forall &)
constexpr int	precedence (const exists &)
constexpr int	precedence (const imp &)
constexpr int	precedence (const or_ &)
constexpr int	precedence (const and_ &)
constexpr int	precedence (const not_ &)
int	precedence (const pbes_expression &x)
bool	is_left_associative (const imp &)
bool	is_left_associative (const or_ &)
bool	is_left_associative (const and_ &)
bool	is_left_associative (const pbes_expression &x)
bool	is_right_associative (const imp &)
bool	is_right_associative (const or_ &)
bool	is_right_associative (const and_ &)
bool	is_right_associative (const pbes_expression &x)
template<typename T >
std::string	pp (const T &x)
	Returns a string representation of the object x.
template<class... ARGUMENTS>
void	make_propositional_variable (atermpp::aterm_appl &t, const ARGUMENTS &... args)
bool	is_propositional_variable (const atermpp::aterm_appl &x)
std::string	pp (const propositional_variable &x)
std::ostream &	operator<< (std::ostream &out, const propositional_variable &x)
void	swap (propositional_variable &t1, propositional_variable &t2)
	\brief swap overload
std::string	pp (const propositional_variable_list &x)
std::string	pp (const propositional_variable_vector &x)
void	quantifier_propagate (pbes &p)
pbes	quantifier_propagate (const pbes &p)
std::set< propositional_variable >	reachable_variables (const pbes &p)
std::vector< propositional_variable >	remove_unreachable_variables (pbes &p)
	Removes equations that are not (syntactically) reachable from the initial state of a PBES.
remove_level	parse_remove_level (const std::string &s)
std::string	print_remove_level (const remove_level s)
std::istream &	operator>> (std::istream &is, remove_level &level)
std::ostream &	operator<< (std::ostream &os, const remove_level s)
std::string	description (const remove_level s)
template<typename T >
T	remove_parameters (const T &x, const std::vector< std::size_t > &to_be_removed, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Removes parameters from propositional variable instantiations in a pbes expression.
template<typename T >
void	remove_parameters (T &x, const std::vector< std::size_t > &to_be_removed, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
	Removes parameters from propositional variable instantiations in a pbes expression.
template<typename T >
T	remove_parameters (const T &x, const std::map< core::identifier_string, std::vector< std::size_t > > &to_be_removed, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Removes parameters from propositional variable instantiations in a pbes expression.
template<typename T >
void	remove_parameters (T &x, const std::map< core::identifier_string, std::vector< std::size_t > > &to_be_removed, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Removes parameters from propositional variable instantiations in a pbes expression.
template<typename T >
T	remove_parameters (const T &x, const std::set< data::variable > &to_be_removed, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0)
	Removes parameters from propositional variable instantiations in a pbes expression.
template<typename T >
void	remove_parameters (T &x, const std::set< data::variable > &to_be_removed, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Removes parameters from propositional variable instantiations in a pbes expression.
template<typename T , typename Substitution >
void	replace_sort_expressions (T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
T	replace_sort_expressions (const T &x, const Substitution &sigma, bool innermost, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
void	replace_data_expressions (T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
T	replace_data_expressions (const T &x, const Substitution &sigma, bool innermost, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
void	replace_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
T	replace_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
void	replace_all_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
T	replace_all_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
void	replace_free_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
T	replace_free_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution , typename VariableContainer >
void	replace_free_variables (T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution , typename VariableContainer >
T	replace_free_variables (const T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
void	replace_propositional_variables (T &x, const Substitution &sigma, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Applies a propositional variable substitution.
template<typename T , typename Substitution >
T	replace_propositional_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Applies a propositional variable substitution.
template<typename T , typename Substitution >
void	replace_propositional_variables (T &result, const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Applies a propositional variable substitution.
template<typename T , typename Substitution >
void	replace_pbes_expressions (T &x, const Substitution &sigma, bool innermost=true, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
template<typename T , typename Substitution >
T	replace_pbes_expressions (const T &x, const Substitution &sigma, bool innermost=true, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
void	replace_variables_capture_avoiding (T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
void	replace_variables_capture_avoiding (T &x, Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution >
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution , typename IdentifierGenerator >
void	replace_variables_capture_avoiding_with_an_identifier_generator (T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Substitution , typename IdentifierGenerator >
T	replace_variables_capture_avoiding_with_an_identifier_generator (const T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T >
void	replace_constants_by_variables (T &x, const data::rewriter &r, data::mutable_indexed_substitution<> &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times.
template<typename T >
T	replace_constants_by_variables (const T &x, const data::rewriter &r, data::mutable_indexed_substitution<> &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times.
pbes_expression	replace_subterm (const pbes_expression &expr, std::size_t x, std::size_t y, const pbes_expression &replacement)
	Replace the subterm at position (x, y) with a given term.
pbes	replace_subterm (const pbes &p, std::size_t x, std::size_t y, const pbes_expression &replacement)
	Replace the subterm at position (x, y) with a given term.
pbes_expression	find_subterm (const pbes &pbesspec, std::size_t x, std::size_t y)
void	resolve_summand_variable_name_clashes (srf_pbes &pbesspec, const data::variable_list &process_parameters)
	Renames summand variables such that there are no name clashes between summand variables and process parameters.
template<typename T , typename Rewriter >
void	rewrite (T &x, Rewriter R, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Rewriter >
T	rewrite (const T &x, Rewriter R, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Rewriter , typename Substitution >
void	rewrite (T &x, Rewriter R, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Rewriter , typename Substitution >
T	rewrite (const T &x, Rewriter R, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T , typename Rewriter >
void	pbes_rewrite (T &x, const Rewriter &R, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
	Rewrites all embedded pbes expressions in an object x.
template<typename T , typename Rewriter >
T	pbes_rewrite (const T &x, const Rewriter &R, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0)
	Rewrites all embedded pbes expressions in an object x.
template<typename T , typename Rewriter , typename Substitution >
void	pbes_rewrite (T &x, const Rewriter &R, Substitution sigma, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
	Rewrites all embedded pbes expressions in an object x, and applies a substitution to variables on the fly.
template<typename T , typename Rewriter , typename Substitution >
T	pbes_rewrite (const T &x, const Rewriter &R, Substitution sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0)
	Rewrites all embedded pbes expressions in an object x, and applies a substitution to variables on the fly.
search_strategy	parse_search_strategy (const std::string &s)
std::string	print_search_strategy (const search_strategy s)
std::istream &	operator>> (std::istream &is, search_strategy &strategy)
std::ostream &	operator<< (std::ostream &os, const search_strategy s)
std::string	description (const search_strategy s)
std::set< data::variable >	significant_variables (const pbes_expression &x)
std::ostream &	operator<< (std::ostream &out, const simple_structure_graph &G)
template<typename T >
bool	is_odd (T t)
template<typename T >
bool	is_even (T t)
template<typename InputIterator1 , typename InputIterator2 >
int	lexicographical_compare_3way (InputIterator1 first1, InputIterator1 last1, InputIterator2 first2, InputIterator2 last2)
bool	is_disjunctive (const pbes_expression &x)
int	maximum_rank (const pbes &b)
std::ostream &	operator<< (std::ostream &out, const progress_measure &pm)
void	inc (std::vector< int > &alpha, int m, const std::vector< int > &beta)
std::ostream &	operator<< (std::ostream &out, const progress_measures_vertex &v)
bool	small_progress_measures (pbes &b)
static std::string	solution_strategy_to_string (const solution_strategy_t s)
static std::ostream &	operator<< (std::ostream &os, const solution_strategy_t s)
static solution_strategy_t	parse_solution_strategy (const std::string &s)
static std::istream &	operator>> (std::istream &is, solution_strategy_t &s)
static std::string	description (const solution_strategy_t s)
std::tuple< std::size_t, std::size_t, vertex_set >	get_minmax_rank (const structure_graph &G)
bool	has_counter_example_information (const pbes &pbesspec)
	Guesses if a pbes has counter example information.
bool	solve_structure_graph (structure_graph &G, bool check_strategy=false)
std::pair< bool, lps::specification >	solve_structure_graph_with_counter_example (structure_graph &G, const lps::specification &lpsspec, const pbes &p, const pbes_equation_index &p_index)
bool	solve_structure_graph_with_counter_example (structure_graph &G, lts::lts_lts_t &ltsspec)
	Solve this pbes_system using a structure graph generating a counter example.
std::ostream &	operator<< (std::ostream &out, const srf_summand &summand)
std::ostream &	operator<< (std::ostream &out, const srf_equation &eqn)
srf_pbes	pbes2srf (const pbes &p)
	Converts a PBES into standard recursive form.
void	stategraph (pbes &p, const pbesstategraph_options &options)
	Apply the stategraph algorithm.
constexpr unsigned int	undefined_vertex ()
template<typename StructureGraph >
std::vector< typename StructureGraph::index_type >	structure_graph_predecessors (const StructureGraph &G, typename StructureGraph::index_type u)
template<typename StructureGraph >
std::vector< typename StructureGraph::index_type >	structure_graph_successors (const StructureGraph &G, typename StructureGraph::index_type u)
std::ostream &	operator<< (std::ostream &out, const structure_graph::decoration_type &decoration)
std::ostream &	operator<< (std::ostream &out, const structure_graph::vertex &u)
template<typename StructureGraph >
std::ostream &	print_structure_graph (std::ostream &out, const StructureGraph &G)
std::ostream &	operator<< (std::ostream &out, const structure_graph &G)
void	pbesrewr (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type)
void	pbesconstelm (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type, bool compute_conditions, bool remove_redundant_equations, bool check_quantifiers)
void	pbesinfo (const std::string &input_filename, const std::string &input_file_message, const utilities::file_format &file_format, bool opt_full)
void	pbesparelm (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format)
void	pbespareqelm (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type, bool ignore_initial_state)
void	pbespp (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, core::print_format_type format, bool use_pfnf_printer)
void	txt2pbes (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, bool normalize)
void	lps2pbes (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, const std::string &formula_filename, bool timed, bool structured, bool unoptimized, bool preprocess_modal_operators, bool generate_counter_example, bool check_only)
void	complps2pbes (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, const std::string &formula_filename)
void	lpsbisim2pbes (const std::string &input_filename1, const std::string &input_filename2, const std::string &output_filename, const utilities::file_format &output_format, bisimulation_type type, bool normalize)
void	pbesabstract (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, const std::string &parameter_selection, bool value_true)
void	pbesabsinthe (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, const std::string &abstraction_file, absinthe_strategy strategy, bool print_used_function_symbols, bool enable_logging)
void	pbesstategraph (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, const pbesstategraph_options &options)
void	pbespor (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, pbespor_options options)
transformation_strategy	parse_transformation_strategy (const std::string &s)
std::string	print_transformation_strategy (const transformation_strategy s)
std::istream &	operator>> (std::istream &is, transformation_strategy &strategy)
std::ostream &	operator<< (std::ostream &os, const transformation_strategy s)
std::string	description (const transformation_strategy s)
pbes_expression	order_quantified_variables (const pbes_expression &x, const data::data_specification &dataspec)
template<typename T >
void	translate_user_notation (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T >
T	translate_user_notation (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0)
pbes	txt2pbes (std::istream &spec_stream, bool normalize=true)
	Parses a PBES specification from an input stream.
pbes	txt2pbes (const std::string &text, bool normalize=true)
	Parses a PBES specification from a string.
void	typecheck_pbes (pbes &pbesspec)
	Type check a parsed mCRL2 pbes specification. Throws an exception if something went wrong.
template<typename VariableContainer >
propositional_variable	typecheck_propositional_variable (const propositional_variable &x, const VariableContainer &variables, const data::data_specification &dataspec=data::data_specification())
	Type check a parsed mCRL2 propositional variable. Throws an exception if something went wrong.
template<typename VariableContainer , typename PropositionalVariableContainer >
pbes_expression	typecheck_pbes_expression (pbes_expression &x, const VariableContainer &variables, const PropositionalVariableContainer &propositional_variables, const data::data_specification &dataspec=data::data_specification())
	Type check a parsed mCRL2 pbes expression. Throws an exception if something went wrong.
void	unify_parameters (pbes &p)
void	unify_parameters (srf_pbes &p, bool reset=true)
static atermpp::aterm_appl	remove_index_impl (const atermpp::aterm_appl &x)
static atermpp::aterm_appl	add_index_impl (const atermpp::aterm_appl &x)
atermpp::aterm_ostream &	operator<< (atermpp::aterm_ostream &stream, const pbes_equation &equation)
atermpp::aterm_istream &	operator>> (atermpp::aterm_istream &stream, pbes_equation &equation)
atermpp::aterm	pbes_marker ()
template<typename Iter >
std::string	boolean_variables2pgsolver (Iter first, Iter last, const variable_map &variables)
	Convert a sequence of Boolean variables to PGSolver format.
static std::string	bes_expression2pgsolver (const pbes_expression &p, const variable_map &variables)
	Convert a BES expression to PGSolver format.
template<typename Iter >
void	bes2pgsolver (Iter first, Iter last, std::ostream &out, bool maxpg)
	Save a sequence of BES equations in to a stream in PGSolver format.
pbespg_solver_type	parse_solver_type (const std::string &s)
std::string	print (const pbespg_solver_type solver_type)
std::string	description (const pbespg_solver_type solver_type)
std::istream &	operator>> (std::istream &is, pbespg_solver_type &t)
std::ostream &	operator<< (std::ostream &os, const pbespg_solver_type t)
std::string	print (StaticGraph::EdgeDirection edge_direction)
bool	pbespgsolve (pbes &p, const pbespgsolve_options &options=pbespgsolve_options())
	Solves a pbes using a parity game solver.
bool	pbespgsolve (pbes &p, utilities::execution_timer &timer, const pbespgsolve_options &options=pbespgsolve_options())
	Solves a pbes using a parity game solver.

Detailed Description

The main namespace for the PBES library.

Typedef Documentation

fixpoint_symbol_list

typedef atermpp::term_list<fixpoint_symbol> mcrl2::pbes_system::fixpoint_symbol_list

\brief list of fixpoint_symbols

Definition at line 78 of file fixpoint_symbol.h.

fixpoint_symbol_vector

typedef std::vector<fixpoint_symbol> mcrl2::pbes_system::fixpoint_symbol_vector

\brief vector of fixpoint_symbols

Definition at line 81 of file fixpoint_symbol.h.

identifier_t

typedef unsigned long long mcrl2::pbes_system::identifier_t

Definition at line 32 of file pg_parse.h.

owner_t

typedef bool mcrl2::pbes_system::owner_t

Definition at line 35 of file pg_parse.h.

pbes_equation_list

typedef atermpp::term_list<pbes_equation> mcrl2::pbes_system::pbes_equation_list

\brief list of pbes_equations

Definition at line 140 of file pbes_equation.h.

pbes_equation_vector

typedef std::vector<pbes_equation> mcrl2::pbes_system::pbes_equation_vector

\brief vector of pbes_equations

Definition at line 143 of file pbes_equation.h.

pbes_expression_list

typedef atermpp::term_list<pbes_expression> mcrl2::pbes_system::pbes_expression_list

\brief list of pbes_expressions

Definition at line 66 of file pbes_expression.h.

pbes_expression_vector

typedef std::vector<pbes_expression> mcrl2::pbes_system::pbes_expression_vector

\brief vector of pbes_expressions

Definition at line 69 of file pbes_expression.h.

pbesinst_index_map

typedef std::map<core::identifier_string, std::vector<std::size_t> > mcrl2::pbes_system::pbesinst_index_map

Data structure for storing the indices of the variables that should be expanded by the finite pbesinst algorithm.

Definition at line 30 of file pbesinst_finite_algorithm.h.

pbesinst_variable_map

typedef std::map<core::identifier_string, std::vector<data::variable> > mcrl2::pbes_system::pbesinst_variable_map

Data structure for storing the variables that should be expanded by the finite pbesinst algorithm.

Definition at line 33 of file pbesinst_finite_algorithm.h.

priority_t

typedef unsigned short mcrl2::pbes_system::priority_t

Definition at line 33 of file pg_parse.h.

propositional_variable_instantiation_list

typedef atermpp::term_list<propositional_variable_instantiation> mcrl2::pbes_system::propositional_variable_instantiation_list

\brief list of propositional_variable_instantiations

Definition at line 189 of file pbes_expression.h.

propositional_variable_instantiation_vector

typedef std::vector<propositional_variable_instantiation> mcrl2::pbes_system::propositional_variable_instantiation_vector

\brief vector of propositional_variable_instantiations

Definition at line 192 of file pbes_expression.h.

propositional_variable_list

typedef atermpp::term_list<propositional_variable> mcrl2::pbes_system::propositional_variable_list

\brief list of propositional_variables

Definition at line 89 of file propositional_variable.h.

propositional_variable_vector

typedef std::vector<propositional_variable> mcrl2::pbes_system::propositional_variable_vector

\brief vector of propositional_variables

Definition at line 92 of file propositional_variable.h.

summand_set

typedef boost::dynamic_bitset mcrl2::pbes_system::summand_set

Definition at line 54 of file partial_order_reduction.h.

variable_map

typedef std::map<core::identifier_string, std::size_t> mcrl2::pbes_system::variable_map

Definition at line 22 of file pgsolver.cpp.

Enumeration Type Documentation

absinthe_strategy

enum mcrl2::pbes_system::absinthe_strategy

The approximation strategies of the absinthe tool.

Enumerator
absinthe_over
absinthe_under

Definition at line 23 of file absinthe_strategy.h.

bisimulation_type

enum mcrl2::pbes_system::bisimulation_type

An enumerated type for the available bisimulation types.

Enumerator
strong_bisim
weak_bisim
branching_bisim
branching_sim

Definition at line 23 of file bisimulation_type.h.

pbes_rewriter_type

enum mcrl2::pbes_system::pbes_rewriter_type

An enumerated type for the available pbes rewriters.

Enumerator
simplify
quantifier_all
quantifier_finite
quantifier_inside
quantifier_one_point
prover
pfnf
ppg
bqnf_quantifier

Definition at line 23 of file pbes_rewriter_type.h.

pbesinst_strategy

enum mcrl2::pbes_system::pbesinst_strategy

pbesinst transformation strategies

Enumerator
pbesinst_lazy_strategy
pbesinst_alternative_lazy_strategy
pbesinst_finite_strategy

Definition at line 23 of file pbesinst_strategy.h.

pbespg_solver_type

enum mcrl2::pbes_system::pbespg_solver_type

Enumerator
spm_solver
alternative_spm_solver
recursive_solver
priority_promotion

Definition at line 28 of file pbespgsolve.h.

remove_level

enum mcrl2::pbes_system::remove_level

BES variable remove level when generating a BES from a PBES.

Enumerator
none
some
all

Definition at line 25 of file remove_level.h.

search_strategy

enum mcrl2::pbes_system::search_strategy

Search strategy when generating a BES from a PBES.

Enumerator
breadth_first
depth_first
breadth_first_short
depth_first_short

Definition at line 25 of file search_strategy.h.

solution_strategy_t

enum mcrl2::pbes_system::solution_strategy_t

Enumerator
gauss
small_progr_measures

Definition at line 24 of file solution_strategy.h.

transformation_strategy

enum mcrl2::pbes_system::transformation_strategy

Strategies for the generation of a BES from a PBES.

Enumerator
lazy
optimize
on_the_fly
on_the_fly_with_fixed_points

Definition at line 25 of file transformation_strategy.h.

tribool

enum mcrl2::pbes_system::tribool

Enumerator
no
maybe
yes

Definition at line 199 of file partial_order_reduction.h.

Function Documentation

add_index_impl()

static atermpp::aterm_appl mcrl2::pbes_system::add_index_impl ( const atermpp::aterm_appl &  x )

static

Definition at line 186 of file io.cpp.

alternative_lazy_algorithm_test()

bool mcrl2::pbes_system::alternative_lazy_algorithm_test ( pbes &  pbes_spec, const bool  expected_outcome, const transformation_strategy  trans_strat, const search_strategy  search_strat, const data::rewriter::strategy  rewrite_strategy  )

inline

Definition at line 61 of file pbes_solver_test.h.

anonymize()

void mcrl2::pbes_system::anonymize ( pbes &  pbesspec )

inline

Definition at line 81 of file anonymize.h.

attr_default()

template<typename StructureGraph >

vertex_set mcrl2::pbes_system::attr_default	(	const StructureGraph &	G,
		vertex_set	A,
		std::size_t	alpha
	)

Definition at line 165 of file pbessolve_attractors.h.

attr_default_generic()

template<typename StructureGraph , typename Strategy >

vertex_set mcrl2::pbes_system::attr_default_generic	(	const StructureGraph &	G,
		vertex_set	A,
		std::size_t	alpha,
		Strategy	tau
	)

Definition at line 140 of file pbessolve_attractors.h.

attr_default_no_strategy()

template<typename StructureGraph >

vertex_set mcrl2::pbes_system::attr_default_no_strategy	(	const StructureGraph &	G,
		vertex_set	A,
		std::size_t	alpha
	)

Definition at line 172 of file pbessolve_attractors.h.

attr_default_with_tau()

template<typename StructureGraph >

vertex_set mcrl2::pbes_system::attr_default_with_tau	(	const StructureGraph &	G,
		vertex_set	A,
		std::size_t	alpha,
		std::array< strategy_vector, 2 > &	tau
	)

Definition at line 182 of file pbessolve_attractors.h.

bes2pgsolver()

template<typename Iter >

void mcrl2::pbes_system::bes2pgsolver	(	Iter	first,
		Iter	last,
		std::ostream &	out,
		bool	maxpg
	)

Save a sequence of BES equations in to a stream in PGSolver format.

Definition at line 83 of file pgsolver.cpp.

bes_expression2pgsolver()

static std::string mcrl2::pbes_system::bes_expression2pgsolver ( const pbes_expression &  p, const variable_map &  variables  )

static

Convert a BES expression to PGSolver format.

Definition at line 47 of file pgsolver.cpp.

boolean_variables2pgsolver()

template<typename Iter >

std::string mcrl2::pbes_system::boolean_variables2pgsolver	(	Iter	first,
		Iter	last,
		const variable_map &	variables
	)

Convert a sequence of Boolean variables to PGSolver format.

Definition at line 28 of file pgsolver.cpp.

branching_bisimulation()

pbes mcrl2::pbes_system::branching_bisimulation ( const lps::specification &  model, const lps::specification &  spec  )

inline

Returns a pbes that expresses branching bisimulation between two specifications.

Parameters

model	A linear process specification
spec	A linear process specification

Returns

A pbes that expresses branching bisimulation between the two specifications.

Definition at line 512 of file bisimulation.h.

branching_simulation_equivalence()

pbes mcrl2::pbes_system::branching_simulation_equivalence ( const lps::specification &  model, const lps::specification &  spec  )

inline

Returns a pbes that expresses branching simulation equivalence between two specifications.

Parameters

model	A linear process specification
spec	A linear process specification

Returns

A pbes that expresses branching simulation equivalence between the two specifications.

Definition at line 883 of file bisimulation.h.

check_whether_argument_is_a_well_formed_bes()

void mcrl2::pbes_system::check_whether_argument_is_a_well_formed_bes

(

const pbes_expression &

x

)

This function checks whether x is a well formed bes expression, without quantifiers and.

Parameters

x	a pbes expression to be checked.

Definition at line 56 of file check_well_formed_bes.h.

complement()

pbes_expression mcrl2::pbes_system::complement ( const pbes_expression &  x )

inline

Returns the complement of a pbes expression.

Parameters

x	A PBES expression

Returns

The expression obtained by pushing the negations in the pbes expression as far as possible inwards towards a data expression.

Definition at line 89 of file complement.h.

complete_data_specification()

void mcrl2::pbes_system::complete_data_specification ( pbes &  p )

inline

Adds all sorts that appear in the PBES p to the data specification of p.

Parameters

p

a PBES.

Definition at line 314 of file pbes.h.

complps2pbes() [1/2]

pbes_system::pbes mcrl2::pbes_system::complps2pbes ( const process::process_specification &  procspec, const state_formulas::state_formula &    )

inline

Definition at line 25 of file complps2pbes.h.

complps2pbes() [2/2]

void mcrl2::pbes_system::complps2pbes	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const utilities::file_format &	output_format,
		const std::string &	formula_filename
	)

Definition at line 24 of file complps2pbes.h.

constelm()

void mcrl2::pbes_system::constelm ( pbes &  p, data::rewrite_strategy  rewrite_strategy, pbes_rewriter_type  rewriter_type, bool  compute_conditions = false, bool  remove_redundant_equations = true, bool  check_quantifiers = true  )

inline

Apply the constelm algorithm.

Parameters

p	A PBES to which the algorithm is applied
rewrite_strategy	A data rewrite strategy
rewriter_type	A PBES rewriter type
compute_conditions	If true, conditions for the edges of the dependency graph are used N.B. Very inefficient!
remove_redundant_equations	If true, unreachable equations will be removed.

Definition at line 994 of file constelm.h.

description() [1/9]

std::string mcrl2::pbes_system::description ( const absinthe_strategy  strategy )

inline

Prints an absinthe strategy.

Definition at line 86 of file absinthe_strategy.h.

description() [2/9]

std::string mcrl2::pbes_system::description ( const bisimulation_type  t )

inline

Returns a description of a bisimulation type.

Definition at line 63 of file bisimulation_type.h.

description() [3/9]

std::string mcrl2::pbes_system::description ( const pbes_rewriter_type  type )

inline

Returns a description of a pbes rewriter.

Definition at line 110 of file pbes_rewriter_type.h.

description() [4/9]

std::string mcrl2::pbes_system::description ( const pbesinst_strategy  strategy )

inline

Returns a string representation of a pbesinst transformation strategy.

Definition at line 96 of file pbesinst_strategy.h.

description() [5/9]

std::string mcrl2::pbes_system::description ( const pbespg_solver_type  solver_type )

inline

Definition at line 74 of file pbespgsolve.h.

description() [6/9]

std::string mcrl2::pbes_system::description ( const remove_level  s )

inline

Definition at line 79 of file remove_level.h.

description() [7/9]

std::string mcrl2::pbes_system::description ( const search_strategy  s )

inline

Definition at line 80 of file search_strategy.h.

description() [8/9]

static std::string mcrl2::pbes_system::description ( const solution_strategy_t  s )

static

Definition at line 82 of file solution_strategy.h.

description() [9/9]

std::string mcrl2::pbes_system::description ( const transformation_strategy  s )

inline

Definition at line 95 of file transformation_strategy.h.

eqelm()

void mcrl2::pbes_system::eqelm ( pbes &  p, data::rewrite_strategy  rewrite_strategy, pbes_rewriter_type  rewriter_type, bool  ignore_initial_state = false  )

inline

Apply the eqelm algorithm.

Parameters

p	A PBES to which the algorithm is applied.
rewrite_strategy	A data rewrite strategy.
rewriter_type	A PBES rewriter type.
ignore_initial_state	If true, the initial state will be ignored.

Definition at line 321 of file eqelm.h.

exclusive_predecessors()

template<typename StructureGraph >

deque_vertex_set mcrl2::pbes_system::exclusive_predecessors	(	const StructureGraph &	G,
		const vertex_set &	A
	)

Definition at line 104 of file pbessolve_attractors.h.

extract_minimal_structure_graph() [1/3]

template<typename StructureGraph >

std::set< structure_graph::index_type > mcrl2::pbes_system::extract_minimal_structure_graph	(	StructureGraph &	G,
		typename StructureGraph::index_type	init,
		bool	is_disjunctive
	)

Definition at line 549 of file pbessolve_vertex_set.h.

extract_minimal_structure_graph() [2/3]

template<typename StructureGraph >

std::set< structure_graph::index_type > mcrl2::pbes_system::extract_minimal_structure_graph	(	StructureGraph &	G,
		typename StructureGraph::index_type	init,
		const vertex_set &	S0,
		const vertex_set &	S1
	)

Definition at line 450 of file pbessolve_vertex_set.h.

extract_minimal_structure_graph() [3/3]

template<typename StructureGraph >

std::set< structure_graph::index_type > mcrl2::pbes_system::extract_minimal_structure_graph	(	StructureGraph &	G,
		typename StructureGraph::index_type	init,
		const vertex_set &	S0,
		const vertex_set &	S1,
		const strategy_vector &	tau0,
		const strategy_vector &	tau1
	)

Definition at line 491 of file pbessolve_vertex_set.h.

false_()

const pbes_expression & mcrl2::pbes_system::false_ ( )

inline

Returns

Returns the value false

Definition at line 697 of file pbes_expression.h.

find_all_variables() [1/3]

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

(

const pbes_system::pbes &

x

)

Definition at line 53 of file pbes.cpp.

find_all_variables() [2/3]

template<typename T >

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

(

const T &

x

)

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

Definition at line 75 of file find.h.

find_all_variables() [3/3]

template<typename T , typename OutputIterator >

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

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

Definition at line 66 of file find.h.

find_equalities()

std::map< data::variable, std::set< data::data_expression > > mcrl2::pbes_system::find_equalities ( const pbes_expression &  x )

inline

Definition at line 104 of file find_equalities.h.

find_free_variables() [1/5]

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

(

const pbes_system::pbes &

x

)

Definition at line 54 of file pbes.cpp.

find_free_variables() [2/5]

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

(

const pbes_system::pbes_equation &

x

)

Definition at line 56 of file pbes.cpp.

find_free_variables() [3/5]

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

(

const pbes_system::pbes_expression &

x

)

Definition at line 55 of file pbes.cpp.

find_free_variables() [4/5]

template<typename T >

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

(

const T &

x

)

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

Definition at line 107 of file find.h.

find_free_variables() [5/5]

template<typename T , typename OutputIterator >

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

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

Definition at line 87 of file find.h.

find_free_variables_with_bound() [1/2]

template<typename T , typename OutputIterator , typename VariableContainer >

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

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

Definition at line 98 of file find.h.

find_free_variables_with_bound() [2/2]

template<typename T , typename VariableContainer >

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

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

Definition at line 119 of file find.h.

find_function_symbols() [1/3]

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

(

const pbes_system::pbes &

x

)

Definition at line 57 of file pbes.cpp.

find_function_symbols() [2/3]

template<typename T >

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

(

const T &

x

)

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

Definition at line 182 of file find.h.

find_function_symbols() [3/3]

template<typename T , typename OutputIterator >

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

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

Definition at line 173 of file find.h.

find_identifiers() [1/3]

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

(

const pbes_system::pbes_expression &

x

)

Definition at line 59 of file pbes.cpp.

find_identifiers() [2/3]

template<typename T >

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

(

const T &

x

)

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

Definition at line 140 of file find.h.

find_identifiers() [3/3]

template<typename T , typename OutputIterator >

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

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

Definition at line 131 of file find.h.

find_inequalities()

std::map< data::variable, std::set< data::data_expression > > mcrl2::pbes_system::find_inequalities ( const pbes_expression &  x )

inline

Definition at line 114 of file find_equalities.h.

find_propositional_variable_instantiations() [1/3]

std::set< pbes_system::propositional_variable_instantiation > mcrl2::pbes_system::find_propositional_variable_instantiations

(

const pbes_system::pbes_expression &

x

)

Definition at line 58 of file pbes.cpp.

find_propositional_variable_instantiations() [2/3]

template<typename Container >

std::set< propositional_variable_instantiation > mcrl2::pbes_system::find_propositional_variable_instantiations

(

Container const &

container

)

Returns all data variables that occur in a range of expressions.

Parameters

[in]

container

a container with expressions

Returns

All data variables that occur in the term t

Definition at line 205 of file find.h.

find_propositional_variable_instantiations() [3/3]

template<typename Container , typename OutputIterator >

void mcrl2::pbes_system::find_propositional_variable_instantiations	(	Container const &	container,
		OutputIterator	o
	)

Returns all data variables that occur in a range of expressions.

Parameters

[in]	container	a container with expressions
[in,out]	o	an output iterator to which all data variables occurring in t are added.

Returns

All data variables that occur in the term t

Definition at line 196 of file find.h.

find_sort_expressions() [1/3]

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

(

const pbes_system::pbes &

x

)

Definition at line 52 of file pbes.cpp.

find_sort_expressions() [2/3]

template<typename T >

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

(

const T &

x

)

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

Definition at line 161 of file find.h.

find_sort_expressions() [3/3]

template<typename T , typename OutputIterator >

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

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

Definition at line 152 of file find.h.

find_subterm()

pbes_expression mcrl2::pbes_system::find_subterm ( const pbes &  pbesspec, std::size_t  x, std::size_t  y  )

inline

Definition at line 192 of file replace_subterm.h.

find_successor_in()

template<typename StructureGraph , typename VertexSet >

structure_graph::index_type mcrl2::pbes_system::find_successor_in	(	const StructureGraph &	G,
		structure_graph::index_type	u,
		const VertexSet &	A
	)

Definition at line 339 of file pbessolve_vertex_set.h.

formula()

pbes_expression mcrl2::pbes_system::formula ( std::set< identifier_t > const &  v, const owner_t  owner, const std::string &  prefix = "X"  )

inline

Definition at line 54 of file pg_parse.h.

free_variables()

data::variable_list mcrl2::pbes_system::free_variables ( const pbes_expression &  x )

inline

Definition at line 1067 of file pbes_expression.h.

gauss_elimination()

int mcrl2::pbes_system::gauss_elimination ( pbes &  p )

inline

Solves a PBES equation system using Gauss elimination.

Precondition

The pbes p is a bes.

Parameters

p

A pbes

Returns

0 if the solution is false, 1 if the solution is true, 2 if the solution is unknown

Definition at line 122 of file pbes_gauss_elimination.h.

get_minmax_rank()

std::tuple< std::size_t, std::size_t, vertex_set > mcrl2::pbes_system::get_minmax_rank ( const structure_graph &  G )

inline

Definition at line 26 of file solve_structure_graph.h.

guess_format()

const utilities::file_format mcrl2::pbes_system::guess_format ( const std::string &  filename )

inline

Definition at line 51 of file io.h.

has_counter_example_information()

bool mcrl2::pbes_system::has_counter_example_information ( const pbes &  pbesspec )

inline

Guesses if a pbes has counter example information.

Definition at line 59 of file solve_structure_graph.h.

has_propositional_variables()

bool mcrl2::pbes_system::has_propositional_variables

(

const pbes_expression &

x

)

inc()

void mcrl2::pbes_system::inc ( std::vector< int > &  alpha, int  m, const std::vector< int > &  beta  )

inline

Definition at line 126 of file small_progress_measures.h.

includes_successors()

template<typename StructureGraph , typename VertexSet >

bool mcrl2::pbes_system::includes_successors	(	const StructureGraph &	G,
		typename StructureGraph::index_type	u,
		const VertexSet &	A
	)

Definition at line 90 of file pbessolve_attractors.h.

insert_predecessors()

template<typename StructureGraph >

void mcrl2::pbes_system::insert_predecessors	(	const StructureGraph &	G,
		structure_graph::index_type	u,
		const vertex_set &	A,
		deque_vertex_set &	todo
	)

Definition at line 123 of file pbessolve_attractors.h.

is_and()

bool mcrl2::pbes_system::is_and ( const atermpp::aterm_appl &  x )

inline

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

Definition at line 345 of file pbes_expression.h.

is_bes()

template<typename T >

bool mcrl2::pbes_system::is_bes

(

const T &

x

)

Returns true if a PBES object is in BES form.

Parameters

x	a PBES object

Definition at line 76 of file is_bes.h.

is_constant()

bool mcrl2::pbes_system::is_constant ( const pbes_expression &  x )

inline

Definition at line 1047 of file pbes_expression.h.

is_data()

bool mcrl2::pbes_system::is_data ( const pbes_expression &  t )

inline

Returns true if the term t is a data expression.

Parameters

t	A PBES expression

Returns

True if the term t is a data expression

Definition at line 795 of file pbes_expression.h.

is_disjunctive()

bool mcrl2::pbes_system::is_disjunctive ( const pbes_expression &  x )

inline

Definition at line 70 of file small_progress_measures.h.

is_even()

template<typename T >

bool mcrl2::pbes_system::is_even

(

T

t

)

Definition at line 37 of file small_progress_measures.h.

is_exists()

bool mcrl2::pbes_system::is_exists ( const atermpp::aterm_appl &  x )

inline

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

Definition at line 649 of file pbes_expression.h.

is_false()

bool mcrl2::pbes_system::is_false ( const pbes_expression &  t )

inline

Test for the value false.

Parameters

t	A PBES expression

Returns

True if it is the value false

Definition at line 715 of file pbes_expression.h.

is_forall()

bool mcrl2::pbes_system::is_forall ( const atermpp::aterm_appl &  x )

inline

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

Definition at line 573 of file pbes_expression.h.

is_imp()

bool mcrl2::pbes_system::is_imp ( const atermpp::aterm_appl &  x )

inline

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

Definition at line 497 of file pbes_expression.h.

is_left_associative() [1/4]

bool mcrl2::pbes_system::is_left_associative ( const and_ &  )

inline

Definition at line 42 of file print.h.

is_left_associative() [2/4]

bool mcrl2::pbes_system::is_left_associative ( const imp &  )

inline

Definition at line 40 of file print.h.

is_left_associative() [3/4]

bool mcrl2::pbes_system::is_left_associative ( const or_ &  )

inline

Definition at line 41 of file print.h.

is_left_associative() [4/4]

bool mcrl2::pbes_system::is_left_associative ( const pbes_expression &  x )

inline

Definition at line 43 of file print.h.

is_monotonous() [1/3]

bool mcrl2::pbes_system::is_monotonous ( const pbes &  p )

inline

Returns true if the pbes is monotonous.

Definition at line 142 of file is_monotonous.h.

is_monotonous() [2/3]

bool mcrl2::pbes_system::is_monotonous ( const pbes_equation &  e )

inline

Returns true if the pbes equation is monotonous.

Definition at line 135 of file is_monotonous.h.

is_monotonous() [3/3]

bool mcrl2::pbes_system::is_monotonous ( pbes_expression  f )

inline

Returns true if the pbes expression is monotonous.

Parameters

f	A pbes expression.

Returns

True if the pbes expression is monotonous.

Definition at line 27 of file is_monotonous.h.

is_non_simple_conjunct()

bool mcrl2::pbes_system::is_non_simple_conjunct ( const pbes_expression &  t )

inline

Test for a conjunction.

Parameters

t	A PBES expression

Returns

True if it is a conjunction and not a simple expression

Definition at line 122 of file pbes_functions.h.

is_non_simple_disjunct()

bool mcrl2::pbes_system::is_non_simple_disjunct ( const pbes_expression &  t )

inline

Test for a disjunction.

Parameters

t	A PBES expression

Returns

True if it is a disjunction and not a simple expression

Definition at line 114 of file pbes_functions.h.

is_normalized()

template<typename T >

bool mcrl2::pbes_system::is_normalized

(

const T &

x

)

Checks if a pbes expression is normalized.

Parameters

x	A PBES expression

Returns

True if the pbes expression is normalized

Definition at line 166 of file normalize.h.

is_not()

bool mcrl2::pbes_system::is_not ( const atermpp::aterm_appl &  x )

inline

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

Definition at line 269 of file pbes_expression.h.

is_odd()

template<typename T >

bool mcrl2::pbes_system::is_odd

(

T

t

)

Definition at line 31 of file small_progress_measures.h.

is_or()

bool mcrl2::pbes_system::is_or ( const atermpp::aterm_appl &  x )

inline

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

Definition at line 421 of file pbes_expression.h.

is_pbes_and()

bool mcrl2::pbes_system::is_pbes_and ( const pbes_expression &  t )

inline

Returns true if the term t is an and expression.

Parameters

t	A PBES expression

Returns

True if the term t is an and expression

Definition at line 731 of file pbes_expression.h.

is_pbes_exists()

bool mcrl2::pbes_system::is_pbes_exists ( const pbes_expression &  t )

inline

Returns true if the term t is an existential quantification.

Parameters

t	A PBES expression

Returns

True if the term t is an existential quantification

Definition at line 763 of file pbes_expression.h.

is_pbes_expression()

bool mcrl2::pbes_system::is_pbes_expression ( const atermpp::aterm_appl &  x )

inline

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

Definition at line 84 of file pbes_expression.h.

is_pbes_file_format()

bool mcrl2::pbes_system::is_pbes_file_format ( const utilities::file_format &  format )

inline

Definition at line 29 of file io.h.

is_pbes_forall()

bool mcrl2::pbes_system::is_pbes_forall ( const pbes_expression &  t )

inline

Returns true if the term t is a universal quantification.

Parameters

t	A PBES expression

Returns

True if the term t is a universal quantification

Definition at line 755 of file pbes_expression.h.

is_pbes_imp()

bool mcrl2::pbes_system::is_pbes_imp ( const pbes_expression &  t )

inline

Returns true if the term t is an imp expression.

Parameters

t	A PBES expression

Returns

True if the term t is an imp expression

Definition at line 747 of file pbes_expression.h.

is_pbes_not()

bool mcrl2::pbes_system::is_pbes_not ( const pbes_expression &  t )

inline

Returns true if the term t is a not expression.

Parameters

t	A PBES expression

Returns

True if the term t is a not expression

Definition at line 723 of file pbes_expression.h.

is_pbes_or()

bool mcrl2::pbes_system::is_pbes_or ( const pbes_expression &  t )

inline

Returns true if the term t is an or expression.

Parameters

t	A PBES expression

Returns

True if the term t is an or expression

Definition at line 739 of file pbes_expression.h.

is_propositional_variable()

bool mcrl2::pbes_system::is_propositional_variable ( const atermpp::aterm_appl &  x )

inline

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

Definition at line 98 of file propositional_variable.h.

is_propositional_variable_instantiation()

bool mcrl2::pbes_system::is_propositional_variable_instantiation ( const atermpp::aterm_appl &  x )

inline

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

Definition at line 198 of file pbes_expression.h.

is_right_associative() [1/4]

bool mcrl2::pbes_system::is_right_associative ( const and_ &  )

inline

Definition at line 53 of file print.h.

is_right_associative() [2/4]

bool mcrl2::pbes_system::is_right_associative ( const imp &  )

inline

Definition at line 51 of file print.h.

is_right_associative() [3/4]

bool mcrl2::pbes_system::is_right_associative ( const or_ &  )

inline

Definition at line 52 of file print.h.

is_right_associative() [4/4]

bool mcrl2::pbes_system::is_right_associative ( const pbes_expression &  x )

inline

Definition at line 54 of file print.h.

is_simple_expression()

template<typename T >

bool mcrl2::pbes_system::is_simple_expression

(

const T &

x

)

Determines if an expression is a simple expression. An expression is simple if it is free of propositional variables.

Parameters

x	a PBES object

Returns

true if x is a simple expression.

Definition at line 104 of file pbes_functions.h.

is_subset_of()

bool mcrl2::pbes_system::is_subset_of ( const vertex_set &  V, const vertex_set &  W  )

inline

Definition at line 332 of file pbessolve_vertex_set.h.

is_true()

bool mcrl2::pbes_system::is_true ( const pbes_expression &  t )

inline

Test for the value true.

Parameters

t	A PBES expression

Returns

True if it is the value true

Definition at line 707 of file pbes_expression.h.

is_universal_and()

bool mcrl2::pbes_system::is_universal_and ( const pbes_expression &  t )

inline

Test for a conjunction.

Parameters

t	A PBES expression or a data expression

Returns

True if it is a conjunction

Definition at line 779 of file pbes_expression.h.

is_universal_not()

bool mcrl2::pbes_system::is_universal_not ( const pbes_expression &  t )

inline

Test for a conjunction.

Parameters

t	A PBES expression or a data expression

Returns

True if it is a conjunction

Definition at line 771 of file pbes_expression.h.

is_universal_or()

bool mcrl2::pbes_system::is_universal_or ( const pbes_expression &  t )

inline

Test for a disjunction.

Parameters

t	A PBES expression or a data expression

Returns

True if it is a disjunction

Definition at line 787 of file pbes_expression.h.

is_well_typed()

bool mcrl2::pbes_system::is_well_typed

(

const pbes_equation &

eqn

)

Definition at line 77 of file pbes.cpp.

is_well_typed_equation()

bool mcrl2::pbes_system::is_well_typed_equation	(	const pbes_equation &	eqn,
		const std::set< data::sort_expression > &	declared_sorts,
		const std::set< data::variable > &	declared_global_variables,
		const data::data_specification &	data_spec
	)

Definition at line 82 of file pbes.cpp.

is_well_typed_pbes()

bool mcrl2::pbes_system::is_well_typed_pbes	(	const std::set< data::sort_expression > &	declared_sorts,
		const std::set< data::variable > &	declared_global_variables,
		const std::set< data::variable > &	occurring_global_variables,
		const std::set< propositional_variable > &	declared_variables,
		const std::set< propositional_variable_instantiation > &	occ,
		const propositional_variable_instantiation &	init,
		const data::data_specification &	data_spec
	)

Definition at line 91 of file pbes.cpp.

join_and()

template<typename FwdIt >

pbes_expression mcrl2::pbes_system::join_and	(	FwdIt	first,
		FwdIt	last
	)

Returns and applied to the sequence of pbes expressions [first, last)

Parameters

first	Start of a sequence of pbes expressions
last	End of a sequence of of pbes expressions

Returns

And applied to the sequence of pbes expressions [first, last)

Definition at line 36 of file join.h.

join_or()

template<typename FwdIt >

pbes_expression mcrl2::pbes_system::join_or	(	FwdIt	first,
		FwdIt	last
	)

Returns or applied to the sequence of pbes expressions [first, last)

Parameters

first	Start of a sequence of pbes expressions
last	End of a sequence of of pbes expressions

Returns

Or applied to the sequence of pbes expressions [first, last)

Definition at line 26 of file join.h.

lexicographical_compare_3way()

template<typename InputIterator1 , typename InputIterator2 >

int mcrl2::pbes_system::lexicographical_compare_3way	(	InputIterator1	first1,
		InputIterator1	last1,
		InputIterator2	first2,
		InputIterator2	last2
	)

Definition at line 43 of file small_progress_measures.h.

load_pbes() [1/2]

void mcrl2::pbes_system::load_pbes	(	pbes &	pbes,
		const std::string &	filename,
		utilities::file_format	format = utilities::file_format()
	)

Load pbes from file.

Parameters

pbes	The pbes to which the result is loaded.
filename	The file from which to load the PBES.
format	The format in which the PBES is stored in the file.

The format of the file in infilename is guessed if format is not given or if it is equal to utilities::file_format().

Definition at line 148 of file io.cpp.

load_pbes() [2/2]

void mcrl2::pbes_system::load_pbes	(	pbes &	pbes,
		std::istream &	stream,
		utilities::file_format	format,
		const std::string &	source = ""
	)

Load a PBES from file.

Parameters

pbes	The PBES to which the result is loaded.
stream	The stream from which to load the PBES.
format	The format that should be assumed for the file in infilename. If unspecified, or pbes_file_unknown is specified, then a default format is chosen.
source	The source from which the stream originates. Used for error messages.

Definition at line 82 of file io.cpp.

log_vertex_set()

template<typename StructureGraph >

void mcrl2::pbes_system::log_vertex_set	(	const StructureGraph &	G,
		const vertex_set &	V,
		const std::string &	name
	)

Definition at line 353 of file pbessolve_vertex_set.h.

lps2pbes() [1/4]

pbes mcrl2::pbes_system::lps2pbes ( const lps::specification &  lpsspec, const state_formulas::state_formula &  formula, bool  timed = false, bool  structured = false, bool  unoptimized = false, bool  preprocess_modal_operators = false, bool  generate_counter_example = false, bool  check_only = false  )

inline

Translates a linear process specification and a state formula to a PBES. If the solution of the PBES is true, the formula holds for the specification.

Parameters

lpsspec	A linear process specification.
formula	A modal formula.
timed	determines whether the timed or untimed variant of the algorithm is chosen.
structured	use the 'structured' approach of generating equations.
unoptimized	if true, the resulting PBES is not simplified, if false (default), the PBES is simplified.
preprocess_modal_operators	A boolean indicating that the modal operators can be preprocessed to obtain a more compact PBES.
generate_counter_example	A boolean indicating that a counter example must be generated.

Returns

The resulting pbes.

Definition at line 158 of file lps2pbes.h.

lps2pbes() [2/4]

pbes mcrl2::pbes_system::lps2pbes ( const lps::specification &  lpsspec, const state_formulas::state_formula_specification &  formspec, bool  timed = false, bool  structured = false, bool  unoptimized = false, bool  preprocess_modal_operators = false, bool  generate_counter_example = false, bool  check_only = false  )

inline

Translates a linear process specification and a state formula to a PBES. If the solution of the PBES is true, the formula holds for the specification.

Parameters

lpsspec	A linear process specification.
formspec	A modal formula specification.
timed	determines whether the timed or untimed variant of the algorithm is chosen.
structured	use the 'structured' approach of generating equations.
unoptimized	if true, the resulting PBES is not simplified, if false (default), the PBES is simplified.
preprocess_modal_operators	A boolean indicating that the modal operators can be preprocessed to obtain a more compact PBES.
generate_counter_example	A boolean indicating that a counter example must be generated.
check_only	If check_only is true, only the formula will be checked, but no PBES is generated

Returns

The resulting pbes.

Definition at line 207 of file lps2pbes.h.

lps2pbes() [3/4]

void mcrl2::pbes_system::lps2pbes	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const utilities::file_format &	output_format,
		const std::string &	formula_filename,
		bool	timed,
		bool	structured,
		bool	unoptimized,
		bool	preprocess_modal_operators,
		bool	generate_counter_example,
		bool	check_only
	)

Definition at line 42 of file lps2pbes.h.

lps2pbes() [4/4]

pbes mcrl2::pbes_system::lps2pbes ( const std::string &  spec_text, const std::string &  formula_text, bool  timed = false, bool  structured = false, bool  unoptimized = false, bool  preprocess_modal_operators = false, bool  generate_counter_example = false, bool  check_only = false  )

inline

Applies the lps2pbes algorithm.

Parameters

spec_text	A string.
formula_text	A string.
timed	Determines whether the timed or untimed version of the translation algorithm is used.
structured	use the 'structured' approach of generating equations.
unoptimized	if true, the resulting PBES is not simplified, if false (default), the PBES is simplified.
preprocess_modal_operators	A boolean indicating that the modal operators can be preprocessed to obtain a more compact PBES.
generate_counter_example	A boolean indicating that a counter example must be generated.
check_only	If check_only is true, only the formula will be checked, but no PBES is generated

Returns

The result of the algorithm

Definition at line 237 of file lps2pbes.h.

lpsbisim2pbes()

void mcrl2::pbes_system::lpsbisim2pbes	(	const std::string &	input_filename1,
		const std::string &	input_filename2,
		const std::string &	output_filename,
		const utilities::file_format &	output_format,
		bisimulation_type	type,
		bool	normalize
	)

Definition at line 25 of file lpsbisim2pbes.h.

lpsstategraph() [1/2]

void mcrl2::pbes_system::lpsstategraph	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const pbesstategraph_options &	options
	)

Definition at line 218 of file lpsstategraph_algorithm.h.

lpsstategraph() [2/2]

void mcrl2::pbes_system::lpsstategraph ( lps::specification &  lpsspec, const pbesstategraph_options &  options  )

inline

Apply the stategraph algorithm.

Parameters

p	A PBES to which the algorithm is applied.
options	The options for the algorithm.

Definition at line 202 of file lpsstategraph_algorithm.h.

lts2pbes()

pbes mcrl2::pbes_system::lts2pbes ( const lts::lts_lts_t &  l, const state_formulas::state_formula_specification &  formspec, bool  preprocess_modal_operators = false, bool  generate_counter_example = false  )

inline

Translates an LTS and a modal formula into a PBES that represents the corresponding model checking problem.

Parameters

l	A labelled transition system.
formspec	A modal formula specification.
preprocess_modal_operators	A boolean indicating that modal operators must be preprocessed.
generate_counter_example	A boolean indicating that a counter example must be generated.

Definition at line 100 of file lts2pbes.h.

make_and_()

template<class... ARGUMENTS>

void mcrl2::pbes_system::make_and_ ( atermpp::aterm_appl &  t, const ARGUMENTS &...  args  )

inline

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

Parameters

t	The reference into which the new and_ is constructed.

Definition at line 336 of file pbes_expression.h.

make_exists()

template<class... ARGUMENTS>

void mcrl2::pbes_system::make_exists ( atermpp::aterm_appl &  t, const ARGUMENTS &...  args  )

inline

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

Parameters

t	The reference into which the new exists is constructed.

Definition at line 640 of file pbes_expression.h.

make_exists_()

pbes_expression mcrl2::pbes_system::make_exists_ ( const data::variable_list &  l, const pbes_expression &  p  )

inline

Make an existential quantification. It checks for an empty variable list, which is not allowed.

Parameters

l	A sequence of data variables
p	A PBES expression

Returns

The value exists l.p

Definition at line 942 of file pbes_expression.h.

make_forall()

template<class... ARGUMENTS>

void mcrl2::pbes_system::make_forall ( atermpp::aterm_appl &  t, const ARGUMENTS &...  args  )

inline

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

Parameters

t	The reference into which the new forall is constructed.

Definition at line 564 of file pbes_expression.h.

make_forall_()

pbes_expression mcrl2::pbes_system::make_forall_ ( const data::variable_list &  l, const pbes_expression &  p  )

inline

Make a universal quantification. It checks for an empty variable list, which is not allowed.

Parameters

l	A sequence of data variables
p	A PBES expression

Returns

The value forall l.p

Definition at line 927 of file pbes_expression.h.

make_imp()

template<class... ARGUMENTS>

void mcrl2::pbes_system::make_imp ( atermpp::aterm_appl &  t, const ARGUMENTS &...  args  )

inline

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

Parameters

t	The reference into which the new imp is constructed.

Definition at line 488 of file pbes_expression.h.

make_not_()

template<class... ARGUMENTS>

void mcrl2::pbes_system::make_not_ ( atermpp::aterm_appl &  t, const ARGUMENTS &...  args  )

inline

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

Parameters

t	The reference into which the new not_ is constructed.

Definition at line 260 of file pbes_expression.h.

make_or_()

template<class... ARGUMENTS>

void mcrl2::pbes_system::make_or_ ( atermpp::aterm_appl &  t, const ARGUMENTS &...  args  )

inline

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

Parameters

t	The reference into which the new or_ is constructed.

Definition at line 412 of file pbes_expression.h.

make_pbes_equation_solver()

template<typename Rewriter >

pbes_equation_solver< Rewriter > mcrl2::pbes_system::make_pbes_equation_solver

(

const Rewriter &

rewriter

)

Utility function for creating a pbes_equation_solver.

Definition at line 112 of file pbes_gauss_elimination.h.

make_pbesinst_substitution()

void mcrl2::pbes_system::make_pbesinst_substitution ( const data::variable_list &  v, const data::data_expression_list &  e, data::rewriter::substitution_type &  sigma  )

inline

Creates a substitution function for the pbesinst rewriter.

Parameters

v	A sequence of data variables
e	A sequence of data expressions
sigma	The substitution that maps the i-th element of v to the i-th element of e

Definition at line 32 of file pbesinst_algorithm.h.

make_propositional_variable()

template<class... ARGUMENTS>

void mcrl2::pbes_system::make_propositional_variable ( atermpp::aterm_appl &  t, const ARGUMENTS &...  args  )

inline

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

Parameters

t	The reference into which the new propositional_variable is constructed.

Definition at line 83 of file propositional_variable.h.

make_propositional_variable_instantiation()

template<class... ARGUMENTS>

void mcrl2::pbes_system::make_propositional_variable_instantiation ( atermpp::aterm_appl &  t, const ARGUMENTS &...  args  )

inline

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

Parameters

t	The reference into which the new propositional_variable_instantiation is constructed.

Definition at line 183 of file pbes_expression.h.

make_standard_form()

void mcrl2::pbes_system::make_standard_form ( pbes &  eqn, bool  recursive_form = false  )

inline

Transforms a PBES into standard form.

Parameters

eqn	A pbes equation system
recursive_form	Determines whether or not the result will be in standard recursive normal form

Definition at line 305 of file normal_forms.h.

maximum_rank()

int mcrl2::pbes_system::maximum_rank ( const pbes &  b )

inline

Definition at line 76 of file small_progress_measures.h.

normalize() [1/2]

template<typename T >

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

The function normalize brings (embedded) pbes expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.

Parameters

x	an object containing pbes expressions

Definition at line 189 of file normalize.h.

normalize() [2/2]

template<typename T >

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

The function normalize brings (embedded) pbes expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.

Parameters

x	an object containing pbes expressions

Definition at line 177 of file normalize.h.

normalize_sorts() [1/5]

pbes_system::pbes_expression mcrl2::pbes_system::normalize_sorts	(	const pbes_system::pbes_expression &	x,
		const data::sort_specification &	sortspec
	)

Definition at line 49 of file pbes.cpp.

normalize_sorts() [2/5]

template<typename T >

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

Definition at line 34 of file normalize_sorts.h.

normalize_sorts() [3/5]

void mcrl2::pbes_system::normalize_sorts	(	pbes_system::pbes &	x,
		const data::sort_specification &	sortspec
	)

Definition at line 48 of file pbes.cpp.

normalize_sorts() [4/5]

void mcrl2::pbes_system::normalize_sorts	(	pbes_system::pbes_equation_vector &	x,
		const data::sort_specification &	sortspec
	)

Definition at line 47 of file pbes.cpp.

normalize_sorts() [5/5]

template<typename T >

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

Definition at line 25 of file normalize_sorts.h.

operator!=()

bool mcrl2::pbes_system::operator!= ( const pbes_equation &  x, const pbes_equation &  y  )

inline

Definition at line 174 of file pbes_equation.h.

operator&&() [1/2]

static bool mcrl2::pbes_system::operator&& ( const std::function< tribool()> &  a, const std::function< tribool(bool)> &  b  )

inlinestatic

Definition at line 210 of file partial_order_reduction.h.

operator&&() [2/2]

static bool mcrl2::pbes_system::operator&& ( tribool  a, tribool  b  )

inlinestatic

Definition at line 203 of file partial_order_reduction.h.

operator<<() [1/37]

atermpp::aterm_ostream & mcrl2::pbes_system::operator<<	(	atermpp::aterm_ostream &	stream,
		const pbes &	pbes
	)

Writes the pbes to a stream.

Definition at line 234 of file io.cpp.

operator<<() [2/37]

atermpp::aterm_ostream & mcrl2::pbes_system::operator<< ( atermpp::aterm_ostream &  stream, const pbes_equation &  equation  )

inline

Definition at line 206 of file io.cpp.

operator<<() [3/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  os, const absinthe_strategy  strategy  )

inline

Definition at line 78 of file absinthe_strategy.h.

operator<<() [4/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  os, const bisimulation_type  t  )

inline

Definition at line 96 of file bisimulation_type.h.

operator<<() [5/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  os, const pbes_rewriter_type  t  )

inline

Definition at line 157 of file pbes_rewriter_type.h.

operator<<() [6/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  os, const pbesinst_strategy  strategy  )

inline

Definition at line 88 of file pbesinst_strategy.h.

operator<<() [7/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  os, const pbespg_solver_type  t  )

inline

Definition at line 103 of file pbespgsolve.h.

operator<<() [8/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  os, const remove_level  s  )

inline

Definition at line 72 of file remove_level.h.

operator<<() [9/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  os, const search_strategy  s  )

inline

Definition at line 73 of file search_strategy.h.

operator<<() [10/37]

static std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  os, const solution_strategy_t  s  )

static

Definition at line 42 of file solution_strategy.h.

operator<<() [11/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  os, const transformation_strategy  s  )

inline

Definition at line 88 of file transformation_strategy.h.

operator<<() [12/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const and_ &  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 358 of file pbes_expression.h.

operator<<() [13/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const exists &  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 662 of file pbes_expression.h.

operator<<() [14/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const fixpoint_symbol &  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 fixpoint_symbol.h.

operator<<() [15/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const forall &  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 586 of file pbes_expression.h.

operator<<() [16/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const imp &  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 510 of file pbes_expression.h.

operator<<() [17/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const lazy_union &  V  )

inline

Definition at line 326 of file pbessolve_vertex_set.h.

operator<<() [18/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const not_ &  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 282 of file pbes_expression.h.

operator<<() [19/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const or_ &  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 434 of file pbes_expression.h.

operator<<() [20/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const pbes &  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 304 of file pbes.h.

operator<<() [21/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const pbes_equation &  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 153 of file pbes_equation.h.

operator<<() [22/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const pbes_equation_index &  index  )

inline

Definition at line 70 of file pbes_equation_index.h.

operator<<() [23/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const pbes_expression &  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 106 of file pbes_expression.h.

operator<<() [24/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const pbesinst_lazy_todo &  todo  )

inline

Definition at line 168 of file pbesinst_lazy.h.

operator<<() [25/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const pbessolve_options &  options  )

inline

Definition at line 45 of file pbessolve_options.h.

operator<<() [26/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const progress_measure &  pm  )

inline

Definition at line 111 of file small_progress_measures.h.

operator<<() [27/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const progress_measures_vertex &  v  )

inline

Definition at line 196 of file small_progress_measures.h.

operator<<() [28/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const propositional_variable &  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 propositional_variable.h.

operator<<() [29/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const propositional_variable_instantiation &  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 211 of file pbes_expression.h.

operator<<() [30/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const simple_structure_graph &  G  )

inline

Definition at line 105 of file simple_structure_graph.h.

operator<<() [31/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const srf_equation &  eqn  )

inline

Definition at line 196 of file srf_pbes.h.

operator<<() [32/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const srf_summand &  summand  )

inline

Definition at line 113 of file srf_pbes.h.

operator<<() [33/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const strategy_vector &  tau_alpha  )

inline

Definition at line 424 of file pbessolve_vertex_set.h.

operator<<() [34/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const structure_graph &  G  )

inline

Definition at line 329 of file structure_graph.h.

operator<<() [35/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const structure_graph::decoration_type &  decoration  )

inline

Definition at line 275 of file structure_graph.h.

operator<<() [36/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const structure_graph::vertex &  u  )

inline

Definition at line 289 of file structure_graph.h.

operator<<() [37/37]

std::ostream & mcrl2::pbes_system::operator<< ( std::ostream &  out, const vertex_set &  V  )

inline

Definition at line 265 of file pbessolve_vertex_set.h.

operator==() [1/2]

bool mcrl2::pbes_system::operator== ( const pbes &  p1, const pbes &  p2  )

inline

Equality operator on PBESs.

Returns

True if the PBESs have exactly the same internal representation. Note that this is in general not a very useful test.

Definition at line 325 of file pbes.h.

operator==() [2/2]

bool mcrl2::pbes_system::operator== ( const pbes_equation &  x, const pbes_equation &  y  )

inline

Definition at line 166 of file pbes_equation.h.

operator>>() [1/12]

atermpp::aterm_istream & mcrl2::pbes_system::operator>>	(	atermpp::aterm_istream &	stream,
		pbes &	pbes
	)

Reads a pbes from a stream.

Definition at line 247 of file io.cpp.

operator>>() [2/12]

atermpp::aterm_istream & mcrl2::pbes_system::operator>> ( atermpp::aterm_istream &  stream, pbes_equation &  equation  )

inline

Definition at line 214 of file io.cpp.

operator>>() [3/12]

std::istream & mcrl2::pbes_system::operator>> ( std::istream &  from, pbes &  result  )

inline

Reads a PBES from an input stream.

Parameters

from	An input stream
result	A PBES

Returns

The input stream

Definition at line 52 of file parse.h.

operator>>() [4/12]

std::istream & mcrl2::pbes_system::operator>> ( std::istream &  is, absinthe_strategy &  strategy  )

inline

Definition at line 62 of file absinthe_strategy.h.

operator>>() [5/12]

std::istream & mcrl2::pbes_system::operator>> ( std::istream &  is, bisimulation_type &  t  )

inline

Definition at line 80 of file bisimulation_type.h.

operator>>() [6/12]

std::istream & mcrl2::pbes_system::operator>> ( std::istream &  is, pbes_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 141 of file pbes_rewriter_type.h.

operator>>() [7/12]

std::istream & mcrl2::pbes_system::operator>> ( std::istream &  is, pbesinst_strategy &  s  )

inline

Definition at line 53 of file pbesinst_strategy.h.

operator>>() [8/12]

std::istream & mcrl2::pbes_system::operator>> ( std::istream &  is, pbespg_solver_type &  t  )

inline

Definition at line 87 of file pbespgsolve.h.

operator>>() [9/12]

std::istream & mcrl2::pbes_system::operator>> ( std::istream &  is, remove_level &  level  )

inline

Definition at line 56 of file remove_level.h.

operator>>() [10/12]

std::istream & mcrl2::pbes_system::operator>> ( std::istream &  is, search_strategy &  strategy  )

inline

Definition at line 57 of file search_strategy.h.

operator>>() [11/12]

static std::istream & mcrl2::pbes_system::operator>> ( std::istream &  is, solution_strategy_t &  s  )

static

Definition at line 66 of file solution_strategy.h.

operator>>() [12/12]

std::istream & mcrl2::pbes_system::operator>> ( std::istream &  is, transformation_strategy &  strategy  )

inline

Definition at line 72 of file transformation_strategy.h.

optimized_and()

void mcrl2::pbes_system::optimized_and ( pbes_expression &  result, const pbes_expression &  p, const pbes_expression &  q  )

inline

Make a conjunction.

Parameters

p	A PBES expression
q	A PBES expression

Returns

The value p && q

Definition at line 965 of file pbes_expression.h.

optimized_exists()

void mcrl2::pbes_system::optimized_exists ( pbes_expression &  result, const data::variable_list &  l, const pbes_expression &  p  )

inline

Make an existential quantification If l is empty, p is returned.

Parameters

l	A sequence of data variables
p	A PBES expression

Returns

The value exists l.p

Definition at line 1024 of file pbes_expression.h.

optimized_forall()

void mcrl2::pbes_system::optimized_forall ( pbes_expression &  result, const data::variable_list &  l, const pbes_expression &  p  )

inline

Make a universal quantification If l is empty, p is returned.

Parameters

l	A sequence of data variables
p	A PBES expression

Returns

The value forall l.p

Definition at line 996 of file pbes_expression.h.

optimized_imp()

void mcrl2::pbes_system::optimized_imp ( pbes_expression &  result, const pbes_expression &  p, const pbes_expression &  q  )

inline

Make an implication.

Parameters

p	A PBES expression
q	A PBES expression

Returns

The value p => q

Definition at line 985 of file pbes_expression.h.

optimized_join_and()

template<typename FwdIt >

pbes_expression mcrl2::pbes_system::optimized_join_and ( FwdIt  first, FwdIt  last  )

inline

Returns and applied to the sequence of pbes expressions [first, last)

Parameters

first	Start of a sequence of pbes expressions
last	End of a sequence of pbes expressions

Returns

And applied to the sequence of pbes expressions [first, last)

Definition at line 116 of file join.h.

optimized_join_or()

template<typename FwdIt >

pbes_expression mcrl2::pbes_system::optimized_join_or ( FwdIt  first, FwdIt  last  )

inline

Returns or applied to the sequence of pbes expressions [first, last)

Parameters

first	Start of a sequence of pbes expressions
last	End of a sequence of pbes expressions

Returns

Or applied to the sequence of pbes expressions [first, last)

Definition at line 98 of file join.h.

optimized_not()

void mcrl2::pbes_system::optimized_not ( pbes_expression &  result, const pbes_expression &  p  )

inline

Make a negation.

Parameters

p	A PBES expression

Returns

The value !p

Definition at line 955 of file pbes_expression.h.

optimized_or()

void mcrl2::pbes_system::optimized_or ( pbes_expression &  result, const pbes_expression &  p, const pbes_expression &  q  )

inline

Make a disjunction.

Parameters

p	A PBES expression
q	A PBES expression

Returns

The value p || q

Definition at line 975 of file pbes_expression.h.

order_quantified_variables()

pbes_expression mcrl2::pbes_system::order_quantified_variables ( const pbes_expression &  x, const data::data_specification &  dataspec  )

inline

Definition at line 54 of file transformations.h.

parelm()

void mcrl2::pbes_system::parelm ( pbes &  p )

inline

Apply the parelm algorithm.

Parameters

p	A PBES to which the algorithm is applied

Definition at line 309 of file parelm.h.

parse_absinthe_strategy()

absinthe_strategy mcrl2::pbes_system::parse_absinthe_strategy ( const std::string &  strategy )

inline

Parses an absinthe strategy.

Definition at line 31 of file absinthe_strategy.h.

parse_bisimulation_type()

bisimulation_type mcrl2::pbes_system::parse_bisimulation_type ( const std::string &  type )

inline

Returns the string corresponding to a bisimulation type.

Definition at line 33 of file bisimulation_type.h.

parse_pbes() [1/2]

pbes mcrl2::pbes_system::parse_pbes ( const std::string &  text )

inline

Definition at line 59 of file parse.h.

parse_pbes() [2/2]

pbes mcrl2::pbes_system::parse_pbes ( std::istream &  in )

inline

Definition at line 39 of file parse.h.

parse_pbes_expression() [1/4]

template<typename SubstitutionFunction >

pbes_expression mcrl2::pbes_system::parse_pbes_expression	(	const std::string &	expr,
		const std::string &	subst,
		const pbes &	p,
		SubstitutionFunction &	sigma
	)

Parses a pbes expression.

Parameters

expr	A string
subst	A string
p	A PBES
sigma	A substitution function

Returns

The parsed expression

Definition at line 188 of file parse.h.

parse_pbes_expression() [2/4]

template<typename VariableContainer , typename PropositionalVariableContainer >

pbes_expression mcrl2::pbes_system::parse_pbes_expression	(	const std::string &	text,
		const data::data_specification &	dataspec,
		const VariableContainer &	variables,
		const PropositionalVariableContainer &	propositional_variables,
		bool	type_check = true,
		bool	translate_user_notation = true,
		bool	normalize_sorts = true
	)

Parse a pbes expression. Throws an exception if something went wrong.

Parameters

[in]	text	A string containing a pbes expression.
[in]	variables	A sequence of data variables that may appear in x.
[in]	propositional_variables	A sequence of propositional variables that may appear in x.
[in]	dataspec	A data specification.
[in]	type_check	If true the parsed input is also typechecked.

Returns

The parsed PBES expression.

Definition at line 85 of file parse.h.

parse_pbes_expression() [3/4]

template<typename VariableContainer >

pbes_expression mcrl2::pbes_system::parse_pbes_expression	(	const std::string &	text,
		const pbes &	pbesspec,
		const VariableContainer &	variables,
		bool	type_check = true,
		bool	translate_user_notation = true,
		bool	normalize_sorts = true
	)

Parse a pbes expression. Throws an exception if something went wrong.

Parameters

[in]	text	A string containing a pbes expression.
[in]	pbesspec	A PBES used as context.
[in]	variables	A sequence of data variables that may appear in x.
[in]	type_check	If true the parsed input is also typechecked.

Returns

The parsed PBES expression.

Definition at line 119 of file parse.h.

parse_pbes_expression() [4/4]

pbes_expression mcrl2::pbes_system::parse_pbes_expression ( const std::string &  text, const std::string &  var_decl = "datavar\npredvar\n", const std::string &  data_spec = ""  )

inline

Parses a single pbes expression.

Parameters

text	A string
var_decl	A string with their types. An example of this is: datavar n: Nat; predvar X: Pos; Y: Nat, Bool;
data_spec	A string

Returns

The parsed expression

Definition at line 176 of file parse.h.

parse_pbes_expressions()

std::pair< std::vector< pbes_expression >, data::data_specification > mcrl2::pbes_system::parse_pbes_expressions ( std::string  text, const std::string &  data_spec = ""  )

inline

Parses a sequence of pbes expressions. The format of the text is as follows:

• "datavar", followed by a sequence of data variable declarations
• "predvar", followed by a sequence of predicate variable declarations
• "expressions", followed by a sequence of pbes expressions separated by newlines

An example of this is:

datavar
  n: Nat;
predvar
  X: Pos;
  Y: Nat, Bool;

Parameters

text	A string
data_spec	A string N.B. A side effect of the data specification is that it determines whether rewrite rules for types like Pos and Nat are generated or not.

Returns

The parsed expression and the data specification that was used.

Definition at line 42 of file parse.h.

parse_pbes_rewriter_type()

pbes_rewriter_type mcrl2::pbes_system::parse_pbes_rewriter_type ( const std::string &  type )

inline

Parses a pbes rewriter type.

Definition at line 38 of file pbes_rewriter_type.h.

parse_pbesinst_strategy()

pbesinst_strategy mcrl2::pbes_system::parse_pbesinst_strategy ( const std::string &  s )

inline

Parse a pbesinst transformation strategy.

Definition at line 32 of file pbesinst_strategy.h.

parse_pgsolver() [1/2]

void mcrl2::pbes_system::parse_pgsolver ( const std::string &  filename, pbes &  b, bool  maxpg = true  )

inline

Parse parity game in PGSolver format from filename, and store the resulting BES in b.

Definition at line 236 of file pg_parse.h.

parse_pgsolver() [2/2]

void mcrl2::pbes_system::parse_pgsolver ( std::istream &  from, pbes &  result, bool  maxpg = true  )

inline

Reads a parity game from an input stream, and stores it as a BES.

Parameters

from	An input stream
result	A boolean equation system
maxpg	If true a max-parity game is generated in result, otherwise a min-parity game is obtained.

Definition at line 228 of file pg_parse.h.

parse_pgsolver_string()

void mcrl2::pbes_system::parse_pgsolver_string ( const std::string &  text, pbes &  result, bool  maxpg = true  )

inline

Reads a parity game from an input stream, and stores it as a BES.

Parameters

text	A string
result	A boolean equation system
maxpg	If true a max-parity game is generated in result, otherwise a min-parity game is obtained.

Definition at line 213 of file pg_parse.h.

parse_propositional_variable()

template<typename VariableContainer >

propositional_variable mcrl2::pbes_system::parse_propositional_variable	(	const std::string &	text,
		const VariableContainer &	variables,
		const data::data_specification &	dataspec = data::data_specification()
	)

Definition at line 66 of file parse.h.

parse_remove_level()

remove_level mcrl2::pbes_system::parse_remove_level ( const std::string &  s )

inline

Definition at line 35 of file remove_level.h.

parse_search_strategy()

search_strategy mcrl2::pbes_system::parse_search_strategy ( const std::string &  s )

inline

Definition at line 34 of file search_strategy.h.

parse_solution_strategy()

static solution_strategy_t mcrl2::pbes_system::parse_solution_strategy ( const std::string &  s )

static

Definition at line 49 of file solution_strategy.h.

parse_solver_type()

pbespg_solver_type mcrl2::pbes_system::parse_solver_type ( const std::string &  s )

inline

Definition at line 37 of file pbespgsolve.h.

parse_transformation_strategy()

transformation_strategy mcrl2::pbes_system::parse_transformation_strategy ( const std::string &  s )

inline

Definition at line 49 of file transformation_strategy.h.

pbes2_bool_test()

bool mcrl2::pbes_system::pbes2_bool_test	(	pbes &	pbes_spec,
		const bool	expected_outcome,
		data::rewriter::strategy	rewrite_strategy = data::jitty
	)

Definition at line 100 of file pbes_solver_test.h.

pbes2srf()

srf_pbes mcrl2::pbes_system::pbes2srf ( const pbes &  p )

inline

Converts a PBES into standard recursive form.

Precondition

The pbes p must be normalized

Definition at line 634 of file srf_pbes.h.

pbes_equation_to_aterm()

atermpp::aterm_appl mcrl2::pbes_system::pbes_equation_to_aterm ( const pbes_equation &  eqn )

inline

Conversion to atermaPpl.

Returns

The specification converted to aterm format.

Definition at line 182 of file pbes_equation.h.

pbes_expression_order_quantified_variables()

mcrl2::pbes_system::pbes_expression mcrl2::pbes_system::pbes_expression_order_quantified_variables ( const mcrl2::pbes_system::pbes_expression &  p, const mcrl2::data::data_specification &  data_spec  )

inline

Definition at line 79 of file pbesinst_alternative_lazy_algorithm.h.

pbes_file_formats()

const std::vector< utilities::file_format > & mcrl2::pbes_system::pbes_file_formats

(

)

Definition at line 26 of file io.cpp.

pbes_format_internal()

const utilities::file_format & mcrl2::pbes_system::pbes_format_internal ( )

inline

Definition at line 42 of file io.h.

pbes_format_internal_bes()

const utilities::file_format & mcrl2::pbes_system::pbes_format_internal_bes ( )

inline

Definition at line 46 of file io.h.

pbes_format_pgsolver()

const utilities::file_format & mcrl2::pbes_system::pbes_format_pgsolver ( )

inline

Definition at line 48 of file io.h.

pbes_format_text()

const utilities::file_format & mcrl2::pbes_system::pbes_format_text ( )

inline

Definition at line 44 of file io.h.

pbes_instantiation_test_algorithm_test()

bool mcrl2::pbes_system::pbes_instantiation_test_algorithm_test ( pbes &  pbes_spec, const bool  expected_outcome, const data::rewriter::strategy  rewrite_strategy  )

inline

Definition at line 33 of file pbes_solver_test.h.

pbes_marker()

atermpp::aterm mcrl2::pbes_system::pbes_marker

(

)

Definition at line 229 of file io.cpp.

pbes_rewrite() [1/4]

template<typename T , typename Rewriter , typename Substitution >

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

Rewrites all embedded pbes expressions in an object x, and applies a substitution to variables on the fly.

Parameters

x	an object containing expressions
R	a pbes rewriter
sigma	a substitution

Returns

the rewrite result

Definition at line 199 of file rewrite.h.

pbes_rewrite() [2/4]

template<typename T , typename Rewriter >

T mcrl2::pbes_system::pbes_rewrite	(	const T &	x,
		const Rewriter &	R,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= 0
	)

Rewrites all embedded pbes expressions in an object x.

Parameters

x	an object containing expressions
R	a pbes rewriter

Returns

the rewrite result

Definition at line 169 of file rewrite.h.

pbes_rewrite() [3/4]

template<typename T , typename Rewriter , typename Substitution >

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

Rewrites all embedded pbes expressions in an object x, and applies a substitution to variables on the fly.

Parameters

x	an object containing expressions
R	a pbes rewriter
sigma	a substitution

Definition at line 184 of file rewrite.h.

pbes_rewrite() [4/4]

template<typename T , typename Rewriter >

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

Rewrites all embedded pbes expressions in an object x.

Parameters

x	an object containing expressions
R	a pbes rewriter

Definition at line 156 of file rewrite.h.

pbes_to_aterm()

atermpp::aterm_appl mcrl2::pbes_system::pbes_to_aterm

(

const pbes &

p

)

Conversion to atermappl.

Returns

The PBES converted to aterm format.

Definition at line 328 of file io.cpp.

pbesabsinthe()

void mcrl2::pbes_system::pbesabsinthe	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const utilities::file_format &	input_format,
		const utilities::file_format &	output_format,
		const std::string &	abstraction_file,
		absinthe_strategy	strategy,
		bool	print_used_function_symbols,
		bool	enable_logging
	)

Definition at line 23 of file pbesabsinthe.h.

pbesabstract()

void mcrl2::pbes_system::pbesabstract ( const std::string &  input_filename, const std::string &  output_filename, const utilities::file_format &  input_format, const utilities::file_format &  output_format, const std::string &  parameter_selection, bool  value_true  )

inline

Definition at line 24 of file pbesabstract.h.

pbesconstelm()

void mcrl2::pbes_system::pbesconstelm	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const utilities::file_format &	input_format,
		const utilities::file_format &	output_format,
		data::rewrite_strategy	rewrite_strategy,
		pbes_rewriter_type	rewriter_type,
		bool	compute_conditions,
		bool	remove_redundant_equations,
		bool	check_quantifiers
	)

Definition at line 22 of file pbesconstelm.h.

pbesinfo()

void mcrl2::pbes_system::pbesinfo	(	const std::string &	input_filename,
		const std::string &	input_file_message,
		const utilities::file_format &	file_format,
		bool	opt_full
	)

Definition at line 22 of file pbesinfo.h.

pbesinst_finite()

void mcrl2::pbes_system::pbesinst_finite ( pbes &  p, data::rewrite_strategy  rewrite_strategy, const std::string &  finite_parameter_selection  )

inline

Definition at line 410 of file pbesinst_finite_algorithm.h.

pbesinst_is_constant()

bool mcrl2::pbes_system::pbesinst_is_constant ( const pbes_expression &  x )

inline

Definition at line 44 of file pbesinst_algorithm.h.

pbesparelm()

void mcrl2::pbes_system::pbesparelm	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const utilities::file_format &	input_format,
		const utilities::file_format &	output_format
	)

Definition at line 22 of file pbesparelm.h.

pbespareqelm()

void mcrl2::pbes_system::pbespareqelm	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const utilities::file_format &	input_format,
		const utilities::file_format &	output_format,
		data::rewrite_strategy	rewrite_strategy,
		pbes_rewriter_type	rewriter_type,
		bool	ignore_initial_state
	)

Definition at line 22 of file pbespareqelm.h.

pbespgsolve() [1/2]

bool mcrl2::pbes_system::pbespgsolve ( pbes &  p, const pbespgsolve_options &  options = pbespgsolve_options()  )

inline

Solves a pbes using a parity game solver.

Returns

The solution of the pbes

Definition at line 260 of file pbespgsolve.h.

pbespgsolve() [2/2]

bool mcrl2::pbes_system::pbespgsolve ( pbes &  p, utilities::execution_timer &  timer, const pbespgsolve_options &  options = pbespgsolve_options()  )

inline

Solves a pbes using a parity game solver.

Returns

The solution of the pbes

Definition at line 271 of file pbespgsolve.h.

pbespor()

void mcrl2::pbes_system::pbespor	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const utilities::file_format &	input_format,
		const utilities::file_format &	output_format,
		pbespor_options	options
	)

Definition at line 152 of file pbespor.h.

pbespp()

void mcrl2::pbes_system::pbespp	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const utilities::file_format &	input_format,
		core::print_format_type	format,
		bool	use_pfnf_printer
	)

Definition at line 22 of file pbespp.h.

pbesrewr()

void mcrl2::pbes_system::pbesrewr	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const utilities::file_format &	input_format,
		const utilities::file_format &	output_format,
		data::rewrite_strategy	rewrite_strategy,
		pbes_rewriter_type	rewriter_type
	)

Definition at line 31 of file pbesrewr.h.

pbesstategraph()

void mcrl2::pbes_system::pbesstategraph	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const utilities::file_format &	input_format,
		const utilities::file_format &	output_format,
		const pbesstategraph_options &	options
	)

Definition at line 22 of file pbesstategraph.h.

pfnf_pp()

template<typename T >

std::string mcrl2::pbes_system::pfnf_pp

(

const T &

x

)

Returns a PFNF string representation of the object x.

Definition at line 147 of file pfnf_print.h.

pp() [1/20]

std::string mcrl2::pbes_system::pp

(

const and_ &

x

)

Definition at line 35 of file pbes.cpp.

pp() [2/20]

std::string mcrl2::pbes_system::pp

(

const exists &

x

)

Definition at line 36 of file pbes.cpp.

pp() [3/20]

std::string mcrl2::pbes_system::pp

(

const fixpoint_symbol &

x

)

Definition at line 37 of file pbes.cpp.

pp() [4/20]

std::string mcrl2::pbes_system::pp

(

const forall &

x

)

Definition at line 38 of file pbes.cpp.

pp() [5/20]

std::string mcrl2::pbes_system::pp

(

const imp &

x

)

Definition at line 39 of file pbes.cpp.

pp() [6/20]

std::string mcrl2::pbes_system::pp

(

const not_ &

x

)

Definition at line 40 of file pbes.cpp.

pp() [7/20]

std::string mcrl2::pbes_system::pp

(

const or_ &

x

)

Definition at line 41 of file pbes.cpp.

pp() [8/20]

std::string mcrl2::pbes_system::pp

(

const pbes &

x

)

Definition at line 42 of file pbes.cpp.

pp() [9/20]

std::string mcrl2::pbes_system::pp

(

const pbes_equation &

x

)

Definition at line 43 of file pbes.cpp.

pp() [10/20]

std::string mcrl2::pbes_system::pp

(

const pbes_equation_vector &

x

)

Definition at line 28 of file pbes.cpp.

pp() [11/20]

std::string mcrl2::pbes_system::pp

(

const pbes_expression &

x

)

Definition at line 44 of file pbes.cpp.

pp() [12/20]

std::string mcrl2::pbes_system::pp

(

const pbes_expression_list &

x

)

Definition at line 29 of file pbes.cpp.

pp() [13/20]

std::string mcrl2::pbes_system::pp

(

const pbes_expression_vector &

x

)

Definition at line 30 of file pbes.cpp.

pp() [14/20]

std::string mcrl2::pbes_system::pp

(

const propositional_variable &

x

)

Definition at line 45 of file pbes.cpp.

pp() [15/20]

std::string mcrl2::pbes_system::pp

(

const propositional_variable_instantiation &

x

)

Definition at line 46 of file pbes.cpp.

pp() [16/20]

std::string mcrl2::pbes_system::pp

(

const propositional_variable_instantiation_list &

x

)

Definition at line 33 of file pbes.cpp.

pp() [17/20]

std::string mcrl2::pbes_system::pp

(

const propositional_variable_instantiation_vector &

x

)

Definition at line 34 of file pbes.cpp.

pp() [18/20]

std::string mcrl2::pbes_system::pp

(

const propositional_variable_list &

x

)

Definition at line 31 of file pbes.cpp.

pp() [19/20]

std::string mcrl2::pbes_system::pp

(

const propositional_variable_vector &

x

)

Definition at line 32 of file pbes.cpp.

pp() [20/20]

template<typename T >

std::string mcrl2::pbes_system::pp

(

const T &

x

)

Returns a string representation of the object x.

Definition at line 255 of file print.h.

precedence() [1/7]

constexpr int mcrl2::pbes_system::precedence ( const and_ &  )

inlineconstexpr

Definition at line 26 of file print.h.

precedence() [2/7]

constexpr int mcrl2::pbes_system::precedence ( const exists &  )

inlineconstexpr

Definition at line 23 of file print.h.

precedence() [3/7]

constexpr int mcrl2::pbes_system::precedence ( const forall &  )

inlineconstexpr

Definition at line 22 of file print.h.

precedence() [4/7]

constexpr int mcrl2::pbes_system::precedence ( const imp &  )

inlineconstexpr

Definition at line 24 of file print.h.

precedence() [5/7]

constexpr int mcrl2::pbes_system::precedence ( const not_ &  )

inlineconstexpr

Definition at line 27 of file print.h.

precedence() [6/7]

constexpr int mcrl2::pbes_system::precedence ( const or_ &  )

inlineconstexpr

Definition at line 25 of file print.h.

precedence() [7/7]

int mcrl2::pbes_system::precedence ( const pbes_expression &  x )

inline

Definition at line 28 of file print.h.

print() [1/2]

std::string mcrl2::pbes_system::print ( const pbespg_solver_type  solver_type )

inline

Returns

A string representation of the solver type.

Definition at line 60 of file pbespgsolve.h.

print() [2/2]

std::string mcrl2::pbes_system::print ( StaticGraph::EdgeDirection  edge_direction )

inline

Returns

A string representation of the edge direction.

Definition at line 112 of file pbespgsolve.h.

print_absinthe_strategy()

std::string mcrl2::pbes_system::print_absinthe_strategy ( const absinthe_strategy  strategy )

inline

Prints an absinthe strategy.

Definition at line 49 of file absinthe_strategy.h.

print_bisimulation_type()

std::string mcrl2::pbes_system::print_bisimulation_type ( const bisimulation_type  t )

inline

Returns a description of a bisimulation type.

Definition at line 45 of file bisimulation_type.h.

print_brief()

template<typename T >

std::string mcrl2::pbes_system::print_brief

(

const T &

x

)

Returns a string representation of the root node of a PBES.

Parameters

x	a PBES object

Definition at line 69 of file pbes_functions.h.

print_pbes_rewriter_type()

std::string mcrl2::pbes_system::print_pbes_rewriter_type ( const pbes_rewriter_type  type )

inline

Prints a pbes rewriter type.

Definition at line 81 of file pbes_rewriter_type.h.

print_pbesinst_strategy()

std::string mcrl2::pbes_system::print_pbesinst_strategy ( const pbesinst_strategy  strategy )

inline

Returns a string representation of a pbesinst transformation strategy.

Definition at line 70 of file pbesinst_strategy.h.

print_remove_level()

std::string mcrl2::pbes_system::print_remove_level ( const remove_level  s )

inline

Definition at line 44 of file remove_level.h.

print_search_strategy()

std::string mcrl2::pbes_system::print_search_strategy ( const search_strategy  s )

inline

Definition at line 44 of file search_strategy.h.

print_strategy_vector()

std::string mcrl2::pbes_system::print_strategy_vector ( const vertex_set &  S_alpha, const strategy_vector &  tau_alpha  )

inline

Definition at line 430 of file pbessolve_vertex_set.h.

print_structure_graph()

template<typename StructureGraph >

std::ostream & mcrl2::pbes_system::print_structure_graph	(	std::ostream &	out,
		const StructureGraph &	G
	)

Definition at line 302 of file structure_graph.h.

print_summand_set()

std::string mcrl2::pbes_system::print_summand_set ( const summand_set &  s )

inline

Definition at line 57 of file partial_order_reduction.h.

print_symbol()

template<typename Term >

std::string mcrl2::pbes_system::print_symbol

(

const Term &

x

)

Definition at line 37 of file absinthe.h.

print_term()

template<typename Term >

std::string mcrl2::pbes_system::print_term

(

const Term &

x

)

Definition at line 31 of file absinthe.h.

print_transformation_strategy()

std::string mcrl2::pbes_system::print_transformation_strategy ( const transformation_strategy  s )

inline

Definition at line 59 of file transformation_strategy.h.

quantifier_propagate() [1/2]

pbes mcrl2::pbes_system::quantifier_propagate ( const pbes &  p )

inline

Definition at line 404 of file quantifier_propagate.h.

quantifier_propagate() [2/2]

void mcrl2::pbes_system::quantifier_propagate ( pbes &  p )

inline

Definition at line 375 of file quantifier_propagate.h.

quantifier_variables()

const data::variable_list & mcrl2::pbes_system::quantifier_variables ( const pbes_expression &  x )

inline

Definition at line 1053 of file pbes_expression.h.

reachable_variables()

std::set< propositional_variable > mcrl2::pbes_system::reachable_variables ( const pbes &  p )

inline

Definition at line 38 of file remove_equations.h.

remove_index_impl()

static atermpp::aterm_appl mcrl2::pbes_system::remove_index_impl ( const atermpp::aterm_appl &  x )

static

Definition at line 174 of file io.cpp.

remove_parameters() [1/6]

template<typename T >

T mcrl2::pbes_system::remove_parameters	(	const T &	x,
		const std::map< core::identifier_string, std::vector< std::size_t > > &	to_be_removed,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters

x	A PBES library object that derives from atermpp::aterm_appl
to_be_removed	A mapping that maps propositional variable names to indices of parameters that are removed

Returns

The expression x with parameters removed according to the mapping to_be_removed

Definition at line 208 of file remove_parameters.h.

remove_parameters() [2/6]

template<typename T >

T mcrl2::pbes_system::remove_parameters	(	const T &	x,
		const std::set< data::variable > &	to_be_removed,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= 0
	)

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters

x	A PBES library object that derives from atermpp::aterm_appl
to_be_removed	A set of parameters that are to be removed

Returns

The expression x with parameters removed according to the mapping to_be_removed

Definition at line 318 of file remove_parameters.h.

remove_parameters() [3/6]

template<typename T >

T mcrl2::pbes_system::remove_parameters	(	const T &	x,
		const std::vector< std::size_t > &	to_be_removed,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters

x	A PBES library object that derives from atermpp::aterm_appl
to_be_removed	The indices of parameters that are to be removed

Returns

The expression x with parameters removed according to the mapping to_be_removed

Definition at line 107 of file remove_parameters.h.

remove_parameters() [4/6]

template<typename T >

void mcrl2::pbes_system::remove_parameters	(	T &	x,
		const std::map< core::identifier_string, std::vector< std::size_t > > &	to_be_removed,
		typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters

x	A PBES library object that does not derive from atermpp::aterm_appl
to_be_removed	A mapping that maps propositional variable names to a sorted vector of parameter indices that need to be removed

Returns

The expression x with parameters removed according to the mapping to_be_removed

Definition at line 224 of file remove_parameters.h.

remove_parameters() [5/6]

template<typename T >

void mcrl2::pbes_system::remove_parameters	(	T &	x,
		const std::set< data::variable > &	to_be_removed,
		typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters

x	A PBES library object that does not derive from atermpp::aterm_appl
to_be_removed	A set of parameters that are to be removed

Returns

The expression x with parameters removed according to the mapping to_be_removed

Definition at line 333 of file remove_parameters.h.

remove_parameters() [6/6]

template<typename T >

void mcrl2::pbes_system::remove_parameters	(	T &	x,
		const std::vector< std::size_t > &	to_be_removed,
		typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *	= 0
	)

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters

x	A PBES library object that does not derive from atermpp::aterm_appl
to_be_removed	The indices of parameters that are to be removed

Returns

The expression x with parameters removed according to the mapping to_be_removed

Definition at line 122 of file remove_parameters.h.

remove_unreachable_variables()

std::vector< propositional_variable > mcrl2::pbes_system::remove_unreachable_variables ( pbes &  p )

inline

Removes equations that are not (syntactically) reachable from the initial state of a PBES.

Returns

The removed variables

Definition at line 82 of file remove_equations.h.

replace_all_variables() [1/2]

template<typename T , typename Substitution >

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

Definition at line 169 of file replace.h.

replace_all_variables() [2/2]

template<typename T , typename Substitution >

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

Definition at line 160 of file replace.h.

replace_constants_by_variables() [1/2]

template<typename T >

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

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

Definition at line 55 of file replace_constants_by_variables.h.

replace_constants_by_variables() [2/2]

template<typename T >

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

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

Definition at line 41 of file replace_constants_by_variables.h.

replace_data_expressions() [1/2]

template<typename T , typename Substitution >

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

Definition at line 127 of file replace.h.

replace_data_expressions() [2/2]

template<typename T , typename Substitution >

void mcrl2::pbes_system::replace_data_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Definition at line 117 of file replace.h.

replace_free_variables() [1/4]

template<typename T , typename Substitution , typename VariableContainer >

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

\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 221 of file replace.h.

replace_free_variables() [2/4]

template<typename T , typename Substitution >

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

\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 194 of file replace.h.

replace_free_variables() [3/4]

template<typename T , typename Substitution , typename VariableContainer >

void mcrl2::pbes_system::replace_free_variables	(	T &	x,
		const Substitution &	sigma,
		const VariableContainer &	bound_variables,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\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 208 of file replace.h.

replace_free_variables() [4/4]

template<typename T , typename Substitution >

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

\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 182 of file replace.h.

replace_pbes_expressions() [1/2]

template<typename T , typename Substitution >

T mcrl2::pbes_system::replace_pbes_expressions	(	const T &	x,
		const Substitution &	sigma,
		bool	innermost = true,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Definition at line 278 of file replace.h.

replace_pbes_expressions() [2/2]

template<typename T , typename Substitution >

void mcrl2::pbes_system::replace_pbes_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost = true,
		typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *	= 0
	)

Definition at line 268 of file replace.h.

replace_propositional_variables() [1/3]

template<typename T , typename Substitution >

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

Applies a propositional variable substitution.

Definition at line 246 of file replace.h.

replace_propositional_variables() [2/3]

template<typename T , typename Substitution >

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

Applies a propositional variable substitution.

Definition at line 258 of file replace.h.

replace_propositional_variables() [3/3]

template<typename T , typename Substitution >

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

Applies a propositional variable substitution.

Definition at line 236 of file replace.h.

replace_sort_expressions() [1/2]

template<typename T , typename Substitution >

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

Definition at line 105 of file replace.h.

replace_sort_expressions() [2/2]

template<typename T , typename Substitution >

void mcrl2::pbes_system::replace_sort_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Definition at line 95 of file replace.h.

replace_subterm() [1/2]

pbes mcrl2::pbes_system::replace_subterm ( const pbes &  p, std::size_t  x, std::size_t  y, const pbes_expression &  replacement  )

inline

Replace the subterm at position (x, y) with a given term.

Definition at line 183 of file replace_subterm.h.

replace_subterm() [2/2]

pbes_expression mcrl2::pbes_system::replace_subterm ( const pbes_expression &  expr, std::size_t  x, std::size_t  y, const pbes_expression &  replacement  )

inline

Replace the subterm at position (x, y) with a given term.

Definition at line 173 of file replace_subterm.h.

replace_variables() [1/2]

template<typename T , typename Substitution >

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

Definition at line 149 of file replace.h.

replace_variables() [2/2]

template<typename T , typename Substitution >

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

Definition at line 140 of file replace.h.

replace_variables_capture_avoiding() [1/4]

template<typename T , typename Substitution >

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

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

Definition at line 102 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [2/4]

template<typename T , typename Substitution >

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

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

Definition at line 136 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [3/4]

template<typename T , typename Substitution >

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

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

Definition at line 87 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [4/4]

template<typename T , typename Substitution >

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

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

Definition at line 118 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [1/2]

template<typename T , typename Substitution , typename IdentifierGenerator >

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

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

Definition at line 114 of file replace_capture_avoiding_with_an_identifier_generator.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [2/2]

template<typename T , typename Substitution , typename IdentifierGenerator >

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

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

Definition at line 95 of file replace_capture_avoiding_with_an_identifier_generator.h.

resolve_summand_variable_name_clashes()

void mcrl2::pbes_system::resolve_summand_variable_name_clashes ( srf_pbes &  pbesspec, const data::variable_list &  process_parameters  )

inline

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

Definition at line 50 of file resolve_name_clashes.h.

rewrite() [1/4]

template<typename T , typename Rewriter , typename Substitution >

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

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

Definition at line 140 of file rewrite.h.

rewrite() [2/4]

template<typename T , typename Rewriter >

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

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

Definition at line 110 of file rewrite.h.

rewrite() [3/4]

template<typename T , typename Rewriter , typename Substitution >

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

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

Definition at line 125 of file rewrite.h.

rewrite() [4/4]

template<typename T , typename Rewriter >

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

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

Definition at line 97 of file rewrite.h.

save_bes_pgsolver()

void mcrl2::pbes_system::save_bes_pgsolver	(	const pbes &	bes,
		std::ostream &	stream,
		bool	maxpg = true
	)

Definition at line 142 of file pgsolver.cpp.

save_pbes() [1/2]

void mcrl2::pbes_system::save_pbes	(	const pbes &	pbes,
		const std::string &	filename,
		utilities::file_format	format = utilities::file_format(),
		bool	welltypedness_check = true
	)

save_pbes Saves a PBES to a file.

Parameters

pbes	The PBES to save.
filename	The file to save the PBES in.
format	The format in which to save the PBES.
welltypedness_check	If set to false, skips checking whether pbes is well typed before saving it to file.

The format of the file in infilename is guessed if format is not given or if it is equal to utilities::file_format().

Definition at line 113 of file io.cpp.

save_pbes() [2/2]

void mcrl2::pbes_system::save_pbes	(	const pbes &	pbes,
		std::ostream &	stream,
		utilities::file_format	format = utilities::file_format()
	)

Save a PBES in the format specified.

Parameters

pbes	The PBES to be stored
stream	The stream to which the output is saved.
format	Determines the format in which the result is written. If unspecified, or pbes_file_unknown is specified, then a default format is chosen.

Definition at line 49 of file io.cpp.

search_variable() [1/2]

bool mcrl2::pbes_system::search_variable	(	const pbes_system::pbes_expression &	x,
		const data::variable &	v
	)

Definition at line 60 of file pbes.cpp.

search_variable() [2/2]

template<typename T >

bool mcrl2::pbes_system::search_variable	(	const T &	x,
		const data::variable &	v
	)

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

Parameters

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

Returns

True if v occurs in x.

Definition at line 217 of file find.h.

set_intersection()

template<typename VertexSet >

vertex_set mcrl2::pbes_system::set_intersection	(	const VertexSet &	V,
		const vertex_set &	W
	)

Definition at line 283 of file pbessolve_vertex_set.h.

set_minus()

vertex_set mcrl2::pbes_system::set_minus ( const vertex_set &  V, const vertex_set &  W  )

inline

Definition at line 297 of file pbessolve_vertex_set.h.

set_union()

vertex_set mcrl2::pbes_system::set_union ( const vertex_set &  V, const vertex_set &  W  )

inline

Definition at line 271 of file pbessolve_vertex_set.h.

significant_variables()

std::set< data::variable > mcrl2::pbes_system::significant_variables ( const pbes_expression &  x )

inline

Definition at line 111 of file significant_variables.h.

small_progress_measures()

bool mcrl2::pbes_system::small_progress_measures ( pbes &  b )

inline

Definition at line 367 of file small_progress_measures.h.

solution_strategy_to_string()

static std::string mcrl2::pbes_system::solution_strategy_to_string ( const solution_strategy_t  s )

static

Definition at line 27 of file solution_strategy.h.

solve_structure_graph()

bool mcrl2::pbes_system::solve_structure_graph ( structure_graph &  G, bool  check_strategy = false  )

inline

Definition at line 568 of file solve_structure_graph.h.

solve_structure_graph_with_counter_example() [1/2]

std::pair< bool, lps::specification > mcrl2::pbes_system::solve_structure_graph_with_counter_example ( structure_graph &  G, const lps::specification &  lpsspec, const pbes &  p, const pbes_equation_index &  p_index  )

inline

Definition at line 576 of file solve_structure_graph.h.

solve_structure_graph_with_counter_example() [2/2]

bool mcrl2::pbes_system::solve_structure_graph_with_counter_example ( structure_graph &  G, lts::lts_lts_t &  ltsspec  )

inline

Solve this pbes_system using a structure graph generating a counter example.

Parameters

G	The structure graph.
ltsspec	The original LTS that was used to create the PBES.

Definition at line 586 of file solve_structure_graph.h.

split_and()

std::set< pbes_expression > mcrl2::pbes_system::split_and ( const pbes_expression &  expr, bool  split_data_expressions = false  )

inline

Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 && p2 && .... && pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main function symbol.

Parameters

expr	A PBES expression
split_data_expressions	if true, both data and pbes conjunctions are split, otherwise only pbes conjunctions are split.

Returns

A sequence of operands

Definition at line 76 of file join.h.

split_conjuncts()

std::vector< pbes_expression > mcrl2::pbes_system::split_conjuncts ( const pbes_expression &  expr, bool  split_simple_expr = false  )

inline

Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 && p2 && .... && pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main function symbol.

Parameters

expr	A PBES expression
split_simple_expr	If true, pbes conjuncts are split, even if no proposition variables occur. If false, pbes conjuncts are only split if a proposition variable occurs somewhere in expr.

Note

This never splits data conjuncts.

Returns

A sequence of operands

Definition at line 166 of file pbes_functions.h.

split_disjuncts()

std::vector< pbes_expression > mcrl2::pbes_system::split_disjuncts ( const pbes_expression &  expr, bool  split_simple_expr = false  )

inline

Splits a disjunction into a sequence of operands. Given a pbes expression of the form p1 || p2 || .... || pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main function symbol.

Parameters

expr	A PBES expression.
split_simple_expr	If true, pbes disjuncts are split, even if no proposition variables occur. If false, pbes disjuncts are only split if a proposition variable occurs somewhere in expr.

Note

This never splits data disjuncts.

Returns

A sequence of operands.

Definition at line 138 of file pbes_functions.h.

split_or()

std::set< pbes_expression > mcrl2::pbes_system::split_or ( const pbes_expression &  expr, bool  split_data_expressions = false  )

inline

Splits a disjunction into a sequence of operands Given a pbes expression of the form p1 || p2 || .... || pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main function symbol.

Parameters

expr	A PBES expression
split_data_expressions	if true, both data and pbes disjunctions are split, otherwise only pbes disjunctions are split.

Returns

A sequence of operands

Definition at line 50 of file join.h.

stategraph()

void mcrl2::pbes_system::stategraph ( pbes &  p, const pbesstategraph_options &  options  )

inline

Apply the stategraph algorithm.

Parameters

p	A PBES to which the algorithm is applied.
options	The options for the algorithm.

Definition at line 26 of file stategraph.h.

strong_bisimulation()

pbes mcrl2::pbes_system::strong_bisimulation ( const lps::specification &  model, const lps::specification &  spec  )

inline

Returns a pbes that expresses strong bisimulation between two specifications.

Parameters

model	A linear process specification
spec	A linear process specification

Returns

A pbes that expresses strong bisimulation between the two specifications.

Definition at line 602 of file bisimulation.h.

structure_graph_predecessors()

template<typename StructureGraph >

std::vector< typename StructureGraph::index_type > mcrl2::pbes_system::structure_graph_predecessors	(	const StructureGraph &	G,
		typename StructureGraph::index_type	u
	)

Definition at line 253 of file structure_graph.h.

structure_graph_successors()

template<typename StructureGraph >

std::vector< typename StructureGraph::index_type > mcrl2::pbes_system::structure_graph_successors	(	const StructureGraph &	G,
		typename StructureGraph::index_type	u
	)

Definition at line 264 of file structure_graph.h.

swap() [1/11]

void mcrl2::pbes_system::swap ( and_ &  t1, and_ &  t2  )

inline

\brief swap overload

Definition at line 364 of file pbes_expression.h.

swap() [2/11]

void mcrl2::pbes_system::swap ( exists &  t1, exists &  t2  )

inline

\brief swap overload

Definition at line 668 of file pbes_expression.h.

swap() [3/11]

void mcrl2::pbes_system::swap ( fixpoint_symbol &  t1, fixpoint_symbol &  t2  )

inline

\brief swap overload

Definition at line 97 of file fixpoint_symbol.h.

swap() [4/11]

void mcrl2::pbes_system::swap ( forall &  t1, forall &  t2  )

inline

\brief swap overload

Definition at line 592 of file pbes_expression.h.

swap() [5/11]

void mcrl2::pbes_system::swap ( imp &  t1, imp &  t2  )

inline

\brief swap overload

Definition at line 516 of file pbes_expression.h.

swap() [6/11]

void mcrl2::pbes_system::swap ( not_ &  t1, not_ &  t2  )

inline

\brief swap overload

Definition at line 288 of file pbes_expression.h.

swap() [7/11]

void mcrl2::pbes_system::swap ( or_ &  t1, or_ &  t2  )

inline

\brief swap overload

Definition at line 440 of file pbes_expression.h.

swap() [8/11]

void mcrl2::pbes_system::swap ( pbes_equation &  t1, pbes_equation &  t2  )

inline

\brief swap overload

Definition at line 159 of file pbes_equation.h.

swap() [9/11]

void mcrl2::pbes_system::swap ( pbes_expression &  t1, pbes_expression &  t2  )

inline

\brief swap overload

Definition at line 112 of file pbes_expression.h.

swap() [10/11]

void mcrl2::pbes_system::swap ( propositional_variable &  t1, propositional_variable &  t2  )

inline

\brief swap overload

Definition at line 117 of file propositional_variable.h.

swap() [11/11]

void mcrl2::pbes_system::swap ( propositional_variable_instantiation &  t1, propositional_variable_instantiation &  t2  )

inline

\brief swap overload

Definition at line 217 of file pbes_expression.h.

translate_user_notation() [1/4]

pbes_system::pbes_expression mcrl2::pbes_system::translate_user_notation

(

const pbes_system::pbes_expression &

x

)

Definition at line 51 of file pbes.cpp.

translate_user_notation() [2/4]

template<typename T >

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

Definition at line 33 of file translate_user_notation.h.

translate_user_notation() [3/4]

void mcrl2::pbes_system::translate_user_notation

(

pbes_system::pbes &

x

)

Definition at line 50 of file pbes.cpp.

translate_user_notation() [4/4]

template<typename T >

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

Definition at line 25 of file translate_user_notation.h.

true_()

const pbes_expression & mcrl2::pbes_system::true_ ( )

inline

Returns

Returns the value true

Definition at line 688 of file pbes_expression.h.

txt2pbes() [1/3]

void mcrl2::pbes_system::txt2pbes	(	const std::string &	input_filename,
		const std::string &	output_filename,
		const utilities::file_format &	output_format,
		bool	normalize
	)

Definition at line 21 of file txt2pbes.h.

txt2pbes() [2/3]

pbes mcrl2::pbes_system::txt2pbes ( const std::string &  text, bool  normalize = true  )

inline

Parses a PBES specification from a string.

Parameters

text	A string
normalize	If true, the resulting PBES is normalized after reading.

Returns

The parsed PBES

Definition at line 47 of file txt2pbes.h.

txt2pbes() [3/3]

pbes mcrl2::pbes_system::txt2pbes ( std::istream &  spec_stream, bool  normalize = true  )

inline

Parses a PBES specification from an input stream.

Parameters

spec_stream	A stream from which can be read
normalize	If true, the resulting PBES is normalized after reading.

Returns

The parsed PBES

Definition at line 30 of file txt2pbes.h.

typecheck_pbes()

void mcrl2::pbes_system::typecheck_pbes ( pbes &  pbesspec )

inline

Type check a parsed mCRL2 pbes specification. Throws an exception if something went wrong.

Parameters

[in]

pbesspec

A process specification that has not been type checked.

Postcondition

pbesspec is type checked.

Definition at line 275 of file typecheck.h.

typecheck_pbes_expression()

template<typename VariableContainer , typename PropositionalVariableContainer >

pbes_expression mcrl2::pbes_system::typecheck_pbes_expression	(	pbes_expression &	x,
		const VariableContainer &	variables,
		const PropositionalVariableContainer &	propositional_variables,
		const data::data_specification &	dataspec = data::data_specification()
	)

Type check a parsed mCRL2 pbes expression. Throws an exception if something went wrong.

Parameters

[in]	x	A pbes expression.
[in]	variables	A sequence of data variables that may appear in x.
[in]	propositional_variables	A sequence of propositional variables that may appear in x.
[in]	dataspec	A data specification.

Returns

the type checked expression

Definition at line 328 of file typecheck.h.

typecheck_propositional_variable()

template<typename VariableContainer >

propositional_variable mcrl2::pbes_system::typecheck_propositional_variable	(	const propositional_variable &	x,
		const VariableContainer &	variables,
		const data::data_specification &	dataspec = data::data_specification()
	)

Type check a parsed mCRL2 propositional variable. Throws an exception if something went wrong.

Parameters

[in]	x	A propositional variable.
[in]	variables	A sequence of data variables that may appear in x.
[in]	dataspec	A data specification.

Returns

the type checked expression

Definition at line 296 of file typecheck.h.

undefined_vertex()

constexpr unsigned int mcrl2::pbes_system::undefined_vertex ( )

inlineconstexpr

Definition at line 35 of file structure_graph.h.

unify_parameters() [1/2]

void mcrl2::pbes_system::unify_parameters ( pbes &  p )

inline

Definition at line 129 of file unify_parameters.h.

unify_parameters() [2/2]

void mcrl2::pbes_system::unify_parameters ( srf_pbes &  p, bool  reset = true  )

inline

Definition at line 154 of file unify_parameters.h.

weak_bisimulation()

pbes mcrl2::pbes_system::weak_bisimulation ( const lps::specification &  model, const lps::specification &  spec  )

inline

Returns a pbes that expresses weak bisimulation between two specifications.

Parameters

model	A linear process specification
spec	A linear process specification

Returns

A pbes that expresses weak bisimulation between the two specifications.

Definition at line 824 of file bisimulation.h.