A PBES instantiation algorithm that uses a lazy strategy. More...

#include <pbesinst_lazy.h>

Inheritance diagram for mcrl2::pbes_system::pbesinst_lazy_algorithm:

Classes
struct	true_false_substitution

Public Member Functions
	pbesinst_lazy_algorithm (const pbessolve_options &options, const pbes &p, std::optional< data::rewriter > rewriter=std::nullopt)
	Constructor.

virtual	~pbesinst_lazy_algorithm ()=default

virtual void	on_report_equation (const std::size_t, const propositional_variable_instantiation &, const pbes_expression &, std::size_t)
	Reports BES equations that are produced by the algorithm. This function is called for every BES equation X = psi with rank k that is produced. By default it does nothing.

virtual void	on_discovered_elements (const std::set< propositional_variable_instantiation > &)
	This function is called when new elements are added to discovered.

virtual void	on_end_while_loop ()
	This function is called right after the while loop is finished.

void	next_todo (propositional_variable_instantiation &result)

const fixpoint_symbol &	symbol (std::size_t i) const

virtual std::function< pbes_expression(const propositional_variable_instantiation &)>	phi_substitution (const std::size_t, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &)

virtual void	rewrite_psi (const std::size_t, pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi)

virtual bool	solution_found (const propositional_variable_instantiation &) const

virtual void	run_thread (const std::size_t thread_index, pbesinst_lazy_todo &todo, std::atomic< std::size_t > &number_of_active_processes, data::mutable_indexed_substitution<> sigma, enumerate_quantifiers_rewriter R)

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

const pbes_equation_index &	equation_index () const

enumerate_quantifiers_rewriter &	rewriter ()

const data::rewriter &	data_rewriter () const

Protected Member Functions
virtual std::optional< std::string >	status_message (std::size_t equation_count)

pbes	preprocess (const pbes &x) const

data::rewriter	construct_rewriter (const pbes &pbesspec)

Protected Attributes
const pbessolve_options &	m_options
	Algorithm options.

data::rewriter	datar
	Data rewriter.

pbes	m_pbes
	A PBES.

pbes_equation_index	m_equation_index
	A lookup map for PBES equations.

pbesinst_lazy_todo	todo
	The propositional variable instantiations that need to be handled.

atermpp::indexed_set< propositional_variable_instantiation, true >	discovered
	The propositional variable instantiations that have been discovered (not necessarily handled).

propositional_variable_instantiation	init
	The initial value (after rewriting).

std::size_t	m_iteration_count = 0

enumerate_quantifiers_rewriter	m_global_R
	The rewriter.

utilities::mutex	m_todo_access

std::size_t	global_current_prune_round = 0

volatile bool	m_must_abort = false

Detailed Description

A PBES instantiation algorithm that uses a lazy strategy.

Definition at line 131 of file pbesinst_lazy.h.

Constructor & Destructor Documentation

◆ pbesinst_lazy_algorithm()

mcrl2::pbes_system::pbesinst_lazy_algorithm::pbesinst_lazy_algorithm	(	const pbessolve_options &	options,
		const pbes &	p,
		std::optional< data::rewriter >	rewriter = `std::nullopt`
	)

inlineexplicit

Constructor.

Parameters

p	The pbes used in the exploration algorithm.
options	Te.
search_strategy	The search strategy used to explore the pbes, typically depth or breadth first.
optimization	An indication of the optimisation level.

Definition at line 247 of file pbesinst_lazy.h.

◆ ~pbesinst_lazy_algorithm()

virtual mcrl2::pbes_system::pbesinst_lazy_algorithm::~pbesinst_lazy_algorithm ( )

virtualdefault

Member Function Documentation

◆ construct_rewriter()

data::rewriter mcrl2::pbes_system::pbesinst_lazy_algorithm::construct_rewriter ( const pbes & pbesspec )

inlineprotected

Definition at line 226 of file pbesinst_lazy.h.

◆ data_rewriter()

const data::rewriter & mcrl2::pbes_system::pbesinst_lazy_algorithm::data_rewriter ( ) const

inline

Definition at line 491 of file pbesinst_lazy.h.

◆ equation_index()

const pbes_equation_index & mcrl2::pbes_system::pbesinst_lazy_algorithm::equation_index ( ) const

inline

Definition at line 481 of file pbesinst_lazy.h.

◆ next_todo()

void mcrl2::pbes_system::pbesinst_lazy_algorithm::next_todo ( propositional_variable_instantiation & result )

inline

Definition at line 278 of file pbesinst_lazy.h.

◆ on_discovered_elements()

virtual void mcrl2::pbes_system::pbesinst_lazy_algorithm::on_discovered_elements ( const std::set< propositional_variable_instantiation > & )

inlinevirtual

This function is called when new elements are added to discovered.

Reimplemented in mcrl2::pbes_system::pbesinst_structure_graph_algorithm2.

Definition at line 271 of file pbesinst_lazy.h.

◆ on_end_while_loop()

virtual void mcrl2::pbes_system::pbesinst_lazy_algorithm::on_end_while_loop ( )

inlinevirtual

This function is called right after the while loop is finished.

Reimplemented in mcrl2::pbes_system::pbesinst_structure_graph_algorithm2.

Definition at line 275 of file pbesinst_lazy.h.

◆ on_report_equation()

virtual void mcrl2::pbes_system::pbesinst_lazy_algorithm::on_report_equation	(	const std::size_t	,
		const propositional_variable_instantiation &	,
		const pbes_expression &	,
		std::size_t
	)

inlinevirtual

Reports BES equations that are produced by the algorithm. This function is called for every BES equation X = psi with rank k that is produced. By default it does nothing.

Reimplemented in mcrl2::pbes_system::pbesinst_structure_graph_algorithm2, and mcrl2::pbes_system::pbesinst_structure_graph_algorithm.

Definition at line 264 of file pbesinst_lazy.h.

◆ phi_substitution()

virtual std::function< pbes_expression(const propositional_variable_instantiation &)> mcrl2::pbes_system::pbesinst_lazy_algorithm::phi_substitution	(	const std::size_t	,
		const fixpoint_symbol &	symbol,
		const propositional_variable_instantiation &	X,
		const pbes_expression &
	)

inlinevirtual

Reimplemented in mcrl2::pbes_system::pbesinst_counter_example_structure_graph_algorithm, and mcrl2::pbes_system::pbesinst_counter_example_structure_graph_algorithm2.

Definition at line 299 of file pbesinst_lazy.h.

◆ preprocess()

pbes mcrl2::pbes_system::pbesinst_lazy_algorithm::preprocess ( const pbes & x ) const

inlineprotected

Definition at line 185 of file pbesinst_lazy.h.

◆ rewrite_psi()

virtual void mcrl2::pbes_system::pbesinst_lazy_algorithm::rewrite_psi	(	const std::size_t	,
		pbes_expression &	result,
		const fixpoint_symbol &	symbol,
		const propositional_variable_instantiation &	X,
		const pbes_expression &	psi
	)

inlinevirtual

Reimplemented in mcrl2::pbes_system::pbesinst_structure_graph_algorithm2.

Definition at line 313 of file pbesinst_lazy.h.

◆ rewriter()

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

inline

Definition at line 486 of file pbesinst_lazy.h.

◆ run()

virtual void mcrl2::pbes_system::pbesinst_lazy_algorithm::run ( )

inlinevirtual

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

Reimplemented in mcrl2::pbes_system::pbesinst_structure_graph_algorithm.

Definition at line 425 of file pbesinst_lazy.h.

◆ run_thread()

virtual void mcrl2::pbes_system::pbesinst_lazy_algorithm::run_thread	(	const std::size_t	thread_index,
		pbesinst_lazy_todo &	todo,
		std::atomic< std::size_t > &	number_of_active_processes,
		data::mutable_indexed_substitution<>	sigma,
		enumerate_quantifiers_rewriter	R
	)

inlinevirtual

Definition at line 326 of file pbesinst_lazy.h.

◆ solution_found()

virtual bool mcrl2::pbes_system::pbesinst_lazy_algorithm::solution_found ( const propositional_variable_instantiation & ) const

inlinevirtual

Reimplemented in mcrl2::pbes_system::pbesinst_structure_graph_algorithm2.

Definition at line 321 of file pbesinst_lazy.h.

◆ status_message()

virtual std::optional< std::string > mcrl2::pbes_system::pbesinst_lazy_algorithm::status_message ( std::size_t equation_count )

inlineprotectedvirtual

Reimplemented in mcrl2::pbes_system::pbesinst_structure_graph_algorithm.

Definition at line 171 of file pbesinst_lazy.h.

◆ symbol()

const fixpoint_symbol & mcrl2::pbes_system::pbesinst_lazy_algorithm::symbol ( std::size_t i ) const

inline

Definition at line 292 of file pbesinst_lazy.h.

Member Data Documentation

◆ datar

data::rewriter mcrl2::pbes_system::pbesinst_lazy_algorithm::datar

protected

Data rewriter.

Definition at line 138 of file pbesinst_lazy.h.

◆ discovered

atermpp::indexed_set<propositional_variable_instantiation, true> mcrl2::pbes_system::pbesinst_lazy_algorithm::discovered

protected

The propositional variable instantiations that have been discovered (not necessarily handled).

Definition at line 150 of file pbesinst_lazy.h.

◆ global_current_prune_round

std::size_t mcrl2::pbes_system::pbesinst_lazy_algorithm::global_current_prune_round = 0

protected

Definition at line 166 of file pbesinst_lazy.h.

◆ init

propositional_variable_instantiation mcrl2::pbes_system::pbesinst_lazy_algorithm::init

protected

The initial value (after rewriting).

Definition at line 153 of file pbesinst_lazy.h.

◆ m_equation_index

pbes_equation_index mcrl2::pbes_system::pbesinst_lazy_algorithm::m_equation_index

protected

A lookup map for PBES equations.

Definition at line 144 of file pbesinst_lazy.h.

◆ m_global_R

enumerate_quantifiers_rewriter mcrl2::pbes_system::pbesinst_lazy_algorithm::m_global_R

protected

The rewriter.

Definition at line 160 of file pbesinst_lazy.h.

◆ m_iteration_count

std::size_t mcrl2::pbes_system::pbesinst_lazy_algorithm::m_iteration_count = 0

protected

Definition at line 156 of file pbesinst_lazy.h.

◆ m_must_abort

volatile bool mcrl2::pbes_system::pbesinst_lazy_algorithm::m_must_abort = false

protected

Definition at line 168 of file pbesinst_lazy.h.

◆ m_options

const pbessolve_options& mcrl2::pbes_system::pbesinst_lazy_algorithm::m_options

protected

Algorithm options.

Definition at line 135 of file pbesinst_lazy.h.

◆ m_pbes

pbes mcrl2::pbes_system::pbesinst_lazy_algorithm::m_pbes

protected

A PBES.

Definition at line 141 of file pbesinst_lazy.h.

◆ m_todo_access

utilities::mutex mcrl2::pbes_system::pbesinst_lazy_algorithm::m_todo_access

protected

Definition at line 163 of file pbesinst_lazy.h.

◆ todo

pbesinst_lazy_todo mcrl2::pbes_system::pbesinst_lazy_algorithm::todo

protected

The propositional variable instantiations that need to be handled.

Definition at line 147 of file pbesinst_lazy.h.

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

pbes/include/mcrl2/pbes/pbesinst_lazy.h

Classes

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ pbesinst_lazy_algorithm()

◆ ~pbesinst_lazy_algorithm()

Member Function Documentation

◆ construct_rewriter()

◆ data_rewriter()

◆ equation_index()

◆ next_todo()

◆ on_discovered_elements()

◆ on_end_while_loop()

◆ on_report_equation()

◆ phi_substitution()

◆ preprocess()

◆ rewrite_psi()

◆ rewriter()

◆ run()

◆ run_thread()

◆ solution_found()

◆ status_message()

◆ symbol()

Member Data Documentation

◆ datar

◆ discovered

◆ global_current_prune_round

◆ init

◆ m_equation_index

◆ m_global_R

◆ m_iteration_count

◆ m_must_abort

◆ m_options

◆ m_pbes

◆ m_todo_access

◆ todo