Include file:

#include "mcrl2/pbes/solve_structure_graph.h
class mcrl2::pbes_system::lps_solve_structure_graph_algorithm

Protected static member functions

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

lps_solve_structure_graph_algorithm() = default
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.


  • 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.