mcrl2::pbes_system::lps2pbes_algorithm
===============================================================================


Include file:

.. code-block:: c++

   #include "mcrl2/pbes/lps2pbes.h

.. cpp:class:: mcrl2::pbes_system::lps2pbes_algorithm

  Algorithm for translating a state formula and a timed specification to a pbes. 

  

Protected attributes
-------------------------------------------------------------------------------

.. cpp:member:: bool mcrl2::pbes_system::lps2pbes_algorithm::m_check_only
  
  

  

.. cpp:member:: data::set_identifier_generator mcrl2::pbes_system::lps2pbes_algorithm::m_generator
  
  

  

Protected member functions
-------------------------------------------------------------------------------

.. cpp:function:: void run(const state_formulas::state_formula &f, bool structured, bool unoptimized, std::vector< pbes_equation > &equations, Parameters &parameters)
  
  

  

Public member functions
-------------------------------------------------------------------------------

.. cpp:function:: lps2pbes_algorithm(bool check_only=false)
  
  Constructor. 

  

.. cpp:function:: pbes run(const state_formulas::state_formula &formula, const lps::specification &lpsspec, bool structured=false, bool unoptimized=false, bool preprocess_modal_operators=false, bool generate_counter_example=false, const data::variable &T=data::undefined_real_variable())
  
  Runs the translation algorithm. 

  
  
  **Parameters:**

  * **formula** A modal formula that represents a property about the system modeled by the given specification 

  * **lpsspec** A linear process specification 

  * **structured** use the 'structured' approach of generating equations 

  * **unoptimized** do not optimize the resulting PBES. 

  * **preprocess_modal_operators** insert dummy fixpoints in modal operators, which may lead to smaller PBESs 

  * **generate_counter_example** If true, then the PBES is enhanced with additional equations that are used to extract a counter example. 

  * **T** The time parameter. If T == data::variable() the untimed version of lps2pbes is applied. 


      
  **Returns:** A PBES that encodes the property applied to the given specification