#include <pbesinst_lazy_counter_example.h>

Inheritance diagram for mcrl2::pbes_system::pbesinst_counter_example_structure_graph_algorithm:

Public Member Functions
	pbesinst_counter_example_structure_graph_algorithm (const pbessolve_options &options, const pbes &p, const structure_graph &SG, bool _alpha, const std::unordered_map< pbes_expression, structure_graph::index_type > &_mapping, structure_graph &G, std::optional< data::rewriter > rewriter=std::nullopt, const std::unordered_map< std::string, std::set< int > > R={})

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

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

Private Attributes
const structure_graph &	G

bool	alpha

const std::unordered_map< pbes_expression, structure_graph::index_type > &	mapping

const std::unordered_map< std::string, std::set< int > >	R

Additional Inherited Members
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 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

Definition at line 230 of file pbesinst_lazy_counter_example.h.

Constructor & Destructor Documentation

◆ pbesinst_counter_example_structure_graph_algorithm()

mcrl2::pbes_system::pbesinst_counter_example_structure_graph_algorithm::pbesinst_counter_example_structure_graph_algorithm	(	const pbessolve_options &	options,
		const pbes &	p,
		const structure_graph &	SG,
		bool	_alpha,
		const std::unordered_map< pbes_expression, structure_graph::index_type > &	_mapping,
		structure_graph &	G,
		std::optional< data::rewriter >	rewriter = `std::nullopt`,
		const std::unordered_map< std::string, std::set< int > >	R = `{}`
	)

inline

Definition at line 233 of file pbesinst_lazy_counter_example.h.

Member Function Documentation

◆ phi_substitution()

std::function< pbes_expression(const propositional_variable_instantiation &)> mcrl2::pbes_system::pbesinst_counter_example_structure_graph_algorithm::phi_substitution	(	const std::size_t	thread_index,
		const fixpoint_symbol &	symbol,
		const propositional_variable_instantiation &	X,
		const pbes_expression &	phi
	)

inlineoverridevirtual

Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.

Definition at line 250 of file pbesinst_lazy_counter_example.h.

Member Data Documentation

◆ alpha

bool mcrl2::pbes_system::pbesinst_counter_example_structure_graph_algorithm::alpha

private

Definition at line 262 of file pbesinst_lazy_counter_example.h.

◆ G

const structure_graph& mcrl2::pbes_system::pbesinst_counter_example_structure_graph_algorithm::G

private

Definition at line 261 of file pbesinst_lazy_counter_example.h.

◆ mapping

const std::unordered_map<pbes_expression, structure_graph::index_type>& mcrl2::pbes_system::pbesinst_counter_example_structure_graph_algorithm::mapping

private

Definition at line 263 of file pbesinst_lazy_counter_example.h.