Adds an optimization to pbesinst_structure_graph. More...

#include <pbesinst_structure_graph2.h>

Inheritance diagram for mcrl2::pbes_system::pbesinst_structure_graph_algorithm2:

Classes
struct	Rplus_traverser

Public Types
using	super = pbesinst_structure_graph_algorithm

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

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

void	on_report_equation (const std::size_t thread_index, 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	report_found_solutions (stopwatch &timer)

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

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

Public Member Functions inherited from 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)

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
template<typename T >
pbes_expression	expr (const T &x) const

Rplus_traverser::stack_element	Rplus (const pbes_expression &x)

bool	solution_found (const propositional_variable_instantiation &init) const override

bool	todo_has_only_undefined_nodes () const

void	prune_todo_list (const propositional_variable_instantiation &init, pbesinst_lazy_todo &todo, std::size_t &calculation_steps)

void	prune_todo_list_conditional (const propositional_variable_instantiation &init, pbesinst_lazy_todo &todo, std::size_t &calculation_steps)

void	prune_todo_list_time_triggered (const propositional_variable_instantiation &init, pbesinst_lazy_todo &todo)

bool	strategies_are_set_in_solved_nodes () const

Protected Member Functions inherited from mcrl2::pbes_system::pbesinst_structure_graph_algorithm
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
std::array< vertex_set, 2 >	S

std::array< strategy_vector, 2 >	tau

std::array< detail::computation_guard, 2 >	S_guard

atermpp::vector< pbes_expression >	b

detail::periodic_guard	on_the_fly_solve_trigger

detail::periodic_guard	reset_guard

Protected Attributes inherited from mcrl2::pbes_system::pbesinst_structure_graph_algorithm
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

Adds an optimization to pbesinst_structure_graph.

Definition at line 85 of file pbesinst_structure_graph2.h.

Member Typedef Documentation

◆ super

using mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::super = pbesinst_structure_graph_algorithm

Definition at line 562 of file pbesinst_structure_graph2.h.

Constructor & Destructor Documentation

◆ pbesinst_structure_graph_algorithm2()

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

inline

Definition at line 564 of file pbesinst_structure_graph2.h.

Member Function Documentation

◆ expr()

template<typename T >

pbes_expression mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::expr ( const T & x ) const

inlineprotected

Definition at line 97 of file pbesinst_structure_graph2.h.

◆ on_discovered_elements()

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

inlineoverridevirtual

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

Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.

Definition at line 627 of file pbesinst_structure_graph2.h.

◆ on_end_while_loop()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::on_end_while_loop ( )

inlineoverridevirtual

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

Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.

Definition at line 705 of file pbesinst_structure_graph2.h.

◆ on_report_equation()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::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_structure_graph_algorithm.

Definition at line 599 of file pbesinst_structure_graph2.h.

◆ prune_todo_list()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::prune_todo_list	(	const propositional_variable_instantiation &	init,
		pbesinst_lazy_todo &	todo,
		std::size_t &	calculation_steps
	)

inlineprotected

Definition at line 408 of file pbesinst_structure_graph2.h.

◆ prune_todo_list_conditional()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::prune_todo_list_conditional	(	const propositional_variable_instantiation &	init,
		pbesinst_lazy_todo &	todo,
		std::size_t &	calculation_steps
	)

inlineprotected

Definition at line 505 of file pbesinst_structure_graph2.h.

◆ prune_todo_list_time_triggered()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::prune_todo_list_time_triggered	(	const propositional_variable_instantiation &	init,
		pbesinst_lazy_todo &	todo
	)

inlineprotected

Definition at line 519 of file pbesinst_structure_graph2.h.

◆ report_found_solutions()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::report_found_solutions ( stopwatch & timer )

inline

Definition at line 621 of file pbesinst_structure_graph2.h.

◆ rewrite_psi()

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