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	abstract_param_state
struct	abstractable_parameter
	One entry of the universe of abstractable parameters: the variable itself and its index inside the parameters of its equation. More...
class	abstraction_progress_log
	An append-only checkpoint of an enumeration, so that an interrupted run can be resumed without re-checking anything already decided. More...
struct	abstraction_rewriter
class	abstraction_set_writer
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...
class	dataspec_prune_rewriter
	A rewriter that removes unused data specifications. 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	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	lps_to_lts_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	no_substitution
	An empty struct that can be used to indicate that there is no substitution that should be applied to propositional variables. More...
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_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...
struct	pbes_parameter_domain
	The values that a single parameter of a predicate variable may reach. More...
class	pbes_parelm_algorithm
	Algorithm class for the parelm algorithm. More...
class	pbes_parvalues_algorithm
	Algorithm that enumerates the values that the parameters of the predicate variables of a PBES can take during exploration, starting from the initial state. More...
struct	pbes_traits
	Traits class for pbes expressions. More...
class	pbes_type_checker
struct	pbesbackelm_options
struct	pbesbackelm_pbes_backward_substituter
struct	pbescegps_iterator
struct	pbescegps_options
struct	pbescegps_refine_strategies
	Refinement strategies for the CEGPS algorithm. More...
struct	pbeschain_options
struct	pbeschain_pbes_backward_substituter
class	pbesfindabs_engine
	The engine that enumerates all valid abstraction sets of a PBES. More...
struct	pbesfindabs_options
	Options for the all-abstraction-sets tool. More...
struct	pbesfixpointsolve_options
struct	pbesfixpointsolve_pbes_fixpoint_iterator
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_counter_example_structure_graph_algorithm
class	pbesinst_counter_example_structure_graph_algorithm2
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	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...
struct	rewrite_if_builder
struct	ruling_relation_type
class	simple_structure_graph
struct	simplify_data_rewriter
	A rewriter that simplifies boolean expressions in a term, and rewrites data expressions using DataRewriter. 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...
struct	skipped_t
	Marker for a check whose verdict is unknown, e.g. because its time limit expired. Such a set is neither reported nor used for pruning; its supersets are still explored. 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	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	substitute_propositional_variables_builder
struct	substitute_propositional_variables_for_true_false_builder
struct	substitute_propositional_variables_i_builder
struct	summand_class
struct	summand_equivalence_key
struct	timing_tracker
	Helper class to track multiple time measurements and call counts. More...
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
using	pbesinst_index_map = std::map< core::identifier_string, std::vector< std::size_t > >
	Data structure for storing the indices of the variables that should be expanded by the finite pbesinst algorithm.
using	pbesinst_variable_map = std::map< core::identifier_string, std::vector< data::variable > >
	Data structure for storing the variables that should be expanded by the finite pbesinst algorithm.
using	variable_map = std::map< core::identifier_string, std::size_t >
using	propositional_variable_list = atermpp::term_list< propositional_variable >
	\brief list of propositional_variables
using	propositional_variable_vector = std::vector< propositional_variable >
	\brief vector of propositional_variables
using	fixpoint_symbol_list = atermpp::term_list< fixpoint_symbol >
	\brief list of fixpoint_symbols
using	fixpoint_symbol_vector = std::vector< fixpoint_symbol >
	\brief vector of fixpoint_symbols
using	summand_set = boost::dynamic_bitset<>
using	pbes_equation_list = atermpp::term_list< pbes_equation >
	\brief list of pbes_equations
using	pbes_equation_vector = std::vector< pbes_equation >
	\brief vector of pbes_equations
using	pbes_expression_list = atermpp::term_list< pbes_expression >
	\brief list of pbes_expressions
using	pbes_expression_vector = std::vector< pbes_expression >
	\brief vector of pbes_expressions
using	propositional_variable_instantiation_list = atermpp::term_list< propositional_variable_instantiation >
	\brief list of propositional_variable_instantiations
using	propositional_variable_instantiation_vector = std::vector< propositional_variable_instantiation >
	\brief vector of propositional_variable_instantiations
using	identifier_t = unsigned long long
using	priority_t = unsigned short
using	owner_t = bool
using	srf_summand = detail::pre_srf_summand< false >
using	srf_equation = detail::pre_srf_equation< false >
using	srf_pbes = detail::pre_srf_pbes< false >
	This is a PBES in SRF format.
using	srf_pbes_with_ce = detail::pre_srf_pbes< true >
using	check_outcome = std::variant< abstraction_set_verdict, skipped_t >
	The outcome of checking one candidate set: a verdict, or skipped.

Enumerations
enum class	absinthe_strategy { absinthe_over , absinthe_under }
	The approximation strategies of the absinthe tool. More...
enum class	bisimulation_type { strong_bisim , weak_bisim , branching_bisim , branching_sim }
	An enumerated type for the available bisimulation types. More...
enum class	var_choice_strategy {   lhs , rhs , count , all ,   ruling }
enum class	tribool { no , maybe , yes }
enum class	pbes_rewriter_type {   simplify , quantifier_all , quantifier_finite , quantifier_inside ,   quantifier_one_point , prover , pfnf , ppg ,   srf , pre_srf , prune_dataspec , bqnf_quantifier ,   remove_cex_variables }
	An enumerated type for the available pbes rewriters. More...
enum class	pbesinst_strategy { pbesinst_lazy_strategy , pbesinst_alternative_lazy_strategy , pbesinst_finite_strategy }
	pbesinst transformation strategies More...
enum class	partial_solve_strategy : int {   none = -1 , no_optimisation = 0 , remove_self_loops = 1 , propagate_solved_equations_using_substitution = 2 ,   propagate_solved_equations_using_attractor = 3 , detect_winning_loops_using_fatal_attractor = 4 , solve_subgames_using_fatal_attractor_local = 5 , solve_subgames_using_fatal_attractor_original = 6 ,   solve_subgames_using_solver = 7 , detect_winning_loops_original = 8 }
	Enumeration of partial strategies for solving PBESs. More...
enum class	remove_level { none , some , all }
	BES variable remove level when generating a BES from a PBES. More...
enum class	enumerate_quantifiers_mode { expand_finite_sorts , expand_infinite_sorts , expand_infinite_sorts_and_use_data_rewriter }
enum class	search_strategy { breadth_first , depth_first , breadth_first_short , depth_first_short }
	Search strategy when generating a BES from a PBES. More...
enum class	solution_strategy_t { gauss , small_progr_measures }
enum class	abstraction_set_verdict { valid , not_closed , blocked }
	The verdict of checking a single candidate abstraction set. More...
enum class	InvResult { INV_TRUE , INV_FALSE , EQ_FALSE }
enum class	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 class	pbespg_solver_type { spm_solver , alternative_spm_solver , recursive_solver , priority_promotion }

Functions
template<typename T >
bool	is_normalized (const T &x)
	Checks if a pbes expression is normalized.
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	normalize (T &x)
	The function normalize brings (embedded) pbes expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	normalize (const T &x)
	The function normalize brings (embedded) pbes expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.
void	pbesinst_finite (pbes &p, data::rewrite_strategy rewrite_strategy, const std::string &finite_parameter_selection)
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.
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	remove_parameters (const T &x, const std::vector< std::size_t > &to_be_removed)
	Removes parameters from propositional variable instantiations in a pbes expression.
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	remove_parameters (T &x, const std::vector< std::size_t > &to_be_removed)
	Removes parameters from propositional variable instantiations in a pbes expression.
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	remove_parameters (const T &x, const std::map< core::identifier_string, std::vector< std::size_t > > &to_be_removed)
	Removes parameters from propositional variable instantiations in a pbes expression.
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	remove_parameters (T &x, const std::map< core::identifier_string, std::vector< std::size_t > > &to_be_removed)
	Removes parameters from propositional variable instantiations in a pbes expression.
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	remove_parameters (const T &x, const std::set< data::variable > &to_be_removed)
	Removes parameters from propositional variable instantiations in a pbes expression.
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	remove_parameters (T &x, const std::set< data::variable > &to_be_removed)
	Removes parameters from propositional variable instantiations in a pbes expression.
std::set< data::variable >	significant_variables (const pbes_expression &x)
const std::vector< utilities::file_format > &	pbes_file_formats ()
void	save_pbes (const pbes &pbes, std::ostream &stream, utilities::file_format format)
	Save a PBES in the format specified.
void	load_pbes (pbes &pbes, std::istream &stream, utilities::file_format format, const std::string &)
	Load a PBES from file.
void	save_pbes (const pbes &pbes, const std::string &filename, utilities::file_format format, bool welltypedness_check)
	save_pbes Saves a PBES to a file.
void	load_pbes (pbes &pbes, const std::string &filename, utilities::file_format format)
	Load pbes from file.
static atermpp::aterm	remove_index_impl (const atermpp::aterm &x)
static atermpp::aterm	add_index_impl (const atermpp::aterm &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 ()
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.
atermpp::aterm	pbes_to_aterm (const pbes &p)
	Conversion to atermappl.
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	pp (const pbes_system::pbes_equation_vector &x, bool arg0)
std::string	pp (const pbes_system::pbes_expression_list &x, bool arg0)
std::string	pp (const pbes_system::pbes_expression_vector &x, bool arg0)
std::string	pp (const pbes_system::propositional_variable_list &x, bool arg0)
std::string	pp (const pbes_system::propositional_variable_vector &x, bool arg0)
std::string	pp (const pbes_system::propositional_variable_instantiation_list &x, bool arg0)
std::string	pp (const pbes_system::propositional_variable_instantiation_vector &x, bool arg0)
std::string	pp (const pbes_system::and_ &x, bool arg0)
std::string	pp (const pbes_system::exists &x, bool arg0)
std::string	pp (const pbes_system::fixpoint_symbol &x, bool arg0)
std::string	pp (const pbes_system::forall &x, bool arg0)
std::string	pp (const pbes_system::imp &x, bool arg0)
std::string	pp (const pbes_system::not_ &x, bool arg0)
std::string	pp (const pbes_system::or_ &x, bool arg0)
std::string	pp (const pbes_system::pbes &x, bool arg0)
std::string	pp (const pbes_system::pbes_equation &x, bool arg0)
std::string	pp (const pbes_system::pbes_expression &x, bool arg0)
std::string	pp (const pbes_system::propositional_variable &x, bool arg0)
std::string	pp (const pbes_system::propositional_variable_instantiation &x, bool arg0)
void	normalize_sorts (pbes_system::pbes_equation_vector &x, const data::sort_specification &sortspec)
void	normalize_sorts (pbes_system::pbes &x, const data::sort_specification &)
pbes_system::pbes_expression	normalize_sorts (const pbes_system::pbes_expression &x, const data::sort_specification &sortspec)
void	translate_user_notation (pbes_system::pbes &x)
pbes_system::pbes_expression	translate_user_notation (const pbes_system::pbes_expression &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::variable >	find_free_variables (const pbes_system::pbes_expression &x)
std::set< data::variable >	find_free_variables (const pbes_system::pbes_equation &x)
std::set< data::function_symbol >	find_function_symbols (const pbes_system::pbes &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)
bool	search_variable (const pbes_system::pbes_expression &x, const data::variable &v)
bool	is_well_typed (const pbes_equation &eqn)
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)
template<typename T >
bool	is_bes (const T &x)
	Returns true if a PBES object is in BES form.
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, bool precedence_aware=true)
	Returns a string representation of the object x.
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	translate_user_notation (T &x)
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	translate_user_notation (const T &x)
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.
void	save_bes_pgsolver (const pbes &bes, std::ostream &stream, bool maxpg)
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 ()
utilities::file_format	guess_format (const std::string &filename)
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)
void	make_standard_form (pbes &eqn, bool recursive_form=false)
	Transforms a PBES into standard form.
