diff --git a/ChangeLog b/ChangeLog index c74ecd67a..77ce38e7c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2011-02-21 Alexandre Duret-Lutz + + * src/tgba/bdddict.hh: Add more documentation. + 2011-02-21 Alexandre Duret-Lutz * src/misc/escape.hh: Correct documentation. diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh index 434d77703..70528d863 100644 --- a/src/tgba/bdddict.hh +++ b/src/tgba/bdddict.hh @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement 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 // et Marie Curie. @@ -33,8 +35,15 @@ namespace spot { - /// Map BDD variables to formulae. /// \ingroup tgba_essentials + /// \brief Map BDD variables to formulae. + /// + /// The BDD library uses integers to designate Boolean variables in + /// its decision diagrams. This class is used to map such integers + /// to objects actually used in Spot. These objects are usually + /// atomic propositions, but they can also be acceptance conditions, + /// or "Now/Next" variables (although the latter should be + /// eventually removed). class bdd_dict: public bdd_allocator { public: