mcrl2::pbes_system::lts2pbes_algorithm
===============================================================================


Include file:

.. code-block:: c++

   #include "mcrl2/pbes/lts2pbes.h

.. cpp:class:: mcrl2::pbes_system::lts2pbes_algorithm

  Algorithm for translating a state formula and an untimed specification to a pbes. 

  

Public types
-------------------------------------------------------------------------------

.. cpp:type:: mcrl2::pbes_system::lts2pbes_algorithm::edge_list

  typedef for :cpp:type:`pbes_system::detail::lts2pbes_lts::edge_list`
  
  

  

.. cpp:type:: mcrl2::pbes_system::lts2pbes_algorithm::state_type

  typedef for :cpp:type:`lts::lts_lts_t::states_size_type`
  
  

  

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

.. cpp:member:: const lts::lts_lts_t & mcrl2::pbes_system::lts2pbes_algorithm::lts0
  
  

  

.. cpp:member:: pbes_system::detail::lts2pbes_lts mcrl2::pbes_system::lts2pbes_algorithm::lts1
  
  

  

.. cpp:member:: data::set_identifier_generator mcrl2::pbes_system::lts2pbes_algorithm::m_id_generator
  
  

  

.. cpp:member:: utilities::progress_meter mcrl2::pbes_system::lts2pbes_algorithm::m_progress_meter
  
  

  

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

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

  

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

.. cpp:function:: lts2pbes_algorithm(const lts::lts_lts_t &l)
  
  Constructor. 

  

.. cpp:function:: pbes run(const state_formulas::state_formula_specification &formspec, bool preprocess_modal_operators=false, bool generate_counter_example=false)
  
  Runs the translation algorithm. 

  
  
  **Parameters:**

  * **formspec** A state formula specification. 

  * **preprocess_modal_operators** A boolean indicating that the modal operators can be preprocessed 

  * **generate_counter_example** A boolean indicating whether a counterexample must be generated. 


      
  **Returns:** The result of the translation