template<class... ARGUMENTS>
void	make_propositional_variable (atermpp::aterm &t, const ARGUMENTS &... args)
bool	is_propositional_variable (const atermpp::aterm &x)
std::ostream &	operator<< (std::ostream &out, const propositional_variable &x)
void	swap (propositional_variable &t1, propositional_variable &t2) noexcept
	\brief swap overload
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	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.
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.
std::string	to_string (const var_choice_strategy &strategy)
std::ostream &	operator<< (std::ostream &os, const var_choice_strategy &strategy)
std::istream &	operator>> (std::istream &is, var_choice_strategy &strategy)
bool	needs_ruling_relation (const pbescegps_options &options)
ruling_relation_type	compute_ruling_relation (const pbes &p, const data::rewriter &datar)
template<typename T >
std::string	pfnf_pp (const T &x, bool precedence_aware=true)
	Returns a PFNF string representation of the object x.
template<bool allow_ce>
detail::pre_srf_pbes< allow_ce >	split_conditions (const detail::pre_srf_pbes< allow_ce > &pbes, std::size_t granularity)
	Splits SRF summand conditions to reduce their dependencies.
void	eqelm (pbes &p, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type, bool ignore_initial_state=false)
	Apply the eqelm algorithm.
bool	solve_structure_graph_with_evidence_lts (structure_graph &G, const lps::specification &lpsspec, const pbes &p, const pbes_equation_index &p_index, data::rewrite_strategy strategy, lts::lts_type format, const std::string &filename)
	Solve this pbes_system using a structure graph, directly writing the evidence as an LTS.
template<typename T , typename OutputIterator >
void	find_all_variables (const T &x, OutputIterator o)
	Writes all variables that occur in an object to an output iterator.
template<typename T >
std::set< data::variable >	find_all_variables (const T &x)
	Returns all variables that occur in an object.
template<typename T , typename OutputIterator >
void	find_free_variables (const T &x, OutputIterator o)
	Writes all free variables that occur in an object to an output iterator.
template<typename T , typename OutputIterator , typename VariableContainer >
void	find_free_variables_with_bound (const T &x, OutputIterator o, const VariableContainer &bound)
	Writes all free variables that occur in an object to an output iterator.
template<typename T >
std::set< data::variable >	find_free_variables (const T &x)
	Returns all free variables that occur in an object.
template<typename T , typename VariableContainer >
std::set< data::variable >	find_free_variables_with_bound (const T &x, VariableContainer const &bound)
	Returns all free variables that occur in an object.
template<typename T , typename OutputIterator >
void	find_identifiers (const T &x, OutputIterator o)
	Writes all identifiers that occur in an object to an output iterator.
template<typename T >
std::set< core::identifier_string >	find_identifiers (const T &x)
	Returns all identifiers that occur in an object.
template<typename T , typename OutputIterator >
void	find_sort_expressions (const T &x, OutputIterator o)
	Writes all sort expressions that occur in an object to an output iterator.
template<typename T >
std::set< data::sort_expression >	find_sort_expressions (const T &x)
	Returns all sort expressions that occur in an object.
template<typename T , typename OutputIterator >
void	find_function_symbols (const T &x, OutputIterator o)
	Writes all function symbols that occur in an object to an output iterator.
template<typename T >
std::set< data::function_symbol >	find_function_symbols (const T &x)
	Returns all function symbols that occur in an object.
template<typename Container , typename OutputIterator >
void	find_propositional_variable_instantiations (Container const &container, OutputIterator o)
	Writes all propositional variable instantiations that occur in a range of expressions to an output iterator.
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::ostream &	operator<< (std::ostream &out, const fixpoint_symbol &x)
void	swap (fixpoint_symbol &t1, fixpoint_symbol &t2) noexcept
	\brief swap overload
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.
pbes	lps2pbes (const lps::stochastic_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 &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::stochastic_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.
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	normalize_sorts (T &x, const data::sort_specification &sortspec)
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	normalize_sorts (const T &x, const data::sort_specification &sortspec)
void	parelm (pbes &p, bool ignore_cex)
	Apply the parelm algorithm.
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::ostream &	operator<< (std::ostream &out, const pbes &x)
bool	operator== (const pbes &p1, const pbes &p2)
	Equality operator on PBESs.
atermpp::aterm	pbes_equation_to_aterm (const pbes_equation &eqn)
	Conversion to atermaPpl.
bool	has_propositional_variables (const pbes_expression &x)
std::ostream &	operator<< (std::ostream &out, const pbes_equation &x)
void	swap (pbes_equation &t1, pbes_equation &t2) noexcept
	\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)
