#include <pbes_greybox_interface.h>

Inheritance diagram for mcrl2::pbes_system::detail::pbes_greybox_interface:

Public Member Functions
	pbes_greybox_interface (pbes &p, bool true_false_dependencies=false, bool is_min_parity=true, data::rewriter::strategy rewrite_strategy=data::jitty)
	Constructor.

virtual	~pbes_greybox_interface ()

propositional_variable_instantiation	get_initial_state ()
	Returns the initial state, rewritten and simplified.

pbes_expression	rewrite_and_simplify_expression (const pbes_expression &e, const bool=true)
	Rewrites and simplifies an expression.

pbes_equation	get_pbes_equation (const core::identifier_string &s)
	Returns the equation for variable s.

std::set< pbes_expression >	get_successors (const pbes_expression &phi)
	Returns the successors of a state, which is a instantiated propositional variable. Fetches the right hand side of the equation for the variable of the state, Substitutes the variables in the right hand side with the parameter variables in the state and rewrites the expression.

virtual pbes_expression	expand_group (const pbes_expression &psi, const pbes_expression &expr)
	Expands a formula expr for a instantiated state variable psi, which means substituting the variables in expr by the parameter values in psi and rewriting the expression.

virtual std::string	print_successors (const std::set< pbes_expression > &successors)
	Prints the set of successors states.

std::set< pbes_expression >	get_successors (const pbes_expression &phi, const std::string &var, const pbes_expression &expr)
	Returns the successors of a state, which is a instantiated propositional variable, for a certain 'transition group'. Checks if the name of the state variable equals the variable associated with the transition group var. If so, in the expression expr the variables are substituted with the parameter variables in the state and the expression is rewritten.

Public Member Functions inherited from mcrl2::pbes_system::parity_game_generator
	parity_game_generator (pbes &p, bool true_false_dependencies=false, bool is_min_parity=true, data::rewriter::strategy rewrite_strategy=data::jitty)
	Constructor.

virtual	~parity_game_generator ()=default

virtual propositional_variable_instantiation	get_initial_state ()
	Returns the (rewritten) initial state.

virtual operation_type	get_operation (std::size_t index)
	Returns the vertex type.

virtual operation_type	get_expression_operation (const pbes_expression &phi)
	Returns the vertex type.

virtual std::size_t	get_priority (std::size_t index)
	Returns the priority of a vertex. The priority of the first equation is 0 if it is a maximal fixpoint, and 1 if it is a minimal fixpoint.

virtual std::set< std::size_t >	get_initial_values ()
	Returns the vertices for which a solution is requested. By default a set containing the values 0, 1 and 2 is returned, corresponding to the expressions true, false and the initial state of the PBES.

virtual std::set< std::size_t >	get_dependencies (std::size_t index)
	Returns the successors of a vertex in the graph.

virtual void	print_variable_mapping ()
	Prints the mapping from BES variables to the corresponding PBES expressions.

Protected Attributes
data::rewriter	datar

pbes_system::enumerate_quantifiers_rewriter	pbes_rewriter

Protected Attributes inherited from mcrl2::pbes_system::parity_game_generator
bool	m_initialized
	Mark whether initialization has been initialized. Needed to properly cope with virtual inheritance!

pbes &	m_pbes
	The PBES that is being solved.

data::rewriter	datar
	Data rewriter.

pbes_system::enumerate_quantifiers_rewriter	R
	PBES rewriter.

std::map< core::identifier_string, std::vector< pbes_equation >::const_iterator >	m_pbes_equation_index
	Maps propositional variables to corresponding PBES equations.

std::map< core::identifier_string, std::size_t >	m_priorities
	Maps propositional variables to corresponding priorities.

std::map< pbes_expression, std::size_t >	m_pbes_expression_index
	Maps PBES closed expressions to corresponding BES variables.

std::vector< std::pair< pbes_expression, std::size_t > >	m_bes
	Contains intermediate results of the BES that is being generated. m_bes[i] represents a BES equation corresponding to BES variable i. m_bes[i].first is the right hand side of the BES equation m_bes[i].second is the block nesting depth of the corresponding PBES variable.

bool	m_true_false_dependencies
	Determines what kind of BES equations are generated for true and false.

bool	m_is_min_parity_game
	True if it is a min-parity game.

std::size_t	m_max_priority = 0
	The maximum priority value of the game.

Additional Inherited Members
Public Types inherited from mcrl2::pbes_system::parity_game_generator
enum	operation_type { PGAME_OR , PGAME_AND }
	The operation type of the vertices. More...

Protected Types inherited from mcrl2::pbes_system::parity_game_generator
typedef data::rewriter::substitution_type	substitution_function
	Substitution function type used by the PBES rewriter.

Protected Member Functions inherited from mcrl2::pbes_system::parity_game_generator
std::size_t	add_bes_equation (pbes_expression t, std::size_t priority)
	Adds a BES equation for a given PBES expression, if it not already exists.

void	make_substitution (const data::variable_list &v, const data::data_expression_list &e, substitution_function &sigma) const
	Generates a substitution function for the pbesinst rewriter.

pbes_expression	expand_rhs (const pbes_expression &psi)

void	compute_equation_index_map ()
	Compute equation index map.

void	compute_priorities (const std::vector< pbes_equation > &equations)
	Compute priorities of PBES propositional variables.

virtual std::string	print_bes_equation (std::size_t index, const std::set< std::size_t > &rhs)

std::string	print_equation_count (std::size_t size, std::size_t step=1000) const
	Prints a log message for every step-th equation.

virtual void	initialize_generation ()

Detailed Description

A class that provides initial state and successors functions for PBESs, allowing to explore the PBES as a transition system, where states are instantiated propositional variables.

Definition at line 30 of file pbes_greybox_interface.h.

Constructor & Destructor Documentation

◆ pbes_greybox_interface()

mcrl2::pbes_system::detail::pbes_greybox_interface::pbes_greybox_interface	(	pbes &	p,
		bool	true_false_dependencies = `false`,
		bool	is_min_parity = `true`,
		data::rewriter::strategy	rewrite_strategy = `data::jitty`
	)

inline

Constructor.

Parameters

p	A PBES
true_false_dependencies	If true, nodes are generated for the values `true` and `false`.
is_min_parity	If true a min-parity game is produced, otherwise a max-parity game
rewrite_strategy	The rewrite engine to use. (Default: jitty)

Definition at line 42 of file pbes_greybox_interface.h.

◆ ~pbes_greybox_interface()

virtual mcrl2::pbes_system::detail::pbes_greybox_interface::~pbes_greybox_interface ( )

inlinevirtual

Definition at line 50 of file pbes_greybox_interface.h.

Member Function Documentation

◆ expand_group()

virtual pbes_expression mcrl2::pbes_system::detail::pbes_greybox_interface::expand_group	(	const pbes_expression &	psi,
		const pbes_expression &	expr
	)

inlinevirtual

Expands a formula expr for a instantiated state variable psi, which means substituting the variables in expr by the parameter values in psi and rewriting the expression.

Parameters

psi	the instantiated propositional variable.
expr	the expression to be expanded.

Returns: the result of the expansion.

Definition at line 149 of file pbes_greybox_interface.h.

◆ get_initial_state()

propositional_variable_instantiation mcrl2::pbes_system::detail::pbes_greybox_interface::get_initial_state ( )

inlinevirtual

Returns the initial state, rewritten and simplified.

Returns: the initial state.

Reimplemented from mcrl2::pbes_system::parity_game_generator.

Definition at line 54 of file pbes_greybox_interface.h.

◆ get_pbes_equation()

pbes_equation mcrl2::pbes_system::detail::pbes_greybox_interface::get_pbes_equation ( const core::identifier_string & s )

inline

Returns the equation for variable s.

Parameters

s	the identifier string of a variable.

Returns: the equation for variable s.

Definition at line 75 of file pbes_greybox_interface.h.

◆ get_successors() [1/2]

std::set< pbes_expression > mcrl2::pbes_system::detail::pbes_greybox_interface::get_successors ( const pbes_expression & phi )

inline

Returns the successors of a state, which is a instantiated propositional variable. Fetches the right hand side of the equation for the variable of the state, Substitutes the variables in the right hand side with the parameter variables in the state and rewrites the expression.

Parameters

phi	An instantiated propositional variable

Returns: The set of variable instantiations (successor states) that appear in the rewritten right hand side expression.

Definition at line 88 of file pbes_greybox_interface.h.

◆ get_successors() [2/2]

std::set< pbes_expression > mcrl2::pbes_system::detail::pbes_greybox_interface::get_successors	(	const pbes_expression &	phi,
		const std::string &	var,
		const pbes_expression &	expr
	)

inline

Returns the successors of a state, which is a instantiated propositional variable, for a certain 'transition group'. Checks if the name of the state variable equals the variable associated with the transition group var. If so, in the expression expr the variables are substituted with the parameter variables in the state and the expression is rewritten.

Parameters

phi	An instantiated propositional variable
var	The variable name associated with the transition group.
expr	The expression associated with the transition group.

Returns: The set of variable instantiations (successor states) that appear in the rewritten expression.

Definition at line 195 of file pbes_greybox_interface.h.

◆ print_successors()

virtual std::string mcrl2::pbes_system::detail::pbes_greybox_interface::print_successors ( const std::set< pbes_expression > & successors )

inlinevirtual

Prints the set of successors states.

Parameters

successors a set of successor expressions.

Returns: a string representation of successors.

Definition at line 174 of file pbes_greybox_interface.h.

◆ rewrite_and_simplify_expression()

pbes_expression mcrl2::pbes_system::detail::pbes_greybox_interface::rewrite_and_simplify_expression	(	const pbes_expression &	e,
		const bool	= `true`
	)

inline

Rewrites and simplifies an expression.

Parameters

e	a PBES expression.

Returns: the result of the rewrite.

Definition at line 65 of file pbes_greybox_interface.h.

Member Data Documentation

◆ datar

data::rewriter mcrl2::pbes_system::detail::pbes_greybox_interface::datar

protected

Definition at line 33 of file pbes_greybox_interface.h.

◆ pbes_rewriter

pbes_system::enumerate_quantifiers_rewriter mcrl2::pbes_system::detail::pbes_greybox_interface::pbes_rewriter

protected

Definition at line 34 of file pbes_greybox_interface.h.

The documentation for this class was generated from the following file:

pbes/include/mcrl2/pbes/detail/pbes_greybox_interface.h

Public Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ pbes_greybox_interface()

◆ ~pbes_greybox_interface()

Member Function Documentation

◆ expand_group()

◆ get_initial_state()

◆ get_pbes_equation()

◆ get_successors() [1/2]

◆ get_successors() [2/2]

◆ print_successors()

◆ rewrite_and_simplify_expression()

Member Data Documentation

◆ datar

◆ pbes_rewriter