Touch up some doxygen comments and copyrights.
* eltlparse/public.hh, saba/saba.hh, tgba/tgbakvcomplement.hh, tgba/tgbasafracomplement.hh, tgbaalgos/eltl2tgba_lacim.cc, tgbaalgos/eltl2tgba_lacim.hh, tgbaalgos/ltl2taa.hh: Comment changes.
This commit is contained in:
parent
a4766f2f82
commit
dac0502706
8 changed files with 24 additions and 15 deletions
|
|
@ -1,3 +1,12 @@
|
||||||
|
2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
|
Touch up some doxygen comments and copyrights.
|
||||||
|
|
||||||
|
* eltlparse/public.hh, saba/saba.hh, tgba/tgbakvcomplement.hh,
|
||||||
|
tgba/tgbasafracomplement.hh, tgbaalgos/eltl2tgba_lacim.cc,
|
||||||
|
tgbaalgos/eltl2tgba_lacim.hh, tgbaalgos/ltl2taa.hh: Comment
|
||||||
|
changes.
|
||||||
|
|
||||||
2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
Add SCC pruning options to the CGI script.
|
Add SCC pruning options to the CGI script.
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,5 @@
|
||||||
// Copyright (C) 2003, 2004, 2005, 2006, 2008 Laboratoire
|
// Copyright (C) 2008, 2010 Laboratoire de Recherche et Développement
|
||||||
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
|
// de l'Epita (LRDE).
|
||||||
// Coopératifs (SRC), Université Pierre et Marie Curie.
|
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -46,7 +45,7 @@ namespace spot
|
||||||
|
|
||||||
namespace eltl
|
namespace eltl
|
||||||
{
|
{
|
||||||
/// \addtogroup eltl_io
|
/// \addtogroup ltl_io
|
||||||
/// @{
|
/// @{
|
||||||
|
|
||||||
typedef std::pair<std::string, std::string> spair;
|
typedef std::pair<std::string, std::string> spair;
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
// Copyright (C) 2009 Laboratoire de Recherche et Développement
|
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
|
||||||
// de l'Epita (LRDE).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -27,7 +27,7 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
/// \defgroup saba SABA (State-based Alternating Büchi Automata)
|
/// \defgroup saba SABA (State-based Alternating Büchi Automata)
|
||||||
///
|
///
|
||||||
/// Spot was centered around non-deterministic \ref tgba.
|
/// Spot was centered around non-deterministic \ref tgba.
|
||||||
/// Alternating automata are an extension to non-deterministic
|
/// Alternating automata are an extension to non-deterministic
|
||||||
|
|
@ -38,7 +38,7 @@ namespace spot
|
||||||
/// \addtogroup saba_essentials Essential SABA types
|
/// \addtogroup saba_essentials Essential SABA types
|
||||||
/// \ingroup saba
|
/// \ingroup saba
|
||||||
|
|
||||||
/// \brief A State-based Alternating (Generalized) Büchi Automaton.
|
/// \brief A State-based Alternating (Generalized) Büchi Automaton.
|
||||||
/// \ingroup saba_essentials
|
/// \ingroup saba_essentials
|
||||||
///
|
///
|
||||||
/// Browsing such automaton can be achieved using two functions:
|
/// Browsing such automaton can be achieved using two functions:
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
|
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
|
||||||
// de l'Epita (LRDE).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -62,11 +62,11 @@ namespace spot
|
||||||
typedef std::vector<bdd_ordered> acc_list_t;
|
typedef std::vector<bdd_ordered> acc_list_t;
|
||||||
|
|
||||||
/// \brief Build a complemented automaton.
|
/// \brief Build a complemented automaton.
|
||||||
/// \ingroup tgba
|
/// \ingroup tgba_on_the_fly_algorithms
|
||||||
///
|
///
|
||||||
/// The construction comes from:
|
/// The construction comes from:
|
||||||
/// @Article{ kupferman.05.tcs,
|
/// @Article{ kupferman.05.tcs,
|
||||||
/// title = {{From complementation to certification}},
|
/// title = {From complementation to certification},
|
||||||
/// author = {Kupferman, O. and Vardi, M.Y.},
|
/// author = {Kupferman, O. and Vardi, M.Y.},
|
||||||
/// journal = {Theoretical Computer Science},
|
/// journal = {Theoretical Computer Science},
|
||||||
/// volume = {345},
|
/// volume = {345},
|
||||||
|
|
|
||||||
|
|
@ -34,7 +34,7 @@ namespace spot
|
||||||
struct safra_tree_automaton;
|
struct safra_tree_automaton;
|
||||||
|
|
||||||
/// \brief Build a complemented automaton.
|
/// \brief Build a complemented automaton.
|
||||||
/// \ingroup tgba
|
/// \ingroup tgba_on_the_fly_algorithms
|
||||||
///
|
///
|
||||||
/// It creates an automaton that recognizes the
|
/// It creates an automaton that recognizes the
|
||||||
/// negated language of \a aut.
|
/// negated language of \a aut.
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
|
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
|
||||||
// de l'Epita (LRDE).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
// Copyright (C) 2008 Laboratoire de Recherche et Développement
|
// Copyright (C) 2008, 2010 Laboratoire de Recherche et Développement
|
||||||
// de l'Epita (LRDE).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -27,7 +27,7 @@
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
/// \brief Build a spot::tgba_bdd_concrete from an ELTL formula.
|
/// \brief Build a spot::tgba_bdd_concrete from an ELTL formula.
|
||||||
/// \ingroup tgba_eltl
|
/// \ingroup tgba_ltl
|
||||||
///
|
///
|
||||||
/// This is based on the following paper.
|
/// This is based on the following paper.
|
||||||
/// \verbatim
|
/// \verbatim
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
// Copyright (C) 2009 Laboratoire de Recherche et Développement
|
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
|
||||||
// de l'Epita (LRDE).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -27,6 +27,7 @@
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
/// \brief Build a spot::taa* from an LTL formula.
|
/// \brief Build a spot::taa* from an LTL formula.
|
||||||
|
/// \ingroup tgba_ltl
|
||||||
///
|
///
|
||||||
/// This is based on the following.
|
/// This is based on the following.
|
||||||
/// \verbatim
|
/// \verbatim
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue