Algorithm class for the eqelm algorithm. More...

#include <eqelm.h>

Public Member Functions
	pbes_eqelm_algorithm (const DataRewriter &datar, const PbesRewriter &pbesr)
	Constructor.

void	run (pbes &p, bool ignore_initial_state=false)
	Runs the eqelm algorithm.

Protected Types
using	equivalence_class = std::set< data::variable >

Protected Member Functions
std::vector< equivalence_class >	compute_equivalence_sets (const propositional_variable &X) const
	Puts all parameters of the same sort in the same equivalence set.

std::string	print_vertices () const
	Prints the vertices of the dependency graph.

std::string	print_edges () const
	Prints the edges of the dependency graph.

std::string	print_equivalence_classes () const
	Prints the equivalence classes.

void	log_todo_list (const std::set< core::identifier_string > &todo, const std::string &msg="") const
	Prints the todo list.

bool	evaluate_guard (const core::identifier_string &, const propositional_variable_instantiation &)
	Returns true if the vertex X should propagate its values to Y.

template<typename VariableContainer >
std::size_t	index_of (const data::variable &x, const VariableContainer &v)
	Returns the index of the element x in the sequence v.

template<typename Substitution >
void	update_equivalence_classes (const propositional_variable_instantiation &Ye, const Substitution &vX, std::set< core::identifier_string > &todo)
	Propagate the equivalence relations given by the substitution vX over the edge Ye.

data::mutable_map_substitution	compute_substitution (const core::identifier_string &X)
	Computes a substitution that corresponds to the equivalence relations in X.

void	apply_equivalence_relations (pbes &p)
	Chooses one parameter for every equivalence class, and removes the others. All occurrences of the removed parameters are replaced by the chosen parameter.

Protected Attributes
const DataRewriter &	m_data_rewriter
	Compares data expressions for equality.

const PbesRewriter &	m_pbes_rewriter
	Compares data expressions for equality.

std::map< core::identifier_string, std::vector< equivalence_class > >	m_vertices
	The vertices of the grapth, i.e. the equivalence relations. It stores the equivalence sets for each propositional variable, for example X -> [ {x1, x3}, {x2, x4} ]. Equivalence sets of size 1 are not stored.

std::map< core::identifier_string, std::set< propositional_variable_instantiation > >	m_edges
	The edges of the graph. It is a mapping from X to iocc(X).

std::map< core::identifier_string, std::vector< data::variable > >	m_parameters
	The parameters of the propositional variable declarations. These are stored inside a vector, for efficiency reasons.

std::map< core::identifier_string, bool >	m_discovered
	Used for determining if a vertex has been visited before.

Detailed Description

template<typename Term, typename DataRewriter, typename PbesRewriter>
class mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >

Algorithm class for the eqelm algorithm.

Definition at line 24 of file eqelm.h.

Member Typedef Documentation

◆ equivalence_class

template<typename Term , typename DataRewriter , typename PbesRewriter >

using mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::equivalence_class = std::set<data::variable>

protected

Definition at line 27 of file eqelm.h.

Constructor & Destructor Documentation

◆ pbes_eqelm_algorithm()

template<typename Term , typename DataRewriter , typename PbesRewriter >

mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::pbes_eqelm_algorithm	(	const DataRewriter &	datar,
		const PbesRewriter &	pbesr
	)

inline

Constructor.

Parameters

datar	A data rewriter
pbesr	A PBES rewriter

Definition at line 237 of file eqelm.h.

Member Function Documentation

◆ apply_equivalence_relations()

template<typename Term , typename DataRewriter , typename PbesRewriter >

void mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::apply_equivalence_relations ( pbes & p )

inlineprotected

Chooses one parameter for every equivalence class, and removes the others. All occurrences of the removed parameters are replaced by the chosen parameter.

Definition at line 200 of file eqelm.h.

◆ compute_equivalence_sets()

template<typename Term , typename DataRewriter , typename PbesRewriter >

std::vector< equivalence_class > mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::compute_equivalence_sets ( const propositional_variable & X ) const

inlineprotected

Puts all parameters of the same sort in the same equivalence set.

Definition at line 52 of file eqelm.h.

◆ compute_substitution()

template<typename Term , typename DataRewriter , typename PbesRewriter >

data::mutable_map_substitution mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::compute_substitution ( const core::identifier_string & X )

inlineprotected

Computes a substitution that corresponds to the equivalence relations in X.

Definition at line 182 of file eqelm.h.

◆ evaluate_guard()

template<typename Term , typename DataRewriter , typename PbesRewriter >

bool mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::evaluate_guard	(	const core::identifier_string &	,
		const propositional_variable_instantiation &
	)

inlineprotected

Returns true if the vertex X should propagate its values to Y.

Definition at line 126 of file eqelm.h.

◆ index_of()

template<typename Term , typename DataRewriter , typename PbesRewriter >

template<typename VariableContainer >

std::size_t mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::index_of	(	const data::variable &	x,
		const VariableContainer &	v
	)

inlineprotected

Returns the index of the element x in the sequence v.

Definition at line 133 of file eqelm.h.

◆ log_todo_list()

template<typename Term , typename DataRewriter , typename PbesRewriter >

void mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::log_todo_list	(	const std::set< core::identifier_string > &	todo,
		const std::string &	msg = `""`
	)		const

inlineprotected

Prints the todo list.

Definition at line 119 of file eqelm.h.

◆ print_edges()

template<typename Term , typename DataRewriter , typename PbesRewriter >

std::string mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::print_edges ( ) const

inlineprotected

Prints the edges of the dependency graph.

Definition at line 92 of file eqelm.h.

◆ print_equivalence_classes()

template<typename Term , typename DataRewriter , typename PbesRewriter >

std::string mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::print_equivalence_classes ( ) const

inlineprotected

Prints the equivalence classes.

Definition at line 103 of file eqelm.h.

◆ print_vertices()

template<typename Term , typename DataRewriter , typename PbesRewriter >

std::string mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::print_vertices ( ) const

inlineprotected

Prints the vertices of the dependency graph.

Definition at line 71 of file eqelm.h.

◆ run()

template<typename Term , typename DataRewriter , typename PbesRewriter >

void mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::run	(	pbes &	p,
		bool	ignore_initial_state = `false`
	)

inline

Runs the eqelm algorithm.

Parameters

p	A pbes
ignore_initial_state	If true, the initial state is ignored.

Definition at line 245 of file eqelm.h.

◆ update_equivalence_classes()

template<typename Term , typename DataRewriter , typename PbesRewriter >

template<typename Substitution >

void mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::update_equivalence_classes	(	const propositional_variable_instantiation &	Ye,
		const Substitution &	vX,
		std::set< core::identifier_string > &	todo
	)

inlineprotected

Propagate the equivalence relations given by the substitution vX over the edge Ye.

Definition at line 140 of file eqelm.h.

Member Data Documentation

◆ m_data_rewriter

template<typename Term , typename DataRewriter , typename PbesRewriter >

const DataRewriter& mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::m_data_rewriter

protected

Compares data expressions for equality.

Definition at line 30 of file eqelm.h.

◆ m_discovered

template<typename Term , typename DataRewriter , typename PbesRewriter >

std::map<core::identifier_string, bool> mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::m_discovered

protected

Used for determining if a vertex has been visited before.

Definition at line 49 of file eqelm.h.

◆ m_edges

template<typename Term , typename DataRewriter , typename PbesRewriter >

std::map<core::identifier_string, std::set<propositional_variable_instantiation> > mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::m_edges

protected

The edges of the graph. It is a mapping from X to iocc(X).

Definition at line 42 of file eqelm.h.

◆ m_parameters

template<typename Term , typename DataRewriter , typename PbesRewriter >

std::map<core::identifier_string, std::vector<data::variable> > mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::m_parameters

protected

The parameters of the propositional variable declarations. These are stored inside a vector, for efficiency reasons.

Definition at line 46 of file eqelm.h.

◆ m_pbes_rewriter

template<typename Term , typename DataRewriter , typename PbesRewriter >

const PbesRewriter& mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::m_pbes_rewriter

protected

Compares data expressions for equality.

Definition at line 33 of file eqelm.h.

◆ m_vertices

template<typename Term , typename DataRewriter , typename PbesRewriter >

std::map<core::identifier_string, std::vector<equivalence_class> > mcrl2::pbes_system::pbes_eqelm_algorithm< Term, DataRewriter, PbesRewriter >::m_vertices

protected

The vertices of the grapth, i.e. the equivalence relations. It stores the equivalence sets for each propositional variable, for example X -> [ {x1, x3}, {x2, x4} ]. Equivalence sets of size 1 are not stored.

Definition at line 38 of file eqelm.h.

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

pbes/include/mcrl2/pbes/eqelm.h

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ equivalence_class

Constructor & Destructor Documentation

◆ pbes_eqelm_algorithm()

Member Function Documentation

◆ apply_equivalence_relations()

◆ compute_equivalence_sets()

◆ compute_substitution()

◆ evaluate_guard()

◆ index_of()

◆ log_todo_list()

◆ print_edges()

◆ print_equivalence_classes()

◆ print_vertices()

◆ run()

◆ update_equivalence_classes()

Member Data Documentation

◆ m_data_rewriter

◆ m_discovered

◆ m_edges

◆ m_parameters

◆ m_pbes_rewriter

◆ m_vertices