Emptiness-checks

Modules
	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
	Shared pointer to emptiness_check_result.
typedef std::shared_ptr< emptiness_check >	spot::emptiness_check_ptr
	Shared pointer to emptiness_check.
typedef std::shared_ptr< emptiness_check_instantiator >	spot::emptiness_check_instantiator_ptr
	Shared pointer to emptiness_check_instantiator.

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 Emptiness-check algorithms), or indirectly via 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 the properties of the emptiness check selected.

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

If 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 find the automaton to be empty even if it is not actually empty.)

When emptiness_check::check() does not return 0, it returns an instance of emptiness_check_result. You can try to call emptiness_check_result::accepting_run() to obtain an accepting run. For some emptiness-check algorithms, 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 emptiness_check_result::accepting_run() can return 0 (this does not mean in any way that no accepting run exists).

The acceptance run returned by emptiness_check_result::accepting_run(), if any, is of type twa_run. See TωA runs and supporting functions for existing operations on these objects.

Typedef Documentation

emptiness_check_instantiator_ptr

typedef std::shared_ptr<emptiness_check_instantiator> spot::emptiness_check_instantiator_ptr

#include <spot/twaalgos/emptiness.hh>

Shared pointer to emptiness_check_instantiator.

emptiness_check_ptr

typedef std::shared_ptr<emptiness_check> spot::emptiness_check_ptr

#include <spot/twaalgos/emptiness.hh>

Shared pointer to emptiness_check.

emptiness_check_result_ptr

typedef std::shared_ptr<emptiness_check_result> spot::emptiness_check_result_ptr

#include <spot/twaalgos/emptiness.hh>

Shared pointer to emptiness_check_result.

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)".
err	on error, *err is set to point to the problematic part of name: if the algorithm name was unknown, *err is set to name; if some option fragment could not be parsed, *err points to that fragment.

Returns

Return an emptiness-check instantiator. On error, the function returns nullptr.

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)