mcrl2::pbes_system::lts_solve_structure_graph_algorithm

Include file:

#include "mcrl2/pbes/solve_structure_graph.h

class mcrl2::pbes_system::lts_solve_structure_graph_algorithm

Protected static member functions

static void create_counter_example_lts(structure_graph &G, const std::set<structure_graph::index_type> &V, lts::lts_lts_t &ltsspec)

static void filter_transitions(lts::lts_lts_t &ltsspec, const std::set<std::size_t> &transition_indices)

Public member functions

lts_solve_structure_graph_algorithm() = default

bool solve_with_counter_example(structure_graph &G, lts::lts_lts_t &ltsspec)

Solve a boolean equation system while generating a counter example.

Parameters:

• G A structure graph.
• ltsspec The original LTS that was used to create the PBES.