From cc9c08b6cf5437313bd4092d6a0d5988c6e53f7d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Feb 2008 09:22:19 +0000 Subject: [PATCH] * src/tgba/tgbabddconcretefactory.hh (create_state): Clarify comments. --- ChangeLog | 5 +++++ src/tgba/tgbabddconcretefactory.hh | 13 +++++++------ 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/ChangeLog b/ChangeLog index d96946bf6..e5dc67cee 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2008-02-22 Alexandre Duret-Lutz + + * src/tgba/tgbabddconcretefactory.hh (create_state): + Clarify comments. + 2008-02-01 Alexandre Duret-Lutz * src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::dump_queue): diff --git a/src/tgba/tgbabddconcretefactory.hh b/src/tgba/tgbabddconcretefactory.hh index 969102725..a2c987e30 100644 --- a/src/tgba/tgbabddconcretefactory.hh +++ b/src/tgba/tgbabddconcretefactory.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -36,14 +36,15 @@ namespace spot virtual ~tgba_bdd_concrete_factory(); - /// Create a state variable for formula \a f. + /// Create a Now/Next variables for formula \a f. /// /// \param f The formula to create a state for. - /// \return The variable number for this state. + /// \return The BDD variable number v for the Now state. The + /// Next BDD corresponds to v+1. /// - /// The state is not created if it already exists. Instead its - /// existing variable number is returned. Variable numbers - /// can be turned into BDD using ithvar(). + /// The state variables are not created if they already exist. + /// Instead their existing variable numbers are returned. + /// Variable numbers can be turned into BDD using ithvar(). int create_state(const ltl::formula* f); /// Create an atomic proposition variable for formula \a f.