Class for generating a BES from a PBES. This BES can be interpreted as a graph corresponding to a parity game problem. The proposition variables of the BES correspond to the vertices of the graph. An interface to the graph is provided in which the vertices correspond to integer values. The values are in the range [0, 1, ..., n], i.e. there are no holes in the sequence. Each vertex is labeled with a priority value, which is the block nesting depth of the proposition variable in the BES. More...

#include <parity_game_generator.h>

Inheritance diagram for mcrl2::pbes_system::parity_game_generator:

Public Types
enum	operation_type { PGAME_OR , PGAME_AND }
	The operation type of the vertices. More...

Public Member Functions
	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 Types
typedef data::rewriter::substitution_type	substitution_function
	Substitution function type used by the PBES rewriter.

Protected Member Functions
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 ()

Protected Attributes
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.

Detailed Description

Class for generating a BES from a PBES. This BES can be interpreted as a graph corresponding to a parity game problem. The proposition variables of the BES correspond to the vertices of the graph. An interface to the graph is provided in which the vertices correspond to integer values. The values are in the range [0, 1, ..., n], i.e. there are no holes in the sequence. Each vertex is labeled with a priority value, which is the block nesting depth of the proposition variable in the BES.

Definition at line 35 of file parity_game_generator.h.

Member Typedef Documentation

◆ substitution_function

typedef data::rewriter::substitution_type mcrl2::pbes_system::parity_game_generator::substitution_function

protected

Substitution function type used by the PBES rewriter.

Definition at line 39 of file parity_game_generator.h.

Member Enumeration Documentation

◆ operation_type

enum mcrl2::pbes_system::parity_game_generator::operation_type

The operation type of the vertices.

Enumerator
PGAME_OR
PGAME_AND

Definition at line 259 of file parity_game_generator.h.

Constructor & Destructor Documentation

