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 &parameters) 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 &parameters) 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