An alternative lazy algorithm for instantiating a PBES, ported from bes_deprecated.h. More...

#include <pbesinst_alternative_lazy_algorithm.h>

Public Types
using	pbes_expression_pair = std::pair< pbes_expression, pbes_expression >

Public Member Functions
	pbesinst_alternative_lazy_algorithm (const data::data_specification &data_spec, const data::rewriter &datar, search_strategy search_strategy=search_strategy::breadth_first, transformation_strategy transformation_strategy=transformation_strategy::lazy, const mcrl2::pbes_system::remove_level erase_unused_bes_variables=mcrl2::pbes_system::remove_level::none, const std::size_t maximum_todo_size=std::numeric_limits< std::size_t >::max(), const bool approximate_true=true)
	Constructor.

propositional_variable_instantiation	next_todo ()

void	add_todo (const propositional_variable_instantiation &X)

std::size_t	get_rank (const propositional_variable_instantiation &X)

template<bool is_mu>
bool	find_loop_rec (const pbes_expression &expr, propositional_variable_instantiation X, std::size_t rank, std::unordered_map< propositional_variable_instantiation, bool > &visited)

template<bool is_mu>
bool	find_loop (pbes_expression expr, propositional_variable_instantiation X)

void	regenerate_states ()

pbes_expression_pair	simplify_pbes_expression (const pbes_expression &p, const std::unordered_map< propositional_variable_instantiation, pbes_expression > &trivial)

void	run (pbes &p)
	Runs the algorithm. The result is obtained by calling the function `get_result`.

pbes	get_result (bool short_rename_scheme=true)
	Returns the computed bes in pbes format.

enumerate_quantifiers_rewriter &	rewriter ()

Protected Member Functions
void	print_equation_count (const std::size_t nr_of_processed_variables, const std::size_t nr_of_generated_variables, const std::size_t todo_size) const
	Prints a log message for every 1000-th equation.

Protected Attributes
const data::data_specification &	m_data_spec

const data::rewriter &	m_datar
	Data rewriter.

enumerate_quantifiers_rewriter	R
	The rewriter.

const std::size_t	m_maximum_todo_size
	The maximum size that the todo buffer is allowed to have.

const bool	m_approximate_true

std::size_t	m_elements_not_stored_in_todo_buffer = 0

const mcrl2::pbes_system::remove_level	m_erase_unused_bes_variables

std::deque< propositional_variable_instantiation >	todo
	Propositional variable instantiations that need to be handled.

std::unordered_set< propositional_variable_instantiation >	todo_set
	The content of todo as a set.

std::unordered_map< propositional_variable_instantiation, std::unordered_set< propositional_variable_instantiation > >	occurrence
	Map a variable instantiation to a set of other variable instantiations on whose right hand sides it appears.

std::unordered_map< propositional_variable_instantiation, pbes_expression >	equation
	Map a variable instantiation to its right hand side.

std::unordered_map< propositional_variable_instantiation, pbes_expression >	trivial
	Map a variable instantiations to its right hand side when the latter is trivial (either true or false).

std::vector< std::vector< propositional_variable_instantiation > >	instantiations
	instantiations[i] contains all instantiations of the variable of the i-th equation in the PBES.

std::vector< fixpoint_symbol >	symbols
	symbols[i] contains the fixedpoint symbol of the i-th equation in the PBES.

std::vector< std::size_t >	ranks
	ranks[i] contains the rank of the i-th equation in the PBES.

propositional_variable_instantiation	init
	The initial value.

std::unordered_map< core::identifier_string, std::size_t >	equation_index
	A lookup map for PBES equations.

search_strategy	m_search_strategy
	The search strategy to use when exploring the state space.

transformation_strategy	m_transformation_strategy
	Transformation strategy.

Static Protected Attributes
static const std::size_t	regeneration_count_init = 100
	Initial value for regeneration_period.

Detailed Description

An alternative lazy algorithm for instantiating a PBES, ported from bes_deprecated.h.

Definition at line 126 of file pbesinst_alternative_lazy_algorithm.h.

Member Typedef Documentation

◆ pbes_expression_pair

using mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::pbes_expression_pair = std::pair<pbes_expression, pbes_expression>

Definition at line 488 of file pbesinst_alternative_lazy_algorithm.h.

Constructor & Destructor Documentation

◆ pbesinst_alternative_lazy_algorithm()

mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::pbesinst_alternative_lazy_algorithm	(	const data::data_specification &	data_spec,
		const data::rewriter &	datar,
		search_strategy	search_strategy = `search_strategy::breadth_first`,
		transformation_strategy	transformation_strategy = `transformation_strategy::lazy`,
		const mcrl2::pbes_system::remove_level	erase_unused_bes_variables = `mcrl2::pbes_system::remove_level::none`,
		const std::size_t	maximum_todo_size = `std::numeric_limits<std::size_t>::max()`,
		const bool	approximate_true = `true`
	)

inline

Constructor.

Parameters

data_spec	A data specification.
datar	A data rewriter.
search_strategy	A search strategy (e.g. breadth_first).
transformation_strategy	A strategy to transform the PBES into a BES.
erase_unused_bes_variables	An indicator how often unreachable variables must be garbage collected.
maximum_todo_size	An indication of the maximal size of the stack with explorable BES variables. If the stack exceeds this size, the ignored variable is set to true or false, depending on the parameter `approximate_true`.
approximate_true	If true BES variables that are not investigated are set to false. If false these variables are set to true.

Definition at line 234 of file pbesinst_alternative_lazy_algorithm.h.

Member Function Documentation

◆ add_todo()

void mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::add_todo ( const propositional_variable_instantiation & X )

inline

Definition at line 288 of file pbesinst_alternative_lazy_algorithm.h.

◆ find_loop()

template<bool is_mu>

bool mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::find_loop	(	pbes_expression	expr,
		propositional_variable_instantiation	X
	)

inline

Definition at line 394 of file pbesinst_alternative_lazy_algorithm.h.

◆ find_loop_rec()

template<bool is_mu>

bool mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::find_loop_rec	(	const pbes_expression &	expr,
		propositional_variable_instantiation	X,
		std::size_t	rank,
		std::unordered_map< propositional_variable_instantiation, bool > &	visited
	)

inline

Definition at line 325 of file pbesinst_alternative_lazy_algorithm.h.

◆ get_rank()

std::size_t mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::get_rank ( const propositional_variable_instantiation & X )

inline

Definition at line 319 of file pbesinst_alternative_lazy_algorithm.h.

◆ get_result()

pbes mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::get_result ( bool short_rename_scheme = true )

inline

Returns the computed bes in pbes format.

Returns: The computed bes in pbes format

Definition at line 716 of file pbesinst_alternative_lazy_algorithm.h.

◆ next_todo()

propositional_variable_instantiation mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::next_todo ( )

inline

Definition at line 269 of file pbesinst_alternative_lazy_algorithm.h.

◆ print_equation_count()

void mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::print_equation_count	(	const std::size_t	nr_of_processed_variables,
		const std::size_t	nr_of_generated_variables,
		const std::size_t	todo_size
	)		const

inlineprotected

Prints a log message for every 1000-th equation.

Definition at line 198 of file pbesinst_alternative_lazy_algorithm.h.

◆ regenerate_states()

void mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::regenerate_states ( )

inline

Definition at line 400 of file pbesinst_alternative_lazy_algorithm.h.

◆ rewriter()

enumerate_quantifiers_rewriter & mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::rewriter ( )

inline

Definition at line 741 of file pbesinst_alternative_lazy_algorithm.h.

◆ run()

void mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::run ( pbes & p )

inline

Runs the algorithm. The result is obtained by calling the function get_result.

Parameters

p A PBES

Definition at line 555 of file pbesinst_alternative_lazy_algorithm.h.

◆ simplify_pbes_expression()

pbes_expression_pair mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::simplify_pbes_expression	(	const pbes_expression &	p,
		const std::unordered_map< propositional_variable_instantiation, pbes_expression > &	trivial
	)

inline

Definition at line 489 of file pbesinst_alternative_lazy_algorithm.h.

Member Data Documentation

◆ equation

std::unordered_map<propositional_variable_instantiation, pbes_expression> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::equation

protected

Map a variable instantiation to its right hand side.

Definition at line 168 of file pbesinst_alternative_lazy_algorithm.h.

◆ equation_index

std::unordered_map<core::identifier_string, std::size_t> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::equation_index

protected

A lookup map for PBES equations.

Definition at line 189 of file pbesinst_alternative_lazy_algorithm.h.

◆ init

propositional_variable_instantiation mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::init

protected

The initial value.

Definition at line 186 of file pbesinst_alternative_lazy_algorithm.h.

◆ instantiations

std::vector<std::vector<propositional_variable_instantiation> > mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::instantiations

protected

instantiations[i] contains all instantiations of the variable of the i-th equation in the PBES.

Definition at line 176 of file pbesinst_alternative_lazy_algorithm.h.

◆ m_approximate_true

const bool mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_approximate_true

protected

The variable m_approximimate_true indicates whether boolean variables that cannot be dealt with as the todo buffer would otherwise exceeds m_maximum_todo_size are set to true or to false

