#include <partial_order_reduction.h>

Classes
struct	invis_pair

struct	parameter_info

class	summand_relations_data

Public Member Functions
	partial_order_reduction_algorithm (const pbes &p, pbespor_options options)

const propositional_variable_instantiation &	initial_state () const

const std::vector< data::variable > &	parameters () const

const fixpoint_symbol &	symbol (const core::identifier_string &X) const

void	print () const

template<typename EmitNode = utilities::skip, typename EmitEdge = utilities::skip>
void	explore (const propositional_variable_instantiation &X_init, EmitNode emit_node=EmitNode(), EmitEdge emit_edge=EmitEdge())

template<typename EmitNode = utilities::skip, typename EmitEdge = utilities::skip>
void	explore_full (const propositional_variable_instantiation &X_init, EmitNode emit_node=EmitNode(), EmitEdge emit_edge=EmitEdge())

Protected Types
using	enumerator_element = data::enumerator_list_element_with_substitution< data::data_expression >

Protected Member Functions
std::size_t	summand_index (const srf_summand &summand) const

std::size_t	parameter_position (const data::variable &v) const

const summand_set &	DNA (std::size_t k) const

summand_set &	DNA (std::size_t k)

const summand_set &	DNS (std::size_t k) const

summand_set &	DNS (std::size_t k)

const summand_set &	DNL (std::size_t k) const

summand_set &	DNL (std::size_t k)

const summand_set &	NES (std::size_t k) const

summand_set &	NES (std::size_t k)

summand_set	en (const propositional_variable_instantiation &X_e)

summand_set	invis (const summand_set &K)

const summand_set &	choose_minimal_NES (std::size_t k, const propositional_variable_instantiation &X_e) const

const summand_set &	DNX (std::size_t k, const summand_set &Twork, const summand_set &Ts, const summand_set &en_X_e) const

summand_set	stubborn_set (const propositional_variable_instantiation &X_e, const summand_set &en_X_e)

std::set< propositional_variable_instantiation >	succ (const propositional_variable_instantiation &X_e, const summand_set &K)

void	compute_nxt ()

std::set< std::size_t >	FV (const pbes_expression &x) const

bool	is_true (data::data_expression expr)

bool	dependency_permanently_disables (const std::size_t k, const std::size_t k1) const
	Return true iff k1 can never happen after k happens, as deduced from predicate dependencies.

void	compute_dependency_NES ()

bool	depends (std::size_t i, std::size_t k, std::size_t j) const

bool	depends (std::size_t i, std::size_t k) const

tribool	left_accords_equations (std::size_t k, std::size_t k1) const

tribool	square_accords_equations (std::size_t k, std::size_t k1) const

tribool	triangle_accords_equations (std::size_t k, std::size_t k1) const

void	compute_DNA_DNL_NES (const std::vector< parameter_info > &info)

void	compute_NES_DNA_DNL ()

bool	compute_deterministic_equations (std::size_t k)

bool	compute_deterministic_data (std::size_t k)

void	compute_deterministic ()

void	compute_summand_classes ()

void	compute_vis_invis ()

std::string	print_variables (const data::variable_list &v) const

void	print_summand (const srf_summand &summand, bool is_conjunctive) const

void	print_pbes () const

void	print_summand_classes () const

Static Protected Member Functions
static summand_equivalence_key	rename_duplicate_variables (data::set_identifier_generator &id_gen, const summand_equivalence_key &summ)

Protected Attributes
data::rewriter	m_rewr

data::enumerator_identifier_generator	m_id_generator

data::enumerator_algorithm	m_enumerator

srf_pbes	m_pbes

pbes_equation_index	m_equation_index

data::mutable_indexed_substitution	m_sigma

std::size_t	m_largest_equation_size = 0

std::vector< data::variable >	m_parameters

std::map< data::variable, std::size_t >	m_parameter_positions

std::unordered_map< summand_equivalence_key, std::size_t >	m_summand_index

std::vector< summand_class >	m_summand_classes

summand_set	m_invis

summand_set	m_vis

std::vector< summand_set >	m_dependency_nes

std::chrono::high_resolution_clock::duration	m_static_analysis_duration {}

std::chrono::high_resolution_clock::duration	m_exploration_duration {}

std::unique_ptr< smt::smt_solver >	m_solver

pbespor_options	m_options

Detailed Description

Definition at line 240 of file partial_order_reduction.h.

Member Typedef Documentation

◆ enumerator_element

using mcrl2::pbes_system::partial_order_reduction_algorithm::enumerator_element = data::enumerator_list_element_with_substitution<data::data_expression>

protected

Definition at line 243 of file partial_order_reduction.h.

Constructor & Destructor Documentation

◆ partial_order_reduction_algorithm()

mcrl2::pbes_system::partial_order_reduction_algorithm::partial_order_reduction_algorithm	(	const pbes &	p,
		pbespor_options	options
	)

inlineexplicit

Definition at line 1363 of file partial_order_reduction.h.

Member Function Documentation

◆ choose_minimal_NES()

const summand_set & mcrl2::pbes_system::partial_order_reduction_algorithm::choose_minimal_NES	(	std::size_t	k,
		const propositional_variable_instantiation &	X_e
	)		const

inlineprotected

Definition at line 594 of file partial_order_reduction.h.

◆ compute_dependency_NES()

void mcrl2::pbes_system::partial_order_reduction_algorithm::compute_dependency_NES ( )

inlineprotected

Definition at line 880 of file partial_order_reduction.h.

◆ compute_deterministic()

void mcrl2::pbes_system::partial_order_reduction_algorithm::compute_deterministic ( )

inlineprotected

Definition at line 1223 of file partial_order_reduction.h.

◆ compute_deterministic_data()

bool mcrl2::pbes_system::partial_order_reduction_algorithm::compute_deterministic_data ( std::size_t k )

inlineprotected

Definition at line 1193 of file partial_order_reduction.h.

◆ compute_deterministic_equations()

bool mcrl2::pbes_system::partial_order_reduction_algorithm::compute_deterministic_equations ( std::size_t k )

inlineprotected

Definition at line 1178 of file partial_order_reduction.h.

◆ compute_DNA_DNL_NES()

void mcrl2::pbes_system::partial_order_reduction_algorithm::compute_DNA_DNL_NES ( const std::vector< parameter_info > & info )

inlineprotected

Definition at line 1052 of file partial_order_reduction.h.

◆ compute_NES_DNA_DNL()

void mcrl2::pbes_system::partial_order_reduction_algorithm::compute_NES_DNA_DNL ( )

inlineprotected

Definition at line 1122 of file partial_order_reduction.h.

◆ compute_nxt()

void mcrl2::pbes_system::partial_order_reduction_algorithm::compute_nxt ( )

inlineprotected

Definition at line 786 of file partial_order_reduction.h.

◆ compute_summand_classes()

void mcrl2::pbes_system::partial_order_reduction_algorithm::compute_summand_classes ( )

inlineprotected

Definition at line 1236 of file partial_order_reduction.h.

◆ compute_vis_invis()

void mcrl2::pbes_system::partial_order_reduction_algorithm::compute_vis_invis ( )

inlineprotected

Definition at line 1264 of file partial_order_reduction.h.

◆ dependency_permanently_disables()

bool mcrl2::pbes_system::partial_order_reduction_algorithm::dependency_permanently_disables	(	const std::size_t	k,
		const std::size_t	k1
	)		const

inlineprotected

Return true iff k1 can never happen after k happens, as deduced from predicate dependencies.

Definition at line 845 of file partial_order_reduction.h.

◆ depends() [1/2]

bool mcrl2::pbes_system::partial_order_reduction_algorithm::depends	(	std::size_t	i,
		std::size_t	k
	)		const

inlineprotected

Definition at line 910 of file partial_order_reduction.h.

◆ depends() [2/2]

bool mcrl2::pbes_system::partial_order_reduction_algorithm::depends	(	std::size_t	i,
		std::size_t	k,
		std::size_t	j
	)		const

inlineprotected

Definition at line 903 of file partial_order_reduction.h.

◆ DNA() [1/2]

summand_set & mcrl2::pbes_system::partial_order_reduction_algorithm::DNA ( std::size_t k )

inlineprotected

Definition at line 517 of file partial_order_reduction.h.

◆ DNA() [2/2]

const summand_set & mcrl2::pbes_system::partial_order_reduction_algorithm::DNA ( std::size_t k ) const

inlineprotected

Definition at line 512 of file partial_order_reduction.h.

◆ DNL() [1/2]

summand_set & mcrl2::pbes_system::partial_order_reduction_algorithm::DNL ( std::size_t k )

inlineprotected

Definition at line 537 of file partial_order_reduction.h.

◆ DNL() [2/2]

const summand_set & mcrl2::pbes_system::partial_order_reduction_algorithm::DNL ( std::size_t k ) const

inlineprotected

Definition at line 532 of file partial_order_reduction.h.

◆ DNS() [1/2]

summand_set & mcrl2::pbes_system::partial_order_reduction_algorithm::DNS ( std::size_t k )

inlineprotected

Definition at line 527 of file partial_order_reduction.h.

◆ DNS() [2/2]

const summand_set & mcrl2::pbes_system::partial_order_reduction_algorithm::DNS ( std::size_t k ) const

inlineprotected

Definition at line 522 of file partial_order_reduction.h.

◆ DNX()

const summand_set & mcrl2::pbes_system::partial_order_reduction_algorithm::DNX	(	std::size_t	k,
		const summand_set &	Twork,
		const summand_set &	Ts,
		const summand_set &	en_X_e
	)		const

inlineprotected

Definition at line 606 of file partial_order_reduction.h.

◆ en()

summand_set mcrl2::pbes_system::partial_order_reduction_algorithm::en ( const propositional_variable_instantiation & X_e )

inlineprotected

Definition at line 552 of file partial_order_reduction.h.

◆ explore()

template<typename EmitNode = utilities::skip, typename EmitEdge = utilities::skip>

void mcrl2::pbes_system::partial_order_reduction_algorithm::explore	(	const propositional_variable_instantiation &	X_init,
		EmitNode	emit_node = `EmitNode()`,
		EmitEdge	emit_edge = `EmitEdge()`
	)

inline

< Will be partially expanded

< Has been partially expanded

< Needs to be fully expanded, because it starts a cycle

< Has been fully expanded

Definition at line 1427 of file partial_order_reduction.h.

◆ explore_full()

template<typename EmitNode = utilities::skip, typename EmitEdge = utilities::skip>

void mcrl2::pbes_system::partial_order_reduction_algorithm::explore_full	(	const propositional_variable_instantiation &	X_init,
		EmitNode	emit_node = `EmitNode()`,
		EmitEdge	emit_edge = `EmitEdge()`
	)

inline

Definition at line 1594 of file partial_order_reduction.h.

◆ FV()

std::set< std::size_t > mcrl2::pbes_system::partial_order_reduction_algorithm::FV ( const pbes_expression & x ) const

inlineprotected

Definition at line 802 of file partial_order_reduction.h.

◆ initial_state()

const propositional_variable_instantiation & mcrl2::pbes_system::partial_order_reduction_algorithm::initial_state ( ) const

inline

Definition at line 1402 of file partial_order_reduction.h.

◆ invis()

summand_set mcrl2::pbes_system::partial_order_reduction_algorithm::invis ( const summand_set & K )

inlineprotected

Definition at line 588 of file partial_order_reduction.h.

◆ is_true()

bool mcrl2::pbes_system::partial_order_reduction_algorithm::is_true ( data::data_expression expr )

inlineprotected

Definition at line 812 of file partial_order_reduction.h.

◆ left_accords_equations()

tribool mcrl2::pbes_system::partial_order_reduction_algorithm::left_accords_equations	(	std::size_t	k,
		std::size_t	k1
	)		const

inlineprotected

Definition at line 949 of file partial_order_reduction.h.

◆ NES() [1/2]

summand_set & mcrl2::pbes_system::partial_order_reduction_algorithm::NES ( std::size_t k )

inlineprotected

Definition at line 547 of file partial_order_reduction.h.

◆ NES() [2/2]

const summand_set & mcrl2::pbes_system::partial_order_reduction_algorithm::NES ( std::size_t k ) const

inlineprotected

Definition at line 542 of file partial_order_reduction.h.

◆ parameter_position()

std::size_t mcrl2::pbes_system::partial_order_reduction_algorithm::parameter_position ( const data::variable & v ) const

inlineprotected

Definition at line 506 of file partial_order_reduction.h.

◆ parameters()

const std::vector< data::variable > & mcrl2::pbes_system::partial_order_reduction_algorithm::parameters ( ) const

inline

Definition at line 1407 of file partial_order_reduction.h.

◆ print()

void mcrl2::pbes_system::partial_order_reduction_algorithm::print ( ) const

inline

Definition at line 1418 of file partial_order_reduction.h.

◆ print_pbes()

void mcrl2::pbes_system::partial_order_reduction_algorithm::print_pbes ( ) const

inlineprotected

Definition at line 1327 of file partial_order_reduction.h.

◆ print_summand()

void mcrl2::pbes_system::partial_order_reduction_algorithm::print_summand	(	const srf_summand &	summand,
		bool	is_conjunctive
	)		const

inlineprotected

Definition at line 1313 of file partial_order_reduction.h.

◆ print_summand_classes()

void mcrl2::pbes_system::partial_order_reduction_algorithm::print_summand_classes ( ) const

inlineprotected

Definition at line 1341 of file partial_order_reduction.h.

◆ print_variables()

std::string mcrl2::pbes_system::partial_order_reduction_algorithm::print_variables ( const data::variable_list & v ) const

inlineprotected

Definition at line 1299 of file partial_order_reduction.h.

◆ rename_duplicate_variables()

static summand_equivalence_key mcrl2::pbes_system::partial_order_reduction_algorithm::rename_duplicate_variables	(	data::set_identifier_generator &	id_gen,
		const summand_equivalence_key &	summ
	)

inlinestaticprotected

Definition at line 923 of file partial_order_reduction.h.

◆ square_accords_equations()

tribool mcrl2::pbes_system::partial_order_reduction_algorithm::square_accords_equations	(	std::size_t	k,
		std::size_t	k1
	)		const

inlineprotected

Definition at line 986 of file partial_order_reduction.h.

◆ stubborn_set()

summand_set mcrl2::pbes_system::partial_order_reduction_algorithm::stubborn_set	(	const propositional_variable_instantiation &	X_e,
		const summand_set &	en_X_e
	)

inlineprotected

Definition at line 639 of file partial_order_reduction.h.

◆ succ()

std::set< propositional_variable_instantiation > mcrl2::pbes_system::partial_order_reduction_algorithm::succ	(	const propositional_variable_instantiation &	X_e,
		const summand_set &	K
	)

inlineprotected

Definition at line 747 of file partial_order_reduction.h.

◆ summand_index()

std::size_t mcrl2::pbes_system::partial_order_reduction_algorithm::summand_index ( const srf_summand & summand ) const

inlineprotected

Definition at line 499 of file partial_order_reduction.h.

◆ symbol()

const fixpoint_symbol & mcrl2::pbes_system::partial_order_reduction_algorithm::symbol ( const core::identifier_string & X ) const

inline

Definition at line 1412 of file partial_order_reduction.h.

◆ triangle_accords_equations()

tribool mcrl2::pbes_system::partial_order_reduction_algorithm::triangle_accords_equations	(	std::size_t	k,
		std::size_t	k1
	)		const

inlineprotected

Definition at line 1024 of file partial_order_reduction.h.

Member Data Documentation

◆ m_dependency_nes

std::vector<summand_set> mcrl2::pbes_system::partial_order_reduction_algorithm::m_dependency_nes

protected

Definition at line 293 of file partial_order_reduction.h.

◆ m_enumerator

data::enumerator_algorithm mcrl2::pbes_system::partial_order_reduction_algorithm::m_enumerator

protected

Definition at line 269 of file partial_order_reduction.h.

◆ m_equation_index

pbes_equation_index mcrl2::pbes_system::partial_order_reduction_algorithm::m_equation_index

protected

Definition at line 271 of file partial_order_reduction.h.

◆ m_exploration_duration

std::chrono::high_resolution_clock::duration mcrl2::pbes_system::partial_order_reduction_algorithm::m_exploration_duration {}

protected

Definition at line 296 of file partial_order_reduction.h.

◆ m_id_generator

data::enumerator_identifier_generator mcrl2::pbes_system::partial_order_reduction_algorithm::m_id_generator

protected

Definition at line 268 of file partial_order_reduction.h.

◆ m_invis

summand_set mcrl2::pbes_system::partial_order_reduction_algorithm::m_invis

protected

Definition at line 288 of file partial_order_reduction.h.

◆ m_largest_equation_size

std::size_t mcrl2::pbes_system::partial_order_reduction_algorithm::m_largest_equation_size = 0

protected

Definition at line 273 of file partial_order_reduction.h.

◆ m_options

pbespor_options mcrl2::pbes_system::partial_order_reduction_algorithm::m_options

protected

Definition at line 300 of file partial_order_reduction.h.

◆ m_parameter_positions

std::map<data::variable, std::size_t> mcrl2::pbes_system::partial_order_reduction_algorithm::m_parameter_positions

protected

Definition at line 279 of file partial_order_reduction.h.

◆ m_parameters

std::vector<data::variable> mcrl2::pbes_system::partial_order_reduction_algorithm::m_parameters

protected

Definition at line 276 of file partial_order_reduction.h.

◆ m_pbes

srf_pbes mcrl2::pbes_system::partial_order_reduction_algorithm::m_pbes

protected

Definition at line 270 of file partial_order_reduction.h.

◆ m_rewr

data::rewriter mcrl2::pbes_system::partial_order_reduction_algorithm::m_rewr

protected

Definition at line 267 of file partial_order_reduction.h.

◆ m_sigma

data::mutable_indexed_substitution mcrl2::pbes_system::partial_order_reduction_algorithm::m_sigma

protected

Definition at line 272 of file partial_order_reduction.h.

◆ m_solver

std::unique_ptr<smt::smt_solver> mcrl2::pbes_system::partial_order_reduction_algorithm::m_solver

protected

Definition at line 298 of file partial_order_reduction.h.

◆ m_static_analysis_duration

std::chrono::high_resolution_clock::duration mcrl2::pbes_system::partial_order_reduction_algorithm::m_static_analysis_duration {}

protected

Definition at line 295 of file partial_order_reduction.h.

◆ m_summand_classes

std::vector<summand_class> mcrl2::pbes_system::partial_order_reduction_algorithm::m_summand_classes

protected

Definition at line 286 of file partial_order_reduction.h.

◆ m_summand_index

std::unordered_map<summand_equivalence_key, std::size_t> mcrl2::pbes_system::partial_order_reduction_algorithm::m_summand_index

protected

Definition at line 282 of file partial_order_reduction.h.

◆ m_vis

summand_set mcrl2::pbes_system::partial_order_reduction_algorithm::m_vis

protected

Definition at line 289 of file partial_order_reduction.h.

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

pbes/include/mcrl2/pbes/partial_order_reduction.h

Classes

Public Member Functions

Protected Types

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ enumerator_element

Constructor & Destructor Documentation

◆ partial_order_reduction_algorithm()

Member Function Documentation

◆ choose_minimal_NES()

◆ compute_dependency_NES()

◆ compute_deterministic()

◆ compute_deterministic_data()

◆ compute_deterministic_equations()

◆ compute_DNA_DNL_NES()

◆ compute_NES_DNA_DNL()

◆ compute_nxt()

◆ compute_summand_classes()

◆ compute_vis_invis()

◆ dependency_permanently_disables()

◆ depends() [1/2]

◆ depends() [2/2]

◆ DNA() [1/2]

◆ DNA() [2/2]

◆ DNL() [1/2]

◆ DNL() [2/2]

◆ DNS() [1/2]

◆ DNS() [2/2]

◆ DNX()

◆ en()

◆ explore()

◆ explore_full()

◆ FV()

◆ initial_state()

◆ invis()

◆ is_true()

◆ left_accords_equations()

◆ NES() [1/2]

◆ NES() [2/2]

◆ parameter_position()

◆ parameters()

◆ print()

◆ print_pbes()

◆ print_summand()

◆ print_summand_classes()

◆ print_variables()

◆ rename_duplicate_variables()

◆ square_accords_equations()

◆ stubborn_set()

◆ succ()

◆ summand_index()

◆ symbol()

◆ triangle_accords_equations()

Member Data Documentation

◆ m_dependency_nes

◆ m_enumerator

◆ m_equation_index

◆ m_exploration_duration

◆ m_id_generator

◆ m_invis

◆ m_largest_equation_size

◆ m_options

◆ m_parameter_positions

◆ m_parameters

◆ m_pbes

◆ m_rewr

◆ m_sigma

◆ m_solver

◆ m_static_analysis_duration

◆ m_summand_classes

◆ m_summand_index

◆ m_vis