mcrl2::pbes_system::bisimulation_algorithm =============================================================================== Include file: .. code-block:: c++ #include "mcrl2/pbes/bisimulation.h .. cpp:class:: mcrl2::pbes_system::bisimulation_algorithm Base class for bisimulation algorithms. Public types ------------------------------------------------------------------------------- .. cpp:type:: mcrl2::pbes_system::bisimulation_algorithm::my_iterator typedef for :cpp:type:`lps::action_summand_vector::const_iterator` The iterator type for non-delta summands. Protected types ------------------------------------------------------------------------------- .. cpp:type:: mcrl2::pbes_system::bisimulation_algorithm::name_map typedef for :cpp:type:`std::map\< const lps::action_summand *, std::string >` A map type for mapping summands to strings. Protected attributes ------------------------------------------------------------------------------- .. cpp:member:: const lps::linear_process * mcrl2::pbes_system::bisimulation_algorithm::model_ptr Store the address of the model. .. cpp:member:: name_map mcrl2::pbes_system::bisimulation_algorithm::summand_names Maps summands to strings. Protected member functions ------------------------------------------------------------------------------- .. cpp:function:: std::string action_list_name(const process::action_list &l) const Generates a name for an action_list. **Parameters:** * **l** A sequence of actions **Returns:** A string representation of the list l .. cpp:function:: bool is_from_model(const lps::linear_process &p) const 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. .. cpp:function:: void make_substitution(const data::variable_list &v, const data::data_expression_list &e, data::mutable_map_substitution<> &result) const .. cpp:function:: std::string process_name(const lps::linear_process &p) const Returns a name of a linear process. **Parameters:** * **p** A linear process **Returns:** The name of the linear process. .. cpp:function:: void set_summand_names(const lps::linear_process &p) Used for initializing summand names. **Parameters:** * **p** A linear process .. cpp:function:: std::string summand_name(my_iterator i) const Returns the name of a summand. **Parameters:** * **i** A summand iterator **Returns:** The name of the summand referred to by i Public member functions ------------------------------------------------------------------------------- .. cpp:function:: pbes build_pbes(const std::vector< pbes_equation > &equations, const lps::specification &M, const lps::specification &S) Builds a pbes from the given equations. **Parameters:** * **equations** A sequence of pbes equations * **M** A specification * **S** A specification **Returns:** The constructed pbes .. cpp:function:: 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. **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(). .. cpp:function:: 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. **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. .. cpp:function:: 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. **Parameters:** * **a** A sequence of actions * **b** A sequence of actions **Returns:** Necessary conditions for the equality of a and b .. cpp:function:: void init(const lps::linear_process &model, const lps::linear_process &spec) Initializes the name lookup table. **Parameters:** * **model** A linear process * **spec** A linear process **Pre:** model and spec must have the same data specification .. cpp:function:: fixpoint_symbol mu() const Returns the fixpoint symbol mu. **Returns:** The fixpoint symbol mu. .. cpp:function:: fixpoint_symbol nu() const Returns the fixpoint symbol nu. **Returns:** The fixpoint symbol nu. .. cpp:function:: void resolve_name_clashes(const lps::specification &model, lps::specification &spec, bool include_summand_variables=false) Resolves name clashes between model and spec. .. cpp:function:: propositional_variable_instantiation var(const core::identifier_string &name, const data::data_expression_list ¶meters) const Creates a propositional variable. **Parameters:** * **name** A * **parameters** A sequence of data expressions **Returns:** The created propositional variable .. cpp:function:: propositional_variable_instantiation var(const core::identifier_string &name, const data::variable_list ¶meters) const Creates a propositional variable. **Parameters:** * **name** A * **parameters** A sequence of data variables **Returns:** The created propositional variable .. cpp:function:: core::identifier_string X(const lps::linear_process &p, const lps::linear_process &q) const 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 .. cpp:function:: core::identifier_string Y(const lps::linear_process &p, const lps::linear_process &q) const 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 .. cpp:function:: 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. **Pre:** 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 .. cpp:function:: 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. **Pre:** 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 .. cpp:function:: 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. **Pre:** 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