Definition at line 147 of file pbesinst_alternative_lazy_algorithm.h.

◆ m_data_spec

const data::data_specification& mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_data_spec

protected

Definition at line 129 of file pbesinst_alternative_lazy_algorithm.h.

◆ m_datar

const data::rewriter& mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_datar

protected

Data rewriter.

Definition at line 132 of file pbesinst_alternative_lazy_algorithm.h.

◆ m_elements_not_stored_in_todo_buffer

std::size_t mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_elements_not_stored_in_todo_buffer = 0

protected

When the todo buffer is limited, due to m_maximum_todo_size, then the variable below counts how many elements are dropped out of the todo buffer.

Definition at line 151 of file pbesinst_alternative_lazy_algorithm.h.

◆ m_erase_unused_bes_variables

const mcrl2::pbes_system::remove_level mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_erase_unused_bes_variables

protected

Indicate to which extent explored bes equations that turn out not to reachable can be thrown away. Values are: none, some or all.

Definition at line 155 of file pbesinst_alternative_lazy_algorithm.h.

◆ m_maximum_todo_size

const std::size_t mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_maximum_todo_size

protected

The maximum size that the todo buffer is allowed to have.

Definition at line 141 of file pbesinst_alternative_lazy_algorithm.h.

◆ m_search_strategy

search_strategy mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_search_strategy

protected

The search strategy to use when exploring the state space.

Definition at line 192 of file pbesinst_alternative_lazy_algorithm.h.

◆ m_transformation_strategy

transformation_strategy mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_transformation_strategy

protected

Transformation strategy.

Definition at line 195 of file pbesinst_alternative_lazy_algorithm.h.

◆ occurrence

std::unordered_map<propositional_variable_instantiation, std::unordered_set<propositional_variable_instantiation> > mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::occurrence

protected

Map a variable instantiation to a set of other variable instantiations on whose right hand sides it appears.

Definition at line 165 of file pbesinst_alternative_lazy_algorithm.h.

◆ R

enumerate_quantifiers_rewriter mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::R

protected

The rewriter.

Definition at line 135 of file pbesinst_alternative_lazy_algorithm.h.

◆ ranks

std::vector<std::size_t> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::ranks

protected

ranks[i] contains the rank of the i-th equation in the PBES.

Definition at line 183 of file pbesinst_alternative_lazy_algorithm.h.

◆ regeneration_count_init

const std::size_t mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::regeneration_count_init = 100

staticprotected

Initial value for regeneration_period.

Definition at line 138 of file pbesinst_alternative_lazy_algorithm.h.

◆ symbols

std::vector<fixpoint_symbol> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::symbols

protected

symbols[i] contains the fixedpoint symbol of the i-th equation in the PBES.

Definition at line 180 of file pbesinst_alternative_lazy_algorithm.h.

◆ todo

std::deque<propositional_variable_instantiation> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::todo

protected

Propositional variable instantiations that need to be handled.

Definition at line 158 of file pbesinst_alternative_lazy_algorithm.h.

◆ todo_set

std::unordered_set<propositional_variable_instantiation> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::todo_set

protected

The content of todo as a set.

Definition at line 161 of file pbesinst_alternative_lazy_algorithm.h.

◆ trivial

std::unordered_map<propositional_variable_instantiation, pbes_expression> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::trivial

protected

Map a variable instantiations to its right hand side when the latter is trivial (either true or false).

Definition at line 172 of file pbesinst_alternative_lazy_algorithm.h.

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

pbes/include/mcrl2/pbes/pbesinst_alternative_lazy_algorithm.h

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Static Protected Attributes

Detailed Description

Member Typedef Documentation

◆ pbes_expression_pair

Constructor & Destructor Documentation

◆ pbesinst_alternative_lazy_algorithm()

Member Function Documentation

◆ add_todo()

◆ find_loop()

◆ find_loop_rec()

◆ get_rank()

◆ get_result()

◆ next_todo()

◆ print_equation_count()

◆ regenerate_states()

◆ rewriter()

◆ run()

◆ simplify_pbes_expression()

Member Data Documentation

◆ equation

◆ equation_index

◆ init

◆ instantiations

◆ m_approximate_true

◆ m_data_spec

◆ m_datar

◆ m_elements_not_stored_in_todo_buffer

◆ m_erase_unused_bes_variables

◆ m_maximum_todo_size

◆ m_search_strategy

◆ m_transformation_strategy

◆ occurrence

◆ R

◆ ranks

◆ regeneration_count_init

◆ symbols

◆ todo

◆ todo_set

◆ trivial