Variant of pbesinst that will compute a structure graph for a PBES. The result will be put in the structure graph that is passed in the constructor. More...

#include <pbesinst_structure_graph.h>

Inheritance diagram for mcrl2::pbes_system::pbesinst_structure_graph_algorithm:

Public Member Functions
	pbesinst_structure_graph_algorithm (const pbessolve_options &options, const pbes &p, structure_graph &G, std::optional< data::rewriter > rewriter=std::nullopt)

void	on_report_equation (const std::size_t, const propositional_variable_instantiation &X, const pbes_expression &psi, std::size_t k) override
	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.

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

Public Member Functions inherited from mcrl2::pbes_system::pbesinst_lazy_algorithm
	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
void	SG0 (const propositional_variable_instantiation &X, const pbes_expression &psi, std::size_t k)

structure_graph::index_type	SG1 (const pbes_expression &psi)

std::optional< std::string >	status_message (std::size_t equation_count) override

Protected Member Functions inherited from mcrl2::pbes_system::pbesinst_lazy_algorithm
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
detail::structure_graph_builder	m_graph_builder

Protected Attributes inherited from mcrl2::pbes_system::pbesinst_lazy_algorithm
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). \detail It appears that the index is not used. The indexed set can probably be replaced with an atermpp::unordered_set.

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

Variant of pbesinst that will compute a structure graph for a PBES. The result will be put in the structure graph that is passed in the constructor.

Definition at line 29 of file pbesinst_structure_graph.h.

Constructor & Destructor Documentation

◆ pbesinst_structure_graph_algorithm()

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

inline

Definition at line 116 of file pbesinst_structure_graph.h.

Member Function Documentation

◆ on_report_equation()

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

inlineoverridevirtual

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 from mcrl2::pbes_system::pbesinst_lazy_algorithm.

Reimplemented in mcrl2::pbes_system::pbesinst_structure_graph_algorithm2.

Definition at line 126 of file pbesinst_structure_graph.h.

◆ run()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm::run ( )

inlineoverridevirtual

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

Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.

Definition at line 140 of file pbesinst_structure_graph.h.

◆ SG0()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm::SG0	(	const propositional_variable_instantiation &	X,
		const pbes_expression &	psi,
		std::size_t	k
	)

inlineprotected

Definition at line 34 of file pbesinst_structure_graph.h.

◆ SG1()

structure_graph::index_type mcrl2::pbes_system::pbesinst_structure_graph_algorithm::SG1 ( const pbes_expression & psi )

inlineprotected

Definition at line 68 of file pbesinst_structure_graph.h.

◆ status_message()

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

inlineoverrideprotectedvirtual

Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.

Definition at line 102 of file pbesinst_structure_graph.h.

Member Data Documentation

◆ m_graph_builder

detail::structure_graph_builder mcrl2::pbes_system::pbesinst_structure_graph_algorithm::m_graph_builder

protected

Definition at line 32 of file pbesinst_structure_graph.h.

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

pbes/include/mcrl2/pbes/pbesinst_structure_graph.h

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ pbesinst_structure_graph_algorithm()

Member Function Documentation

◆ on_report_equation()

◆ run()

◆ SG0()

◆ SG1()

◆ status_message()

Member Data Documentation

◆ m_graph_builder