Classes
struct	add_capture_avoiding_replacement

struct	add_capture_avoiding_replacement_with_an_identifier_generator

struct	add_data_rewriter

struct	add_simplify

struct	add_simplify_quantifiers

struct	apply_e_lts2pres_traverser

struct	apply_e_structured_traverser

struct	apply_e_traverser

struct	apply_enumerate_builder

struct	apply_rewriter_builder

struct	apply_rhs_lts2pres_traverser

struct	apply_rhs_structured_traverser

struct	apply_rhs_traverser

struct	apply_sat_traverser

struct	data_rewriter_builder

struct	e_lts2pres_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 pres 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...

class	internal_and

class	internal_const_multiply

class	internal_or

class	internal_plus

class	internal_propositional_variable

class	internal_real_constant

class	internal_res_expression

struct	linear_fixed_point_equation

struct	lps2pres_parameters

class	lts2pres_lts

struct	lts2pres_parameters

struct	occurring_variable_visitor

struct	par_traverser

struct	pres_actions

class	pres_context

class	pres_property_map
	Stores the following properties of a linear process specification: More...

struct	presinst_finite_builder
	Visitor that applies a propositional variable substitution to a pres expression. More...

struct	printer

struct	QPVI
	A quantified predicate variable instantiation. More...

class	quantified_variable

struct	quantifiers_inside_builder

struct	quantifiers_inside_infimum_builder

struct	quantifiers_inside_supremum_builder

struct	res_equation_limit

struct	rewrite_pres_expressions_builder

struct	rewrite_pres_expressions_with_substitution_builder

struct	rhs_lts2pres_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	typecheck_builder

Typedefs
typedef lts::probabilistic_lts_lts_t::states_size_type	lts2pres_state_type

typedef std::map< core::identifier_string, std::vector< data::variable > >	pres_parameter_map
	Data structure for storing the variables that should be expanded by the finite presinst algorithm.

Enumerations
enum	internal_res_expression_type { propositional_variable , real_constant , plus , and_ , or_ , const_multiply }

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

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

bool	has_propositional_variables (const pres_expression &x)

void	replace_global_variables (pres &p, const data::mutable_map_substitution<> &sigma)
	Applies a global variable substitution to a PRES.

data::mutable_map_substitution	instantiate_global_variables (pres &p)
	Eliminates the global variables of a PRES, 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 pres_expression &x)

bool	has_quantifier_name_clashes (const pres_expression &x)

bool	is_well_typed (const pres_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 pres_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_pres (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< pres_equation > &result, TermTraits tr)

template<typename TermTraits , typename Parameters >
void	E_structured (const state_formulas::state_formula &x, Parameters &parameters, std::vector< pres_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 >
pres_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< pres_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< pres_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.

template<typename TermTraits , typename Parameters >
void	E_lts2pres (const state_formulas::state_formula &x, Parameters &parameters, std::vector< pres_equation > &result, TermTraits tr)

std::ostream &	operator<< (std::ostream &out, const lts::probabilistic_lts_lts_t &ltsspec)

std::ostream &	operator<< (std::ostream &out, const lts2pres_lts &ltsspec)

core::identifier_string	make_identifier (const core::identifier_string &name, lts2pres_state_type s)

template<typename TermTraits , typename Parameters >
pres_expression	RHS (const state_formulas::state_formula &x, lts2pres_state_type s, Parameters &parameters, TermTraits tr)

pres	load_pres (const std::string &filename)
	Loads a PRES from filename, or from stdin if filename equals "".

void	save_pres (const pres &presspec, const std::string &filename)
	Saves an PRES 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 pres &p, const std::string &name, const std::set< std::string > &declarations)
	Find parameter declarations that match a given string.

pres_parameter_map	parse_pres_parameter_map (const pres &p, const std::string &text)
	Parses parameter selection for finite presinst algorithm.

std::ostream &	print_pres_parameter_map (std::ostream &out, const pres_parameter_map &m)
	Print a parameter map.

void	set_res_equation_limit (std::size_t size)

void	check_res_equation_limit (std::size_t size)

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.

pres_expression	parse_pres_expression_new (const std::string &text)

untyped_pres	parse_pres_new (const std::string &text)

void	complete_pres (pres &x)

propositional_variable	parse_propositional_variable (const std::string &text)

pres_expression	parse_pres_expression (const std::string &text)

template<typename PropositionalVariable , typename Parameter >
void	split_parameters (const PropositionalVariable &X, const presinst_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)

pres_expression	group_sums_conjuncts_disjuncts (const pres_expression &conjunctive_disjunctive_nf, const data::rewriter &rewrite)

void	collect_grouped_ands_ors (const pres_expression &conjunctive_disjunctive_nf, const data::rewriter &rewrite, std::set< pres_expression > &collected_terms, const bool collect_ands)

void	collect_grouped_constant_multiplies_mininf_terms_and_constant (const pres_expression &conjunctive_disjunctive_nf, std::map< pres_expression, data::data_expression > &constant_multiply_terms, std::set< pres_expression > &mininf_terms, pres_expression &constant, const data::rewriter &rewrite)

void	push_and_inside (pres_expression &result, const pres_expression t1, const pres_expression &t2, const bool conjunctive_normal_form)

void	push_or_inside (pres_expression &result, const pres_expression t1, const pres_expression &t2, const bool conjunctive_normal_form)

void	push_plus_inside (pres_expression &result, const pres_expression t1, const pres_expression &t2, const bool conjunctive_normal_form)

void	push_constant_inside (pres_expression &result, const data::data_expression &constant, const pres_expression &t)

void	collect_line (linear_fixed_point_equation &line, const propositional_variable &v, const pres_expression &t, const bool minimal_fixed_point)

void	collect_lines (std::vector< linear_fixed_point_equation > &found_lines, const propositional_variable &v, const pres_expression &t, const bool minimal_fixed_point)

void	collect_m_and_split_lines (const std::vector< linear_fixed_point_equation > &lines, pres_expression &m, std::vector< linear_fixed_point_equation > &shallow_lines, std::vector< linear_fixed_point_equation > &steep_lines, std::vector< linear_fixed_point_equation > &flat_lines, const data::rewriter &rewriter, const bool minimal_fixed_point)

void	conjunction_disjunction_f_j (pres_expression &result, bool &result_defined, std::vector< linear_fixed_point_equation > &l, const bool is_conjunction)

pres_expression	conjunction_disjunction_f_j (std::vector< linear_fixed_point_equation > &l1, std::vector< linear_fixed_point_equation > &l2, std::vector< linear_fixed_point_equation > &l3, const bool is_conjunction)

pres_expression	disjunction_infinity_cj_prime (std::vector< linear_fixed_point_equation > &l1, std::vector< linear_fixed_point_equation > &l2, std::vector< linear_fixed_point_equation > &l3)

pres_expression	disjunction_cj_fj (std::vector< linear_fixed_point_equation > &l)

pres_expression	conjunction_cj_fj (std::vector< linear_fixed_point_equation > &l)

pres_expression	disjunction_fj_cj (std::vector< linear_fixed_point_equation > &l, const pres_expression &U, const data::rewriter &rewriter)

pres_expression	conjunction_fj_cj (std::vector< linear_fixed_point_equation > &l, const pres_expression &U, const data::rewriter &rewriter)

pres_expression	solve_fixed_point_inner (const propositional_variable &v, const pres_expression &t, const data::data_specification &dataspec, const data::rewriter &rewriter, const bool minimal_fixed_point)

const pres_expression	solve_single_equation (const fixpoint_symbol &f, const propositional_variable &v, const pres_expression &t, const data::data_specification &dataspec, const data::rewriter &rewriter)

double	evaluate (const pres_expression &p, const std::unordered_map< core::identifier_string, double > &solution)

double	evaluate_directed (const internal_res_expression *p, const std::vector< double > &solution)

template<template< class > class Builder, class Rewriter >
rewrite_pres_expressions_builder< Builder, Rewriter >	make_rewrite_pres_expressions_builder (const Rewriter &R)

template<template< class > class Builder, class Rewriter , class Substitution >
rewrite_pres_expressions_with_substitution_builder< Builder, Rewriter, Substitution >	make_rewrite_pres_expressions_with_substitution_builder (const Rewriter &R, Substitution sigma)

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 data::data_specification &dataspec, 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)

