Commit 543de077 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Improve some Doxygen comments.

This follows up on a mail from Sonali Dutta.

* src/tgba/bdddict.hh (assert_emptiness, ~bdd_dict): Better
documentation.
* src/tgba/formula2bdd.hh (formula_to_bdd): Mention
unregister_all_my_variables().
(bdd_to_formula): Complete the documentation.
* THANKS: Add Sonali Dutta.
parent 370f3296
......@@ -15,5 +15,6 @@ Michael Weber
Nikos Gorogiannis
Rüdiger Ehlers
Silien Hong
Sonali Dutta
Tomáš Babiak
Yann Thierry-Mieg
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
......@@ -44,11 +44,25 @@ namespace spot
/// atomic propositions, but they can also be acceptance conditions,
/// or "Now/Next" variables (although the latter should be
/// eventually removed).
///
/// When a BDD variable is registered using a bdd_dict, it is always
/// associated to a "user" (or "owner") object. This is done by
/// supplying the bdd_dict with a pointer to the intended user of
/// the variable. When the user object dies, it should release the
/// BDD variables it was using by calling (for instance)
/// unregister_all_my_variables(), giving the same pointer.
/// Variables can also by unregistered one by one using
/// unregister_variable().
class bdd_dict: public bdd_allocator
{
public:
bdd_dict();
/// \brief Destroy the BDD dict.
///
/// This always calls assert_emptiness() to diagnose cases where
/// variables have not been unregistered.
~bdd_dict();
/// Formula-to-BDD-variable maps.
......@@ -206,8 +220,15 @@ namespace spot
/// \brief Make sure the dictionary is empty.
///
/// This will print diagnostics and abort if the dictionary
/// is not empty. Use for debugging.
/// This will print diagnostics if the dictionary is not empty.
/// Use for debugging. This is called automatically by the
/// destructor. When Spot is compiled in development mode (i.e.,
/// with <code>./configure --enable-devel</code>), this function
/// will abort if the dictionary is not empty.
///
/// The errors detected by this function usually indicate missing
/// calls to unregister_variable() or
/// unregister_all_my_variables().
void assert_emptiness() const;
protected:
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement de
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
......@@ -28,14 +28,27 @@
namespace spot
{
/// \brief Convert a formula into a BDD.
/// \brief Convert a Boolean formula into a BDD.
///
/// Convert formula \a f into a Bdd, using existing variables from \a
/// d, and registering new one as necessary. \a for_me is the
/// address to use as owner of the variables used in the BDD.
/// Convert the Boolean formula \a f into a BDD, using existing
/// variables from \a d, and registering new ones as necessary. \a
/// for_me, the address of the user of these BDD variables will be
/// passed to \a d when registering the variables.
///
/// If you only use the BDD representation temporarily, for instance
/// passing it right away to bdd_to_formula(), you should not forget
/// to unregister the variables that have been registered for \a
/// for_me. See bdd_dict::unregister_all_my_variables().
bdd formula_to_bdd(const ltl::formula* f, bdd_dict* d, void* for_me);
/// Convert a BDD into a formula.
/// \brief Convert a BDD into a formula.
///
/// Format the BDD as an irredundant sum of product (see the
/// minato_isop class for details) and map the BDD variables back
/// into their atomic propositions. This works only for Boolean
/// formulas, and all the BDD variables used in \a f should have
/// been registered in \a d. Although the result has type
/// ltl::formula*, it obviously does not use any temporal operator.
const ltl::formula* bdd_to_formula(bdd f, const bdd_dict* d);
}
......
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