#include <pbesinst_lazy_counter_example.h>

Inheritance diagram for mcrl2::pbes_system::pbesinst_counter_example_structure_graph_algorithm2:

Public Member Functions
	pbesinst_counter_example_structure_graph_algorithm2 (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_algorithm2
	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

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
Public Types inherited from mcrl2::pbes_system::pbesinst_structure_graph_algorithm2
using	super = pbesinst_structure_graph_algorithm

Protected Member Functions inherited from mcrl2::pbes_system::pbesinst_structure_graph_algorithm2
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 inherited from mcrl2::pbes_system::pbesinst_structure_graph_algorithm2
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

Definition at line 267 of file pbesinst_lazy_counter_example.h.

Constructor & Destructor Documentation

◆ pbesinst_counter_example_structure_graph_algorithm2()

mcrl2::pbes_system::pbesinst_counter_example_structure_graph_algorithm2::pbesinst_counter_example_structure_graph_algorithm2	(	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 270 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_algorithm2::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 285 of file pbesinst_lazy_counter_example.h.

Member Data Documentation

◆ alpha

bool mcrl2::pbes_system::pbesinst_counter_example_structure_graph_algorithm2::alpha

private

Definition at line 297 of file pbesinst_lazy_counter_example.h.

◆ G

const structure_graph& mcrl2::pbes_system::pbesinst_counter_example_structure_graph_algorithm2::G

private

Definition at line 296 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_algorithm2::mapping

private

Definition at line 298 of file pbesinst_lazy_counter_example.h.