pres_expression	quantifiers_inside (const pres_expression &x)

pres_expression	quantifiers_inside_infimum (const std::set< data::variable > &variables, const pres_expression &x)

pres_expression	quantifiers_inside_supremum (const std::set< data::variable > &variables, const pres_expression &x)

template<typename BinaryOperation >
std::tuple< pres_expression, pres_expression >	compute_Phi_Psi (const std::vector< pres_expression > &X, const std::set< data::variable > &V, BinaryOperation op, pres_expression empty_sequence_result)

void	check_lps2pres_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::pres_context &propositional_variables)

Typedef Documentation

◆ lts2pres_state_type

typedef lts::probabilistic_lts_lts_t::states_size_type mcrl2::pres_system::detail::lts2pres_state_type

Definition at line 27 of file lts2pres_rhs.h.

◆ pres_parameter_map

typedef std::map<core::identifier_string, std::vector<data::variable> > mcrl2::pres_system::detail::pres_parameter_map

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

Definition at line 29 of file pres_parameter_map.h.

Enumeration Type Documentation

◆ internal_res_expression_type

enum mcrl2::pres_system::detail::internal_res_expression_type

Enumerator
propositional_variable
real_constant
plus
and_
or_
const_multiply

Definition at line 33 of file ressolve_numerical_directed.h.

Function Documentation

◆ check_lps2pres_actions()

void mcrl2::pres_system::detail::check_lps2pres_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 lps2pres.h.

◆ check_res_equation_limit()

void mcrl2::pres_system::detail::check_res_equation_limit ( std::size_t size )

inline

Definition at line 46 of file res_equation_limit.h.

◆ collect_grouped_ands_ors()

void mcrl2::pres_system::detail::collect_grouped_ands_ors	(	const pres_expression &	conjunctive_disjunctive_nf,
		const data::rewriter &	rewrite,
		std::set< pres_expression > &	collected_terms,
		const bool	collect_ands
	)

Definition at line 62 of file ressolve_gauss_elimination.h.

◆ collect_grouped_constant_multiplies_mininf_terms_and_constant()

void mcrl2::pres_system::detail::collect_grouped_constant_multiplies_mininf_terms_and_constant	(	const pres_expression &	conjunctive_disjunctive_nf,
		std::map< pres_expression, data::data_expression > &	constant_multiply_terms,
		std::set< pres_expression > &	mininf_terms,
		pres_expression &	constant,
		const data::rewriter &	rewrite
	)

Definition at line 109 of file ressolve_gauss_elimination.h.

◆ collect_line()

void mcrl2::pres_system::detail::collect_line	(	linear_fixed_point_equation &	line,
		const propositional_variable &	v,
		const pres_expression &	t,
		const bool	minimal_fixed_point
	)

Definition at line 545 of file ressolve_gauss_elimination.h.

◆ collect_lines()

void mcrl2::pres_system::detail::collect_lines	(	std::vector< linear_fixed_point_equation > &	found_lines,
		const propositional_variable &	v,
		const pres_expression &	t,
		const bool	minimal_fixed_point
	)

Definition at line 599 of file ressolve_gauss_elimination.h.

◆ collect_m_and_split_lines()

void mcrl2::pres_system::detail::collect_m_and_split_lines	(	const std::vector< linear_fixed_point_equation > &	lines,
		pres_expression &	m,
		std::vector< linear_fixed_point_equation > &	shallow_lines,
		std::vector< linear_fixed_point_equation > &	steep_lines,
		std::vector< linear_fixed_point_equation > &	flat_lines,
		const data::rewriter &	rewriter,
		const bool	minimal_fixed_point
	)

Definition at line 623 of file ressolve_gauss_elimination.h.

◆ complete_pres()

void mcrl2::pres_system::detail::complete_pres ( pres & x )

Definition at line 147 of file pres.cpp.

◆ compute_Phi_Psi()

template<typename BinaryOperation >

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

Definition at line 30 of file quantifiers_inside_rewriter.h.

◆ conjunction_cj_fj()

pres_expression mcrl2::pres_system::detail::conjunction_cj_fj ( std::vector< linear_fixed_point_equation > & l )

