Limi::antichain_algo_ind< ImplementationA, InnerImplementationB, Independence > Class Template Reference

The antichain algorithm compares two automata for language inclusion module an independence relation. More...

#include <antichain_algo_ind.h>

Public Member Functions
	antichain_algo_ind (const AutomatonA &a, const InnerAutomatonB &ib, unsigned initial_bound=2, const Independence &independence=Independence())
	Constructor that initialises the language inclusion algorithm. More...
unsigned	get_bound ()
	Returns the current bound.
void	increase_bound (unsigned new_bound)
	Incleases the bound of the language inclusion check. More...
inclusion_result< Symbol >	run ()
	Run the language inclusion. More...

Detailed Description

template<class ImplementationA, class InnerImplementationB, class Independence = independence<typename ImplementationA::Symbol_>>
class Limi::antichain_algo_ind< ImplementationA, InnerImplementationB, Independence >

The antichain algorithm compares two automata for language inclusion module an independence relation.

Language inclusion up to an independence relation is undecidable in general. Therefore this class implements a bounded version where a stack is used to match symbols that may occure in the future. For low stack sizes the algorithm works faster but may produce spurious counter-examples. The bound can be increased to eliminate those. See the main file in the timbuk example to see how to deal with spurious counter-examples.

The class already accepts the automata as constructor arguments and therefore cannot be reused for more than one language inclusion query. The run() function runs until a counter-example is produced. This counter-example can be spurious though. Run can be called again to produce another counter-example. In addition increase_bound() can be called to increase the bound. A subsequent call to the run() function will yield a counter-example for the higher bound. This process is incremental.

Template Parameters

ImplementationA	The implementation class of Automaton A
InnerImplementationB	The implementation class of Automaton B
Independence	The independence relation (defaults to Limi::independence). Instead of giving an empty independence relation (where nothing is independent) it would be more efficient to use the class Limi::antichain_algo.

Constructor & Destructor Documentation

template<class ImplementationA , class InnerImplementationB , class Independence = independence<typename ImplementationA::Symbol_>>

Limi::antichain_algo_ind< ImplementationA, InnerImplementationB, Independence >::antichain_algo_ind ( const AutomatonA &  a, const InnerAutomatonB &  ib, unsigned  initial_bound = 2, const Independence &  independence = Independence()  )

inline

Constructor that initialises the language inclusion algorithm.

Parameters

a	The automaton a
ib	The automaton b
initial_bound	The starting bound
independence	The independence (if there is no default constructor)

Member Function Documentation

template<class ImplementationA , class InnerImplementationB , class Independence = independence<typename ImplementationA::Symbol_>>

void Limi::antichain_algo_ind< ImplementationA, InnerImplementationB, Independence >::increase_bound ( unsigned  new_bound )

inline

Incleases the bound of the language inclusion check.

This causes a partial restart of the language inclusion check the next time run() is called and run may find the same counter-example again.

template<class ImplementationA , class InnerImplementationB , class Independence = independence<typename ImplementationA::Symbol_>>

inclusion_result<Symbol> Limi::antichain_algo_ind< ImplementationA, InnerImplementationB, Independence >::run ( )

inline

Run the language inclusion.

Can be called several time to obtain several counter-examples.

Returns

Language inclusion result and a counter-example trace (if applicable)

---

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

• Limi/antichain_algo_ind.h