Base class for bisimulation algorithms. More...

#include <bisimulation.h>

Inheritance diagram for mcrl2::pbes_system::bisimulation_algorithm:

Public Types
using	my_iterator = lps::action_summand_vector::const_iterator
	The iterator type for non-delta summands.

Public Member Functions
core::identifier_string	X (const lps::linear_process &p, const lps::linear_process &q) const
	Creates a name for the propositional variable Xpq.

core::identifier_string	Y (const lps::linear_process &p, const lps::linear_process &q) const
	Creates a name for the propositional variable Ypq.

core::identifier_string	Y (const lps::linear_process &p, const lps::linear_process &q, my_iterator i) const
	Creates a name for the propositional variable Ypqi.

core::identifier_string	Y1 (const lps::linear_process &p, const lps::linear_process &q, my_iterator i) const
	Creates a name for the propositional variable Y1pqi.

core::identifier_string	Y2 (const lps::linear_process &p, const lps::linear_process &q, my_iterator i) const
	Creates a name for the propositional variable Y2pqi.

propositional_variable_instantiation	var (const core::identifier_string &name, const data::variable_list &parameters) const
	Creates a propositional variable.

propositional_variable_instantiation	var (const core::identifier_string &name, const data::data_expression_list &parameters) const
	Creates a propositional variable.

pbes_expression	equals (const lps::multi_action &a, const lps::multi_action &b) const
	Returns a pbes expression that expresses equality of the multi-actions a and b.

fixpoint_symbol	mu () const
	Returns the fixpoint symbol mu.

fixpoint_symbol	nu () const
	Returns the fixpoint symbol nu.

data::mutable_map_substitution	compute_process_parameter_name_clashes (const lps::specification &p, const lps::specification &q) const
	Returns a substitution of variables in q such that there are no name clashes between p and q.

data::mutable_map_substitution	compute_summand_variable_name_clashes (const lps::specification &p, const lps::specification &q) const
	Returns a substitution of variables in q such that there are no name clashes between the summation variables of p and q.

void	resolve_name_clashes (const lps::specification &model, lps::specification &spec, bool include_summand_variables=false)
	Resolves name clashes between model and spec.

void	init (const lps::linear_process &model, const lps::linear_process &spec)
	Initializes the name lookup table.

pbes	build_pbes (const std::vector< pbes_equation > &equations, const lps::specification &M, const lps::specification &S)
	Builds a pbes from the given equations.

Protected Types
using	name_map = std::map< const lps::action_summand *, std::string >
	A map type for mapping summands to strings.

Protected Member Functions
std::string	action_list_name (const process::action_list &l) const
	Generates a name for an action_list.

std::string	summand_name (my_iterator i) const
	Returns the name of a summand.

bool	is_from_model (const lps::linear_process &p) const
	Returns true if p is the linear process of the model.

std::string	process_name (const lps::linear_process &p) const
	Returns a name of a linear process.

void	set_summand_names (const lps::linear_process &p)
	Used for initializing summand names.

template<std::ranges::range R> requires std::is_same_v<std::ranges::range_value_t<R>, data::data_expression>
void	make_substitution (const data::variable_list &v, R e, data::mutable_map_substitution<> &result) const

Protected Attributes
name_map	summand_names
	Maps summands to strings.

const lps::linear_process *	model_ptr = nullptr
	Store the address of the model.

Detailed Description

Base class for bisimulation algorithms.

Definition at line 30 of file bisimulation.h.

Member Typedef Documentation

◆ my_iterator

using mcrl2::pbes_system::bisimulation_algorithm::my_iterator = lps::action_summand_vector::const_iterator

The iterator type for non-delta summands.

Definition at line 34 of file bisimulation.h.

◆ name_map

using mcrl2::pbes_system::bisimulation_algorithm::name_map = std::map<const lps::action_summand*, std::string>

protected

A map type for mapping summands to strings.

Definition at line 38 of file bisimulation.h.

Member Function Documentation

◆ action_list_name()

std::string mcrl2::pbes_system::bisimulation_algorithm::action_list_name ( const process::action_list & l ) const

inlineprotected

Generates a name for an action_list.

Parameters

l	A sequence of actions

Returns: A string representation of the list l

Definition at line 49 of file bisimulation.h.

◆ build_pbes()

pbes mcrl2::pbes_system::bisimulation_algorithm::build_pbes	(	const std::vector< pbes_equation > &	equations,
		const lps::specification &	M,
		const lps::specification &	S
	)

inline

Builds a pbes from the given equations.

Parameters

equations	A sequence of pbes equations
M	A specification
S	A specification

Returns: The constructed pbes

Definition at line 333 of file bisimulation.h.

◆ compute_process_parameter_name_clashes()

data::mutable_map_substitution mcrl2::pbes_system::bisimulation_algorithm::compute_process_parameter_name_clashes	(	const lps::specification &	p,
		const lps::specification &	q
	)		const

inline

Returns a substitution of variables in q such that there are no name clashes between p and q.

Parameters

p	A linear process specification
q	A linear process specification

Returns: A substitution that should be applied to q to remove name clashes between p and q.

After this substitution the following holds:

$((param(p)\cup glob(p))\cap ((param(q)\cup glob(q))=\emptyset$

where param(p) denotes p.process().process_parameters() and glob(p) denotes p.global_variables().

Definition at line 231 of file bisimulation.h.

◆ compute_summand_variable_name_clashes()

data::mutable_map_substitution mcrl2::pbes_system::bisimulation_algorithm::compute_summand_variable_name_clashes	(	const lps::specification &	p,
		const lps::specification &	q
	)		const

inline

Returns a substitution of variables in q such that there are no name clashes between the summation variables of p and q.

Parameters

p	A linear process specification
q	A linear process specification

Returns: A substitution that should be applied to q to remove name clashes between p and q.

Definition at line 262 of file bisimulation.h.

◆ equals()

pbes_expression mcrl2::pbes_system::bisimulation_algorithm::equals	(	const lps::multi_action &	a,
		const lps::multi_action &	b
	)		const

inline

Returns a pbes expression that expresses equality of the multi-actions a and b.

Parameters

a	A sequence of actions
b	A sequence of actions

Returns: Necessary conditions for the equality of a and b

Definition at line 204 of file bisimulation.h.

◆ init()

void mcrl2::pbes_system::bisimulation_algorithm::init	(	const lps::linear_process &	model,
		const lps::linear_process &	spec
	)

inline

Initializes the name lookup table.

Parameters

model	A linear process
spec	A linear process

Precondition: model and spec must have the same data specification

Definition at line 318 of file bisimulation.h.

◆ is_from_model()

bool mcrl2::pbes_system::bisimulation_algorithm::is_from_model ( const lps::linear_process & p ) const

inlineprotected

Returns true if p is the linear process of the model.

Parameters

p	A linear process

Returns: True if p is the linear process of the model.

Definition at line 78 of file bisimulation.h.

◆ make_substitution()

template<std::ranges::range R>
requires std::is_same_v<std::ranges::range_value_t<R>, data::data_expression>

void mcrl2::pbes_system::bisimulation_algorithm::make_substitution	(	const data::variable_list &	v,
		R	e,
		data::mutable_map_substitution<> &	result
	)		const

inlineprotected

Definition at line 114 of file bisimulation.h.

◆ mu()

fixpoint_symbol mcrl2::pbes_system::bisimulation_algorithm::mu ( ) const

inline

Returns the fixpoint symbol mu.

Returns: The fixpoint symbol mu.

Definition at line 211 of file bisimulation.h.

◆ nu()

fixpoint_symbol mcrl2::pbes_system::bisimulation_algorithm::nu ( ) const

inline

Returns the fixpoint symbol nu.

Returns: The fixpoint symbol nu.

Definition at line 218 of file bisimulation.h.

◆ process_name()

std::string mcrl2::pbes_system::bisimulation_algorithm::process_name ( const lps::linear_process & p ) const

inlineprotected

Returns a name of a linear process.

Parameters

p	A linear process

Returns: The name of the linear process.

Definition at line 86 of file bisimulation.h.

◆ resolve_name_clashes()

void mcrl2::pbes_system::bisimulation_algorithm::resolve_name_clashes	(	const lps::specification &	model,
		lps::specification &	spec,
		bool	include_summand_variables = `false`
	)

inline

Resolves name clashes between model and spec.

Definition at line 302 of file bisimulation.h.

◆ set_summand_names()

void mcrl2::pbes_system::bisimulation_algorithm::set_summand_names ( const lps::linear_process & p )

inlineprotected

Used for initializing summand names.

Parameters

p	A linear process

Definition at line 100 of file bisimulation.h.

◆ summand_name()

std::string mcrl2::pbes_system::bisimulation_algorithm::summand_name ( my_iterator i ) const

inlineprotected

Returns the name of a summand.

Parameters

i	A summand iterator

Returns: The name of the summand referred to by i

Definition at line 67 of file bisimulation.h.

◆ var() [1/2]

propositional_variable_instantiation mcrl2::pbes_system::bisimulation_algorithm::var	(	const core::identifier_string &	name,
		const data::data_expression_list &	parameters
	)		const

inline

Creates a propositional variable.

Parameters

name	A
parameters	A sequence of data expressions

Returns: The created propositional variable

Definition at line 195 of file bisimulation.h.

◆ var() [2/2]

propositional_variable_instantiation mcrl2::pbes_system::bisimulation_algorithm::var	(	const core::identifier_string &	name,
		const data::variable_list &	parameters
	)		const

inline

Creates a propositional variable.

Parameters

name	A
parameters	A sequence of data variables

Returns: The created propositional variable

Definition at line 186 of file bisimulation.h.

◆ X()

core::identifier_string mcrl2::pbes_system::bisimulation_algorithm::X	(	const lps::linear_process &	p,
		const lps::linear_process &	q
	)		const

inline

Creates a name for the propositional variable Xpq.

Parameters

p	A linear process
q	A linear process

Returns: The name for the propositional variable Xpq

Definition at line 130 of file bisimulation.h.

◆ Y() [1/2]

core::identifier_string mcrl2::pbes_system::bisimulation_algorithm::Y	(	const lps::linear_process &	p,
		const lps::linear_process &	q
	)		const

inline

Creates a name for the propositional variable Ypq.

Parameters

p	A linear process
q	A linear process

Returns: The name for the propositional variable Ypq

Definition at line 140 of file bisimulation.h.

◆ Y() [2/2]

core::identifier_string mcrl2::pbes_system::bisimulation_algorithm::Y	(	const lps::linear_process &	p,
		const lps::linear_process &	q,
		my_iterator	i
	)		const

inline

Creates a name for the propositional variable Ypqi.

Precondition: The iterator i must be in p.action_summands().

Parameters

p	A linear process
q	A linear process
i	A summand iterator

Returns: The name for the propositional variable Ypqi

Definition at line 152 of file bisimulation.h.

◆ Y1()

core::identifier_string mcrl2::pbes_system::bisimulation_algorithm::Y1	(	const lps::linear_process &	p,
		const lps::linear_process &	q,
		my_iterator	i
	)		const

inline

Creates a name for the propositional variable Y1pqi.

Precondition: The iterator i must be in p.action_summands().

Parameters

p	A linear process
q	A linear process
i	A summand iterator

Returns: The name for the propositional variable Y1pqi

Definition at line 164 of file bisimulation.h.

◆ Y2()

core::identifier_string mcrl2::pbes_system::bisimulation_algorithm::Y2	(	const lps::linear_process &	p,
		const lps::linear_process &	q,
		my_iterator	i
	)		const

inline

Creates a name for the propositional variable Y2pqi.

Precondition: The iterator i must be in p.action_summands().

Parameters

p	A linear process
q	A linear process
i	A summand iterator

Returns: The name for the propositional variable Y2pqi

Definition at line 176 of file bisimulation.h.

Member Data Documentation

◆ model_ptr

const lps::linear_process* mcrl2::pbes_system::bisimulation_algorithm::model_ptr = nullptr

protected

Store the address of the model.

Definition at line 44 of file bisimulation.h.

◆ summand_names

name_map mcrl2::pbes_system::bisimulation_algorithm::summand_names

protected

Maps summands to strings.

Definition at line 41 of file bisimulation.h.

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

pbes/include/mcrl2/pbes/bisimulation.h

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ my_iterator

◆ name_map

Member Function Documentation

◆ action_list_name()

◆ build_pbes()

◆ compute_process_parameter_name_clashes()

◆ compute_summand_variable_name_clashes()

◆ equals()

◆ init()

◆ is_from_model()

◆ make_substitution()

◆ mu()

◆ nu()

◆ process_name()

◆ resolve_name_clashes()

◆ set_summand_names()

◆ summand_name()

◆ var() [1/2]

◆ var() [2/2]

◆ X()

◆ Y() [1/2]

◆ Y() [2/2]

◆ Y1()

◆ Y2()

Member Data Documentation

◆ model_ptr

◆ summand_names