Definition at line 773 of file ressolve_gauss_elimination.h.

◆ conjunction_disjunction_f_j() [1/2]

void mcrl2::pres_system::detail::conjunction_disjunction_f_j	(	pres_expression &	result,
		bool &	result_defined,
		std::vector< linear_fixed_point_equation > &	l,
		const bool	is_conjunction
	)

Definition at line 678 of file ressolve_gauss_elimination.h.

◆ conjunction_disjunction_f_j() [2/2]

pres_expression mcrl2::pres_system::detail::conjunction_disjunction_f_j	(	std::vector< linear_fixed_point_equation > &	l1,
		std::vector< linear_fixed_point_equation > &	l2,
		std::vector< linear_fixed_point_equation > &	l3,
		const bool	is_conjunction
	)

Definition at line 707 of file ressolve_gauss_elimination.h.

◆ conjunction_fj_cj()

pres_expression mcrl2::pres_system::detail::conjunction_fj_cj	(	std::vector< linear_fixed_point_equation > &	l,
		const pres_expression &	U,
		const data::rewriter &	rewriter
	)

Definition at line 838 of file ressolve_gauss_elimination.h.

◆ data_rewrite() [1/4]

template<typename DataRewriter >

const data::data_expression mcrl2::pres_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::pres_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::pres_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::pres_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.

◆ disjunction_cj_fj()

pres_expression mcrl2::pres_system::detail::disjunction_cj_fj ( std::vector< linear_fixed_point_equation > & l )

Definition at line 749 of file ressolve_gauss_elimination.h.

◆ disjunction_fj_cj()

pres_expression mcrl2::pres_system::detail::disjunction_fj_cj	(	std::vector< linear_fixed_point_equation > &	l,
		const pres_expression &	U,
		const data::rewriter &	rewriter
	)

Definition at line 798 of file ressolve_gauss_elimination.h.

◆ disjunction_infinity_cj_prime()

pres_expression mcrl2::pres_system::detail::disjunction_infinity_cj_prime	(	std::vector< linear_fixed_point_equation > &	l1,
		std::vector< linear_fixed_point_equation > &	l2,
		std::vector< linear_fixed_point_equation > &	l3
	)

Definition at line 720 of file ressolve_gauss_elimination.h.

◆ E()

template<typename TermTraits , typename Parameters >

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

Definition at line 238 of file lps2pres_e.h.

◆ E_lts2pres()

template<typename TermTraits , typename Parameters >

void mcrl2::pres_system::detail::E_lts2pres	(	const state_formulas::state_formula &	x,
		Parameters &	parameters,
		std::vector< pres_equation > &	result,
		TermTraits	tr
	)

Definition at line 215 of file lts2pres_e.h.

◆ E_structured()

template<typename TermTraits , typename Parameters >

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

Definition at line 330 of file lps2pres_e.h.

◆ evaluate()

double mcrl2::pres_system::detail::evaluate	(	const pres_expression &	p,
		const std::unordered_map< core::identifier_string, double > &	solution
	)

Definition at line 30 of file ressolve_numerical.h.

◆ evaluate_directed()

double mcrl2::pres_system::detail::evaluate_directed	(	const internal_res_expression *	p,
		const std::vector< double > &	solution
	)

Definition at line 230 of file ressolve_numerical_directed.h.

◆ find_free_variables()

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

inline

Definition at line 135 of file find_free_variables.h.

◆ find_matching_parameters()

std::vector< data::variable > mcrl2::pres_system::detail::find_matching_parameters	(	const pres &	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 pres_parameter_map.h.

◆ find_quantifier_variables()

std::set< data::variable > mcrl2::pres_system::detail::find_quantifier_variables ( const pres_expression & x )

inline

Definition at line 55 of file is_well_typed.h.

◆ group_sums_conjuncts_disjuncts()

pres_expression mcrl2::pres_system::detail::group_sums_conjuncts_disjuncts	(	const pres_expression &	conjunctive_disjunctive_nf,
		const data::rewriter &	rewrite
	)

Definition at line 180 of file ressolve_gauss_elimination.h.

◆ has_conflicting_type()

template<typename Iter >

bool mcrl2::pres_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 222 of file is_well_typed.h.

◆ has_propositional_variables()

bool mcrl2::pres_system::detail::has_propositional_variables ( const pres_expression & x )

inline

Definition at line 43 of file has_propositional_variables.h.

◆ has_quantifier_name_clashes()

bool mcrl2::pres_system::detail::has_quantifier_name_clashes ( const pres_expression & x )

inline

Definition at line 161 of file is_well_typed.h.

◆ instantiate_global_variables()

data::mutable_map_substitution mcrl2::pres_system::detail::instantiate_global_variables ( pres & p )

inline

Eliminates the global variables of a PRES, 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_well_typed()

bool mcrl2::pres_system::detail::is_well_typed ( const pres_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 176 of file is_well_typed.h.

◆ is_well_typed_equation()

bool mcrl2::pres_system::detail::is_well_typed_equation	(	const pres_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 235 of file is_well_typed.h.

◆ is_well_typed_pres()

bool mcrl2::pres_system::detail::is_well_typed_pres	(	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 285 of file is_well_typed.h.

◆ lhs_variables()

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

inline

Definition at line 56 of file lps2pres_utility.h.

◆ load_pres()

pres mcrl2::pres_system::detail::load_pres ( const std::string & filename )

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

Definition at line 283 of file io.cpp.

◆ make_apply_enumerate_builder()

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

apply_enumerate_builder< Builder, DataRewriter, MutableSubstitution > mcrl2::pres_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 338 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::pres_system::detail::make_apply_rewriter_builder	(	const data::data_specification &	dataspec,
		const DataRewriter &	datar,
		SubstitutionFunction &	sigma
	)

Definition at line 114 of file data_rewriter.h.

◆ make_constelm_substitution()

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

inline

Definition at line 30 of file constelm.h.

◆ make_find_propositional_variables_traverser()

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

find_propositional_variables_traverser< Traverser, OutputIterator > mcrl2::pres_system::detail::make_find_propositional_variables_traverser ( OutputIterator out )

Definition at line 53 of file find.h.

◆ make_fresh_variable_substitution()

data::mutable_map_substitution mcrl2::pres_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 lps2pres_utility.h.

◆ make_identifier()

core::identifier_string mcrl2::pres_system::detail::make_identifier	(	const core::identifier_string &	name,
		lts2pres_state_type	s
	)

inline

Definition at line 30 of file lts2pres_rhs.h.

◆ make_rewrite_pres_expressions_builder()

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

rewrite_pres_expressions_builder< Builder, Rewriter > mcrl2::pres_system::detail::make_rewrite_pres_expressions_builder ( const Rewriter & R )

Definition at line 56 of file rewrite.h.

◆ make_rewrite_pres_expressions_with_substitution_builder()

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

rewrite_pres_expressions_with_substitution_builder< Builder, Rewriter, Substitution > mcrl2::pres_system::detail::make_rewrite_pres_expressions_with_substitution_builder	(	const Rewriter &	R,
		Substitution	sigma
	)

Definition at line 84 of file rewrite.h.

◆ make_typecheck_builder()

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

inline

Definition at line 224 of file typecheck.h.

◆ match_declaration()

bool mcrl2::pres_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 pres_parameter_map.h.

◆ mu_expressions()

data::data_expression_list mcrl2::pres_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 lps2pres_utility.h.

◆ mu_name()

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

inline

Definition at line 78 of file lps2pres_utility.h.

◆ mu_variables()

data::variable_list mcrl2::pres_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 lps2pres_utility.h.

◆ myprint()

std::string mcrl2::pres_system::detail::myprint ( const std::vector< pres_equation > & v )

inline

Definition at line 131 of file lps2pres_utility.h.

◆ operator<<() [1/2]

std::ostream & mcrl2::pres_system::detail::operator<<	(	std::ostream &	out,
		const lts2pres_lts &	ltsspec
	)

Definition at line 114 of file lts2pres_lts.h.

◆ operator<<() [2/2]

std::ostream & mcrl2::pres_system::detail::operator<<	(	std::ostream &	out,
		const lts::probabilistic_lts_lts_t &	ltsspec
	)

inline

Definition at line 24 of file lts2pres_lts.h.

◆ Par()

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

inline

Definition at line 201 of file lps2pres_par.h.

◆ parse_pres_expression()

pres_expression mcrl2::pres_system::detail::parse_pres_expression ( const std::string & text )

Definition at line 163 of file pres.cpp.

◆ parse_pres_expression_new()

pres_expression mcrl2::pres_system::detail::parse_pres_expression_new ( const std::string & text )

Definition at line 125 of file pres.cpp.

◆ parse_pres_new()

untyped_pres mcrl2::pres_system::detail::parse_pres_new ( const std::string & text )

Definition at line 136 of file pres.cpp.

◆ parse_pres_parameter_map()

pres_parameter_map mcrl2::pres_system::detail::parse_pres_parameter_map	(	const pres &	p,
		const std::string &	text
	)

inline

Parses parameter selection for finite presinst algorithm.

Definition at line 78 of file pres_parameter_map.h.

◆ parse_propositional_variable()

propositional_variable mcrl2::pres_system::detail::parse_propositional_variable ( const std::string & text )

Definition at line 154 of file pres.cpp.

◆ print_pres_parameter_map()

std::ostream & mcrl2::pres_system::detail::print_pres_parameter_map	(	std::ostream &	out,
		const pres_parameter_map &	m
	)

inline

Print a parameter map.

Definition at line 156 of file pres_parameter_map.h.

◆ print_removed_equations()

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

inline

Definition at line 24 of file remove_equations.h.

◆ push_and_inside()

void mcrl2::pres_system::detail::push_and_inside	(	pres_expression &	result,
		const pres_expression	t1,
		const pres_expression &	t2,
		const bool	conjunctive_normal_form
	)

Definition at line 272 of file ressolve_gauss_elimination.h.

◆ push_constant_inside()

void mcrl2::pres_system::detail::push_constant_inside	(	pres_expression &	result,
		const data::data_expression &	constant,
		const pres_expression &	t
	)

Definition at line 434 of file ressolve_gauss_elimination.h.

◆ push_or_inside()

void mcrl2::pres_system::detail::push_or_inside	(	pres_expression &	result,
		const pres_expression	t1,
		const pres_expression &	t2,
		const bool	conjunctive_normal_form
	)

Definition at line 314 of file ressolve_gauss_elimination.h.

◆ push_plus_inside()

void mcrl2::pres_system::detail::push_plus_inside	(	pres_expression &	result,
		const pres_expression	t1,
		const pres_expression &	t2,
		const bool	conjunctive_normal_form
	)

Definition at line 356 of file ressolve_gauss_elimination.h.

◆ quantifiers_inside()

pres_expression mcrl2::pres_system::detail::quantifiers_inside ( const pres_expression & x )

inline

Definition at line 300 of file quantifiers_inside_rewriter.h.

◆ quantifiers_inside_infimum()

pres_expression mcrl2::pres_system::detail::quantifiers_inside_infimum	(	const std::set< data::variable > &	variables,
		const pres_expression &	x
	)

inline

Definition at line 309 of file quantifiers_inside_rewriter.h.

◆ quantifiers_inside_supremum()

pres_expression mcrl2::pres_system::detail::quantifiers_inside_supremum	(	const std::set< data::variable > &	variables,
		const pres_expression &	x
	)

inline

Definition at line 318 of file quantifiers_inside_rewriter.h.

◆ replace_global_variables()

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

inline

Applies a global variable substitution to a PRES.

Definition at line 29 of file instantiate_global_variables.h.

◆ RHS() [1/2]

template<typename TermTraits , typename Parameters >

pres_expression mcrl2::pres_system::detail::RHS	(	const state_formulas::state_formula &	x,
		lts2pres_state_type	s,
		Parameters &	parameters,
		TermTraits	tr
	)

Definition at line 347 of file lts2pres_rhs.h.

◆ RHS() [2/2]

template<typename TermTraits , typename Parameters >

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

inline

Definition at line 440 of file lps2pres_rhs.h.

◆ rhs_expressions()

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

inline

Definition at line 67 of file lps2pres_utility.h.

◆ RHS_structured()

template<typename TermTraits , typename Parameters >

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

inline

Definition at line 619 of file lps2pres_rhs.h.

◆ Sat()

template<typename TermTraits >

TermTraits::term_type mcrl2::pres_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 lps2pres_sat.h.

◆ save_pres()

void mcrl2::pres_system::detail::save_pres	(	const pres &	presspec,
		const std::string &	filename
	)

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

Definition at line 298 of file io.cpp.

◆ set_res_equation_limit()

void mcrl2::pres_system::detail::set_res_equation_limit ( std::size_t size )

inline

Definition at line 40 of file res_equation_limit.h.

◆ solve_fixed_point_inner()

pres_expression mcrl2::pres_system::detail::solve_fixed_point_inner	(	const propositional_variable &	v,
		const pres_expression &	t,
		const data::data_specification &	dataspec,
		const data::rewriter &	rewriter,
		const bool	minimal_fixed_point
	)

Definition at line 881 of file ressolve_gauss_elimination.h.

◆ solve_single_equation()

const pres_expression mcrl2::pres_system::detail::solve_single_equation	(	const fixpoint_symbol &	f,
		const propositional_variable &	v,
		const pres_expression &	t,
		const data::data_specification &	dataspec,
		const data::rewriter &	rewriter
	)

Definition at line 948 of file ressolve_gauss_elimination.h.

◆ split_parameters()

template<typename PropositionalVariable , typename Parameter >

void mcrl2::pres_system::detail::split_parameters	(	const PropositionalVariable &	X,
		const presinst_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 presinst algorithm.
finite	A sequence of data expressions
infinite	A sequence of data expressions

Definition at line 98 of file presinst_finite_algorithm.h.

◆ variable_index()

int mcrl2::pres_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.

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ lts2pres_state_type

◆ pres_parameter_map

Enumeration Type Documentation

◆ internal_res_expression_type

Function Documentation

◆ check_lps2pres_actions()

◆ check_res_equation_limit()

◆ collect_grouped_ands_ors()

◆ collect_grouped_constant_multiplies_mininf_terms_and_constant()

◆ collect_line()

◆ collect_lines()

◆ collect_m_and_split_lines()

◆ complete_pres()

◆ compute_Phi_Psi()

◆ conjunction_cj_fj()

◆ conjunction_disjunction_f_j() [1/2]

◆ conjunction_disjunction_f_j() [2/2]

◆ conjunction_fj_cj()

◆ data_rewrite() [1/4]

◆ data_rewrite() [2/4]

◆ data_rewrite() [3/4]

◆ data_rewrite() [4/4]

◆ disjunction_cj_fj()

◆ disjunction_fj_cj()

◆ disjunction_infinity_cj_prime()

◆ E()

◆ E_lts2pres()

◆ E_structured()

◆ evaluate()

◆ evaluate_directed()

◆ find_free_variables()

◆ find_matching_parameters()

◆ find_quantifier_variables()

◆ group_sums_conjuncts_disjuncts()

◆ has_conflicting_type()

◆ has_propositional_variables()

◆ has_quantifier_name_clashes()

◆ instantiate_global_variables()

◆ is_well_typed()

◆ is_well_typed_equation()

◆ is_well_typed_pres()

◆ lhs_variables()

◆ load_pres()

◆ make_apply_enumerate_builder()

◆ make_apply_rewriter_builder()

◆ make_constelm_substitution()

◆ make_find_propositional_variables_traverser()

◆ make_fresh_variable_substitution()

◆ make_identifier()

◆ make_rewrite_pres_expressions_builder()

◆ make_rewrite_pres_expressions_with_substitution_builder()

◆ make_typecheck_builder()

◆ match_declaration()

◆ mu_expressions()

◆ mu_name()

◆ mu_variables()

◆ myprint()

◆ operator<<() [1/2]

◆ operator<<() [2/2]

◆ Par()

◆ parse_pres_expression()

◆ parse_pres_expression_new()

◆ parse_pres_new()

◆ parse_pres_parameter_map()

◆ parse_propositional_variable()

◆ print_pres_parameter_map()

◆ print_removed_equations()

◆ push_and_inside()

◆ push_constant_inside()

◆ push_or_inside()

◆ push_plus_inside()

◆ quantifiers_inside()

◆ quantifiers_inside_infimum()

◆ quantifiers_inside_supremum()

◆ replace_global_variables()