◆ parity_game_generator()

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`
	)

inlineexplicit

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	Strategy to use for the data rewriter

Definition at line 266 of file parity_game_generator.h.

◆ ~parity_game_generator()

virtual mcrl2::pbes_system::parity_game_generator::~parity_game_generator ( )

virtualdefault

Member Function Documentation

◆ add_bes_equation()

std::size_t mcrl2::pbes_system::parity_game_generator::add_bes_equation	(	pbes_expression	t,
		std::size_t	priority
	)

inlineprotected

Adds a BES equation for a given PBES expression, if it not already exists.

Parameters

t	A PBES expression
priority	A positive integer

Returns: The index of a BES equation corresponding to the given PBES expression. If no equation exists for the expression, a new one is added.

Definition at line 83 of file parity_game_generator.h.

◆ compute_equation_index_map()

void mcrl2::pbes_system::parity_game_generator::compute_equation_index_map ( )

inlineprotected

Compute equation index map.

Definition at line 146 of file parity_game_generator.h.

◆ compute_priorities()

void mcrl2::pbes_system::parity_game_generator::compute_priorities ( const std::vector< pbes_equation > & equations )

inlineprotected

Compute priorities of PBES propositional variables.

Definition at line 156 of file parity_game_generator.h.

◆ expand_rhs()

pbes_expression mcrl2::pbes_system::parity_game_generator::expand_rhs ( const pbes_expression & psi )

inlineprotected

Definition at line 127 of file parity_game_generator.h.

◆ get_dependencies()

virtual std::set< std::size_t > mcrl2::pbes_system::parity_game_generator::get_dependencies ( std::size_t index )

inlinevirtual

Returns the successors of a vertex in the graph.

Parameters

index A positive integer

Returns: The indices of the proposition variables that appear in the right hand side of the BES equation of the given index.

Definition at line 381 of file parity_game_generator.h.

◆ get_expression_operation()

virtual operation_type mcrl2::pbes_system::parity_game_generator::get_expression_operation ( const pbes_expression & phi )

inlinevirtual

Returns the vertex type.

Parameters

phi	A PBES expression

Returns: PGAME_AND if the expression is a conjunction, PGAME_OR if it is a disjunction.

Definition at line 306 of file parity_game_generator.h.

◆ get_initial_state()

virtual propositional_variable_instantiation mcrl2::pbes_system::parity_game_generator::get_initial_state ( )

inlinevirtual

Returns the (rewritten) initial state.

Returns: the initial state rewritten by R

Reimplemented in mcrl2::pbes_system::detail::pbes_greybox_interface.

Definition at line 282 of file parity_game_generator.h.

◆ get_initial_values()

virtual std::set< std::size_t > mcrl2::pbes_system::parity_game_generator::get_initial_values ( )

inlinevirtual

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.

Returns: A set of indices corresponding to proposition variables of the generated BES.

Definition at line 362 of file parity_game_generator.h.

◆ get_operation()

virtual operation_type mcrl2::pbes_system::parity_game_generator::get_operation ( std::size_t index )

inlinevirtual

Returns the vertex type.

Parameters

index A positive integer

Returns: PGAME_AND if the corresponding BES equation is a conjunction, PGAME_OR if it is a disjunction.

Definition at line 292 of file parity_game_generator.h.

◆ get_priority()

virtual std::size_t mcrl2::pbes_system::parity_game_generator::get_priority ( std::size_t index )

inlinevirtual

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.

Parameters

index A positive integer

Returns: The block nesting depth of the variable in the BES.

Definition at line 349 of file parity_game_generator.h.

◆ initialize_generation()

virtual void mcrl2::pbes_system::parity_game_generator::initialize_generation ( )

inlineprotectedvirtual

Definition at line 229 of file parity_game_generator.h.

◆ make_substitution()

void mcrl2::pbes_system::parity_game_generator::make_substitution	(	const data::variable_list &	v,
		const data::data_expression_list &	e,
		substitution_function &	sigma
	)		const

inlineprotected

Generates a substitution function for the pbesinst rewriter.

Parameters

v	A sequence of data variables
e	A sequence of data expressions
sigma	The result.

Definition at line 116 of file parity_game_generator.h.

◆ print_bes_equation()

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

inlineprotectedvirtual

Definition at line 201 of file parity_game_generator.h.

◆ print_equation_count()

std::string mcrl2::pbes_system::parity_game_generator::print_equation_count	(	std::size_t	size,
		std::size_t	step = `1000`
	)		const

inlineprotected

Prints a log message for every step-th equation.

Definition at line 217 of file parity_game_generator.h.

◆ print_variable_mapping()

virtual void mcrl2::pbes_system::parity_game_generator::print_variable_mapping ( )

inlinevirtual

Prints the mapping from BES variables to the corresponding PBES expressions.

Definition at line 449 of file parity_game_generator.h.

Member Data Documentation

◆ datar

data::rewriter mcrl2::pbes_system::parity_game_generator::datar

protected

Data rewriter.

Definition at line 49 of file parity_game_generator.h.

◆ m_bes

std::vector<std::pair<pbes_expression, std::size_t> > mcrl2::pbes_system::parity_game_generator::m_bes

protected

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.

Definition at line 67 of file parity_game_generator.h.

◆ m_initialized

bool mcrl2::pbes_system::parity_game_generator::m_initialized

protected

Mark whether initialization has been initialized. Needed to properly cope with virtual inheritance!

Definition at line 43 of file parity_game_generator.h.

◆ m_is_min_parity_game

bool mcrl2::pbes_system::parity_game_generator::m_is_min_parity_game

protected

True if it is a min-parity game.

Definition at line 73 of file parity_game_generator.h.

◆ m_max_priority

std::size_t mcrl2::pbes_system::parity_game_generator::m_max_priority = 0

protected

The maximum priority value of the game.

Definition at line 76 of file parity_game_generator.h.

◆ m_pbes

pbes& mcrl2::pbes_system::parity_game_generator::m_pbes

protected

The PBES that is being solved.

Definition at line 46 of file parity_game_generator.h.

◆ m_pbes_equation_index

std::map<core::identifier_string, std::vector<pbes_equation>::const_iterator > mcrl2::pbes_system::parity_game_generator::m_pbes_equation_index

protected

Maps propositional variables to corresponding PBES equations.

Definition at line 55 of file parity_game_generator.h.

◆ m_pbes_expression_index

std::map<pbes_expression, std::size_t> mcrl2::pbes_system::parity_game_generator::m_pbes_expression_index

protected

Maps PBES closed expressions to corresponding BES variables.

Definition at line 61 of file parity_game_generator.h.

◆ m_priorities

std::map<core::identifier_string, std::size_t> mcrl2::pbes_system::parity_game_generator::m_priorities

protected

Maps propositional variables to corresponding priorities.

Definition at line 58 of file parity_game_generator.h.

◆ m_true_false_dependencies

bool mcrl2::pbes_system::parity_game_generator::m_true_false_dependencies

protected

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

Definition at line 70 of file parity_game_generator.h.

◆ R

pbes_system::enumerate_quantifiers_rewriter mcrl2::pbes_system::parity_game_generator::R

protected

PBES rewriter.

Definition at line 52 of file parity_game_generator.h.

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

pbes/include/mcrl2/pbes/parity_game_generator.h

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ substitution_function

Member Enumeration Documentation

◆ operation_type

Constructor & Destructor Documentation

◆ parity_game_generator()

◆ ~parity_game_generator()

Member Function Documentation

◆ add_bes_equation()

◆ compute_equation_index_map()

◆ compute_priorities()

◆ expand_rhs()

◆ get_dependencies()

◆ get_expression_operation()

◆ get_initial_state()

◆ get_initial_values()

◆ get_operation()

◆ get_priority()

◆ initialize_generation()

◆ make_substitution()

◆ print_bes_equation()

◆ print_equation_count()

◆ print_variable_mapping()

Member Data Documentation

◆ datar

◆ m_bes

◆ m_initialized

◆ m_is_min_parity_game

◆ m_max_priority

◆ m_pbes

◆ m_pbes_equation_index

◆ m_pbes_expression_index

◆ m_priorities

◆ m_true_false_dependencies

◆ R