Commit 370ac51b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

docyment make_emptiness_check_instantiator()

Fixes #161, reported by Yann Thierry-Mieg.

* spot/twaalgos/emptiness.hh: Here.
* NEWS: Mention it.
parent adb99869
New in spot 2.0.0a (not yet released)
Documentation:
* Add missing documentation for the option string passed to
spot::make_emptiness_check_instantiator().
Bug fixes:
* Typo in documentation of the -H option in --help output.
......
......@@ -39,11 +39,18 @@ namespace spot
/// \addtogroup emptiness_check Emptiness-checks
/// \ingroup twa_algorithms
///
/// You can create an emptiness check either by instantiating it
/// explicitly (calling one of the functions of \ref
/// emptiness_check_algorithms "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 (by instantiating a subclass, or calling a
/// functions construct such instance; see \ref
/// emptiness_check_algorithms "this list"), you should call
/// spot::emptiness_check, you should call
/// spot::emptiness_check::check() to check the automaton.
///
/// If spot::emptiness_check::check() returns 0, then the automaton
......@@ -202,7 +209,7 @@ namespace spot
typedef std::shared_ptr<emptiness_check_instantiator>
emptiness_check_instantiator_ptr;
// Dynamically create emptiness checks. Given their name and options.
/// Dynamically create emptiness checks. Given their name and options.
class SPOT_API emptiness_check_instantiator
{
public:
......@@ -239,20 +246,123 @@ namespace spot
option_map o_;
void *info_;
};
/// @}
/// \brief Create an emptiness-check instantiator, given the name
/// of an emptiness check.
///
/// \a name should have the form \c "name" or \c "name(options)".
/// This is a convenient entry point to instantiate an emptiness
/// check with user-supplied options.
///
/// \param name should have the form \c "name" or \c "name(options)".
///
/// On error, the function returns 0. If the name of the algorithm
/// was unknown, \c *err will be set to \c name. If some fragment of
/// \return Return an emptiness-check instantiator. On error, the
/// function returns \c nullptr. If the name of the algorithm was
/// unknown, \c *err will be set to \c name. If some fragment of
/// the options could not be parsed, \c *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:
/// \code
/// Cou99
/// Cou99(shy !group)
/// Cou99(shy group)
/// Cou99(poprem)
/// Cou99(poprem shy !group)
/// Cou99(poprem shy group)
/// \endcode
///
/// - `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:
/// \code
/// GC04
/// \endcode
///
/// - `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:
/// \code
/// CVWY90
/// CVWY90(bsh=4M)
/// \endcode
///
/// - `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:
/// \code
/// SE05
/// SE05(bsh=4M)
/// \endcode
///
/// - `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:
/// \code
/// Tau03
/// \endcode
///
/// - `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:
/// \code
/// Tau03_opt
/// Tau03_opt(!weights)
/// Tau03_opt(!redweights)
/// Tau03_opt(condstack)
/// Tau03_opt(condstack !weights)
/// Tau03_opt(condstack !redweights)
/// \endcode
SPOT_API emptiness_check_instantiator_ptr
make_emptiness_check_instantiator(const char* name, const char** err);
/// @}
/// \addtogroup emptiness_check_algorithms Emptiness-check algorithms
/// \ingroup emptiness_check
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment