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_data_rewriter_with_pbes_substitution_builder
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	count_free_variable_occurrences_traverser
struct	data2pbes_builder
struct	data_rewriter_builder
struct	default_rules_predicate
struct	dominators_cache_type
struct	e_lts2pbes_traverser
struct	e_structured_traverser
struct	e_traverser
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	infinite_quantifier_pvi_traverser
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	pbessolve_tool
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	pre_srf_equation
class	pre_srf_pbes
class	pre_srf_summand
class	predicate_variable
struct	printer
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_other_propositional_variables_with_functions_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_star_substitution
struct	rhs_lts2pbes_traverser
struct	rhs_structured_traverser
struct	rhs_traverser
struct	ruling_statistics_type
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
struct	subsitute_counterexample
struct	substitute_propositional_variables_builder
struct	substitute_propositional_variables_for_bools_builder
class	symbolic_exploration_algorithm
struct	typecheck_builder
struct	variable_data_expression_substitution
struct	variable_variable_substitution

Typedefs
using	standard_form_pair = std::pair< pbes_expression, standard_form_type >
using	lts2pbes_state_type = lts::lts_lts_t::states_size_type
using	pbes_parameter_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	ruling_counts_type = std::map< core::identifier_string, std::map< data::variable, std::map< data::variable, std::size_t > > >
using	pvi_change_counts_type = std::map< core::identifier_string, std::map< data::variable, std::size_t > >
using	ruling_percentages_type = std::map< core::identifier_string, std::map< data::variable, std::map< data::variable, double > > >
using	pfnf_traverser_quantifier = std::pair< bool, data::variable_list >
	Represents a quantifier Qv:V. If the bool is true it is a forall, otherwise an exists.

Enumerations
enum class	standard_form_type { standard_form_both , standard_form_and , standard_form_or }

Functions
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.
std::string	print_removed_equations (const std::vector< propositional_variable > &removed)
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 "".
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)
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.
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 MapContainer >
MapContainer::mapped_type	map_at (const MapContainer &m, typename MapContainer::key_type key)
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	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::map< data::variable, std::size_t >	count_free_variable_occurrences (const pbes_expression &x, const data::variable_list &bound_variables=data::variable_list(), bool search_propositional_variables=true)
std::map< data::variable, std::size_t >	count_free_variable_occurrences (const pbes_expression &x, bool search_propositional_variables=true)
template<typename OutputIterator >
void	find_free_variables (const pbes_expression &x, OutputIterator out, const data::variable_list &bound_variables, bool search_propositional_variables=true)
std::set< data::variable >	find_free_variables (const pbes_expression &x, const data::variable_list &bound_variables, bool search_propositional_variables=true)
std::vector< data::variable >	find_free_variables_in_order (const pbes_expression &x, const data::variable_list &bound_variables, bool search_propositional_variables=true)
std::ostream &	operator<< (std::ostream &out, const guard_expression &x)
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)
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 > requires (std::is_base_of_v<atermpp::aterm, T>)
T	normalize_and_or (const T &x)
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	normalize_and_or (T &x)
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	is_counter_example_positive (const core::identifier_string &name)
	Returns true iff the name is Zpos, name must be a counter example name.
bool	is_counter_example_name (const core::identifier_string &name)
bool	counter_example_index (const core::identifier_string &name, std::size_t &index)
	Extracts the index embedded in a Zpos_<index>_.../Zneg_<index>_... counter example name.
bool	is_counter_example_variable (const propositional_variable &X)
bool	is_counter_example_equation (const pbes_equation &equation)
	Guesses if the PBES equation is a counter example equation.
bool	is_counter_example_instantiation (const propositional_variable_instantiation &inst)
	Guesses if the PBES variable instantiation is for counter example equation.
bool	has_counter_example_information (const pbes &pbesspec)
	Guesses if a pbes has counter example information.
mcrl2::pbes_system::pbes	remove_counterexample_info (const pbes_system::pbes &pbes, bool remove_Lplus=true, bool remove_Lminus=true, bool remove_Lequations=true)
	Removes all equations and expressions related to counter examples from the input PBES.
std::optional< std::reference_wrapper< const pbes_equation > >	find_equation_by_name (const pbes &p, const core::identifier_string &eq_name)
const std::map< data::variable, std::size_t > &	get_or_compute_variable_counts (const core::identifier_string &var_name, const pbes_expression &equation_formula, std::map< core::identifier_string, std::map< data::variable, std::size_t > > &cache)
std::optional< data::variable >	choose_variable_by_count (const core::identifier_string &var_name, const pbes_expression &equation_formula, const std::set< data::variable > &abstracted_vars, std::map< core::identifier_string, std::map< data::variable, std::size_t > > &cache)
std::optional< data::variable >	choose_variable_by_lhs_order (const data::variable_list &all_parameters, const std::set< data::variable > &abstracted_vars, const std::optional< pbes_expression > &formula)
std::optional< data::variable >	choose_variable_by_lhs_order (const propositional_variable &bound_variable, const std::set< data::variable > &abstracted_vars, const std::optional< pbes_expression > &formula)
std::optional< data::variable >	choose_variable_by_rhs_order (const pbes_expression &formula, const std::set< data::variable > &essential_vars)
std::set< data::variable >	dominant_ancestors (const data::variable &start, const ruling_relation_type::equation_relation &ruled_by_map)
std::optional< data::variable >	choose_variable_by_ruling_order (const core::identifier_string &eq_name, const std::set< data::variable > &essential_vars, const ruling_relation_type &ruling_relation, const std::map< data::variable, std::size_t > &var_counts={})
std::string	parse_verbose_equation_name (std::istringstream &iss, const std::string &line)
std::string	parse_bare_equation_name (std::istringstream &iss, const std::string &token, const std::string &line)
void	add_parameter_by_token (const pbes &p, abstract_param_state &state, const core::identifier_string &eq_name, const std::string &token, const std::vector< data::variable > &params)
void	parse_initial_state_line (const pbes &p, abstract_param_state &state, const std::string &line)
void	initialize_initial_abstraction_state (const pbes &p, abstract_param_state &state, const std::string &filename)
ruling_statistics_type	count_rulings (const pbes &p, const data::rewriter &datar)
void	flip_frozen_rulers (ruling_statistics_type &stats)
void	log_ruling_statistics (const ruling_statistics_type &stats)
ruling_percentages_type	compute_ruling_percentages (const ruling_statistics_type &stats)
ruling_relation_type	build_ruling_relation (const ruling_percentages_type &percentages)
void	break_ruling_cycles (const pbes &p, const ruling_percentages_type &percentages, ruling_relation_type &relation)
void	remove_transitive_rulings (ruling_relation_type &relation)
void	log_ruling_relation (const ruling_relation_type &relation)
void	save_ruling_relation (const ruling_relation_type &relation, const std::string &filename)
data::rewriter	construct_rewriter (const pbessolve_options &options, const pbes &pbesspec)
	Constructs a rewriter for the given PBES, optionally restricting the rewrite rules to those that are used by the PBES.
bool	run_solve (const pbes_system::pbes &pbesspec, const data::mutable_map_substitution<> &sigma, structure_graph &G, const pbes_equation_index &equation_index, pbessolve_options options, const std::string &input_filename, const std::string &lpsfile, const std::string &ltsfile, std::string evidence_file, mcrl2::utilities::execution_timer &timer)
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.
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)
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 &calculation_steps, 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 &calculation_steps, 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 &calculation_steps, 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 &calculation_steps, 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)
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 &calculation_steps, 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)
template<bool allow_ce>
void	resolve_summand_variable_name_clashes (pre_srf_summand< allow_ce > &summand, const std::set< core::identifier_string > &process_parameter_names, data::set_identifier_generator &generator)
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	data2pbes (const T &x)
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	data2pbes (T &x)
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 >
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 > class Builder, class DataRewriter , class MutableSubstitution , class PbesSubstitution >
apply_enumerate_builder< Builder, DataRewriter, MutableSubstitution, PbesSubstitution >	make_apply_enumerate_builder (const DataRewriter &R, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes, const data::data_specification &dataspec, data::enumerator_identifier_generator &id_generator, bool enumerate_infinite_sorts)
template<template< class, class, class, class > class Builder, class DataRewriter , class MutableSubstitution >
apply_enumerate_builder< Builder, DataRewriter, MutableSubstitution, no_substitution >	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 > requires (std::is_base_of_v<atermpp::aterm, T>)
data::data_expression	pbes2data (const T &x)
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	pbes2data (T &x)
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)
template<template< class, class, class, class > class Builder, class DataRewriter , class MutableSubstitution , class PbesSubstitution >
apply_data_rewriter_with_pbes_substitution_builder< Builder, DataRewriter, MutableSubstitution, PbesSubstitution >	make_apply_data_rewriter_with_pbes_substitution_builder (const DataRewriter &R, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes)
template<template< class, class, class, class > class Builder, class DataRewriter , class MutableSubstitution >
apply_data_rewriter_with_pbes_substitution_builder< Builder, DataRewriter, MutableSubstitution, no_substitution >	make_apply_data_rewriter_with_pbes_substitution_builder (const DataRewriter &R, MutableSubstitution &sigma)
template<typename Callback >
void	for_each_evidence_transition (structure_graph &G, const std::set< structure_graph::index_type > &V, const lps::specification &lpsspec, const pbes &p, const pbes_equation_index &p_index, Callback yield)
	Walks the extracted evidence vertex set V of a structure graph that was built from the lps2pbes -c encoding, and calls yield once for every Zpos_i/Zneg_i vertex it contains, with the summand it originates from and the transition it encodes. Shared between the LPS-evidence and LTS-evidence sinks so they cannot drift apart.
pbes_expression	make_not (const pbes_expression &x)
template<typename Iterator >
pbes_expression	make_conjunction (Iterator first, Iterator last)
template<typename Iterator >
pbes_expression	make_disjunction (Iterator first, Iterator last)
pbes_expression	distribute_not_over_and (const pbes_expression &x)
	Assuming that x is of the form (x1 && x2 && ... xn), generates expression !x1 || !x2 || ... !xn.
template<bool allow_ce>
std::ostream &	operator<< (std::ostream &out, const pre_srf_summand< allow_ce > &summand)
template<bool allow_ce>
std::ostream &	operator<< (std::ostream &out, const pre_srf_equation< allow_ce > &eqn)
template<bool allow_ce>
std::vector< pre_srf_summand< allow_ce > >	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< pre_srf_equation< allow_ce > > &result, bool merge_simple_expressions)
template<bool allow_ce>
std::vector< pre_srf_summand< allow_ce > >	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< pre_srf_equation< allow_ce > > &result, bool merge_simple_expressions)
bool	is_conjunctive (const pbes_expression &phi, bool allow_ce)
template<bool allow_ce>
detail::pre_srf_pbes< allow_ce >	pbes2pre_srf (const pbes &p, bool merge_simple_expressions=true)
	Converts a PBES into standard recursive form.
atermpp::aterm	remove_opid_index (const atermpp::aterm &x)
atermpp::aterm	add_opid_index (const atermpp::aterm &x)
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

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

Definition at line 27 of file lts2pbes_rhs.h.

pbes_parameter_map

using mcrl2::pbes_system::detail::pbes_parameter_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 23 of file pbes_parameter_map.h.

pfnf_traverser_quantifier

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

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

Definition at line 26 of file pfnf_traverser.h.

pvi_change_counts_type

using mcrl2::pbes_system::detail::pvi_change_counts_type = typedef std::map<core::identifier_string, std::map<data::variable, std::size_t> >

Definition at line 710 of file pbescegps_utilities.h.

ruling_counts_type

using mcrl2::pbes_system::detail::ruling_counts_type = typedef std::map<core::identifier_string, std::map<data::variable, std::map<data::variable, std::size_t> >>

Definition at line 706 of file pbescegps_utilities.h.

ruling_percentages_type

using mcrl2::pbes_system::detail::ruling_percentages_type = typedef std::map<core::identifier_string, std::map<data::variable, std::map<data::variable, double> >>

Definition at line 854 of file pbescegps_utilities.h.

standard_form_pair

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

Definition at line 30 of file normal_forms.h.

Enumeration Type Documentation

standard_form_type

enum class mcrl2::pbes_system::detail::standard_form_type

strong

Enumerator
standard_form_both
standard_form_and
standard_form_or

Definition at line 23 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 57 of file absinthe.h.

absinthe_data_specification()

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

inline

Definition at line 50 of file absinthe.h.

add_opid_index()

atermpp::aterm mcrl2::pbes_system::detail::add_opid_index ( const atermpp::aterm &  x )

inline

Definition at line 48 of file structure_graph_io.h.

add_parameter_by_token()

void mcrl2::pbes_system::detail::add_parameter_by_token ( const pbes &  p, abstract_param_state &  state, const core::identifier_string &  eq_name, const std::string &  token, const std::vector< data::variable > &  params  )

inline

Definition at line 608 of file pbescegps_utilities.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 255 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 )

inline

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 42 of file test_utility.h.

break_ruling_cycles()

void mcrl2::pbes_system::detail::break_ruling_cycles ( const pbes &  p, const ruling_percentages_type &  percentages, ruling_relation_type &  relation  )

inline

Definition at line 921 of file pbescegps_utilities.h.

build_ruling_relation()

ruling_relation_type mcrl2::pbes_system::detail::build_ruling_relation ( const ruling_percentages_type &  percentages )

inline

Definition at line 882 of file pbescegps_utilities.h.

check_bes_equation_limit()

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

inline

Definition at line 44 of file bes_equation_limit.h.

choose_variable_by_count()

std::optional< data::variable > mcrl2::pbes_system::detail::choose_variable_by_count ( const core::identifier_string &  var_name, const pbes_expression &  equation_formula, const std::set< data::variable > &  abstracted_vars, std::map< core::identifier_string, std::map< data::variable, std::size_t > > &  cache  )

inline

Definition at line 375 of file pbescegps_utilities.h.

choose_variable_by_lhs_order() [1/2]

std::optional< data::variable > mcrl2::pbes_system::detail::choose_variable_by_lhs_order ( const data::variable_list &  all_parameters, const std::set< data::variable > &  abstracted_vars, const std::optional< pbes_expression > &  formula  )

inline

Definition at line 400 of file pbescegps_utilities.h.

choose_variable_by_lhs_order() [2/2]

std::optional< data::variable > mcrl2::pbes_system::detail::choose_variable_by_lhs_order ( const propositional_variable &  bound_variable, const std::set< data::variable > &  abstracted_vars, const std::optional< pbes_expression > &  formula  )

inline

Definition at line 416 of file pbescegps_utilities.h.

choose_variable_by_rhs_order()

std::optional< data::variable > mcrl2::pbes_system::detail::choose_variable_by_rhs_order ( const pbes_expression &  formula, const std::set< data::variable > &  essential_vars  )

inline

Definition at line 423 of file pbescegps_utilities.h.

choose_variable_by_ruling_order()

std::optional< data::variable > mcrl2::pbes_system::detail::choose_variable_by_ruling_order ( const core::identifier_string &  eq_name, const std::set< data::variable > &  essential_vars, const ruling_relation_type &  ruling_relation, const std::map< data::variable, std::size_t > &  var_counts = {}  )

inline

Definition at line 482 of file pbescegps_utilities.h.

complete_pbes()

void mcrl2::pbes_system::detail::complete_pbes

(

pbes &

x

)

Definition at line 143 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_ruling_percentages()

ruling_percentages_type mcrl2::pbes_system::detail::compute_ruling_percentages ( const ruling_statistics_type &  stats )

inline

Definition at line 857 of file pbescegps_utilities.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 164 of file pfnf_traverser.h.

construct_rewriter()

data::rewriter mcrl2::pbes_system::detail::construct_rewriter ( const pbessolve_options &  options, const pbes &  pbesspec  )

inline

Constructs a rewriter for the given PBES, optionally restricting the rewrite rules to those that are used by the PBES.

Parameters

options	The algorithm options that determine the rewrite strategy and whether unused rewrite rules are removed.
pbesspec	The PBES for which the rewriter is constructed, used both for its data specification and (if enabled) the set of used function symbols.

Precondition

The data specification of pbesspec must contain every function that may be rewritten during instantiation.

Returns

A rewriter over the data specification of pbesspec.

Definition at line 53 of file pbessolve_algorithm.h.

count_free_variable_occurrences() [1/2]

std::map< data::variable, std::size_t > mcrl2::pbes_system::detail::count_free_variable_occurrences ( const pbes_expression &  x, bool  search_propositional_variables = true  )

inline

Definition at line 96 of file count_free_variables.h.

count_free_variable_occurrences() [2/2]

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

inline

Definition at line 87 of file count_free_variables.h.

count_rulings()

ruling_statistics_type mcrl2::pbes_system::detail::count_rulings ( const pbes &  p, const data::rewriter &  datar  )

inline

Definition at line 719 of file pbescegps_utilities.h.

counter_example_index()

bool mcrl2::pbes_system::detail::counter_example_index ( const core::identifier_string &  name, std::size_t &  index  )

inline

Extracts the index embedded in a Zpos_<index>_.../Zneg_<index>_... counter example name.

Parameters

name	A PBES variable name.
index	Set to the extracted index if the name matches, left unchanged otherwise.

Returns

True iff name is a counter example name, in which case index is updated.

Definition at line 54 of file pbes_remove_counterexample_info.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  )

inline

Definition at line 33 of file pbesinst_alternative_lazy_algorithm.h.

data2pbes() [1/2]

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

T mcrl2::pbes_system::detail::data2pbes

(

const T &

x

)

Definition at line 128 of file data2pbes_rewriter.h.

data2pbes() [2/2]

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

void mcrl2::pbes_system::detail::data2pbes

(

T &

x

)

Definition at line 137 of file data2pbes_rewriter.h.

data_rewrite() [1/2]

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 31 of file data_rewriter.h.

data_rewrite() [2/2]

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 25 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.

distribute_not_over_and()

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

inline

Assuming that x is of the form (x1 && x2 && ... xn), generates expression !x1 || !x2 || ... !xn.

Parameters

x	a pbes_expression that is conjunctive

Returns

disjunctive expression that is equivalent to !x.

Definition at line 99 of file srf_pbes.h.

dominant_ancestors()

std::set< data::variable > mcrl2::pbes_system::detail::dominant_ancestors ( const data::variable &  start, const ruling_relation_type::equation_relation &  ruled_by_map  )

inline

Definition at line 439 of file pbescegps_utilities.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 306 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 &  calculation_steps, std::size_t  equation_count  )

inline

Definition at line 227 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 &	calculation_steps,
		std::size_t	equation_count,
		Compare	compare
	)

Definition at line 131 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 &  calculation_steps, std::size_t  equation_count  )

inline

Definition at line 294 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_equation_by_name()

std::optional< std::reference_wrapper< const pbes_equation > > mcrl2::pbes_system::detail::find_equation_by_name ( const pbes &  p, const core::identifier_string &  eq_name  )

inline

Definition at line 200 of file pbescegps_utilities.h.

find_free_variables() [1/2]

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

inline

Definition at line 143 of file find_free_variables.h.

find_free_variables() [2/2]

template<typename OutputIterator >

void mcrl2::pbes_system::detail::find_free_variables	(	const pbes_expression &	x,
		OutputIterator	out,
		const data::variable_list &	bound_variables,
		bool	search_propositional_variables = true
	)

Definition at line 134 of file find_free_variables.h.

find_free_variables_in_order()

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

inline

Definition at line 152 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 &  calculation_steps, std::size_t  equation_count  )

inline

Definition at line 239 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 45 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 47 of file is_well_typed.h.

flip_frozen_rulers()

void mcrl2::pbes_system::detail::flip_frozen_rulers ( ruling_statistics_type &  stats )

inline

Definition at line 770 of file pbescegps_utilities.h.

for_each_evidence_transition()

template<typename Callback >

void mcrl2::pbes_system::detail::for_each_evidence_transition	(	structure_graph &	G,
		const std::set< structure_graph::index_type > &	V,
		const lps::specification &	lpsspec,
		const pbes &	p,
		const pbes_equation_index &	p_index,
		Callback	yield
	)

Walks the extracted evidence vertex set V of a structure graph that was built from the lps2pbes -c encoding, and calls yield once for every Zpos_i/Zneg_i vertex it contains, with the summand it originates from and the transition it encodes. Shared between the LPS-evidence and LTS-evidence sinks so they cannot drift apart.

Parameters

yield

A callback with signature void(std::size_t summand_index, const data::data_expression_vector& source, const lps::multi_action& a, const data::data_expression_vector& target) where source and target have lpsspec.process().process_parameters().size() elements, positionally corresponding to those process parameters.

Definition at line 36 of file solve_structure_graph.h.

get_or_compute_variable_counts()

const std::map< data::variable, std::size_t > & mcrl2::pbes_system::detail::get_or_compute_variable_counts ( const core::identifier_string &  var_name, const pbes_expression &  equation_formula, std::map< core::identifier_string, std::map< data::variable, std::size_t > > &  cache  )

inline

Definition at line 361 of file pbescegps_utilities.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 200 of file is_well_typed.h.

has_counter_example_information()

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

inline

Guesses if a pbes has counter example information.

Definition at line 88 of file pbes_remove_counterexample_info.h.

has_propositional_variables()

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

inline

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

initialize_initial_abstraction_state()

void mcrl2::pbes_system::detail::initialize_initial_abstraction_state ( const pbes &  p, abstract_param_state &  state, const std::string &  filename  )

inline

Definition at line 681 of file pbescegps_utilities.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 34 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 230 of file bqnf_traverser.h.

is_conjunctive()

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

inline

Definition at line 751 of file srf_pbes.h.

is_counter_example_equation()

bool mcrl2::pbes_system::detail::is_counter_example_equation ( const pbes_equation &  equation )

inline

Guesses if the PBES equation is a counter example equation.

Definition at line 74 of file pbes_remove_counterexample_info.h.

is_counter_example_instantiation()

bool mcrl2::pbes_system::detail::is_counter_example_instantiation ( const propositional_variable_instantiation &  inst )

inline

Guesses if the PBES variable instantiation is for counter example equation.

Definition at line 81 of file pbes_remove_counterexample_info.h.

is_counter_example_name()

bool mcrl2::pbes_system::detail::is_counter_example_name ( const core::identifier_string &  name )

inline

Definition at line 42 of file pbes_remove_counterexample_info.h.

is_counter_example_positive()

bool mcrl2::pbes_system::detail::is_counter_example_positive ( const core::identifier_string &  name )

inline

Returns true iff the name is Zpos, name must be a counter example name.

Definition at line 34 of file pbes_remove_counterexample_info.h.

is_counter_example_variable()

bool mcrl2::pbes_system::detail::is_counter_example_variable ( const propositional_variable &  X )

inline

Definition at line 67 of file pbes_remove_counterexample_info.h.

is_pfnf()

template<typename T >

bool mcrl2::pbes_system::detail::is_pfnf

(

const T &

x

)

Definition at line 184 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 241 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 64 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 154 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 213 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 266 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 279 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 244 of file stategraph_local_reset_variables.h.

log_ruling_relation()

void mcrl2::pbes_system::detail::log_ruling_relation ( const ruling_relation_type &  relation )

inline

Definition at line 1090 of file pbescegps_utilities.h.

log_ruling_statistics()

void mcrl2::pbes_system::detail::log_ruling_statistics ( const ruling_statistics_type &  stats )

inline

Definition at line 815 of file pbescegps_utilities.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_data_rewriter_with_pbes_substitution_builder() [1/2]

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

apply_data_rewriter_with_pbes_substitution_builder< Builder, DataRewriter, MutableSubstitution, no_substitution > mcrl2::pbes_system::detail::make_apply_data_rewriter_with_pbes_substitution_builder	(	const DataRewriter &	R,
		MutableSubstitution &	sigma
	)

Definition at line 314 of file simplify_rewriter.h.

make_apply_data_rewriter_with_pbes_substitution_builder() [2/2]

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

apply_data_rewriter_with_pbes_substitution_builder< Builder, DataRewriter, MutableSubstitution, PbesSubstitution > mcrl2::pbes_system::detail::make_apply_data_rewriter_with_pbes_substitution_builder	(	const DataRewriter &	R,
		MutableSubstitution &	sigma,
		const PbesSubstitution &	sigma_pbes
	)

Definition at line 301 of file simplify_rewriter.h.

make_apply_enumerate_builder() [1/2]

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

apply_enumerate_builder< Builder, DataRewriter, MutableSubstitution, no_substitution > 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 318 of file enumerate_quantifiers_rewriter.h.

make_apply_enumerate_builder() [2/2]

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

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

Definition at line 299 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 102 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_conjunction()

template<typename Iterator >

pbes_expression mcrl2::pbes_system::detail::make_conjunction	(	Iterator	first,
		Iterator	last
	)

Definition at line 54 of file srf_pbes.h.

make_disjunction()

template<typename Iterator >

pbes_expression mcrl2::pbes_system::detail::make_disjunction	(	Iterator	first,
		Iterator	last
	)

Definition at line 75 of file srf_pbes.h.

make_exists_()

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

inline

Definition at line 27 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 50 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 33 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 40 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 39 of file quantifier_propagate.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 156 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 29 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 27 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 )

inline

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 26 of file test_utility.h.

normalize_and_or() [1/2]

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

T mcrl2::pbes_system::detail::normalize_and_or

(

const T &

x

)

Definition at line 91 of file normalize_and_or.h.

normalize_and_or() [2/2]

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

void mcrl2::pbes_system::detail::normalize_and_or

(

T &

x

)

Definition at line 100 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 717 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/13]

template<typename Vertex >

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

Definition at line 509 of file stategraph_graph.h.

operator<<() [2/13]

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/13]

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

inline

Definition at line 722 of file stategraph_graph.h.

operator<<() [4/13]

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

inline

Definition at line 242 of file guard_traverser.h.

operator<<() [5/13]

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/13]

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/13]

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

inline

Definition at line 113 of file lts2pbes_lts.h.

operator<<() [8/13]

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/13]

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

inline

Definition at line 98 of file pfnf_pbes.h.

operator<<() [10/13]

template<bool allow_ce>

std::ostream & mcrl2::pbes_system::detail::operator<< ( std::ostream &  out, const pre_srf_equation< allow_ce > &  eqn  )

inline

Definition at line 263 of file srf_pbes.h.

operator<<() [11/13]

template<bool allow_ce>

std::ostream & mcrl2::pbes_system::detail::operator<< ( std::ostream &  out, const pre_srf_summand< allow_ce > &  summand  )

inline

Definition at line 183 of file srf_pbes.h.

operator<<() [12/13]

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

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 167 of file lps2pbes_par.h.

parse_bare_equation_name()

std::string mcrl2::pbes_system::detail::parse_bare_equation_name ( std::istringstream &  iss, const std::string &  token, const std::string &  line  )

inline

Definition at line 589 of file pbescegps_utilities.h.

parse_initial_state_line()

void mcrl2::pbes_system::detail::parse_initial_state_line ( const pbes &  p, abstract_param_state &  state, const std::string &  line  )

inline

Definition at line 645 of file pbescegps_utilities.h.

parse_pbes_expression()

pbes_expression mcrl2::pbes_system::detail::parse_pbes_expression

(

const std::string &

text

)

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

parse_pbes_new()

untyped_pbes mcrl2::pbes_system::detail::parse_pbes_new

(

const std::string &

text

)

Definition at line 132 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 72 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 150 of file pbes.cpp.

parse_verbose_equation_name()

std::string mcrl2::pbes_system::detail::parse_verbose_equation_name ( std::istringstream &  iss, const std::string &  line  )

inline

Definition at line 558 of file pbescegps_utilities.h.

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

data::data_expression mcrl2::pbes_system::detail::pbes2data

(

const T &

x

)

Definition at line 84 of file pbes2data_rewriter.h.

pbes2data() [2/2]

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

void mcrl2::pbes_system::detail::pbes2data

(

T &

x

)

Definition at line 93 of file pbes2data_rewriter.h.

pbes2pre_srf()

template<bool allow_ce>

detail::pre_srf_pbes< allow_ce > mcrl2::pbes_system::detail::pbes2pre_srf ( const pbes &  p, bool  merge_simple_expressions = true  )

inline

Converts a PBES into standard recursive form.

Precondition

The pbes p must be normalized

Parameters

allow_ce	If true, then counter example expressions are allowed in the simple expressions of the PBES.
merge_simple_expressions	If true, then simple expressions are merged into the summands of the SRF equations.

Returns

A pre-SRF PBES, which is a PBES in SRF format

Definition at line 861 of file srf_pbes.h.

pbessolve()

bool mcrl2::pbes_system::detail::pbessolve ( const pbes &  p )

inline

Definition at line 567 of file pbessolve_algorithm.h.

pfnf_implications()

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

inline

Definition at line 214 of file is_pfnf.h.

pos()

data::variable mcrl2::pbes_system::detail::pos ( const std::string &  name )

inline

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 34 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 75 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 22 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 150 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 23 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 89 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 21 of file stategraph_local_reset_variables.h.

propvar()

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

inline

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 51 of file test_utility.h.

propvarinst()

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

inline

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 60 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 361 of file quantifier_propagate.h.

quantifiers_inside()

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

inline

Definition at line 310 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 328 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 319 of file quantifiers_inside_rewriter.h.

remove_counterexample_info()

mcrl2::pbes_system::pbes mcrl2::pbes_system::detail::remove_counterexample_info ( const pbes_system::pbes &  pbes, bool  remove_Lplus = true, bool  remove_Lminus = true, bool  remove_Lequations = true  )

inline

Removes all equations and expressions related to counter examples from the input PBES.

Replace the corresponding PBES variables by true and false respectively.

Definition at line 138 of file pbes_remove_counterexample_info.h.

remove_opid_index()

atermpp::aterm mcrl2::pbes_system::detail::remove_opid_index ( const atermpp::aterm &  x )

inline

Definition at line 39 of file structure_graph_io.h.

remove_quantifiers()

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

inline

Definition at line 192 of file is_pfnf.h.

remove_transitive_rulings()

void mcrl2::pbes_system::detail::remove_transitive_rulings ( ruling_relation_type &  relation )

inline

Definition at line 1027 of file pbescegps_utilities.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 23 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 381 of file stategraph_global_reset_variables.h.

resolve_summand_variable_name_clashes()

template<bool allow_ce>

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

inline

Definition at line 27 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 506 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 643 of file lps2pbes_rhs.h.

run_solve()

bool mcrl2::pbes_system::detail::run_solve ( const pbes_system::pbes &  pbesspec, const data::mutable_map_substitution<> &  sigma, structure_graph &  G, const pbes_equation_index &  equation_index, pbessolve_options  options, const std::string &  input_filename, const std::string &  lpsfile, const std::string &  ltsfile, std::string  evidence_file, mcrl2::utilities::execution_timer &  timer  )

inline

Definition at line 68 of file pbessolve_algorithm.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 294 of file io.cpp.

save_ruling_relation()

void mcrl2::pbes_system::detail::save_ruling_relation ( const ruling_relation_type &  relation, const std::string &  filename  )

inline

Definition at line 1115 of file pbescegps_utilities.h.

set_bes_equation_limit()

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

inline

Definition at line 38 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 97 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 229 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 28 of file pfnf_pbes.h.

srf_and()

template<bool allow_ce>

std::vector< pre_srf_summand< allow_ce > > 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< pre_srf_equation< allow_ce > > &  result, bool  merge_simple_expressions  )

inline

Definition at line 736 of file srf_pbes.h.

srf_or()

template<bool allow_ce>

std::vector< pre_srf_summand< allow_ce > > 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< pre_srf_equation< allow_ce > > &  result, bool  merge_simple_expressions  )

inline

Definition at line 495 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 386 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 100 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 423 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 28 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.