mcrl2::pbes_system::lps_solve_structure_graph_algorithm
===============================================================================


Include file:

.. code-block:: c++

   #include "mcrl2/pbes/solve_structure_graph.h

.. cpp:class:: mcrl2::pbes_system::lps_solve_structure_graph_algorithm

  

  

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

.. cpp:function:: static lps::specification create_counter_example_lps(structure_graph &G, const std::set< structure_graph::index_type > &V, const lps::specification &lpsspec, const pbes &p, const pbes_equation_index &p_index)
  
  

  

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

.. cpp:function:: lps_solve_structure_graph_algorithm()=default
  
  

  

.. cpp:function:: std::pair<bool, lps::specification> solve_with_counter_example(structure_graph &G, const lps::specification &lpsspec, const pbes &p, const pbes_equation_index &p_index)
  
  Solve a pbes for some equation, while constructing a counter example or wittness based on the accompanying linear process. 

  
  
  **Parameters:**

  * **G** A structure graph. 

  * **lpsspec** The original LPS that was used to create the PBES. 

  * **p** The pbes to be solved. 

  * **p_index** The index of the pbes equation to be solved. 


      
  **Returns:** A boolean indicating the solution and a linear process that represents the counter example.