std::ostream &	operator<< (std::ostream &out, const pbes_equation_index &index)
bool	is_propositional_variable_instantiation (const atermpp::aterm &x)
bool	is_not (const atermpp::aterm &x)
bool	is_and (const atermpp::aterm &x)
bool	is_or (const atermpp::aterm &x)
bool	is_imp (const atermpp::aterm &x)
bool	is_forall (const atermpp::aterm &x)
bool	is_exists (const atermpp::aterm &x)
bool	is_pbes_expression (const atermpp::aterm &x)
std::ostream &	operator<< (std::ostream &out, const pbes_expression &x)
void	swap (pbes_expression &t1, pbes_expression &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_propositional_variable_instantiation (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const propositional_variable_instantiation &x)
void	swap (propositional_variable_instantiation &t1, propositional_variable_instantiation &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_not (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const not_ &x)
void	swap (not_ &t1, not_ &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_and (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const and_ &x)
void	swap (and_ &t1, and_ &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_or (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const or_ &x)
void	swap (or_ &t1, or_ &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_imp (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const imp &x)
void	swap (imp &t1, imp &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_forall (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const forall &x)
void	swap (forall &t1, forall &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_exists (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const exists &x)
void	swap (exists &t1, exists &t2) noexcept
	\brief swap overload
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.
void	make_optimized_not (pbes_expression &result, const pbes_expression &p)
	Make a negation.
pbes_expression	optimized_not (const pbes_expression &p)
	Make a negation.
void	make_optimized_and (pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
	Make a conjunction.
pbes_expression	optimized_and (const pbes_expression &p, const pbes_expression &q)
	Make a conjunction.
void	make_optimized_or (pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
	Make a disjunction.
pbes_expression	optimized_or (const pbes_expression &p, const pbes_expression &q)
	Make a disjunction.
void	make_optimized_imp (pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
	Make an implication.
pbes_expression	optimized_imp (const pbes_expression &p, const pbes_expression &q)
	Make a disjunction.
void	make_optimized_forall (pbes_expression &result, const data::variable_list &l, const pbes_expression &p, bool remove_variables=false)
	Make a universal quantification If l is empty, p is returned.
pbes_expression	optimized_forall (const data::variable_list &l, const pbes_expression &p, bool remove_variables=false)
	Make a universal quantification If l is empty, p is returned.
void	make_optimized_exists (pbes_expression &result, const data::variable_list &l, const pbes_expression &p, bool remove_variables=false)
	Make an optimized existential quantification. If l is empty, p is returned.
pbes_expression	optimized_exists (const data::variable_list &l, const pbes_expression &p, bool remove_variables=false)
	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, bool allow_counter_example_propvar)
	Determines if an expression is a simple expression. An expression is simple if it is free of propositional variables.
template<typename T >
bool	is_simple_expression_with_cache (const T &x, bool allow_counter_example_propvar, std::map< pbes_expression, bool > &cache_true, std::map< pbes_expression, bool > &cache_false)
	Determines if an expression is a simple expression using a cache. 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)
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)
std::ostream &	operator<< (std::ostream &out, const pbesinst_lazy_todo &todo)
propositional_variable_instantiation	rewrite_PVI (const propositional_variable_instantiation PVI, const std::unordered_map< std::string, std::set< int > > R)
	For a given X(e) and set of redundant params R, returns a copy of X(e) without redundancy.
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::istream &	operator>> (std::istream &is, partial_solve_strategy &strategy)
std::ostream &	operator<< (std::ostream &os, const partial_solve_strategy &strategy)
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.
void	quantifier_propagate (pbes &p)
pbes	quantifier_propagate (const pbes &p)
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 , typename Substitution > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_sort_expressions (T &x, const Substitution &sigma, bool innermost)
template<typename T , typename Substitution > requires std::is_base_of_v<atermpp::aterm, T>
T	replace_sort_expressions (const T &x, const Substitution &sigma, bool innermost)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_data_expressions (T &x, const Substitution &sigma, bool innermost)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_data_expressions (const T &x, const Substitution &sigma, bool innermost)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables (T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables (const T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_all_variables (T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_all_variables (const T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_free_variables (T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_free_variables (const T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution, typename VariableContainer > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_free_variables (T &x, const Substitution &sigma, const VariableContainer &bound_variables)
template<typename T , data::IsSubstitution Substitution, typename VariableContainer > requires std::is_base_of_v<atermpp::aterm, T>
T	replace_free_variables (const T &x, const Substitution &sigma, const VariableContainer &bound_variables)
template<typename T , typename Substitution > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_propositional_variables (T &x, const Substitution &sigma)
	Applies a propositional variable substitution.
template<typename T , typename Substitution > requires (std::is_base_of_v<atermpp::aterm, T>)
T	replace_propositional_variables (const T &x, const Substitution &sigma)
	Applies a propositional variable substitution.
template<typename T , typename Substitution > requires (std::is_base_of_v<atermpp::aterm, T>)
void	replace_propositional_variables (T &result, const T &x, const Substitution &sigma)
	Applies a propositional variable substitution.
template<typename T , typename Substitution > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_pbes_expressions (T &x, const Substitution &sigma, bool innermost=true)
template<typename T , typename Substitution > requires (std::is_base_of_v<atermpp::aterm, T>)
T	replace_pbes_expressions (const T &x, const Substitution &sigma, bool innermost=true)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables_capture_avoiding (T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables_capture_avoiding (T &x, Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma)
template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables_capture_avoiding_with_an_identifier_generator (T &x, Substitution &sigma, IdentifierGenerator &id_generator)
template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator > requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables_capture_avoiding_with_an_identifier_generator (const T &x, Substitution &sigma, IdentifierGenerator &id_generator)
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_constants_by_variables (T &x, const data::rewriter &r, data::mutable_indexed_substitution<> &sigma)
	Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times.
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	replace_constants_by_variables (const T &x, const data::rewriter &r, data::mutable_indexed_substitution<> &sigma)
	Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times.
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)
template<bool allow_ce>
void	resolve_summand_variable_name_clashes (detail::pre_srf_pbes< allow_ce > &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 > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	rewrite (T &x, Rewriter R)
template<typename T , typename Rewriter > requires std::is_base_of_v<atermpp::aterm, T>
T	rewrite (const T &x, Rewriter R)
template<typename T , typename Rewriter , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	rewrite (T &x, Rewriter R, const Substitution &sigma)
template<typename T , typename Rewriter , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	rewrite (const T &x, Rewriter R, const Substitution &sigma)
template<typename T , typename Rewriter > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	pbes_rewrite (T &x, const Rewriter &R)
	Rewrites all embedded pbes expressions in an object x.
template<typename T , typename Rewriter > requires (std::is_base_of_v<atermpp::aterm, T>)
T	pbes_rewrite (const T &x, const Rewriter &R)
	Rewrites all embedded pbes expressions in an object x.
template<typename T , typename Rewriter , typename Substitution > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	pbes_rewrite (T &x, const Rewriter &R, Substitution sigma)
	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 > requires (std::is_base_of_v<atermpp::aterm, T>)
T	pbes_rewrite (const T &x, const Rewriter &R, Substitution sigma)
	Rewrites all embedded pbes expressions in an object x, and applies a substitution to variables on the fly.
template<typename Container , typename Value >
bool	contains (const Container &c, const Value &v)
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::ostream &	operator<< (std::ostream &out, const simple_structure_graph &G)
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	solve_structure_graph (structure_graph &G, std::size_t &calculation_steps, bool check_strategy=false)
bool	solve_structure_graph (structure_graph &G, bool check_strategy=false)
std::pair< bool, std::unordered_map< pbes_expression, structure_graph::index_type > >	solve_structure_graph_winning_mapping (structure_graph &G, bool check_strategy=false)
	Returns a mapping from PBES variable instantations to vertices in the structure graph for vertices won by player alpha.
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.
srf_pbes	simplify_srf_pbes (const srf_pbes &p)
	Simplifies a PBES in standard recursive form (SRF) by removing summands whose condition simplifies to true or false.
srf_pbes	pre_srf2srfpbes (const srf_pbes_with_ce &p)
	Converts a pre-SRF PBES into standard recursive form. Note that the counter example information of the pre_srf_pbes is removed since otherwise the result is not in SRF. The result is simplified using simplify_srf_pbes.
srf_pbes_with_ce	pbes2pre_srf (const pbes &p, bool merge_simple_expressions=true)
	Converts a PBES into pre standard recursive form.
srf_pbes	pbes2srf (const pbes &p, bool merge_simple_expressions=true)
	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	save_structure_graph (const structure_graph &G, std::ostream &out)
	Writes a structure graph to a stream in binary aterm format.
void	save_structure_graph (const structure_graph &G, const std::string &filename)
	Writes a structure graph to a file in binary aterm format.
structure_graph	load_structure_graph (std::istream &in)
	Reads a structure graph from a stream in binary aterm format.
structure_graph	load_structure_graph (const std::string &filename)
	Reads a structure graph from a file in binary aterm format.
std::function< pbes_expression(const propositional_variable_instantiation &)>	compose_substitutions (const std::function< pbes_expression(const propositional_variable_instantiation &)> sigma1, const std::function< pbes_expression(const propositional_variable_instantiation &)> sigma2)
void	self_substitute (pbes_equation &equation, substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &substituter)
void	substitute (pbes_equation &into, const pbes_equation &by, substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &substituter)
std::string	structure_graph_temp_path ()
bool	pbescegps (const std::string &input_filename, const utilities::file_format &input_format, const pbescegps_options options)
template<typename Container >
std::vector< propositional_variable_instantiation >	get_propositional_variable_instantiations (Container const &container)
	Returns all data variables that occur in a range of expressions.
template<typename Func >
auto	measure_time (timing_tracker &timer, const std::string &name, Func &&func)
	Generic decorator to wrap any function call with timing measurements.
pbes_expression	simplify_expr (pbes_expression &phi, rewrite_if_builder< pbes_system::pbes_expression_builder > &if_substituter, simplify_data_rewriter< data::rewriter > &pbes_rewriter)
bool	is_quantifier_free (pbes_expression &phi, pbeschain_options options)
bool	is_not_too_big (pbeschain_options &options, propositional_variable_instantiation &cur_x, pbes_expression &phi)
bool	is_avoiding_alternation (const pbeschain_options &options, const propositional_variable_instantiation &new_x, const pbes_equation &eq)
void	log_number_pvi (std::size_t &initial_size, std::size_t &current_size)
void	self_substitute (pbes_equation &equation, std::size_t initial_size, substitute_propositional_variables_for_true_false_builder< pbes_system::pbes_expression_builder > &pvi_substituter, rewrite_if_builder< pbes_system::pbes_expression_builder > &if_substituter, simplify_data_rewriter< data::rewriter > &pbes_rewriter, simplify_data_rewriter< data::rewriter > &pbes_default_rewriter, pbeschain_options options)
pbes	fill_pvi (pbes &p, data::rewriter data_rewriter)
pbes	tosrf (pbes_system::pbes pbesspec, bool split_srf_conditions=false)
void	pbeschain (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, pbeschain_options options)
std::string	encode_abstracted_set (const std::vector< abstractable_parameter > &universe, const std::vector< std::size_t > &set)
std::vector< std::size_t >	decode_abstracted_set (const std::string &text, const std::vector< abstractable_parameter > &universe)
std::string	to_token (abstraction_set_verdict verdict)
std::optional< abstraction_set_verdict >	from_token (const std::string &token)
std::string	outcome_token (const check_outcome &outcome)
check_outcome	outcome_from_token (const std::string &token)
bool	is_not_closed (const check_outcome &outcome)
std::size_t	pbesfindabs (const std::string &input_filename, const utilities::file_format &input_format, const pbesfindabs_options &options)
	Enumerates all valid abstraction sets of the PBES in the input file.
void	pbesfindabs_worker (const std::string &input_filename, const utilities::file_format &input_format, const pbesfindabs_options &options, bool is_overapproximation)
	Runs the worker loop of the tool: reads abstraction sets (by parameter name) from standard input and writes one verdict per line. This is the mode used by the worker processes of the parent run.
void	substitute (pbes_equation &into, const pbes_equation &by, detail::substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &substituter)
data::data_expression	pbestodata (pbes_equation &equation, detail::replace_other_propositional_variables_with_functions_builder< pbes_system::pbes_expression_builder > &replace_substituter)
InvResult	global_invariant_check (pbes_equation &equation, detail::substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &substituter, detail::replace_other_propositional_variables_with_functions_builder< pbes_system::pbes_expression_builder > &replace_substituter, data::data_specification data_spec, simplify_data_rewriter< data::rewriter > pbes_rewriter, std::set< data::variable > &global_variables)
void	perform_iteration (pbes_equation &equation, detail::substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &substituter, detail::replace_other_propositional_variables_with_functions_builder< pbes_system::pbes_expression_builder > &replace_substituter, data::data_specification data_spec, pbesfixpointsolve_options options, propositional_variable_instantiation initial_state, simplify_data_rewriter< data::rewriter > pbes_rewriter)
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)
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, bool ignore_ce_equations, bool reset)
template<bool allow_ce>
void	unify_parameters (detail::pre_srf_pbes< allow_ce > &p, bool ignore_ce_equations, bool reset)
	See unify_parameters(pbes&, bool, bool) for a description of the parameters.
bool	has_unified_parameters (const pbes &pbes)
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

check_outcome

using mcrl2::pbes_system::check_outcome = typedef std::variant<abstraction_set_verdict, skipped_t>

The outcome of checking one candidate set: a verdict, or skipped.

Definition at line 65 of file pbesfindabs.h.

fixpoint_symbol_list

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

\brief list of fixpoint_symbols

Definition at line 75 of file fixpoint_symbol.h.

fixpoint_symbol_vector

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

\brief vector of fixpoint_symbols

Definition at line 78 of file fixpoint_symbol.h.

identifier_t

using mcrl2::pbes_system::identifier_t = typedef unsigned long long

Definition at line 32 of file pg_parse.h.

owner_t

using mcrl2::pbes_system::owner_t = typedef bool

Definition at line 35 of file pg_parse.h.

pbes_equation_list

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

\brief list of pbes_equations

Definition at line 137 of file pbes_equation.h.

pbes_equation_vector

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

\brief vector of pbes_equations

Definition at line 140 of file pbes_equation.h.

pbes_expression_list

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

\brief list of pbes_expressions

Definition at line 58 of file pbes_expression.h.

pbes_expression_vector

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

\brief vector of pbes_expressions

Definition at line 61 of file pbes_expression.h.

pbesinst_index_map

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

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

Definition at line 29 of file pbesinst_finite_algorithm.h.

pbesinst_variable_map

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

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

Definition at line 32 of file pbesinst_finite_algorithm.h.

priority_t

using mcrl2::pbes_system::priority_t = typedef unsigned short

Definition at line 33 of file pg_parse.h.

propositional_variable_instantiation_list

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

\brief list of propositional_variable_instantiations

Definition at line 180 of file pbes_expression.h.

propositional_variable_instantiation_vector

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

\brief vector of propositional_variable_instantiations

Definition at line 183 of file pbes_expression.h.

propositional_variable_list

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

\brief list of propositional_variables

Definition at line 86 of file propositional_variable.h.

propositional_variable_vector

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

\brief vector of propositional_variables

Definition at line 89 of file propositional_variable.h.

srf_equation

using mcrl2::pbes_system::srf_equation = typedef detail::pre_srf_equation<false>

Definition at line 921 of file srf_pbes.h.

srf_pbes

using mcrl2::pbes_system::srf_pbes = typedef detail::pre_srf_pbes<false>

This is a PBES in SRF format.

Definition at line 924 of file srf_pbes.h.

srf_pbes_with_ce

using mcrl2::pbes_system::srf_pbes_with_ce = typedef detail::pre_srf_pbes<true>

This is a PBES in pre-SRF format, where counter example expressions, i.e., propositional variables are allowed in simple expressions.

Definition at line 928 of file srf_pbes.h.

srf_summand

using mcrl2::pbes_system::srf_summand = typedef detail::pre_srf_summand<false>

Definition at line 919 of file srf_pbes.h.

summand_set

using mcrl2::pbes_system::summand_set = typedef boost::dynamic_bitset<>

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 21 of file pgsolver.cpp.

Enumeration Type Documentation

absinthe_strategy

enum class mcrl2::pbes_system::absinthe_strategy

strong

The approximation strategies of the absinthe tool.

Enumerator
absinthe_over
absinthe_under

Definition at line 21 of file absinthe_strategy.h.

abstraction_set_verdict

enum class mcrl2::pbes_system::abstraction_set_verdict

strong

The verdict of checking a single candidate abstraction set.

Enumerator
valid
not_closed
blocked

Definition at line 51 of file pbesfindabs.h.

bisimulation_type

enum class mcrl2::pbes_system::bisimulation_type

strong

An enumerated type for the available bisimulation types.

Enumerator
strong_bisim
weak_bisim
branching_bisim
branching_sim

Definition at line 21 of file bisimulation_type.h.

enumerate_quantifiers_mode

enum class mcrl2::pbes_system::enumerate_quantifiers_mode

strong

Enumerator
expand_finite_sorts
expand_infinite_sorts
expand_infinite_sorts_and_use_data_rewriter

Definition at line 22 of file quantifier_expansion_mode.h.

InvResult

enum class mcrl2::pbes_system::InvResult

strong

Enumerator
INV_TRUE
INV_FALSE
EQ_FALSE

Definition at line 73 of file pbesfixpointsolve.h.

partial_solve_strategy

enum class mcrl2::pbes_system::partial_solve_strategy : int

strong

Enumeration of partial strategies for solving PBESs.

Enumerator
none
no_optimisation
remove_self_loops
propagate_solved_equations_using_substitution
propagate_solved_equations_using_attractor
detect_winning_loops_using_fatal_attractor
solve_subgames_using_fatal_attractor_local
solve_subgames_using_fatal_attractor_original
solve_subgames_using_solver
detect_winning_loops_original

Definition at line 23 of file pbessolve_options.h.

pbes_rewriter_type

enum class mcrl2::pbes_system::pbes_rewriter_type

strong

An enumerated type for the available pbes rewriters.

Enumerator
simplify
quantifier_all
quantifier_finite
quantifier_inside
quantifier_one_point
prover
pfnf
ppg
srf
pre_srf
prune_dataspec
bqnf_quantifier
remove_cex_variables

Definition at line 22 of file pbes_rewriter_type.h.

pbesinst_strategy

enum class mcrl2::pbes_system::pbesinst_strategy

strong

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 class mcrl2::pbes_system::pbespg_solver_type

strong

Enumerator
spm_solver
alternative_spm_solver
recursive_solver
priority_promotion

Definition at line 30 of file pbespgsolve.h.

remove_level

enum class mcrl2::pbes_system::remove_level

strong

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

Enumerator
none
some
all

Definition at line 24 of file remove_level.h.

search_strategy

enum class mcrl2::pbes_system::search_strategy

strong

Search strategy when generating a BES from a PBES.

Enumerator
breadth_first
depth_first
breadth_first_short
depth_first_short

Definition at line 22 of file search_strategy.h.

solution_strategy_t

enum class mcrl2::pbes_system::solution_strategy_t

strong

Enumerator
gauss
small_progr_measures

Definition at line 23 of file solution_strategy.h.

transformation_strategy

enum class mcrl2::pbes_system::transformation_strategy

strong

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 22 of file transformation_strategy.h.

tribool

enum class mcrl2::pbes_system::tribool

strong

Enumerator
no
maybe
yes

Definition at line 196 of file partial_order_reduction.h.

var_choice_strategy

enum class mcrl2::pbes_system::var_choice_strategy

strong

Enumerator
lhs
rhs
count
all
ruling

Definition at line 46 of file pbescegps_utilities.h.

Function Documentation

add_index_impl()

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

static

Definition at line 183 of file io.cpp.

anonymize()

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

inline

Definition at line 79 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 163 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 138 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 170 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 180 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 82 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 46 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 27 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 517 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 888 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 )

inline

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 88 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 307 of file pbes.h.

complps2pbes()

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

inline

Definition at line 23 of file complps2pbes.h.

compose_substitutions()

std::function< pbes_expression(const propositional_variable_instantiation &)> mcrl2::pbes_system::compose_substitutions ( const std::function< pbes_expression(const propositional_variable_instantiation &)>  sigma1, const std::function< pbes_expression(const propositional_variable_instantiation &)>  sigma2  )

inline

Definition at line 203 of file substitutions.h.

compute_ruling_relation()

ruling_relation_type mcrl2::pbes_system::compute_ruling_relation ( const pbes &  p, const data::rewriter &  datar  )

inline

Definition at line 1139 of file pbescegps_utilities.h.

contains()

template<typename Container , typename Value >

bool mcrl2::pbes_system::contains	(	const Container &	c,
		const Value &	v
	)

Definition at line 30 of file abstraction_rewriter.h.

decode_abstracted_set()

std::vector< std::size_t > mcrl2::pbes_system::decode_abstracted_set ( const std::string &  text, const std::vector< abstractable_parameter > &  universe  )

inline

Definition at line 193 of file pbesfindabs.h.

description() [1/9]

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

inline

Prints an absinthe strategy.

Definition at line 84 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 73 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 134 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 76 of file pbespgsolve.h.

description() [6/9]

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

inline

Definition at line 90 of file remove_level.h.

description() [7/9]

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

inline

Definition at line 92 of file search_strategy.h.

description() [8/9]

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

static

Definition at line 85 of file solution_strategy.h.

description() [9/9]

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

inline

Definition at line 107 of file transformation_strategy.h.

encode_abstracted_set()

std::string mcrl2::pbes_system::encode_abstracted_set ( const std::vector< abstractable_parameter > &  universe, const std::vector< std::size_t > &  set  )

inline

Definition at line 178 of file pbesfindabs.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 318 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 102 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 562 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 455 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 500 of file pbessolve_vertex_set.h.

false_()

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

inline

Returns

Returns the value false

Definition at line 688 of file pbes_expression.h.

fill_pvi()

pbes mcrl2::pbes_system::fill_pvi ( pbes &  p, data::rewriter  data_rewriter  )

inline

Definition at line 694 of file pbeschain.h.

find_all_variables() [1/3]

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

(

const pbes_system::pbes &

x

)

Definition at line 52 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

)

Returns all variables that occur in an object.

Parameters

[in]

x

an object containing variables

Returns

All variables that occur in the object x

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

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

Parameters

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

Definition at line 62 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 105 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 53 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 55 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 54 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

)

Returns all free variables that occur in an object.

Parameters

[in]

x

an object containing variables

Returns

All free variables that occur in the object x

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

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

Parameters

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

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

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

Parameters

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

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

Returns all free variables that occur in an object.

Parameters

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

Returns

All free variables that occur in the object x

Definition at line 113 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 56 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

)

Returns all function symbols that occur in an object.

Parameters

[in]

x

an object containing function symbols

Returns

All function symbols that occur in the object x

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

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

Parameters

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

Definition at line 164 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 58 of file pbes.cpp.

find_identifiers() [2/3]

template<typename T >

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

(

const T &

x

)

Returns all identifiers that occur in an object.

Parameters

[in]

x

an object containing identifiers

Returns

All identifiers that occur in the object x

Definition at line 133 of file find.h.

find_identifiers() [3/3]

template<typename T , typename OutputIterator >

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

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

Parameters

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

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

Writes all propositional variable instantiations that occur in a range of expressions to an output iterator.

Parameters

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

Definition at line 186 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 51 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

)

Returns all sort expressions that occur in an object.

Parameters

[in]

x

an object containing sort expressions

Returns

All sort expressions that occur in the object x

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

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

Parameters

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

Definition at line 144 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 191 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 344 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 1062 of file pbes_expression.h.

from_token()

std::optional< abstraction_set_verdict > mcrl2::pbes_system::from_token ( const std::string &  token )

inline

Definition at line 238 of file pbesfindabs.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 119 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 107 of file solve_structure_graph.h.

get_propositional_variable_instantiations()

template<typename Container >

std::vector< propositional_variable_instantiation > mcrl2::pbes_system::get_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 245 of file pbeschain.h.

global_invariant_check()

InvResult mcrl2::pbes_system::global_invariant_check ( pbes_equation &  equation, detail::substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &  substituter, detail::replace_other_propositional_variables_with_functions_builder< pbes_system::pbes_expression_builder > &  replace_substituter, data::data_specification  data_spec, simplify_data_rewriter< data::rewriter >  pbes_rewriter, std::set< data::variable > &  global_variables  )

inline

Definition at line 81 of file pbesfixpointsolve.h.

guess_format()

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

inline

Definition at line 47 of file io.h.

has_propositional_variables()

bool mcrl2::pbes_system::has_propositional_variables

(

const pbes_expression &

x

)

has_unified_parameters()

bool mcrl2::pbes_system::has_unified_parameters ( const pbes &  pbes )

inline

Returns

true iff all PBES equations have the same parameter list.

Definition at line 228 of file unify_parameters.h.

inc()

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

inline

Definition at line 112 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 88 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 121 of file pbessolve_attractors.h.

is_and()

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

inline

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

Definition at line 336 of file pbes_expression.h.

is_avoiding_alternation()

bool mcrl2::pbes_system::is_avoiding_alternation ( const pbeschain_options &  options, const propositional_variable_instantiation &  new_x, const pbes_equation &  eq  )

inline

Definition at line 376 of file pbeschain.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 71 of file is_bes.h.

is_constant()

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

inline

Definition at line 1042 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 786 of file pbes_expression.h.

is_disjunctive()

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

inline

Definition at line 56 of file small_progress_measures.h.

is_exists()

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

inline

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

Definition at line 640 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 706 of file pbes_expression.h.

is_forall()

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

inline

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

Definition at line 564 of file pbes_expression.h.

is_imp()

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

inline

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

Definition at line 488 of file pbes_expression.h.

is_left_associative() [1/4]

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

inline

Definition at line 40 of file print.h.

is_left_associative() [2/4]

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

inline

Definition at line 38 of file print.h.

is_left_associative() [3/4]

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

inline

Definition at line 39 of file print.h.

is_left_associative() [4/4]

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

inline

Definition at line 41 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 141 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 134 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 26 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 227 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 219 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 155 of file normalize.h.

is_not()

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

inline

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

Definition at line 260 of file pbes_expression.h.

is_not_closed()

bool mcrl2::pbes_system::is_not_closed ( const check_outcome &  outcome )

inline

Definition at line 282 of file pbesfindabs.h.

is_not_too_big()

bool mcrl2::pbes_system::is_not_too_big ( pbeschain_options &  options, propositional_variable_instantiation &  cur_x, pbes_expression &  phi  )

inline

Definition at line 370 of file pbeschain.h.

is_or()

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

inline

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

Definition at line 412 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 722 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 754 of file pbes_expression.h.

is_pbes_expression()

bool mcrl2::pbes_system::is_pbes_expression ( const atermpp::aterm &  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 76 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 26 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 746 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 738 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 714 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 730 of file pbes_expression.h.

is_propositional_variable()

bool mcrl2::pbes_system::is_propositional_variable ( const atermpp::aterm &  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 95 of file propositional_variable.h.

is_propositional_variable_instantiation()

bool mcrl2::pbes_system::is_propositional_variable_instantiation ( const atermpp::aterm &  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 189 of file pbes_expression.h.

is_quantifier_free()

bool mcrl2::pbes_system::is_quantifier_free ( pbes_expression &  phi, pbeschain_options  options  )

inline

Definition at line 364 of file pbeschain.h.

is_right_associative() [1/4]

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

inline

Definition at line 51 of file print.h.

is_right_associative() [2/4]

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

inline

Definition at line 49 of file print.h.

is_right_associative() [3/4]

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

inline

Definition at line 50 of file print.h.

is_right_associative() [4/4]

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

inline

Definition at line 52 of file print.h.

is_simple_expression()

template<typename T >

bool mcrl2::pbes_system::is_simple_expression	(	const T &	x,
		bool	allow_counter_example_propvar
	)

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

Parameters

x	a PBES object
allow_counter_example_propvar	If true, counter example propositional variables are seen as simple expressions.

Returns

true if x is a simple expression.

Definition at line 120 of file pbes_functions.h.

is_simple_expression_with_cache()

template<typename T >

bool mcrl2::pbes_system::is_simple_expression_with_cache	(	const T &	x,
		bool	allow_counter_example_propvar,
		std::map< pbes_expression, bool > &	cache_true,
		std::map< pbes_expression, bool > &	cache_false
	)

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

Parameters

x	a PBES object
allow_counter_example_propvar	If true, counter example propositional variables are seen as simple expressions.
cache_true	A cache in which it is stored that expressions are simple when allow_counter_example is true.
cache_false	A cache in which it is stored that expressions are simple when allow_counter_example is false.

Returns

true if x is a simple expression.

Definition at line 204 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 337 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 698 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 770 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 762 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 778 of file pbes_expression.h.

is_well_typed()

bool mcrl2::pbes_system::is_well_typed

(

const pbes_equation &

eqn

)

Definition at line 76 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 81 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 90 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 34 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 24 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 29 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 149 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 83 of file io.cpp.

load_structure_graph() [1/2]

structure_graph mcrl2::pbes_system::load_structure_graph ( const std::string &  filename )

inline

Reads a structure graph from a file in binary aterm format.

Definition at line 185 of file structure_graph_io.h.

load_structure_graph() [2/2]

structure_graph mcrl2::pbes_system::load_structure_graph ( std::istream &  in )

inline

Reads a structure graph from a stream in binary aterm format.

Definition at line 109 of file structure_graph_io.h.

log_number_pvi()

void mcrl2::pbes_system::log_number_pvi ( std::size_t &  initial_size, std::size_t &  current_size  )

inline

Definition at line 381 of file pbeschain.h.

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 358 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 205 of file lps2pbes.h.

lps2pbes() [2/4]

pbes mcrl2::pbes_system::lps2pbes ( const lps::stochastic_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 stochastic 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 157 of file lps2pbes.h.

lps2pbes() [3/4]

pbes mcrl2::pbes_system::lps2pbes ( const lps::stochastic_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 240 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 270 of file lps2pbes.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 98 of file lts2pbes.h.

make_and()

template<class... ARGUMENTS>

void mcrl2::pbes_system::make_and ( atermpp::aterm &  t, const ARGUMENTS &...  args  )

inline

\brief The function make_and constructs a new term into a given address. \

Parameters

t	The reference into which the new and is constructed.

Definition at line 327 of file pbes_expression.h.

make_exists()

template<class... ARGUMENTS>

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

inline

\brief The function make_exists constructs a new term into a given address. \

Parameters

t	The reference into which the new exists is constructed.

Definition at line 631 of file pbes_expression.h.

make_forall()

template<class... ARGUMENTS>

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

inline

\brief The function make_forall constructs a new term into a given address. \

Parameters

t	The reference into which the new forall is constructed.

Definition at line 555 of file pbes_expression.h.

make_imp()

template<class... ARGUMENTS>

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

inline

\brief The function make_imp constructs a new term into a given address. \

Parameters

t	The reference into which the new imp is constructed.

Definition at line 479 of file pbes_expression.h.

make_not()

template<class... ARGUMENTS>

void mcrl2::pbes_system::make_not ( atermpp::aterm &  t, const ARGUMENTS &...  args  )

inline

\brief The function make_not constructs a new term into a given address. \

Parameters

t	The reference into which the new not is constructed.

Definition at line 251 of file pbes_expression.h.

make_optimized_and()

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

inline

Make a conjunction.

Parameters

result	Placeholder for the resulting PBES expression p && q. This is more efficient than delivering it as the result of a function.
p	A PBES expression
q	A PBES expression

Postcondition

result is the optimized negation of !p

Definition at line 937 of file pbes_expression.h.

make_optimized_exists()

void mcrl2::pbes_system::make_optimized_exists ( pbes_expression &  result, const data::variable_list &  l, const pbes_expression &  p, bool  remove_variables = false  )

inline

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

Parameters

result	The placeholder to which the optimised existential quantification is assigned.
l	A sequence of data variables
p	A PBES expression
remove_variables	If true variables not occurring in p will be removed. This requires complexity in the size of p.

Definition at line 1024 of file pbes_expression.h.

make_optimized_forall()

void mcrl2::pbes_system::make_optimized_forall ( pbes_expression &  result, const data::variable_list &  l, const pbes_expression &  p, bool  remove_variables = false  )

inline

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

Parameters

result	The placeholder to which the optimised existential quantification is assigned.
l	A sequence of data variables
p	A PBES expression
remove_variables	If true variables not occurring in p will be removed. This requires complexity in the size of p.

Postcondition

result is the optimized universal quantification forall l.p

Definition at line 1001 of file pbes_expression.h.

make_optimized_imp()

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

inline

Make an implication.

Parameters

result	Placeholder for the resulting PBES expression p => q. This is more efficient than delivering it as the result of a function.
p	A PBES expression
q	A PBES expression

Definition at line 978 of file pbes_expression.h.

make_optimized_not()

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

inline

Make a negation.

Parameters

result	Placeholder for the resulting PBES expression !p. This is more efficient than delivering it as the result of a function.
p	A PBES expression

Definition at line 917 of file pbes_expression.h.

make_optimized_or()

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

inline

Make a disjunction.

Parameters

result	Placeholder for the resulting PBES expression p || q. This is more efficient than delivering it as the result of a function.
p	A PBES expression
q	A PBES expression

Definition at line 957 of file pbes_expression.h.

make_or()

template<class... ARGUMENTS>

void mcrl2::pbes_system::make_or ( atermpp::aterm &  t, const ARGUMENTS &...  args  )

inline

\brief The function make_or constructs a new term into a given address. \

Parameters

t	The reference into which the new or is constructed.

Definition at line 403 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 109 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 31 of file pbesinst_algorithm.h.

make_propositional_variable()

template<class... ARGUMENTS>

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

inline

\brief The function 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 80 of file propositional_variable.h.

make_propositional_variable_instantiation()

template<class... ARGUMENTS>

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

inline

\brief The function 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 174 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 281 of file normal_forms.h.

maximum_rank()

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

inline

Definition at line 62 of file small_progress_measures.h.

measure_time()

template<typename Func >

auto mcrl2::pbes_system::measure_time ( timing_tracker &  timer, const std::string &  name, Func &&  func  )

inline

Generic decorator to wrap any function call with timing measurements.

Definition at line 339 of file pbeschain.h.

needs_ruling_relation()

bool mcrl2::pbes_system::needs_ruling_relation ( const pbescegps_options &  options )

inline

Definition at line 129 of file pbescegps_utilities.h.

normalize() [1/2]

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

T mcrl2::pbes_system::normalize

(

const T &

x

)

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

normalize() [2/2]

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

void mcrl2::pbes_system::normalize

(

T &

x

)

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 167 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 48 of file pbes.cpp.

normalize_sorts() [2/5]

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

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

Definition at line 31 of file normalize_sorts.h.

normalize_sorts() [3/5]

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

Definition at line 47 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 46 of file pbes.cpp.

normalize_sorts() [5/5]

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

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

Definition at line 23 of file normalize_sorts.h.

operator!=()

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

inline

Definition at line 171 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 207 of file partial_order_reduction.h.

operator&&() [2/2]

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

inlinestatic

Definition at line 200 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 221 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 193 of file io.cpp.

operator<<() [3/37]

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

inline

Definition at line 76 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 106 of file bisimulation_type.h.

operator<<() [5/37]

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

inline

Definition at line 53 of file pbessolve_options.h.

operator<<() [6/37]

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

inline

Definition at line 188 of file pbes_rewriter_type.h.

operator<<() [7/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<<() [8/37]

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

inline

Definition at line 105 of file pbespgsolve.h.

operator<<() [9/37]

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

inline

Definition at line 83 of file remove_level.h.

operator<<() [10/37]

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

inline

Definition at line 85 of file search_strategy.h.

operator<<() [11/37]

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

static

Definition at line 45 of file solution_strategy.h.

operator<<() [12/37]

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

inline

Definition at line 100 of file transformation_strategy.h.

operator<<() [13/37]

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

inline

Definition at line 73 of file pbescegps_utilities.h.

operator<<() [14/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 349 of file pbes_expression.h.

operator<<() [15/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 653 of file pbes_expression.h.

operator<<() [16/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 88 of file fixpoint_symbol.h.

operator<<() [17/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 577 of file pbes_expression.h.

operator<<() [18/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 501 of file pbes_expression.h.

operator<<() [19/37]

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

inline

Definition at line 331 of file pbessolve_vertex_set.h.

operator<<() [20/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 273 of file pbes_expression.h.

operator<<() [21/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 425 of file pbes_expression.h.

operator<<() [22/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 297 of file pbes.h.

operator<<() [23/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 150 of file pbes_equation.h.

operator<<() [24/37]

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

inline

Definition at line 84 of file pbes_equation_index.h.

operator<<() [25/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 97 of file pbes_expression.h.

operator<<() [26/37]

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

inline

Definition at line 125 of file pbesinst_lazy.h.

operator<<() [27/37]

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

inline

Definition at line 83 of file pbessolve_options.h.

operator<<() [28/37]

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

inline

Definition at line 97 of file small_progress_measures.h.

operator<<() [29/37]

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

inline

Definition at line 178 of file small_progress_measures.h.

operator<<() [30/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 108 of file propositional_variable.h.

operator<<() [31/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 202 of file pbes_expression.h.

operator<<() [32/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<<() [33/37]

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

inline

Definition at line 429 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 327 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 273 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 287 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 270 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 318 of file pbes.h.

operator==() [2/2]

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

inline

Definition at line 163 of file pbes_equation.h.

operator>>() [1/14]

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

Reads a pbes from a stream.

Definition at line 234 of file io.cpp.

operator>>() [2/14]

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

inline

Definition at line 201 of file io.cpp.

operator>>() [3/14]

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 49 of file parse.h.

operator>>() [4/14]

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

inline

Definition at line 60 of file absinthe_strategy.h.

operator>>() [5/14]

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

inline

Definition at line 90 of file bisimulation_type.h.

operator>>() [6/14]

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

inline

Definition at line 37 of file pbessolve_options.h.

operator>>() [7/14]

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 173 of file pbes_rewriter_type.h.

operator>>() [8/14]

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

inline

Definition at line 53 of file pbesinst_strategy.h.

operator>>() [9/14]

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

inline

Definition at line 89 of file pbespgsolve.h.

operator>>() [10/14]

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

inline

Definition at line 67 of file remove_level.h.

operator>>() [11/14]

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

inline

Definition at line 69 of file search_strategy.h.

operator>>() [12/14]

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

static

Definition at line 69 of file solution_strategy.h.

operator>>() [13/14]

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

inline

Definition at line 84 of file transformation_strategy.h.

operator>>() [14/14]

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

inline

Definition at line 78 of file pbescegps_utilities.h.

optimized_and()

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

inline

Make a conjunction.

Parameters

p	A PBES expression
q	A PBES expression

Postcondition

result is the optimized conjunction of p && q

Definition at line 947 of file pbes_expression.h.

optimized_exists()

pbes_expression mcrl2::pbes_system::optimized_exists ( const data::variable_list &  l, const pbes_expression &  p, bool  remove_variables = false  )

inline

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

Parameters

l	A sequence of data variables
p	A PBES expression
remove_variables	If true variables not occurring in p will be removed. This requires complexity in the size of p.

Postcondition

result is the optimized existential quantification exists l.p

Definition at line 1036 of file pbes_expression.h.

optimized_forall()

pbes_expression mcrl2::pbes_system::optimized_forall ( const data::variable_list &  l, const pbes_expression &  p, bool  remove_variables = false  )

inline

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

Parameters

l	A sequence of data variables
p	A PBES expression
remove_variables	If true variables not occurring in p will be removed. This requires complexity in the size of p.

Returns

The value forall l.p

Definition at line 1013 of file pbes_expression.h.

optimized_imp()

pbes_expression mcrl2::pbes_system::optimized_imp ( 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 988 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 112 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 96 of file join.h.

optimized_not()

pbes_expression mcrl2::pbes_system::optimized_not ( const pbes_expression &  p )

inline

Make a negation.

Parameters

p	A PBES expression

Returns

The value !p

Definition at line 926 of file pbes_expression.h.

optimized_or()

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

inline

Make a disjunction.

Parameters

result	Placeholder for the resulting PBES expression p || q. This is more efficient than delivering it as the result of a function.
p	A PBES expression
q	A PBES expression

Returns

The value p || q

Definition at line 968 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 52 of file transformations.h.

outcome_from_token()

check_outcome mcrl2::pbes_system::outcome_from_token ( const std::string &  token )

inline

Definition at line 264 of file pbesfindabs.h.

outcome_token()

std::string mcrl2::pbes_system::outcome_token ( const check_outcome &  outcome )

inline

Definition at line 255 of file pbesfindabs.h.

parelm()

void mcrl2::pbes_system::parelm ( pbes &  p, bool  ignore_cex  )

inline

Apply the parelm algorithm.

Parameters

p	A PBES to which the algorithm is applied

Definition at line 334 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 29 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 31 of file bisimulation_type.h.

parse_pbes() [1/2]

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

inline

Definition at line 56 of file parse.h.

parse_pbes() [2/2]

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

inline

Definition at line 36 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 186 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 82 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 116 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 174 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 40 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 40 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 243 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 235 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 220 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 63 of file parse.h.

parse_remove_level()

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

inline

Definition at line 34 of file remove_level.h.

parse_search_strategy()

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

inline

Definition at line 31 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 52 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 39 of file pbespgsolve.h.

parse_transformation_strategy()

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

inline

Definition at line 46 of file transformation_strategy.h.

pbes2pre_srf()

srf_pbes_with_ce mcrl2::pbes_system::pbes2pre_srf ( const pbes &  p, bool  merge_simple_expressions = true  )

inline

Converts a PBES into pre standard recursive form.

Precondition

The pbes p must be normalized

Definition at line 1064 of file srf_pbes.h.

pbes2srf()

srf_pbes mcrl2::pbes_system::pbes2srf ( const pbes &  p, bool  merge_simple_expressions = true  )

inline

Converts a PBES into standard recursive form.

Precondition

The pbes p must be normalized

Definition at line 1071 of file srf_pbes.h.

pbes_equation_to_aterm()

atermpp::aterm 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 179 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 78 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 27 of file io.cpp.

pbes_format_internal()

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

inline

Definition at line 39 of file io.h.

pbes_format_internal_bes()

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

inline

Definition at line 43 of file io.h.

pbes_format_pgsolver()

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

inline

Definition at line 45 of file io.h.

pbes_format_text()

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

inline

Definition at line 41 of file io.h.

pbes_marker()

atermpp::aterm mcrl2::pbes_system::pbes_marker

(

)

Definition at line 216 of file io.cpp.

pbes_rewrite() [1/4]

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

T mcrl2::pbes_system::pbes_rewrite	(	const T &	x,
		const Rewriter &	R
	)

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

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

T mcrl2::pbes_system::pbes_rewrite	(	const T &	x,
		const Rewriter &	R,
		Substitution	sigma
	)

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

pbes_rewrite() [3/4]

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

void mcrl2::pbes_system::pbes_rewrite	(	T &	x,
		const Rewriter &	R
	)

Rewrites all embedded pbes expressions in an object x.

Parameters

x	an object containing expressions
R	a pbes rewriter

Definition at line 158 of file rewrite.h.

pbes_rewrite() [4/4]

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

void mcrl2::pbes_system::pbes_rewrite	(	T &	x,
		const Rewriter &	R,
		Substitution	sigma
	)

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

pbes_to_aterm()

atermpp::aterm mcrl2::pbes_system::pbes_to_aterm

(

const pbes &

p

)

Conversion to atermappl.

Returns

The PBES converted to aterm format.

Definition at line 315 of file io.cpp.

pbescegps()

bool mcrl2::pbes_system::pbescegps ( const std::string &  input_filename, const utilities::file_format &  input_format, const pbescegps_options  options  )

inline

Definition at line 1016 of file pbescegps.h.

pbeschain()

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

inline

Definition at line 895 of file pbeschain.h.

pbesfindabs()

std::size_t mcrl2::pbes_system::pbesfindabs ( const std::string &  input_filename, const utilities::file_format &  input_format, const pbesfindabs_options &  options  )

inline

Enumerates all valid abstraction sets of the PBES in the input file.

Parameters

input_filename	The file containing the PBES.
input_format	The format of the input file.
options	The options of the tool.

Returns

The number of valid abstraction sets found.

Definition at line 943 of file pbesfindabs.h.

pbesfindabs_worker()

void mcrl2::pbes_system::pbesfindabs_worker ( const std::string &  input_filename, const utilities::file_format &  input_format, const pbesfindabs_options &  options, bool  is_overapproximation  )

inline

Runs the worker loop of the tool: reads abstraction sets (by parameter name) from standard input and writes one verdict per line. This is the mode used by the worker processes of the parent run.

Definition at line 958 of file pbesfindabs.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 409 of file pbesinst_finite_algorithm.h.

pbesinst_is_constant()

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

inline

Definition at line 43 of file pbesinst_algorithm.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 248 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 259 of file pbespgsolve.h.

pbestodata()

data::data_expression mcrl2::pbes_system::pbestodata ( pbes_equation &  equation, detail::replace_other_propositional_variables_with_functions_builder< pbes_system::pbes_expression_builder > &  replace_substituter  )

inline

Definition at line 57 of file pbesfixpointsolve.h.

perform_iteration()

void mcrl2::pbes_system::perform_iteration ( pbes_equation &  equation, detail::substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &  substituter, detail::replace_other_propositional_variables_with_functions_builder< pbes_system::pbes_expression_builder > &  replace_substituter, data::data_specification  data_spec, pbesfixpointsolve_options  options, propositional_variable_instantiation  initial_state, simplify_data_rewriter< data::rewriter >  pbes_rewriter  )

inline

Definition at line 222 of file pbesfixpointsolve.h.

pfnf_pp()

template<typename T >

std::string mcrl2::pbes_system::pfnf_pp	(	const T &	x,
		bool	precedence_aware = true
	)

Returns a PFNF string representation of the object x.

Definition at line 147 of file pfnf_print.h.

pp() [1/21]

std::string mcrl2::pbes_system::pp

(

const pbes_equation_vector &

x

)

pp() [2/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::and_ &	x,
		bool	arg0 = true
	)

Definition at line 34 of file pbes.cpp.

pp() [3/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::exists &	x,
		bool	arg0 = true
	)

Definition at line 35 of file pbes.cpp.

pp() [4/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::fixpoint_symbol &	x,
		bool	arg0 = true
	)

Definition at line 36 of file pbes.cpp.

pp() [5/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::forall &	x,
		bool	arg0 = true
	)

Definition at line 37 of file pbes.cpp.

pp() [6/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::imp &	x,
		bool	arg0 = true
	)

Definition at line 38 of file pbes.cpp.

pp() [7/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::not_ &	x,
		bool	arg0 = true
	)

Definition at line 39 of file pbes.cpp.

pp() [8/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::or_ &	x,
		bool	arg0 = true
	)

Definition at line 40 of file pbes.cpp.

pp() [9/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::pbes &	x,
		bool	arg0 = true
	)

Definition at line 41 of file pbes.cpp.

pp() [10/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::pbes_equation &	x,
		bool	arg0 = true
	)

Definition at line 42 of file pbes.cpp.

pp() [11/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::pbes_equation_vector &	x,
		bool	arg0
	)

Definition at line 27 of file pbes.cpp.

pp() [12/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::pbes_expression &	x,
		bool	arg0 = true
	)

Definition at line 43 of file pbes.cpp.

pp() [13/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::pbes_expression_list &	x,
		bool	arg0 = true
	)

Definition at line 28 of file pbes.cpp.

pp() [14/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::pbes_expression_vector &	x,
		bool	arg0 = true
	)

Definition at line 29 of file pbes.cpp.

pp() [15/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::propositional_variable &	x,
		bool	arg0 = true
	)

Definition at line 44 of file pbes.cpp.

pp() [16/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::propositional_variable_instantiation &	x,
		bool	arg0 = true
	)

Definition at line 45 of file pbes.cpp.

pp() [17/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::propositional_variable_instantiation_list &	x,
		bool	arg0 = true
	)

Definition at line 32 of file pbes.cpp.

pp() [18/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::propositional_variable_instantiation_vector &	x,
		bool	arg0 = true
	)

Definition at line 33 of file pbes.cpp.

pp() [19/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::propositional_variable_list &	x,
		bool	arg0 = true
	)

Definition at line 30 of file pbes.cpp.

pp() [20/21]

std::string mcrl2::pbes_system::pp	(	const pbes_system::propositional_variable_vector &	x,
		bool	arg0 = true
	)

Definition at line 31 of file pbes.cpp.

pp() [21/21]

template<typename T >

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

Returns a string representation of the object x.

Definition at line 253 of file print.h.

pre_srf2srfpbes()

srf_pbes mcrl2::pbes_system::pre_srf2srfpbes ( const srf_pbes_with_ce &  p )

inline

Converts a pre-SRF PBES into standard recursive form. Note that the counter example information of the pre_srf_pbes is removed since otherwise the result is not in SRF. The result is simplified using simplify_srf_pbes.

Definition at line 1028 of file srf_pbes.h.

precedence() [1/7]

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

inlineconstexpr

Definition at line 24 of file print.h.

precedence() [2/7]

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

inlineconstexpr

Definition at line 21 of file print.h.

precedence() [3/7]

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

inlineconstexpr

Definition at line 20 of file print.h.

precedence() [4/7]

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

inlineconstexpr

Definition at line 22 of file print.h.

precedence() [5/7]

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

inlineconstexpr

Definition at line 25 of file print.h.

precedence() [6/7]

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

inlineconstexpr

Definition at line 23 of file print.h.

precedence() [7/7]

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

inline

Definition at line 26 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 62 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 114 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 47 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 55 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 70 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 98 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 55 of file remove_level.h.

print_search_strategy()

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

inline

Definition at line 56 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 435 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 300 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 42 of file absinthe.h.

print_term()

template<typename Term >

std::string mcrl2::pbes_system::print_term

(

const Term &

x

)

Definition at line 36 of file absinthe.h.

print_transformation_strategy()

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

inline

Definition at line 71 of file transformation_strategy.h.

quantifier_propagate() [1/2]

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

inline

Definition at line 403 of file quantifier_propagate.h.

quantifier_propagate() [2/2]

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

inline

Definition at line 374 of file quantifier_propagate.h.

quantifier_variables()

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

inline

Definition at line 1048 of file pbes_expression.h.

reachable_variables()

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

inline

Definition at line 44 of file remove_equations.h.

remove_index_impl()

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

static

Definition at line 173 of file io.cpp.

remove_parameters() [1/6]

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

T mcrl2::pbes_system::remove_parameters	(	const T &	x,
		const std::map< core::identifier_string, std::vector< std::size_t > > &	to_be_removed
	)

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters

x	A PBES library object that derives from atermpp::aterm
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 204 of file remove_parameters.h.

remove_parameters() [2/6]

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

T mcrl2::pbes_system::remove_parameters	(	const T &	x,
		const std::set< data::variable > &	to_be_removed
	)

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters

x	A PBES library object that derives from atermpp::aterm
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 312 of file remove_parameters.h.

remove_parameters() [3/6]

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

T mcrl2::pbes_system::remove_parameters	(	const T &	x,
		const std::vector< std::size_t > &	to_be_removed
	)

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters

x	A PBES library object that derives from atermpp::aterm
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 105 of file remove_parameters.h.

remove_parameters() [4/6]

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

void mcrl2::pbes_system::remove_parameters	(	T &	x,
		const std::map< core::identifier_string, std::vector< std::size_t > > &	to_be_removed
	)

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters

x	A PBES library object that does not derive from atermpp::aterm
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 219 of file remove_parameters.h.

remove_parameters() [5/6]

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

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

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters

x	A PBES library object that does not derive from atermpp::aterm
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 326 of file remove_parameters.h.

remove_parameters() [6/6]

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

void mcrl2::pbes_system::remove_parameters	(	T &	x,
		const std::vector< std::size_t > &	to_be_removed
	)

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters

x	A PBES library object that does not derive from atermpp::aterm
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 119 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 88 of file remove_equations.h.

replace_all_variables() [1/2]

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

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

Definition at line 167 of file replace.h.

replace_all_variables() [2/2]

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

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

Definition at line 158 of file replace.h.

replace_constants_by_variables() [1/2]

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

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

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

Definition at line 53 of file replace_constants_by_variables.h.

replace_constants_by_variables() [2/2]

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

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

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

Definition at line 40 of file replace_constants_by_variables.h.

replace_data_expressions() [1/2]

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

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

Definition at line 124 of file replace.h.

replace_data_expressions() [2/2]

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

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

Definition at line 114 of file replace.h.

replace_free_variables() [1/4]

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

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

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

Definition at line 192 of file replace.h.

replace_free_variables() [2/4]

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

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

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

Definition at line 219 of file replace.h.

replace_free_variables() [3/4]

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

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

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

Definition at line 180 of file replace.h.

replace_free_variables() [4/4]

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

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

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

Definition at line 206 of file replace.h.

replace_pbes_expressions() [1/2]

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

T mcrl2::pbes_system::replace_pbes_expressions	(	const T &	x,
		const Substitution &	sigma,
		bool	innermost = true
	)

Definition at line 273 of file replace.h.

replace_pbes_expressions() [2/2]

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

void mcrl2::pbes_system::replace_pbes_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost = true
	)

Definition at line 264 of file replace.h.

replace_propositional_variables() [1/3]

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

T mcrl2::pbes_system::replace_propositional_variables	(	const T &	x,
		const Substitution &	sigma
	)

Applies a propositional variable substitution.

Definition at line 244 of file replace.h.

replace_propositional_variables() [2/3]

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

void mcrl2::pbes_system::replace_propositional_variables	(	T &	result,
		const T &	x,
		const Substitution &	sigma
	)

Applies a propositional variable substitution.

Definition at line 255 of file replace.h.

replace_propositional_variables() [3/3]

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

void mcrl2::pbes_system::replace_propositional_variables	(	T &	x,
		const Substitution &	sigma
	)

Applies a propositional variable substitution.

Definition at line 235 of file replace.h.

replace_sort_expressions() [1/2]

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

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

Definition at line 102 of file replace.h.

replace_sort_expressions() [2/2]

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

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

Definition at line 92 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 182 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 172 of file replace_subterm.h.

replace_variables() [1/2]

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

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

Definition at line 146 of file replace.h.

replace_variables() [2/2]

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

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

Definition at line 137 of file replace.h.

replace_variables_capture_avoiding() [1/4]

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

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

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

Definition at line 136 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [2/4]

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

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

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

Definition at line 102 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [3/4]

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

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

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

Definition at line 118 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [4/4]

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

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

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

Definition at line 87 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [1/2]

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

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

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

Definition at line 116 of file replace_capture_avoiding_with_an_identifier_generator.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [2/2]

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

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

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

Definition at line 97 of file replace_capture_avoiding_with_an_identifier_generator.h.

resolve_summand_variable_name_clashes()

template<bool allow_ce>

void mcrl2::pbes_system::resolve_summand_variable_name_clashes ( detail::pre_srf_pbes< allow_ce > &  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 64 of file resolve_name_clashes.h.

rewrite() [1/4]

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

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

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

Definition at line 111 of file rewrite.h.

rewrite() [2/4]

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

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

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

Definition at line 141 of file rewrite.h.

rewrite() [3/4]

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

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

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

Definition at line 98 of file rewrite.h.

rewrite() [4/4]

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

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

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

Definition at line 126 of file rewrite.h.

rewrite_PVI()

propositional_variable_instantiation mcrl2::pbes_system::rewrite_PVI ( const propositional_variable_instantiation  PVI, const std::unordered_map< std::string, std::set< int > >  R  )

inline

For a given X(e) and set of redundant params R, returns a copy of X(e) without redundancy.

Parameters

PVI	A propositional variable instantiation X(e).
R	A set of indices of parameters that are redundant in X(e).

Returns

A copy of X(e) without redundancy.

Definition at line 33 of file pbesinst_lazy_counter_example.h.

save_bes_pgsolver()

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

Definition at line 141 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 114 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 50 of file io.cpp.

save_structure_graph() [1/2]

void mcrl2::pbes_system::save_structure_graph ( const structure_graph &  G, const std::string &  filename  )

inline

Writes a structure graph to a file in binary aterm format.

Definition at line 98 of file structure_graph_io.h.

save_structure_graph() [2/2]

void mcrl2::pbes_system::save_structure_graph ( const structure_graph &  G, std::ostream &  out  )

inline

Writes a structure graph to a stream in binary aterm format.

A sequence of aterms: extent, initial vertex, excluded vertices, then per vertex its formula, decoration, rank, strategy and successors.

Definition at line 63 of file structure_graph_io.h.

search_variable() [1/2]

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

Definition at line 59 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 207 of file find.h.

self_substitute() [1/2]

void mcrl2::pbes_system::self_substitute ( pbes_equation &  equation, std::size_t  initial_size, substitute_propositional_variables_for_true_false_builder< pbes_system::pbes_expression_builder > &  pvi_substituter, rewrite_if_builder< pbes_system::pbes_expression_builder > &  if_substituter, simplify_data_rewriter< data::rewriter > &  pbes_rewriter, simplify_data_rewriter< data::rewriter > &  pbes_default_rewriter, pbeschain_options  options  )

inline

Definition at line 386 of file pbeschain.h.

self_substitute() [2/2]

void mcrl2::pbes_system::self_substitute ( pbes_equation &  equation, substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &  substituter  )

inline

Definition at line 113 of file pbesbackelm.h.

set_intersection()

template<typename VertexSet >

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

Definition at line 288 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 302 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 276 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.

simplify_expr()

pbes_expression mcrl2::pbes_system::simplify_expr ( pbes_expression &  phi, rewrite_if_builder< pbes_system::pbes_expression_builder > &  if_substituter, simplify_data_rewriter< data::rewriter > &  pbes_rewriter  )

inline

Definition at line 355 of file pbeschain.h.

simplify_srf_pbes()

srf_pbes mcrl2::pbes_system::simplify_srf_pbes ( const srf_pbes &  p )

inline

Simplifies a PBES in standard recursive form (SRF) by removing summands whose condition simplifies to true or false.

Such trivial summands commonly arise from pre_srf2srfpbes, where substituting true/false for the counter example variables Zpos/Zneg may turn some summands into ones of the shape exists <> . true && X_true() (disjunctive equations) or exists params . false && X(...) (dead disjuncts), respectively forall <> . false || X_false() (conjunctive equations) or forall params . true || X(...) (vacuous conjuncts). These are recognized and simplified away below: a dead disjunct/vacuous conjunct is dropped, and an unconditionally true/false summand collapses the whole equation to a single summand recursing into X_true/X_false, which is semantically equivalent but avoids spurious dependencies on the other, now irrelevant, summands.

Definition at line 944 of file srf_pbes.h.

small_progress_measures()

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

inline

Definition at line 349 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 30 of file solution_strategy.h.

solve_structure_graph() [1/2]

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

inline

Definition at line 654 of file solve_structure_graph.h.

solve_structure_graph() [2/2]

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

inline

Definition at line 646 of file solve_structure_graph.h.

solve_structure_graph_winning_mapping()

std::pair< bool, std::unordered_map< pbes_expression, structure_graph::index_type > > mcrl2::pbes_system::solve_structure_graph_winning_mapping ( structure_graph &  G, bool  check_strategy = false  )

inline

Returns a mapping from PBES variable instantations to vertices in the structure graph for vertices won by player alpha.

Definition at line 662 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 693 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 703 of file solve_structure_graph.h.

solve_structure_graph_with_evidence_lts()

bool mcrl2::pbes_system::solve_structure_graph_with_evidence_lts ( structure_graph &  G, const lps::specification &  lpsspec, const pbes &  p, const pbes_equation_index &  p_index, data::rewrite_strategy  strategy, lts::lts_type  format, const std::string &  filename  )

inline

Solve this pbes_system using a structure graph, directly writing the evidence as an LTS.

Parameters

G	The structure graph.
lpsspec	The original LPS that was used to create the PBES.
p	The pbes to be solved.
p_index	The index of the pbes equation to be solved.
strategy	The rewrite strategy used to solve G.
format	The LTS format to write filename in.
filename	The file to write the evidence LTS to.

Definition at line 144 of file evidence_lts.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 74 of file join.h.

split_conditions()

template<bool allow_ce>

detail::pre_srf_pbes< allow_ce > mcrl2::pbes_system::split_conditions ( const detail::pre_srf_pbes< allow_ce > &  pbes, std::size_t  granularity  )

inline

Splits SRF summand conditions to reduce their dependencies.

Definition at line 23 of file srf_transformations.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 271 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 243 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 48 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 607 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 251 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 262 of file structure_graph.h.

structure_graph_temp_path()

std::string mcrl2::pbes_system::structure_graph_temp_path ( )

inline

Definition at line 82 of file pbescegps.h.

substitute() [1/2]

void mcrl2::pbes_system::substitute ( pbes_equation &  into, const pbes_equation &  by, detail::substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &  substituter  )

inline

Definition at line 46 of file pbesfixpointsolve.h.

substitute() [2/2]

void mcrl2::pbes_system::substitute ( pbes_equation &  into, const pbes_equation &  by, substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &  substituter  )

inline

Definition at line 128 of file pbesbackelm.h.

swap() [1/11]

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

inlinenoexcept

\brief swap overload

Definition at line 355 of file pbes_expression.h.

swap() [2/11]

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

inlinenoexcept

\brief swap overload

Definition at line 659 of file pbes_expression.h.

swap() [3/11]

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

inlinenoexcept

\brief swap overload

Definition at line 94 of file fixpoint_symbol.h.

swap() [4/11]

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

inlinenoexcept

\brief swap overload

Definition at line 583 of file pbes_expression.h.

swap() [5/11]

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

inlinenoexcept

\brief swap overload

Definition at line 507 of file pbes_expression.h.

swap() [6/11]

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

inlinenoexcept

\brief swap overload

Definition at line 279 of file pbes_expression.h.

swap() [7/11]

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

inlinenoexcept

\brief swap overload

Definition at line 431 of file pbes_expression.h.

swap() [8/11]

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

inlinenoexcept

\brief swap overload

Definition at line 156 of file pbes_equation.h.

swap() [9/11]

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

inlinenoexcept

\brief swap overload

Definition at line 103 of file pbes_expression.h.

swap() [10/11]

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

inlinenoexcept

\brief swap overload

Definition at line 114 of file propositional_variable.h.

swap() [11/11]

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

inlinenoexcept

\brief swap overload

Definition at line 208 of file pbes_expression.h.

to_string()

std::string mcrl2::pbes_system::to_string ( const var_choice_strategy &  strategy )

inline

Definition at line 55 of file pbescegps_utilities.h.

to_token()

std::string mcrl2::pbes_system::to_token ( abstraction_set_verdict  verdict )

inline

Definition at line 224 of file pbesfindabs.h.

tosrf()

pbes mcrl2::pbes_system::tosrf ( pbes_system::pbes  pbesspec, bool  split_srf_conditions = false  )

inline

Definition at line 729 of file pbeschain.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 50 of file pbes.cpp.

translate_user_notation() [2/4]

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

T mcrl2::pbes_system::translate_user_notation

(

const T &

x

)

Definition at line 30 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 49 of file pbes.cpp.

translate_user_notation() [4/4]

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

void mcrl2::pbes_system::translate_user_notation

(

T &

x

)

Definition at line 23 of file translate_user_notation.h.

true_()

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

inline

Returns

Returns the value true

Definition at line 679 of file pbes_expression.h.

txt2pbes() [1/2]

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 44 of file txt2pbes.h.

txt2pbes() [2/2]

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 27 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 272 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 325 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 293 of file typecheck.h.

undefined_vertex()

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

inlineconstexpr

Definition at line 33 of file structure_graph.h.

unify_parameters() [1/2]

template<bool allow_ce>

void mcrl2::pbes_system::unify_parameters ( detail::pre_srf_pbes< allow_ce > &  p, bool  ignore_ce_equations, bool  reset  )

inline

See unify_parameters(pbes&, bool, bool) for a description of the parameters.

Definition at line 177 of file unify_parameters.h.

unify_parameters() [2/2]

void mcrl2::pbes_system::unify_parameters ( pbes &  p, bool  ignore_ce_equations, bool  reset  )

inline

Unify all parameters of the equations, optionally ignoring the equations related to counter example information. Finally, if reset is true, reset the newly introduced parameters to a default value.

Definition at line 141 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 829 of file bisimulation.h.