The result of the language inclusion test. More...

#include <results.h>

Public Member Functions
void	filter_trace (std::function< bool(Symbol)> to_remove)
	Filters the result trace. More...

void	print_long (std::ostream &stream, const printer_base< Symbol > &symbol_printer)
	Print this result. More...

Public Attributes
bool	included = false
	True if automaton A is included in automaton B. More...

bool	bound_hit = false
	Was the bound hit during automata exploration. More...

std::vector< Symbol >	counter_example
	A counter-example if applicable. More...

unsigned	max_bound = 0
	The maximum bound used to obtain this inclusion result. More...

Detailed Description

template<class Symbol>
struct Limi::inclusion_result< Symbol >

The result of the language inclusion test.

Member Function Documentation

template<class Symbol>

void Limi::inclusion_result< Symbol >::filter_trace ( std::function< bool(Symbol)> to_remove )

inline

Filters the result trace.

This is used to remove symbols from the trace that are not of interest. Does nothing if the inclusion result is true.

Parameters

to_remove A function that returns true if a symbol should be filtered out (removed) from the trace.

template<class Symbol>

void Limi::inclusion_result< Symbol >::print_long	(	std::ostream &	stream,
		const printer_base< Symbol > &	symbol_printer
	)

inline

Print this result.

Parameters

stream	The stream to print to.
symbol_printer	The printer to print out the counter-example if any.

Member Data Documentation

template<class Symbol>

bool Limi::inclusion_result< Symbol >::bound_hit = false

Was the bound hit during automata exploration.

If the bound was hit then a false-negative result may be returned. This means that if bound_hit is true and included is false further checks are needed. See the timbuk example to understand how to proceed in that case.

template<class Symbol>

std::vector<Symbol> Limi::inclusion_result< Symbol >::counter_example

A counter-example if applicable.

Only used by Limi::antichain_algo_ind

Only if included is false. The vector represents a word accepted by A and not accepted by B up to bounded independence.

template<class Symbol>

bool Limi::inclusion_result< Symbol >::included = false

True if automaton A is included in automaton B.

A result true can always be trusted. A negative result can be false-negative if bound_hit is true.

template<class Symbol>

unsigned Limi::inclusion_result< Symbol >::max_bound = 0

The maximum bound used to obtain this inclusion result.