mcrl2::pbes_system::detail Namespace Reference

Namespaces
namespace	combined_access
	The namespace for access functions that operate on both pbes and data expressions.

Classes
struct	add_capture_avoiding_replacement
struct	add_capture_avoiding_replacement_with_an_identifier_generator
struct	add_data_rewriter
class	add_edges
struct	add_simplify
struct	add_simplify_quantifiers
struct	anonymize_builder
struct	anonymize_builder_instance
struct	apply_e_lts2pbes_traverser
struct	apply_e_structured_traverser
struct	apply_e_traverser
struct	apply_enumerate_builder
struct	apply_rewriter_builder
struct	apply_rhs_lts2pbes_traverser
struct	apply_rhs_structured_traverser
struct	apply_rhs_traverser
struct	apply_sat_traverser
class	belongs_relation
class	bes_algorithm
	Algorithm class for algorithms on linear process specifications. More...
struct	bes_equation_limit
struct	bqnf2ppg_rewriter
struct	bqnf_quantifier_rewriter
struct	bqnf_visitor
	A visitor class for PBES equations in BQNF. There is a visit_<node> function for each type of node. By default these functions do nothing, but check that the PBES equations are indeed in BQNF, so they must be overridden in order to add behaviour. More...
class	computation_guard
struct	control_flow_graph
struct	data2pbes_builder
struct	data_rewriter_builder
struct	default_rules_predicate
struct	e_lts2pbes_traverser
struct	e_structured_traverser
struct	e_traverser
struct	edge_condition_traverser
struct	edge_details
struct	edge_traverser_stack_elem
struct	enumerate_quantifiers_builder
struct	find_equalities_traverser
struct	find_equalities_traverser_inst
struct	find_free_variables_traverser
struct	find_propositional_variables_traverser
struct	find_quantifier_variables_traverser
	Visitor for collecting the quantifier variables that occur in a pbes expression. More...
struct	find_subterm_traverser
struct	fresh_variable_name_generator
class	GCFP_graph
class	GCFP_vertex
struct	global_control_flow_graph
class	global_control_flow_graph_vertex
class	global_reset_variables_algorithm
	Adds the reset variables procedure to the stategraph algorithm. More...
struct	guard_expression
struct	guard_traverser
	Computes a multimap of propositional variable instantiations and the corresponding guards from a PBES expression. More...
struct	has_propositional_variables_traverser
struct	has_quantifier_name_clashes_traverser
	Visitor for determining if within the scope of a quantifier there are quantifier variables of free variables with the same name. More...
struct	if_rewrite_builder
struct	is_pfnf_traverser
class	LCFP_vertex
struct	local_control_flow_graph
class	local_control_flow_graph_vertex
struct	local_reset_traverser
	N.B. It is essential that this traverser uses the same traversal order as the guard_traverser. More...
class	local_reset_variables_algorithm
	Adds the reset variables procedure to the stategraph algorithm. More...
struct	lps2pbes_counter_example_parameters
struct	lps2pbes_parameters
struct	lps_reset_traverser
class	lpsstategraph_algorithm
struct	lts2pbes_counter_example_parameters
class	lts2pbes_lts
struct	lts2pbes_parameters
struct	manual_structure_graph_builder
struct	normalize_and_or_builder
struct	occurring_variable_visitor
struct	order_quantified_variables_builder
struct	par_traverser
class	parity_game_output
struct	pbes2data_builder
struct	pbes_abstract_builder
	Visitor that implements the pbes-abstract algorithm. More...
struct	pbes_actions
struct	pbes_command
	Command that operates on a PBES. More...
class	pbes_context
class	pbes_greybox_interface
class	pbes_property_map
	Stores the following properties of a linear process specification: More...
struct	pbes_rewriter_command
	PBES command that uses a rewrite strategy. More...
struct	pbesinst_finite_builder
	Visitor that applies a propositional variable substitution to a pbes expression. More...
class	periodic_guard
class	pfnf_equation
class	pfnf_implication
class	pfnf_pbes
struct	pfnf_printer
class	pfnf_quantifier
struct	pfnf_traverser
	Applies the PFNF rewriter to a PBES expression. More...
struct	pfnf_traverser_expression
struct	pfnf_traverser_implication
	Represents the implication g => ( X0(e0) \/ ... \/ Xk(ek) ) More...
struct	position_count_traverser
class	ppg_visitor
class	predicate_variable
struct	printer
struct	QPVI
	A quantified predicate variable instantiation. More...
class	quantified_variable
class	quantifier
struct	quantifier_propagate_builder
struct	quantifiers_inside_builder
struct	quantifiers_inside_exists_builder
struct	quantifiers_inside_forall_builder
class	rename_pbesinst_consecutively
struct	replace_constants_by_variables_builder
struct	replace_subterm_builder
struct	reset_traverser
	reset propositional variables N.B. It is essential that this traverser uses the same traversal order as the guard_traverser. More...
struct	reset_variable_builder
struct	rewrite_pbes_expressions_builder
struct	rewrite_pbes_expressions_with_substitution_builder
struct	rhs_lts2pbes_traverser
struct	rhs_structured_traverser
struct	rhs_traverser
struct	sat_traverser
struct	significant_variables_traverser
struct	simplify_builder
struct	simplify_data_rewriter_builder
struct	simplify_quantifiers_builder
struct	simplify_quantifiers_data_rewriter_builder
struct	srf_and_traverser
struct	srf_or_traverser
class	standard_form_traverser
	Traverser that implements the standard form normalization. More...
class	stategraph_algorithm
	Algorithm class for the computation of the local and global control flow graphs. More...
struct	stategraph_edge
class	stategraph_equation
class	stategraph_global_algorithm
	Algorithm class for the global variant of the stategraph algorithm. More...
struct	stategraph_global_graph
class	stategraph_influence_graph_algorithm
	Algorithm class for the stategraph algorithm. More...
class	stategraph_local_algorithm
	Algorithm class for the local variant of the stategraph algorithm. More...
class	stategraph_pbes
struct	stategraph_simplify_builder
class	stategraph_simplify_rewriter
	A rewriter that simplifies expressions that simplifies quantifiers. More...
struct	stategraph_vertex
struct	structure_graph_builder
class	symbolic_exploration_algorithm
struct	typecheck_builder
struct	variable_data_expression_substitution
struct	variable_variable_substitution

Typedefs
typedef lts::lts_lts_t::states_size_type	lts2pbes_state_type
typedef std::map< core::identifier_string, std::vector< data::variable > >	pbes_parameter_map
	Data structure for storing the variables that should be expanded by the finite pbesinst algorithm.
typedef std::pair< bool, data::variable_list >	pfnf_traverser_quantifier
	Represents a quantifier Qv:V. If the bool is true it is a forall, otherwise an exists.
typedef std::pair< pbes_expression, standard_form_type >	standard_form_pair

Enumerations
enum	standard_form_type { standard_form_both , standard_form_and , standard_form_or }

Functions
data::data_specification &	absinthe_data_specification ()
template<typename T >
void	absinthe_check_expression (const T &x)
bool	is_structured_sort_constructor (const data::data_specification &dataspec, const data::function_symbol &f)
void	print_used_function_symbols (const pbes &p)
data::sort_expression	target_sort (const data::sort_expression &s)
void	make_constelm_substitution (const std::map< data::variable, data::data_expression > &m, data::rewriter::substitution_type &result)
void	set_bes_equation_limit (std::size_t size)
void	check_bes_equation_limit (std::size_t size)
template<typename T >
bool	is_bqnf (const T &x)
	Determines if an expression is a BQNF expression.
static void	inc_indent ()
	Increases the current indent level.
static void	dec_indent ()
	Decreases the current indent level.
static void	indent ()
	Indents according to the current indent level.
std::set< data::variable >	find_free_variables (const pbes_expression &x, const data::variable_list &bound_variables=data::variable_list(), bool search_propositional_variables=true)
std::ostream &	operator<< (std::ostream &out, const guard_expression &x)
bool	has_propositional_variables (const pbes_expression &x)
void	replace_global_variables (pbes &p, const data::mutable_map_substitution<> &sigma)
	Applies a global variable substitution to a PBES.
data::mutable_map_substitution	instantiate_global_variables (pbes &p)
	Eliminates the global variables of a PBES, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown.
void	split_and (const pbes_expression &expr, std::vector< pbes_expression > &result)
	Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 && p2 && ... && pn, this will yield a vector of the form [ p1, p2, ..., pn ], assuming that pi does not have a && as main function symbol.
void	split_or (const pbes_expression &expr, std::vector< pbes_expression > &result)
	Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 || p2 || ... || pn, this will yield a vector of the form [ p1, p2, ..., pn ], assuming that pi does not have a || as main function symbol.
bool	is_pfnf_simple_expression (const pbes_expression &x)
bool	is_pfnf_data_expression (const pbes_expression &x)
bool	is_pfnf_or_expression (const pbes_expression &x)
bool	is_pfnf_or (const pbes_expression &x)
bool	is_pfnf_imp (const pbes_expression &x)
bool	is_pfnf_inner_and (const pbes_expression &x)
bool	is_pfnf_outer_and (const pbes_expression &x)
bool	is_pfnf_expression (const pbes_expression &x)
template<typename T >
bool	is_pfnf (const T &x)
pbes_expression	remove_quantifiers (const pbes_expression &x)
std::vector< pbes_expression >	pfnf_implications (const pbes_expression &x)
void	split_pfnf_expression (const pbes_expression &phi, pbes_expression &h, std::vector< pbes_expression > &g)
std::set< data::variable >	find_quantifier_variables (const pbes_expression &x)
bool	has_quantifier_name_clashes (const pbes_expression &x)
bool	is_well_typed (const pbes_equation &eqn)
	Checks if the equation is well typed.
template<typename Iter >
bool	has_conflicting_type (Iter first, Iter last, const propositional_variable_instantiation &v, const data::data_specification &data_spec)
	Checks if the propositional variable instantiation v has a conflict with the sequence of propositional variable declarations [first, last).
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 TermTraits , typename Parameters >
void	E (const state_formulas::state_formula &x, Parameters &parameters, std::vector< pbes_equation > &result, TermTraits tr)
template<typename TermTraits , typename Parameters >
void	E_structured (const state_formulas::state_formula &x, Parameters &parameters, std::vector< pbes_equation > &result, TermTraits tr)
data::variable_list	Par (const core::identifier_string &X, const data::variable_list &l, const state_formulas::state_formula &x)
template<typename TermTraits , typename Parameters >
pbes_expression	RHS (const state_formulas::state_formula &x, Parameters &parameters, TermTraits tr)
template<typename TermTraits , typename Parameters >
TermTraits::term_type	RHS_structured (const state_formulas::state_formula &x, Parameters &parameters, const data::variable_list &variables, const fixpoint_symbol &sigma, std::vector< pbes_equation > &equations, TermTraits tr)
template<typename TermTraits >
TermTraits::term_type	Sat (const lps::multi_action &a, const action_formulas::action_formula &x, data::set_identifier_generator &id_generator, TermTraits tr)
data::variable_list	lhs_variables (const data::assignment_list &l)
data::data_expression_list	rhs_expressions (const data::assignment_list &l)
const core::identifier_string &	mu_name (const state_formulas::state_formula &f)
data::variable_list	mu_variables (const state_formulas::state_formula &f)
	Returns the variables corresponding to ass(f)
data::data_expression_list	mu_expressions (const state_formulas::state_formula &f)
	Returns the data expressions corresponding to ass(f)
std::string	myprint (const std::vector< pbes_equation > &v)
data::mutable_map_substitution	make_fresh_variable_substitution (const data::variable_list &variables, data::set_identifier_generator &id_generator, bool add_to_context=true)
	Generates a substitution that assigns fresh variables to the given sequence of variables. The identifier generator is used to assign names to the fresh variables. Caveat: the implementation is very inefficient.
void	lps_reset_variables (lpsstategraph_algorithm &algorithm, const pbes_expression &x, const stategraph_equation &eq_X, const data::variable_list &process_parameters, std::vector< lps::action_summand > &summands)
data::assignment_list	make_assignments (const data::variable_list &d, const data::data_expression_list &e)
template<typename TermTraits , typename Parameters >
void	E_lts2pbes (const state_formulas::state_formula &x, Parameters &parameters, std::vector< pbes_equation > &result, TermTraits tr)
std::ostream &	operator<< (std::ostream &out, const lts::lts_lts_t &ltsspec)
std::ostream &	operator<< (std::ostream &out, const lts2pbes_lts &ltsspec)
core::identifier_string	make_identifier (const core::identifier_string &name, lts2pbes_state_type s)
template<typename TermTraits , typename Parameters >
pbes_expression	RHS (const state_formulas::state_formula &x, lts2pbes_state_type s, Parameters &parameters, TermTraits tr)
template<typename T >
T	normalize_and_or (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T >
void	normalize_and_or (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
pbes	load_pbes (const std::string &filename)
	Loads a PBES from filename, or from stdin if filename equals "".
void	save_pbes (const pbes &pbesspec, const std::string &filename)
	Saves an PBES to filename, or to stdout if filename equals "".
bool	match_declaration (const std::string &text, const data::variable &d, const data::data_specification &data_spec)
	Returns true if the declaration text matches with the variable d.
std::vector< data::variable >	find_matching_parameters (const pbes &p, const std::string &name, const std::set< std::string > &declarations)
	Find parameter declarations that match a given string.
pbes_parameter_map	parse_pbes_parameter_map (const pbes &p, const std::string &text)
	Parses parameter selection for finite pbesinst algorithm.
std::ostream &	print_pbes_parameter_map (std::ostream &out, const pbes_parameter_map &m)
	Print a parameter map.
bool	pbessolve (const pbes &p)
void	split_pfnf_implication (const pbes_expression &x, pbes_expression &g, std::vector< propositional_variable_instantiation > &Xij)
std::ostream &	operator<< (std::ostream &out, const pfnf_implication &x)
template<typename Container >
Container	concat (const Container &x, const Container &y)
	Concatenates two containers.
std::vector< std::size_t >	position_counts (const pbes &x)
pbes	to_ppg (pbes x)
	Rewrites a PBES to a PPG.
template<typename T >
bool	is_ppg (const T &x)
	Determines if an expression is a PPG expression.
std::string	print_index (std::size_t index)
std::ostream &	operator<< (std::ostream &out, const stategraph_vertex &u)
pbes_expression	reset_variables (global_reset_variables_algorithm &algorithm, const pbes_expression &x, const stategraph_equation &eq_X)
std::ostream &	operator<< (std::ostream &out, const LCFP_vertex &u)
std::ostream &	operator<< (std::ostream &out, const GCFP_graph &G)
std::ostream &	operator<< (std::ostream &out, const local_control_flow_graph_vertex &u)
bool	operator< (const local_control_flow_graph_vertex &u, const local_control_flow_graph_vertex &v)
template<typename Vertex >
std::ostream &	operator<< (std::ostream &out, const control_flow_graph< Vertex > &G)
std::ostream &	operator<< (std::ostream &out, const global_control_flow_graph_vertex &)
bool	operator< (const global_control_flow_graph_vertex &x, const global_control_flow_graph_vertex &y)
template<typename Container >
std::string	print_vector (const Container &v, const std::string &delim)
pbes_expression	local_reset_variables (local_reset_variables_algorithm &algorithm, const pbes_expression &x, const stategraph_equation &eq_X)
std::ostream &	operator<< (std::ostream &out, const predicate_variable &x)
std::vector< stategraph_equation >::const_iterator	find_equation (const stategraph_pbes &p, const core::identifier_string &X, bool warn=true)
pbes_expression	stategraph_not (const pbes_expression &x)
pbes_expression	smart_and (const pbes_expression &x, const pbes_expression &y)
pbes_expression	smart_or (const pbes_expression &x, const pbes_expression &y)
void	stategraph_split_and (const pbes_expression &expr, std::vector< pbes_expression > &result)
void	stategraph_split_or (const pbes_expression &expr, std::vector< pbes_expression > &result)
std::string	print_equation (const pbes_equation &eq)
std::string	print_set (const std::set< std::size_t > &v)
const data::data_expression &	nth_element (const data::data_expression_list &e, std::size_t n)
std::string	print_pbes_expressions (const std::set< pbes_expression > &v)
void	symbolic_exploration (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, bool optimized=true, bool clustered=false, bool instantiate=false)
data::variable	nat (const std::string &name)
	Returns a data variable of type Nat with a given name.
data::variable	pos (const std::string &name)
	Returns a data variable of type Pos with a given name.
data::variable	bool_ (const std::string &name)
	Returns a data variable of type Bool with a given name.
propositional_variable	propvar (const std::string &name, const data::variable_list &parameters)
	Returns a propositional variable declaration with the given name and parameters.
propositional_variable_instantiation	propvarinst (const std::string &name, const data::data_expression_list &parameters)
	Returns a propositional variable instantiation with the given name and parameters.
template<template< class > class Traverser, class OutputIterator >
find_propositional_variables_traverser< Traverser, OutputIterator >	make_find_propositional_variables_traverser (OutputIterator out)
int	variable_index (const data::variable_list &variables, const data::variable &d)
	Finds the index of a variable in a sequence.
pbes_expression	parse_pbes_expression_new (const std::string &text)
untyped_pbes	parse_pbes_new (const std::string &text)
void	complete_pbes (pbes &x)
propositional_variable	parse_propositional_variable (const std::string &text)
pbes_expression	parse_pbes_expression (const std::string &text)
data::data_expression	make_and (const data::data_expression &x1, const data::data_expression &x2, const data::data_expression &x3)
data::data_expression	equal_to (const data::data_expression_list &x, const data::data_expression_list &y)
template<typename MapContainer >
MapContainer::mapped_type	map_at (const MapContainer &m, typename MapContainer::key_type key)
std::unordered_map< propositional_variable_instantiation, propositional_variable_instantiation >	create_pv_renaming (std::vector< std::vector< propositional_variable_instantiation > > &instantiations, bool short_renaming_scheme)
template<typename StructureGraph , typename Compare >
deque_vertex_set	attr_min_rank_todo_generic (const StructureGraph &G, const vertex_set &A, const vertex_set &U, std::size_t j, Compare compare)
template<typename StructureGraph >
deque_vertex_set	attr_min_rank_original_todo (const StructureGraph &G, const vertex_set &A, const vertex_set &U, std::size_t j)
void	insert_in_rank_map (std::map< std::size_t, vertex_set > &U_rank_map, structure_graph::index_type u, std::size_t j, std::size_t n)
template<typename StructureGraph >
std::map< std::size_t, vertex_set >	compute_U_j_map (const StructureGraph &G, const vertex_set &V)
template<typename StructureGraph , typename Compare >
vertex_set	attr_min_rank_generic (const StructureGraph &G, vertex_set A, std::size_t alpha, const vertex_set &U, std::size_t j, Compare compare)
template<typename Compare >
void	fatal_attractors_generic (const simple_structure_graph &G, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t equation_count, Compare compare)
void	fatal_attractors (const simple_structure_graph &G, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t equation_count)
void	find_loops2 (const simple_structure_graph &G, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t equation_count)
template<typename StructureGraph >
vertex_set	attr_min_rank_original (const StructureGraph &G, vertex_set A, std::size_t alpha, const vertex_set &U, std::size_t j)
void	fatal_attractors_original (const simple_structure_graph &G, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t equation_count)
bool	find_loop (const simple_structure_graph &G, const vertex_set &U, structure_graph::index_type v, structure_graph::index_type w, std::size_t p, std::unordered_map< structure_graph::index_type, bool > &visited)
template<class Container >
void	find_loops (const simple_structure_graph &G, const Container &discovered, const pbesinst_lazy_todo &todo, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t iteration_count, const detail::structure_graph_builder &graph_builder)
template<typename PropositionalVariable , typename Parameter >
void	split_parameters (const PropositionalVariable &X, const pbesinst_index_map &index_map, std::vector< Parameter > &finite, std::vector< Parameter > &infinite)
	Computes the subset with variables of finite sort and infinite.
void	partial_solve (structure_graph &G, const pbesinst_lazy_todo &todo, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t equation_count, const detail::structure_graph_builder &graph_builder)
pbes_expression	quantifier_propagate (const pbes_expression &x)
pbes_expression	make_exists_ (std::set< data::variable > vars, const pbes_expression &expr)
pbes_expression	make_forall_ (std::set< data::variable > vars, const pbes_expression &expr)
pbes_expression	make_quantifier (bool is_forall, const data::variable_list &vars, const pbes_expression &body)
void	quantifier_propagate (std::list< std::pair< core::identifier_string, pbes_equation > > &new_equations, data::set_identifier_generator &id_gen, const quantifier_propagate_builder::equation_map_t eqn_map, pbes_expression &x)
std::string	print_removed_equations (const std::vector< propositional_variable > &removed)
void	resolve_summand_variable_name_clashes (srf_summand &summand, const std::set< core::identifier_string > &process_parameter_names, data::set_identifier_generator &generator)
template<template< class > class Builder, class Rewriter >
rewrite_pbes_expressions_builder< Builder, Rewriter >	make_rewrite_pbes_expressions_builder (const Rewriter &R)
template<template< class > class Builder, class Rewriter , class Substitution >
rewrite_pbes_expressions_with_substitution_builder< Builder, Rewriter, Substitution >	make_rewrite_pbes_expressions_with_substitution_builder (const Rewriter &R, Substitution sigma)
template<typename T >
T	data2pbes (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T >
void	data2pbes (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
template<typename DataRewriter , typename SubstitutionFunction >
const data::data_expression	data_rewrite (const data::data_expression &x, const DataRewriter &R, SubstitutionFunction &sigma)
template<typename DataRewriter , typename SubstitutionFunction >
void	data_rewrite (data::data_expression &result, const data::data_expression &x, const DataRewriter &R, SubstitutionFunction &sigma)
template<typename DataRewriter >
const data::data_expression	data_rewrite (const data::data_expression &x, const DataRewriter &R, data::no_substitution &)
template<typename DataRewriter >
void	data_rewrite (data::data_expression &result, const data::data_expression &x, const DataRewriter &R, data::no_substitution &)
template<template< class, class, class > class Builder, class DataRewriter , class SubstitutionFunction >
apply_rewriter_builder< Builder, DataRewriter, SubstitutionFunction >	make_apply_rewriter_builder (const DataRewriter &datar, SubstitutionFunction &sigma)
template<template< class, class, class > class Builder, class DataRewriter , class MutableSubstitution >
apply_enumerate_builder< Builder, DataRewriter, MutableSubstitution >	make_apply_enumerate_builder (const DataRewriter &R, MutableSubstitution &sigma, const data::data_specification &dataspec, data::enumerator_identifier_generator &id_generator, bool enumerate_infinite_sorts)
template<typename T >
T	pbes2data (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
template<typename T >
void	pbes2data (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
pbes_expression	quantifiers_inside (const pbes_expression &x)
pbes_expression	quantifiers_inside_forall (const std::set< data::variable > &variables, const pbes_expression &x)
pbes_expression	quantifiers_inside_exists (const std::set< data::variable > &variables, const pbes_expression &x)
template<typename BinaryOperation >
std::tuple< pbes_expression, pbes_expression >	compute_Phi_Psi (const std::vector< pbes_expression > &X, const std::set< data::variable > &V, BinaryOperation op, pbes_expression empty_sequence_result)
pbes_expression	make_not (const pbes_expression &x)
std::vector< srf_summand >	srf_or (const pbes_expression &phi, std::deque< pbes_equation > &equations, const pbes_equation &eqn, const data::variable_list &V, data::set_identifier_generator &id_generator, const core::identifier_string &X_true, const core::identifier_string &X_false, std::vector< srf_equation > &result)
std::vector< srf_summand >	srf_and (const pbes_expression &phi, std::deque< pbes_equation > &equations, const pbes_equation &eqn, const data::variable_list &V, data::set_identifier_generator &id_generator, const core::identifier_string &X_true, const core::identifier_string &X_false, std::vector< srf_equation > &result)
bool	is_conjunctive (const pbes_expression &phi)
void	check_lps2pbes_actions (const state_formulas::state_formula &formula, const lps::stochastic_specification &lpsspec)
	Prints a warning if formula contains an action that is not used in lpsspec.
typecheck_builder	make_typecheck_builder (data::data_type_checker &data_typechecker, const data::detail::variable_context &variables, const detail::pbes_context &propositional_variables)

Variables
static int	indent_count = 0
	The current indent level. Used for debug output.

Typedef Documentation

lts2pbes_state_type

typedef lts::lts_lts_t::states_size_type mcrl2::pbes_system::detail::lts2pbes_state_type

Definition at line 27 of file lts2pbes_rhs.h.

pbes_parameter_map

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

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

Definition at line 29 of file pbes_parameter_map.h.

pfnf_traverser_quantifier

typedef std::pair<bool, data::variable_list> mcrl2::pbes_system::detail::pfnf_traverser_quantifier

Represents a quantifier Qv:V. If the bool is true it is a forall, otherwise an exists.

Definition at line 33 of file pfnf_traverser.h.

standard_form_pair

typedef std::pair<pbes_expression, standard_form_type> mcrl2::pbes_system::detail::standard_form_pair

Definition at line 33 of file normal_forms.h.

Enumeration Type Documentation

standard_form_type

enum mcrl2::pbes_system::detail::standard_form_type

Enumerator
standard_form_both
standard_form_and
standard_form_or

Definition at line 26 of file normal_forms.h.

Function Documentation

absinthe_check_expression()

template<typename T >

void mcrl2::pbes_system::detail::absinthe_check_expression ( const T &  x )

inline

Definition at line 53 of file absinthe.h.

absinthe_data_specification()

data::data_specification & mcrl2::pbes_system::detail::absinthe_data_specification ( )

inline

Definition at line 45 of file absinthe.h.

attr_min_rank_generic()

template<typename StructureGraph , typename Compare >

vertex_set mcrl2::pbes_system::detail::attr_min_rank_generic	(	const StructureGraph &	G,
		vertex_set	A,
		std::size_t	alpha,
		const vertex_set &	U,
		std::size_t	j,
		Compare	compare
	)

Definition at line 100 of file pbesinst_fatal_attractors.h.

attr_min_rank_original()

template<typename StructureGraph >

vertex_set mcrl2::pbes_system::detail::attr_min_rank_original	(	const StructureGraph &	G,
		vertex_set	A,
		std::size_t	alpha,
		const vertex_set &	U,
		std::size_t	j
	)

Definition at line 246 of file pbesinst_fatal_attractors.h.

attr_min_rank_original_todo()

template<typename StructureGraph >

deque_vertex_set mcrl2::pbes_system::detail::attr_min_rank_original_todo	(	const StructureGraph &	G,
		const vertex_set &	A,
		const vertex_set &	U,
		std::size_t	j
	)

Definition at line 43 of file pbesinst_fatal_attractors.h.

attr_min_rank_todo_generic()

template<typename StructureGraph , typename Compare >

deque_vertex_set mcrl2::pbes_system::detail::attr_min_rank_todo_generic	(	const StructureGraph &	G,
		const vertex_set &	A,
		const vertex_set &	U,
		std::size_t	j,
		Compare	compare
	)

Definition at line 25 of file pbesinst_fatal_attractors.h.

bool_()

data::variable mcrl2::pbes_system::detail::bool_

(

const std::string &

name

)

Returns a data variable of type Bool with a given name.

Parameters

name

A string

Returns

A data variable of type Bool with a given name

Definition at line 44 of file test_utility.h.

check_bes_equation_limit()

void mcrl2::pbes_system::detail::check_bes_equation_limit ( std::size_t  size )

inline

Definition at line 46 of file bes_equation_limit.h.

check_lps2pbes_actions()

void mcrl2::pbes_system::detail::check_lps2pbes_actions ( const state_formulas::state_formula &  formula, const lps::stochastic_specification &  lpsspec  )

inline

Prints a warning if formula contains an action that is not used in lpsspec.

Definition at line 27 of file lps2pbes.h.

complete_pbes()

void mcrl2::pbes_system::detail::complete_pbes

(

pbes &

x

)

Definition at line 144 of file pbes.cpp.

compute_Phi_Psi()

template<typename BinaryOperation >

std::tuple< pbes_expression, pbes_expression > mcrl2::pbes_system::detail::compute_Phi_Psi	(	const std::vector< pbes_expression > &	X,
		const std::set< data::variable > &	V,
		BinaryOperation	op,
		pbes_expression	empty_sequence_result
	)

Definition at line 30 of file quantifiers_inside_rewriter.h.

compute_U_j_map()

template<typename StructureGraph >

std::map< std::size_t, vertex_set > mcrl2::pbes_system::detail::compute_U_j_map	(	const StructureGraph &	G,
		const vertex_set &	V
	)

Definition at line 72 of file pbesinst_fatal_attractors.h.

concat()

template<typename Container >

Container mcrl2::pbes_system::detail::concat	(	const Container &	x,
		const Container &	y
	)

Concatenates two containers.

Parameters

x	A container
y	A container

Returns

The concatenation of x and y

Definition at line 171 of file pfnf_traverser.h.

create_pv_renaming()

std::unordered_map< propositional_variable_instantiation, propositional_variable_instantiation > mcrl2::pbes_system::detail::create_pv_renaming	(	std::vector< std::vector< propositional_variable_instantiation > > &	instantiations,
		bool	short_renaming_scheme
	)

Definition at line 34 of file pbesinst_alternative_lazy_algorithm.h.

data2pbes() [1/2]

template<typename T >

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

Definition at line 127 of file data2pbes_rewriter.h.

data2pbes() [2/2]

template<typename T >

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

Definition at line 137 of file data2pbes_rewriter.h.

data_rewrite() [1/4]

template<typename DataRewriter >

const data::data_expression mcrl2::pbes_system::detail::data_rewrite	(	const data::data_expression &	x,
		const DataRewriter &	R,
		data::no_substitution &
	)

Definition at line 39 of file data_rewriter.h.

data_rewrite() [2/4]

template<typename DataRewriter , typename SubstitutionFunction >

const data::data_expression mcrl2::pbes_system::detail::data_rewrite	(	const data::data_expression &	x,
		const DataRewriter &	R,
		SubstitutionFunction &	sigma
	)

Definition at line 25 of file data_rewriter.h.

data_rewrite() [3/4]

template<typename DataRewriter >

void mcrl2::pbes_system::detail::data_rewrite	(	data::data_expression &	result,
		const data::data_expression &	x,
		const DataRewriter &	R,
		data::no_substitution &
	)

Definition at line 46 of file data_rewriter.h.

data_rewrite() [4/4]

template<typename DataRewriter , typename SubstitutionFunction >

void mcrl2::pbes_system::detail::data_rewrite	(	data::data_expression &	result,
		const data::data_expression &	x,
		const DataRewriter &	R,
		SubstitutionFunction &	sigma
	)

Definition at line 32 of file data_rewriter.h.

dec_indent()

static void mcrl2::pbes_system::detail::dec_indent ( )

static

Decreases the current indent level.

Definition at line 35 of file bqnf_visitor.h.

E()

template<typename TermTraits , typename Parameters >

void mcrl2::pbes_system::detail::E	(	const state_formulas::state_formula &	x,
		Parameters &	parameters,
		std::vector< pbes_equation > &	result,
		TermTraits	tr
	)

Definition at line 216 of file lps2pbes_e.h.

E_lts2pbes()

template<typename TermTraits , typename Parameters >

void mcrl2::pbes_system::detail::E_lts2pbes	(	const state_formulas::state_formula &	x,
		Parameters &	parameters,
		std::vector< pbes_equation > &	result,
		TermTraits	tr
	)

Definition at line 210 of file lts2pbes_e.h.

E_structured()

template<typename TermTraits , typename Parameters >

void mcrl2::pbes_system::detail::E_structured	(	const state_formulas::state_formula &	x,
		Parameters &	parameters,
		std::vector< pbes_equation > &	result,
		TermTraits	tr
	)

Definition at line 308 of file lps2pbes_e.h.

equal_to()

data::data_expression mcrl2::pbes_system::detail::equal_to ( const data::data_expression_list &  x, const data::data_expression_list &  y  )

inline

Definition at line 40 of file partial_order_reduction.h.

fatal_attractors()

void mcrl2::pbes_system::detail::fatal_attractors ( const simple_structure_graph &  G, std::array< vertex_set, 2 > &  S, std::array< strategy_vector, 2 > &  tau, std::size_t  equation_count  )

inline

Definition at line 221 of file pbesinst_fatal_attractors.h.

fatal_attractors_generic()

template<typename Compare >

void mcrl2::pbes_system::detail::fatal_attractors_generic	(	const simple_structure_graph &	G,
		std::array< vertex_set, 2 > &	S,
		std::array< strategy_vector, 2 > &	tau,
		std::size_t	equation_count,
		Compare	compare
	)

Definition at line 130 of file pbesinst_fatal_attractors.h.

fatal_attractors_original()

void mcrl2::pbes_system::detail::fatal_attractors_original ( const simple_structure_graph &  G, std::array< vertex_set, 2 > &  S, std::array< strategy_vector, 2 > &  tau, std::size_t  equation_count  )

inline

Definition at line 285 of file pbesinst_fatal_attractors.h.

find_equation()

std::vector< stategraph_equation >::const_iterator mcrl2::pbes_system::detail::find_equation ( const stategraph_pbes &  p, const core::identifier_string &  X, bool  warn = true  )

inline

Definition at line 576 of file stategraph_pbes.h.

find_free_variables()

std::set< data::variable > mcrl2::pbes_system::detail::find_free_variables ( const pbes_expression &  x, const data::variable_list &  bound_variables = data::variable_list(), bool  search_propositional_variables = true  )

inline

Definition at line 125 of file find_free_variables.h.

find_loop()

bool mcrl2::pbes_system::detail::find_loop ( const simple_structure_graph &  G, const vertex_set &  U, structure_graph::index_type  v, structure_graph::index_type  w, std::size_t  p, std::unordered_map< structure_graph::index_type, bool > &  visited  )

inline

Definition at line 27 of file pbesinst_find_loops.h.

find_loops()

template<class Container >

void mcrl2::pbes_system::detail::find_loops ( const simple_structure_graph &  G, const Container &  discovered, const pbesinst_lazy_todo &  todo, std::array< vertex_set, 2 > &  S, std::array< strategy_vector, 2 > &  tau, std::size_t  iteration_count, const detail::structure_graph_builder &  graph_builder  )

inline

Definition at line 75 of file pbesinst_find_loops.h.

find_loops2()

void mcrl2::pbes_system::detail::find_loops2 ( const simple_structure_graph &  G, std::array< vertex_set, 2 > &  S, std::array< strategy_vector, 2 > &  tau, std::size_t  equation_count  )

inline

Definition at line 231 of file pbesinst_fatal_attractors.h.

find_matching_parameters()

std::vector< data::variable > mcrl2::pbes_system::detail::find_matching_parameters ( const pbes &  p, const std::string &  name, const std::set< std::string > &  declarations  )

inline

Find parameter declarations that match a given string.

Definition at line 51 of file pbes_parameter_map.h.

find_quantifier_variables()

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

inline

Definition at line 49 of file is_well_typed.h.

has_conflicting_type()

template<typename Iter >

bool mcrl2::pbes_system::detail::has_conflicting_type	(	Iter	first,
		Iter	last,
		const propositional_variable_instantiation &	v,
		const data::data_specification &	data_spec
	)

Checks if the propositional variable instantiation v has a conflict with the sequence of propositional variable declarations [first, last).

Parameters

first	Start of a sequence of propositional variable declarations
last	End of a sequence of propositional variable declarations

Returns

True if a conflict has been detected

Parameters

v	A propositional variable instantiation

Definition at line 206 of file is_well_typed.h.

has_propositional_variables()

bool mcrl2::pbes_system::detail::has_propositional_variables ( const pbes_expression &  x )

inline

Definition at line 43 of file has_propositional_variables.h.

has_quantifier_name_clashes()

bool mcrl2::pbes_system::detail::has_quantifier_name_clashes ( const pbes_expression &  x )

inline

Definition at line 145 of file is_well_typed.h.

inc_indent()

static void mcrl2::pbes_system::detail::inc_indent ( )

static

Increases the current indent level.

Definition at line 30 of file bqnf_visitor.h.

indent()

static void mcrl2::pbes_system::detail::indent ( )

static

Indents according to the current indent level.

Definition at line 41 of file bqnf_visitor.h.

insert_in_rank_map()

void mcrl2::pbes_system::detail::insert_in_rank_map ( std::map< std::size_t, vertex_set > &  U_rank_map, structure_graph::index_type  u, std::size_t  j, std::size_t  n  )

inline

Definition at line 61 of file pbesinst_fatal_attractors.h.

instantiate_global_variables()

data::mutable_map_substitution mcrl2::pbes_system::detail::instantiate_global_variables ( pbes &  p )

inline

Eliminates the global variables of a PBES, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown.

Definition at line 40 of file instantiate_global_variables.h.

is_bqnf()

template<typename T >

bool mcrl2::pbes_system::detail::is_bqnf

(

const T &

x

)

Determines if an expression is a BQNF expression.

Parameters

x	a PBES object

Returns

true if x is a BQNF expression.

Definition at line 237 of file bqnf_traverser.h.

is_conjunctive()

bool mcrl2::pbes_system::detail::is_conjunctive ( const pbes_expression &  phi )

inline

Definition at line 523 of file srf_pbes.h.

is_pfnf()

template<typename T >

bool mcrl2::pbes_system::detail::is_pfnf

(

const T &

x

)

Definition at line 188 of file is_pfnf.h.

is_pfnf_data_expression()

bool mcrl2::pbes_system::detail::is_pfnf_data_expression ( const pbes_expression &  x )

inline

Definition at line 57 of file is_pfnf.h.

is_pfnf_expression()

bool mcrl2::pbes_system::detail::is_pfnf_expression ( const pbes_expression &  x )

inline

Definition at line 152 of file is_pfnf.h.

is_pfnf_imp()

bool mcrl2::pbes_system::detail::is_pfnf_imp ( const pbes_expression &  x )

inline

Definition at line 86 of file is_pfnf.h.

is_pfnf_inner_and()

bool mcrl2::pbes_system::detail::is_pfnf_inner_and ( const pbes_expression &  x )

inline

Definition at line 106 of file is_pfnf.h.

is_pfnf_or()

bool mcrl2::pbes_system::detail::is_pfnf_or ( const pbes_expression &  x )

inline

Definition at line 79 of file is_pfnf.h.

is_pfnf_or_expression()

bool mcrl2::pbes_system::detail::is_pfnf_or_expression ( const pbes_expression &  x )

inline

Definition at line 63 of file is_pfnf.h.

is_pfnf_outer_and()

bool mcrl2::pbes_system::detail::is_pfnf_outer_and ( const pbes_expression &  x )

inline

Definition at line 121 of file is_pfnf.h.

is_pfnf_simple_expression()

bool mcrl2::pbes_system::detail::is_pfnf_simple_expression ( const pbes_expression &  x )

inline

Definition at line 51 of file is_pfnf.h.

is_ppg()

template<typename T >

bool mcrl2::pbes_system::detail::is_ppg

(

const T &

x

)

Determines if an expression is a PPG expression.

Parameters

x	a PBES object

Returns

true if x is a PPG expression.

Definition at line 260 of file ppg_traverser.h.

is_structured_sort_constructor()

bool mcrl2::pbes_system::detail::is_structured_sort_constructor ( const data::data_specification &  dataspec, const data::function_symbol &  f  )

inline

Definition at line 65 of file absinthe.h.

is_well_typed()

bool mcrl2::pbes_system::detail::is_well_typed ( const pbes_equation &  eqn )

inline

Checks if the equation is well typed.

Returns

True if

• the binding variable parameters have unique names
• the names of the quantifier variables in the equation are disjoint with the binding variable parameter names
• within the scope of a quantifier variable in the formula, no other quantifier variables with the same name may occur

Definition at line 160 of file is_well_typed.h.

is_well_typed_equation()

bool mcrl2::pbes_system::detail::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  )

inline

Definition at line 219 of file is_well_typed.h.

is_well_typed_pbes()

bool mcrl2::pbes_system::detail::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  )

inline

Definition at line 269 of file is_well_typed.h.

lhs_variables()

data::variable_list mcrl2::pbes_system::detail::lhs_variables ( const data::assignment_list &  l )

inline

Definition at line 56 of file lps2pbes_utility.h.

load_pbes()

pbes mcrl2::pbes_system::detail::load_pbes

(

const std::string &

filename

)

Loads a PBES from filename, or from stdin if filename equals "".

Definition at line 292 of file io.cpp.

local_reset_variables()

pbes_expression mcrl2::pbes_system::detail::local_reset_variables ( local_reset_variables_algorithm &  algorithm, const pbes_expression &  x, const stategraph_equation &  eq_X  )

inline

Definition at line 259 of file stategraph_local_reset_variables.h.

lps_reset_variables()

void mcrl2::pbes_system::detail::lps_reset_variables ( lpsstategraph_algorithm &  algorithm, const pbes_expression &  x, const stategraph_equation &  eq_X, const data::variable_list &  process_parameters, std::vector< lps::action_summand > &  summands  )

inline

Definition at line 185 of file lpsstategraph_algorithm.h.

make_and()

data::data_expression mcrl2::pbes_system::detail::make_and ( const data::data_expression &  x1, const data::data_expression &  x2, const data::data_expression &  x3  )

inline

Definition at line 34 of file partial_order_reduction.h.

make_apply_enumerate_builder()

template<template< class, class, class > class Builder, class DataRewriter , class MutableSubstitution >

apply_enumerate_builder< Builder, DataRewriter, MutableSubstitution > mcrl2::pbes_system::detail::make_apply_enumerate_builder	(	const DataRewriter &	R,
		MutableSubstitution &	sigma,
		const data::data_specification &	dataspec,
		data::enumerator_identifier_generator &	id_generator,
		bool	enumerate_infinite_sorts
	)

Definition at line 267 of file enumerate_quantifiers_rewriter.h.

make_apply_rewriter_builder()

template<template< class, class, class > class Builder, class DataRewriter , class SubstitutionFunction >

apply_rewriter_builder< Builder, DataRewriter, SubstitutionFunction > mcrl2::pbes_system::detail::make_apply_rewriter_builder	(	const DataRewriter &	datar,
		SubstitutionFunction &	sigma
	)

Definition at line 114 of file data_rewriter.h.

make_assignments()

data::assignment_list mcrl2::pbes_system::detail::make_assignments ( const data::variable_list &  d, const data::data_expression_list &  e  )

inline

Definition at line 137 of file lpsstategraph_algorithm.h.

make_constelm_substitution()

void mcrl2::pbes_system::detail::make_constelm_substitution ( const std::map< data::variable, data::data_expression > &  m, data::rewriter::substitution_type &  result  )

inline

Definition at line 29 of file constelm.h.

make_exists_()

pbes_expression mcrl2::pbes_system::detail::make_exists_ ( std::set< data::variable >  vars, const pbes_expression &  expr  )

inline

Definition at line 28 of file quantifier_propagate.h.

make_find_propositional_variables_traverser()

template<template< class > class Traverser, class OutputIterator >

find_propositional_variables_traverser< Traverser, OutputIterator > mcrl2::pbes_system::detail::make_find_propositional_variables_traverser

(

OutputIterator

out

)

Definition at line 53 of file find.h.

make_forall_()

pbes_expression mcrl2::pbes_system::detail::make_forall_ ( std::set< data::variable >  vars, const pbes_expression &  expr  )

inline

Definition at line 34 of file quantifier_propagate.h.

make_fresh_variable_substitution()

data::mutable_map_substitution mcrl2::pbes_system::detail::make_fresh_variable_substitution ( const data::variable_list &  variables, data::set_identifier_generator &  id_generator, bool  add_to_context = true  )

inline

Generates a substitution that assigns fresh variables to the given sequence of variables. The identifier generator is used to assign names to the fresh variables. Caveat: the implementation is very inefficient.

Parameters

update_context

If true, then generated names are added to the context

Definition at line 148 of file lps2pbes_utility.h.

make_identifier()

core::identifier_string mcrl2::pbes_system::detail::make_identifier ( const core::identifier_string &  name, lts2pbes_state_type  s  )

inline

Definition at line 30 of file lts2pbes_rhs.h.

make_not()

pbes_expression mcrl2::pbes_system::detail::make_not ( const pbes_expression &  x )

inline

Definition at line 28 of file srf_pbes.h.

make_quantifier()

pbes_expression mcrl2::pbes_system::detail::make_quantifier ( bool  is_forall, const data::variable_list &  vars, const pbes_expression &  body  )

inline

Definition at line 40 of file quantifier_propagate.h.

make_rewrite_pbes_expressions_builder()

template<template< class > class Builder, class Rewriter >

rewrite_pbes_expressions_builder< Builder, Rewriter > mcrl2::pbes_system::detail::make_rewrite_pbes_expressions_builder

(

const Rewriter &

R

)

Definition at line 56 of file rewrite.h.

make_rewrite_pbes_expressions_with_substitution_builder()

template<template< class > class Builder, class Rewriter , class Substitution >

rewrite_pbes_expressions_with_substitution_builder< Builder, Rewriter, Substitution > mcrl2::pbes_system::detail::make_rewrite_pbes_expressions_with_substitution_builder	(	const Rewriter &	R,
		Substitution	sigma
	)

Definition at line 84 of file rewrite.h.

make_typecheck_builder()

typecheck_builder mcrl2::pbes_system::detail::make_typecheck_builder ( data::data_type_checker &  data_typechecker, const data::detail::variable_context &  variables, const detail::pbes_context &  propositional_variables  )

inline

Definition at line 159 of file typecheck.h.

map_at()

template<typename MapContainer >

MapContainer::mapped_type mcrl2::pbes_system::detail::map_at	(	const MapContainer &	m,
		typename MapContainer::key_type	key
	)

Definition at line 30 of file pbes_explorer.cpp.

match_declaration()

bool mcrl2::pbes_system::detail::match_declaration ( const std::string &  text, const data::variable &  d, const data::data_specification &  data_spec  )

inline

Returns true if the declaration text matches with the variable d.

Definition at line 33 of file pbes_parameter_map.h.

mu_expressions()

data::data_expression_list mcrl2::pbes_system::detail::mu_expressions ( const state_formulas::state_formula &  f )

inline

Returns the data expressions corresponding to ass(f)

Parameters

f	A modal formula

Returns

The data expressions corresponding to ass(f)

Definition at line 115 of file lps2pbes_utility.h.

mu_name()

const core::identifier_string & mcrl2::pbes_system::detail::mu_name ( const state_formulas::state_formula &  f )

inline

Definition at line 78 of file lps2pbes_utility.h.

mu_variables()

data::variable_list mcrl2::pbes_system::detail::mu_variables ( const state_formulas::state_formula &  f )

inline

Returns the variables corresponding to ass(f)

Parameters

f	A modal formula

Returns

The variables corresponding to ass(f)

Definition at line 96 of file lps2pbes_utility.h.

myprint()

std::string mcrl2::pbes_system::detail::myprint ( const std::vector< pbes_equation > &  v )

inline

Definition at line 131 of file lps2pbes_utility.h.

nat()

data::variable mcrl2::pbes_system::detail::nat

(

const std::string &

name

)

Returns a data variable of type Nat with a given name.

Parameters

name

A string

Returns

A data variable of type Nat with a given name

Definition at line 28 of file test_utility.h.

normalize_and_or() [1/2]

template<typename T >

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

Definition at line 96 of file normalize_and_or.h.

normalize_and_or() [2/2]

template<typename T >

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

Definition at line 106 of file normalize_and_or.h.

nth_element()

const data::data_expression & mcrl2::pbes_system::detail::nth_element ( const data::data_expression_list &  e, std::size_t  n  )

inline

Definition at line 47 of file stategraph_utility.h.

operator<() [1/2]

bool mcrl2::pbes_system::detail::operator< ( const global_control_flow_graph_vertex &  x, const global_control_flow_graph_vertex &  y  )

inline

Definition at line 740 of file stategraph_graph.h.

operator<() [2/2]

bool mcrl2::pbes_system::detail::operator< ( const local_control_flow_graph_vertex &  u, const local_control_flow_graph_vertex &  v  )

inline

Definition at line 295 of file stategraph_graph.h.

operator<<() [1/11]

template<typename Vertex >

std::ostream & mcrl2::pbes_system::detail::operator<<	(	std::ostream &	out,
		const control_flow_graph< Vertex > &	G
	)

Definition at line 510 of file stategraph_graph.h.

operator<<() [2/11]

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

inline

Definition at line 149 of file stategraph_graph.h.

operator<<() [3/11]

std::ostream & mcrl2::pbes_system::detail::operator<<	(	std::ostream &	out,
		const global_control_flow_graph_vertex &	u
	)

Definition at line 745 of file stategraph_graph.h.

operator<<() [4/11]

std::ostream & mcrl2::pbes_system::detail::operator<< ( std::ostream &  out, const guard_expression &  x  )

inline

Definition at line 231 of file guard_traverser.h.

operator<<() [5/11]

std::ostream & mcrl2::pbes_system::detail::operator<< ( std::ostream &  out, const LCFP_vertex &  u  )

inline

Definition at line 59 of file stategraph_graph.h.

operator<<() [6/11]

std::ostream & mcrl2::pbes_system::detail::operator<< ( std::ostream &  out, const local_control_flow_graph_vertex &  u  )

inline

Definition at line 284 of file stategraph_graph.h.

operator<<() [7/11]

std::ostream & mcrl2::pbes_system::detail::operator<<	(	std::ostream &	out,
		const lts2pbes_lts &	ltsspec
	)

Definition at line 113 of file lts2pbes_lts.h.

operator<<() [8/11]

std::ostream & mcrl2::pbes_system::detail::operator<< ( std::ostream &  out, const lts::lts_lts_t &  ltsspec  )

inline

Definition at line 24 of file lts2pbes_lts.h.

operator<<() [9/11]

std::ostream & mcrl2::pbes_system::detail::operator<< ( std::ostream &  out, const pfnf_implication &  x  )

inline

Definition at line 96 of file pfnf_pbes.h.

operator<<() [10/11]

std::ostream & mcrl2::pbes_system::detail::operator<< ( std::ostream &  out, const predicate_variable &  x  )

inline

Definition at line 140 of file stategraph_pbes.h.

operator<<() [11/11]

std::ostream & mcrl2::pbes_system::detail::operator<< ( std::ostream &  out, const stategraph_vertex &  u  )

inline

Definition at line 180 of file stategraph_global_graph.h.

Par()

data::variable_list mcrl2::pbes_system::detail::Par ( const core::identifier_string &  X, const data::variable_list &  l, const state_formulas::state_formula &  x  )

inline

Definition at line 171 of file lps2pbes_par.h.

parse_pbes_expression()

pbes_expression mcrl2::pbes_system::detail::parse_pbes_expression

(

const std::string &

text

)

Definition at line 160 of file pbes.cpp.

parse_pbes_expression_new()

pbes_expression mcrl2::pbes_system::detail::parse_pbes_expression_new

(

const std::string &

text

)

Definition at line 122 of file pbes.cpp.

parse_pbes_new()

untyped_pbes mcrl2::pbes_system::detail::parse_pbes_new

(

const std::string &

text

)

Definition at line 133 of file pbes.cpp.

parse_pbes_parameter_map()

pbes_parameter_map mcrl2::pbes_system::detail::parse_pbes_parameter_map ( const pbes &  p, const std::string &  text  )

inline

Parses parameter selection for finite pbesinst algorithm.

Definition at line 78 of file pbes_parameter_map.h.

parse_propositional_variable()

propositional_variable mcrl2::pbes_system::detail::parse_propositional_variable

(

const std::string &

text

)

Definition at line 151 of file pbes.cpp.

partial_solve()

void mcrl2::pbes_system::detail::partial_solve ( structure_graph &  G, const pbesinst_lazy_todo &  todo, std::array< vertex_set, 2 > &  S, std::array< strategy_vector, 2 > &  tau, std::size_t  equation_count, const detail::structure_graph_builder &  graph_builder  )

inline

Definition at line 27 of file pbesinst_partial_solve.h.

pbes2data() [1/2]

template<typename T >

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

Definition at line 83 of file pbes2data_rewriter.h.

pbes2data() [2/2]

template<typename T >

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

Definition at line 93 of file pbes2data_rewriter.h.

pbessolve()

bool mcrl2::pbes_system::detail::pbessolve

(

const pbes &

p

)

Definition at line 25 of file pbessolve.h.

pfnf_implications()

std::vector< pbes_expression > mcrl2::pbes_system::detail::pfnf_implications ( const pbes_expression &  x )

inline

Definition at line 218 of file is_pfnf.h.

pos()

data::variable mcrl2::pbes_system::detail::pos

(

const std::string &

name

)

Returns a data variable of type Pos with a given name.

Parameters

name

A string

Returns

A data variable of type Pos with a given name

Definition at line 36 of file test_utility.h.

position_counts()

std::vector< std::size_t > mcrl2::pbes_system::detail::position_counts ( const pbes &  x )

inline

Definition at line 78 of file position_count_traverser.h.

print_equation()

std::string mcrl2::pbes_system::detail::print_equation ( const pbes_equation &  eq )

inline

Definition at line 24 of file stategraph_utility.h.

print_index()

std::string mcrl2::pbes_system::detail::print_index ( std::size_t  index )

inline

Definition at line 26 of file stategraph_algorithm.h.

print_pbes_expressions()

std::string mcrl2::pbes_system::detail::print_pbes_expressions ( const std::set< pbes_expression > &  v )

inline

Definition at line 59 of file stategraph_utility.h.

print_pbes_parameter_map()

std::ostream & mcrl2::pbes_system::detail::print_pbes_parameter_map ( std::ostream &  out, const pbes_parameter_map &  m  )

inline

Print a parameter map.

Definition at line 156 of file pbes_parameter_map.h.

print_removed_equations()

std::string mcrl2::pbes_system::detail::print_removed_equations ( const std::vector< propositional_variable > &  removed )

inline

Definition at line 24 of file remove_equations.h.

print_set()

std::string mcrl2::pbes_system::detail::print_set ( const std::set< std::size_t > &  v )

inline

Definition at line 30 of file stategraph_utility.h.

print_used_function_symbols()

void mcrl2::pbes_system::detail::print_used_function_symbols ( const pbes &  p )

inline

Definition at line 90 of file absinthe.h.

print_vector()

template<typename Container >

std::string mcrl2::pbes_system::detail::print_vector	(	const Container &	v,
		const std::string &	delim
	)

Definition at line 25 of file stategraph_local_reset_variables.h.

propvar()

propositional_variable mcrl2::pbes_system::detail::propvar	(	const std::string &	name,
		const data::variable_list &	parameters
	)

Returns a propositional variable declaration with the given name and parameters.

Parameters

name	A string
parameters	A sequence of data variables

Returns

A propositional variable declaration with the given name and parameters

Definition at line 53 of file test_utility.h.

propvarinst()

propositional_variable_instantiation mcrl2::pbes_system::detail::propvarinst	(	const std::string &	name,
		const data::data_expression_list &	parameters
	)

Returns a propositional variable instantiation with the given name and parameters.

Parameters

name	A string
parameters	A sequence of data expressions

Returns

A propositional variable instantiation with the given name and parameters

Definition at line 62 of file test_utility.h.

quantifier_propagate() [1/2]

pbes_expression mcrl2::pbes_system::detail::quantifier_propagate

(

const pbes_expression &

x

)

quantifier_propagate() [2/2]

void mcrl2::pbes_system::detail::quantifier_propagate ( std::list< std::pair< core::identifier_string, pbes_equation > > &  new_equations, data::set_identifier_generator &  id_gen, const quantifier_propagate_builder::equation_map_t  eqn_map, pbes_expression &  x  )

inline

Definition at line 362 of file quantifier_propagate.h.

quantifiers_inside()

pbes_expression mcrl2::pbes_system::detail::quantifiers_inside ( const pbes_expression &  x )

inline

Definition at line 285 of file quantifiers_inside_rewriter.h.

quantifiers_inside_exists()

pbes_expression mcrl2::pbes_system::detail::quantifiers_inside_exists ( const std::set< data::variable > &  variables, const pbes_expression &  x  )

inline

Definition at line 303 of file quantifiers_inside_rewriter.h.

quantifiers_inside_forall()

pbes_expression mcrl2::pbes_system::detail::quantifiers_inside_forall ( const std::set< data::variable > &  variables, const pbes_expression &  x  )

inline

Definition at line 294 of file quantifiers_inside_rewriter.h.

remove_quantifiers()

pbes_expression mcrl2::pbes_system::detail::remove_quantifiers ( const pbes_expression &  x )

inline

Definition at line 196 of file is_pfnf.h.

replace_global_variables()

void mcrl2::pbes_system::detail::replace_global_variables ( pbes &  p, const data::mutable_map_substitution<> &  sigma  )

inline

Applies a global variable substitution to a PBES.

Definition at line 29 of file instantiate_global_variables.h.

reset_variables()

pbes_expression mcrl2::pbes_system::detail::reset_variables ( global_reset_variables_algorithm &  algorithm, const pbes_expression &  x, const stategraph_equation &  eq_X  )

inline

Definition at line 389 of file stategraph_global_reset_variables.h.

resolve_summand_variable_name_clashes()

void mcrl2::pbes_system::detail::resolve_summand_variable_name_clashes ( srf_summand &  summand, const std::set< core::identifier_string > &  process_parameter_names, data::set_identifier_generator &  generator  )

inline

Definition at line 26 of file resolve_name_clashes.h.

RHS() [1/2]

template<typename TermTraits , typename Parameters >

pbes_expression mcrl2::pbes_system::detail::RHS	(	const state_formulas::state_formula &	x,
		lts2pbes_state_type	s,
		Parameters &	parameters,
		TermTraits	tr
	)

Definition at line 414 of file lts2pbes_rhs.h.

RHS() [2/2]

template<typename TermTraits , typename Parameters >

pbes_expression mcrl2::pbes_system::detail::RHS ( const state_formulas::state_formula &  x, Parameters &  parameters, TermTraits  tr  )

inline

Definition at line 504 of file lps2pbes_rhs.h.

rhs_expressions()

data::data_expression_list mcrl2::pbes_system::detail::rhs_expressions ( const data::assignment_list &  l )

inline

Definition at line 67 of file lps2pbes_utility.h.

RHS_structured()

template<typename TermTraits , typename Parameters >

TermTraits::term_type mcrl2::pbes_system::detail::RHS_structured ( const state_formulas::state_formula &  x, Parameters &  parameters, const data::variable_list &  variables, const fixpoint_symbol &  sigma, std::vector< pbes_equation > &  equations, TermTraits  tr  )

inline

Definition at line 641 of file lps2pbes_rhs.h.

Sat()

template<typename TermTraits >

TermTraits::term_type mcrl2::pbes_system::detail::Sat	(	const lps::multi_action &	a,
		const action_formulas::action_formula &	x,
		data::set_identifier_generator &	id_generator,
		TermTraits	tr
	)

Definition at line 166 of file lps2pbes_sat.h.

save_pbes()

void mcrl2::pbes_system::detail::save_pbes	(	const pbes &	pbesspec,
		const std::string &	filename
	)

Saves an PBES to filename, or to stdout if filename equals "".

Definition at line 307 of file io.cpp.

set_bes_equation_limit()

void mcrl2::pbes_system::detail::set_bes_equation_limit ( std::size_t  size )

inline

Definition at line 40 of file bes_equation_limit.h.

smart_and()

pbes_expression mcrl2::pbes_system::detail::smart_and ( const pbes_expression &  x, const pbes_expression &  y  )

inline

Definition at line 57 of file stategraph_simplify_rewriter.h.

smart_or()

pbes_expression mcrl2::pbes_system::detail::smart_or ( const pbes_expression &  x, const pbes_expression &  y  )

inline

Definition at line 67 of file stategraph_simplify_rewriter.h.

split_and()

void mcrl2::pbes_system::detail::split_and ( const pbes_expression &  expr, std::vector< pbes_expression > &  result  )

inline

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

Parameters

expr	A PBES expression

Returns

A sequence of operands

Definition at line 31 of file is_pfnf.h.

split_or()

void mcrl2::pbes_system::detail::split_or ( const pbes_expression &  expr, std::vector< pbes_expression > &  result  )

inline

Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 || p2 || ... || pn, this will yield a vector of the form [ p1, p2, ..., pn ], assuming that pi does not have a || as main function symbol.

Parameters

expr	A PBES expression

Returns

A sequence of operands

Definition at line 44 of file is_pfnf.h.

split_parameters()

template<typename PropositionalVariable , typename Parameter >

void mcrl2::pbes_system::detail::split_parameters	(	const PropositionalVariable &	X,
		const pbesinst_index_map &	index_map,
		std::vector< Parameter > &	finite,
		std::vector< Parameter > &	infinite
	)

Computes the subset with variables of finite sort and infinite.

Parameters

X	A propositional variable instantiation
index_map	a container storing the indices of the variables that should be expanded by the finite pbesinst algorithm.
finite	A sequence of data expressions
infinite	A sequence of data expressions

Definition at line 98 of file pbesinst_finite_algorithm.h.

split_pfnf_expression()

void mcrl2::pbes_system::detail::split_pfnf_expression ( const pbes_expression &  phi, pbes_expression &  h, std::vector< pbes_expression > &  g  )

inline

Definition at line 233 of file is_pfnf.h.

split_pfnf_implication()

void mcrl2::pbes_system::detail::split_pfnf_implication ( const pbes_expression &  x, pbes_expression &  g, std::vector< propositional_variable_instantiation > &  Xij  )

inline

Definition at line 26 of file pfnf_pbes.h.

srf_and()

std::vector< srf_summand > mcrl2::pbes_system::detail::srf_and ( const pbes_expression &  phi, std::deque< pbes_equation > &  equations, const pbes_equation &  eqn, const data::variable_list &  V, data::set_identifier_generator &  id_generator, const core::identifier_string &  X_true, const core::identifier_string &  X_false, std::vector< srf_equation > &  result  )

inline

Definition at line 506 of file srf_pbes.h.

srf_or()

std::vector< srf_summand > mcrl2::pbes_system::detail::srf_or ( const pbes_expression &  phi, std::deque< pbes_equation > &  equations, const pbes_equation &  eqn, const data::variable_list &  V, data::set_identifier_generator &  id_generator, const core::identifier_string &  X_true, const core::identifier_string &  X_false, std::vector< srf_equation > &  result  )

inline

Definition at line 349 of file srf_pbes.h.

stategraph_not()

pbes_expression mcrl2::pbes_system::detail::stategraph_not ( const pbes_expression &  x )

inline

Definition at line 27 of file stategraph_simplify_rewriter.h.

stategraph_split_and()

void mcrl2::pbes_system::detail::stategraph_split_and ( const pbes_expression &  expr, std::vector< pbes_expression > &  result  )

inline

Definition at line 64 of file stategraph_split.h.

stategraph_split_or()

void mcrl2::pbes_system::detail::stategraph_split_or ( const pbes_expression &  expr, std::vector< pbes_expression > &  result  )

inline

Definition at line 71 of file stategraph_split.h.

symbolic_exploration()

void mcrl2::pbes_system::detail::symbolic_exploration ( const std::string &  input_filename, const std::string &  output_filename, const utilities::file_format &  input_format, const utilities::file_format &  output_format, bool  optimized = true, bool  clustered = false, bool  instantiate = false  )

inline

Definition at line 409 of file symbolic_exploration.h.

target_sort()

data::sort_expression mcrl2::pbes_system::detail::target_sort ( const data::sort_expression &  s )

inline

Definition at line 101 of file absinthe.h.

to_ppg()

pbes mcrl2::pbes_system::detail::to_ppg ( pbes  x )

inline

Rewrites a PBES to a PPG.

Parameters

x

a PBES

Returns

a PPG.

Definition at line 431 of file ppg_rewriter.h.

variable_index()

int mcrl2::pbes_system::detail::variable_index ( const data::variable_list &  variables, const data::variable &  d  )

inline

Finds the index of a variable in a sequence.

Parameters

variables	A sequence of data variables
d	A data variable

Returns

The index of d in v, or -1 if the variable wasn't found

Definition at line 27 of file parelm.h.

Variable Documentation

indent_count

int mcrl2::pbes_system::detail::indent_count = 0

static

The current indent level. Used for debug output.

Definition at line 28 of file bqnf_visitor.h.