mcrl2::pbes_system::lps_solve_structure_graph_algorithm¶
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.
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.
