Emptiness-checks

Topics
	Emptiness-check algorithms
	TωA runs and supporting functions
	Emptiness-check statistics

Classes
class	spot::emptiness_check_result
	The result of an emptiness check. More...
class	spot::emptiness_check
	Common interface to emptiness check algorithms. More...
class	spot::emptiness_check_instantiator
	Dynamically create emptiness checks. Given their name and options. More...

Typedefs
typedef std::shared_ptr< emptiness_check_result >	spot::emptiness_check_result_ptr
typedef std::shared_ptr< emptiness_check >	spot::emptiness_check_ptr
typedef std::shared_ptr< emptiness_check_instantiator >	spot::emptiness_check_instantiator_ptr

Functions
emptiness_check_instantiator_ptr	spot::make_emptiness_check_instantiator (const char *name, const char **err)
	Create an emptiness-check instantiator, given the name of an emptiness check.

Detailed Description

You can create an emptiness check either by instantiating it explicitly (calling one of the functions of this list), or indirectly via spot::make_emptiness_check_instantiator(). The latter function allows user-options to influence the choice of the emptiness-check algorithm used, and the intermediate instantiator object can be used to query to properties of the emptiness check selected.

All emptiness-check algorithms follow the same interface. Basically once you have constructed an instance of spot::emptiness_check, you should call spot::emptiness_check::check() to check the automaton.

If spot::emptiness_check::check() returns 0, then the automaton was found empty. Otherwise the automaton accepts some run. (Beware that some algorithms—those using bit-state hashing—may found the automaton to be empty even if it is not actually empty.)

When spot::emptiness_check::check() does not return 0, it returns an instance of spot::emptiness_check_result. You can try to call spot::emptiness_check_result::accepting_run() to obtain an accepting run. For some emptiness-check algorithms, spot::emptiness_check_result::accepting_run() will require some extra computation. Most emptiness-check algorithms are able to return such an accepting run, however this is not mandatory and spot::emptiness_check_result::accepting_run() can return 0 (this does not means by anyway that no accepting run exist).

The acceptance run returned by spot::emptiness_check_result::accepting_run(), if any, is of type spot::twa_run. This page gathers existing operations on these objects.

Function Documentation

make_emptiness_check_instantiator()

emptiness_check_instantiator_ptr spot::make_emptiness_check_instantiator	(	const char *	name,
		const char **	err )

#include <spot/twaalgos/emptiness.hh>

Create an emptiness-check instantiator, given the name of an emptiness check.

This is a convenient entry point to instantiate an emptiness check with user-supplied options.

Parameters

name	should have the form "name" or "name(options)".

Returns

Return an emptiness-check instantiator. On error, the function returns nullptr. If the name of the algorithm was unknown, *err will be set to name. If some fragment of the options could not be parsed, *err will point to that fragment.

The following names supported and correspond to different emptiness check algorithms:

• Cou99 uses spot::couvreur99(), that works with Fin-less acceptance conditions, with any number of acceptance sets. The following options can be used:

  • shy Compute all successors of each state, then explore already visited states first. This usually helps to merge SCCs, and thus exit sooner. However because all successors have to be computed and stored, it often consume more memory.
  • group Setting this option is meaningful only when shy is used. If set (the default), the successors of all the states that belong to the same SCC will be considered when choosing a successor. Otherwise, only the successor of the topmost state on the DFS stack are considered.
  • poprem Specifies how the algorithm should handle the destruction of non-accepting maximal strongly connected components. If poprem is set, the algorithm will keep a list of all states of a SCC that are fully processed and should be removed once the MSCC is popped. If poprem is unset (the default), the MSCC will be traversed again (i.e. generating the successors of the root recursively) for deletion. This is a choice between memory and speed.

  Examples:

  Cou99
  Cou99(shy !group)
  Cou99(shy group)
  Cou99(poprem)
  Cou99(poprem shy !group)
  Cou99(poprem shy group)

• GC04 uses spot::explicit_gv04_check() and works on automata with Fin-less acceptance conditions using at most one acceptance set. No options are supported.

  Example:

  GC04

• CVWY90 uses spot::magic_search() and work on automata with Fin-less acceptance conditions using at most one acceptance set. Set option bsh to the size of a hash-table if you want to activate bit-state hashing.

  Examples:

  CVWY90
  CVWY90(bsh=4M)

• SE05 uses spot::se05() and works on work on automata with Fin-less acceptance conditions using at most one acceptance set. Set option bsh to the size of a hash-table if you want to activate bit-state hashing.

  Examples:

  SE05
  SE05(bsh=4M)

• Tau03 uses spot::explicit_tau03_search() and work on automata with Fin-less acceptance conditions using at least one acceptance set. No options are supported.

  Example:

  Tau03

• Tau03_opt uses spot::explicit_tau03_opt_search() and work on automata with any Fin-less acceptance. The following options are supported:

  • weights This option is set by default and activates the usage of weights in the top-level DFS as well as in nested DFSs.
  • redweights This option is set by default, and activates the usage of weights in nested DFSs. It is meaningful only if weights is set.
  • condstack This option is unset by default, and activates the use of the "conditional stack" optimization described by Heikki Tauriainen.
  • ordering This option is unset by default, and activates the use of the "ordering" heuristic described by Heikki Tauriainen in Research Report A96 from the Helsinki University of Technology.

  Example:

  Tau03_opt
  Tau03_opt(!weights)
  Tau03_opt(!redweights)
  Tau03_opt(condstack)
  Tau03_opt(condstack !weights)
  Tau03_opt(condstack !redweights)