mcrl2::pbes_system::branching_simulation_equivalence_algorithm Class Reference

Algorithm class for branching simulation equivalence. More...

#include <bisimulation.h>

Inheritance diagram for mcrl2::pbes_system::branching_simulation_equivalence_algorithm:

Public Member Functions
pbes	run (const lps::specification &model, const lps::specification &spec)
	Runs the algorithm.
Public Member Functions inherited from mcrl2::pbes_system::branching_bisimulation_algorithm
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_expression	close (const lps::linear_process &p, const lps::linear_process &q, my_iterator i) const
	The close function.
pbes	run (const lps::specification &model, const lps::specification &spec)
	Returns a pbes that expresses branching bisimulation between two specifications.
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 branching simulation equivalence.

Definition at line 839 of file bisimulation.h.

Member Function Documentation

run()

pbes mcrl2::pbes_system::branching_simulation_equivalence_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 branching simulation equivalence between two specifications.

Definition at line 846 of file bisimulation.h.

---

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

• pbes/include/mcrl2/pbes/bisimulation.h