Algorithm class for strong bisimulation. More...

#include <bisimulation.h>

Inheritance diagram for mcrl2::pbes_system::strong_bisimulation_algorithm:

Public Member Functions
pbes_expression	match (const lps::linear_process &p, const lps::linear_process &q) const
	The match function.

pbes_expression	step (const lps::linear_process &p, const lps::linear_process &q, my_iterator i) const
	The step function.

pbes	run (const lps::specification &model, const lps::specification &spec)
	Runs the algorithm.

Public Member Functions inherited from mcrl2::pbes_system::bisimulation_algorithm
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.

Additional Inherited Members
Public Types inherited from mcrl2::pbes_system::bisimulation_algorithm
using	my_iterator = lps::action_summand_vector::const_iterator
	The iterator type for non-delta summands.

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

Protected Member Functions inherited from mcrl2::pbes_system::bisimulation_algorithm
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 inherited from mcrl2::pbes_system::bisimulation_algorithm
name_map	summand_names
	Maps summands to strings.

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

Detailed Description

Algorithm class for strong bisimulation.

Definition at line 527 of file bisimulation.h.

Member Function Documentation

◆ match()

pbes_expression mcrl2::pbes_system::strong_bisimulation_algorithm::match	(	const lps::linear_process &	p,
		const lps::linear_process &	q
	)		const

inline

The match function.

Parameters

p	A linear process
q	A linear process

Returns: The function result

Definition at line 534 of file bisimulation.h.

◆ run()

pbes mcrl2::pbes_system::strong_bisimulation_algorithm::run	(	const lps::specification &	model,
		const lps::specification &	spec
	)

inline

Runs the algorithm.

Parameters

model	A linear process specification
spec	A linear process specification

Returns: A pbes that expresses strong bisimulation between stwo specifications.

Definition at line 579 of file bisimulation.h.

◆ step()

pbes_expression mcrl2::pbes_system::strong_bisimulation_algorithm::step	(	const lps::linear_process &	p,
		const lps::linear_process &	q,
		my_iterator	i
	)		const

inline

The step function.

Parameters

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

Returns: The function result

Definition at line 554 of file bisimulation.h.

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

pbes/include/mcrl2/pbes/bisimulation.h

Public Member Functions

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ match()

◆ run()

◆ step()