Inheritance diagram for mcrl2::pbes_system::lts_solve_structure_graph_algorithm:

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.

Public Member Functions inherited from mcrl2::pbes_system::solve_structure_graph_algorithm
std::pair< vertex_set, vertex_set >	solve_recursive (structure_graph &G, const vertex_set &A, std::size_t &calculation_steps)

	solve_structure_graph_algorithm (bool check_strategy_=false, bool use_toms_optimization_=false)

bool	solve (structure_graph &G, std::size_t &calculation_steps)
	Returns the winning player (alpha)

bool	solve (structure_graph &G)

std::pair< vertex_set, vertex_set >	solve_partitions (structure_graph &G, std::size_t &calculation_steps)
	Returns the winning partition.

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

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

Static Protected Member Functions inherited from mcrl2::pbes_system::solve_structure_graph_algorithm
static structure_graph::index_type	succ (const structure_graph &G, structure_graph::index_type u)

static structure_graph::index_type	succ (const structure_graph &G, structure_graph::index_type u, const vertex_set &U)

static void	insert_edge (structure_graph::vertex_vector &V, structure_graph::index_type ui, structure_graph::index_type vi)

Additional Inherited Members
Protected Member Functions inherited from mcrl2::pbes_system::solve_structure_graph_algorithm
std::pair< vertex_set, vertex_set >	solve_recursive (structure_graph &G, std::size_t &calculation_steps)

std::pair< vertex_set, vertex_set >	solve_recursive_extended (structure_graph &G, std::size_t &calculation_steps)

void	check_solve_recursive_solution (const structure_graph &G, bool is_disjunctive, const vertex_set &Wdisj, const vertex_set &Wconj, std::size_t &calculation_steps)

std::pair< bool, std::set< structure_graph::index_type > >	extract_evidence (structure_graph &G)

Protected Attributes inherited from mcrl2::pbes_system::solve_structure_graph_algorithm
bool	check_strategy = false

bool	use_toms_optimization = false

Detailed Description

Definition at line 577 of file solve_structure_graph.h.

Constructor & Destructor Documentation

mcrl2::pbes_system::lts_solve_structure_graph_algorithm::lts_solve_structure_graph_algorithm ( )

default

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

inlinestaticprotected

Definition at line 604 of file solve_structure_graph.h.

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

inlinestaticprotected

Definition at line 583 of file solve_structure_graph.h.

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

inline

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.

Definition at line 637 of file solve_structure_graph.h.

The documentation for this class was generated from the following file: