Inheritance diagram for mcrl2::pbes_system::lps_solve_structure_graph_algorithm:

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.

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 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)

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 504 of file solve_structure_graph.h.

Constructor & Destructor Documentation

mcrl2::pbes_system::lps_solve_structure_graph_algorithm::lps_solve_structure_graph_algorithm ( )

default

static lps::specification mcrl2::pbes_system::lps_solve_structure_graph_algorithm::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
	)

inlinestaticprotected

Definition at line 507 of file solve_structure_graph.h.

std::pair< bool, lps::specification > mcrl2::pbes_system::lps_solve_structure_graph_algorithm::solve_with_counter_example	(	structure_graph &	G,
		const lps::specification &	lpsspec,
		const pbes &	p,
		const pbes_equation_index &	p_index
	)

inline

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.

Definition at line 561 of file solve_structure_graph.h.

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