* src/tgba/tgba.hh, src/tgbaalgos/dotty.hh,
src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness.hh, src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/neverclaim.hh, src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh src/tgbaalgos/save.hh, src/tgbaalgos/stats.hh, src/tgbaparse/public.hh: Add Doxygen groups for TGBA algorithms.
This commit is contained in:
parent
36aadba740
commit
c3e399c837
20 changed files with 75 additions and 14 deletions
12
ChangeLog
12
ChangeLog
|
|
@ -1,5 +1,16 @@
|
||||||
2004-11-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
2004-11-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||||
|
|
||||||
|
* src/tgba/tgba.hh, src/tgbaalgos/dotty.hh,
|
||||||
|
src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh,
|
||||||
|
src/tgbaalgos/emptiness.hh, src/tgbaalgos/lbtt.hh,
|
||||||
|
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh,
|
||||||
|
src/tgbaalgos/neverclaim.hh, src/tgbaalgos/powerset.hh,
|
||||||
|
src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh,
|
||||||
|
src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.hh,
|
||||||
|
src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh
|
||||||
|
src/tgbaalgos/save.hh, src/tgbaalgos/stats.hh,
|
||||||
|
src/tgbaparse/public.hh: Add Doxygen groups for TGBA algorithms.
|
||||||
|
|
||||||
* src/ltlast/atomic_prop.hh, src/ltlast/binop.hh,
|
* src/ltlast/atomic_prop.hh, src/ltlast/binop.hh,
|
||||||
src/ltlast/constant.hh, src/ltlast/formula.hh,
|
src/ltlast/constant.hh, src/ltlast/formula.hh,
|
||||||
src/ltlast/multop.hh, src/ltlast/refformula.hh,
|
src/ltlast/multop.hh, src/ltlast/refformula.hh,
|
||||||
|
|
@ -13,7 +24,6 @@
|
||||||
groups for LTL algorithms and types.
|
groups for LTL algorithms and types.
|
||||||
* doc/Makefile.am (fast-doc): New target.
|
* doc/Makefile.am (fast-doc): New target.
|
||||||
|
|
||||||
|
|
||||||
* src/misc/hashfunc.hh: Include cstddef to define size_t, and guard
|
* src/misc/hashfunc.hh: Include cstddef to define size_t, and guard
|
||||||
the file for multiple inclusions.
|
the file for multiple inclusions.
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -218,11 +218,26 @@ namespace spot
|
||||||
/// \addtogroup tgba_representation TGBA representations
|
/// \addtogroup tgba_representation TGBA representations
|
||||||
/// \ingroup tgba
|
/// \ingroup tgba
|
||||||
|
|
||||||
/// \addtogroup tgba_on_the_fly_algorithms TGBA on-the-fly algorithms
|
|
||||||
/// \ingroup tgba
|
|
||||||
|
|
||||||
/// \addtogroup tgba_algorithms TGBA algorithms
|
/// \addtogroup tgba_algorithms TGBA algorithms
|
||||||
/// \ingroup tgba
|
/// \ingroup tgba
|
||||||
|
|
||||||
|
/// \addtogroup tgba_on_the_fly_algorithms TGBA on-the-fly algorithms
|
||||||
|
/// \ingroup tgba_algorithms
|
||||||
|
|
||||||
|
/// \addtogroup tgba_io Input/Output of TGBA
|
||||||
|
/// \ingroup tgba_algorithms
|
||||||
|
|
||||||
|
/// \addtogroup tgba_ltl Translating LTL formulae into TGBA
|
||||||
|
/// \ingroup tgba_algorithms
|
||||||
|
|
||||||
|
/// \addtogroup tgba_generic Algorithm patterns
|
||||||
|
/// \ingroup tgba_algorithms
|
||||||
|
|
||||||
|
/// \addtogroup tgba_reduction TGBA simplifications
|
||||||
|
/// \ingroup tgba_algorithms
|
||||||
|
|
||||||
|
/// \addtogroup tgba_misc Miscellaneous algorithms on TGBA
|
||||||
|
/// \ingroup tgba_algorithms
|
||||||
}
|
}
|
||||||
|
|
||||||
#endif // SPOT_TGBA_TGBA_HH
|
#endif // SPOT_TGBA_TGBA_HH
|
||||||
|
|
|
||||||
|
|
@ -30,6 +30,10 @@ namespace spot
|
||||||
class tgba;
|
class tgba;
|
||||||
|
|
||||||
/// \brief Print reachable states in dot format.
|
/// \brief Print reachable states in dot format.
|
||||||
|
/// \ingroup tgba_io
|
||||||
|
/// The \a dd argument allows to customize the output in various
|
||||||
|
/// ways. See \ref tgba_dotty "this page" for a list of available
|
||||||
|
/// decorators.
|
||||||
std::ostream&
|
std::ostream&
|
||||||
dotty_reachable(std::ostream& os,
|
dotty_reachable(std::ostream& os,
|
||||||
const tgba* g,
|
const tgba* g,
|
||||||
|
|
|
||||||
|
|
@ -30,7 +30,11 @@ namespace spot
|
||||||
class tgba;
|
class tgba;
|
||||||
class tgba_succ_iterator;
|
class tgba_succ_iterator;
|
||||||
|
|
||||||
/// Choose state and link styles for spot::dotty_reachable.
|
/// \addtogroup tgba_dotty Decorating the dot output
|
||||||
|
/// \ingroup tgba_io
|
||||||
|
|
||||||
|
/// \brief Choose state and link styles for spot::dotty_reachable.
|
||||||
|
/// \ingroup tgba_dotty
|
||||||
class dotty_decorator
|
class dotty_decorator
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||||
// et Marie Curie.
|
// et Marie Curie.
|
||||||
//
|
//
|
||||||
|
|
@ -26,11 +26,13 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
/// Build an explicit automata from all states of \a aut, numbering
|
/// \brief Build an explicit automata from all states of \a aut,
|
||||||
/// states in bread first order as they are processed.
|
/// numbering states in bread first order as they are processed.
|
||||||
|
/// \ingroup tgba_misc
|
||||||
tgba_explicit* tgba_dupexp_bfs(const tgba* aut);
|
tgba_explicit* tgba_dupexp_bfs(const tgba* aut);
|
||||||
/// Build an explicit automata from all states of \a aut, numbering
|
/// \brief Build an explicit automata from all states of \a aut,
|
||||||
/// states in depth first order as they are processed.
|
/// numbering states in depth first order as they are processed.
|
||||||
|
/// \ingroup tgba_misc
|
||||||
tgba_explicit* tgba_dupexp_dfs(const tgba* aut);
|
tgba_explicit* tgba_dupexp_dfs(const tgba* aut);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -32,7 +32,7 @@ namespace spot
|
||||||
class tgba;
|
class tgba;
|
||||||
struct tgba_run;
|
struct tgba_run;
|
||||||
|
|
||||||
/// \addtogroup emptiness_check Emptiness-check
|
/// \addtogroup emptiness_check Emptiness-checks
|
||||||
/// \ingroup tgba_algorithms
|
/// \ingroup tgba_algorithms
|
||||||
///
|
///
|
||||||
/// All emptiness-check algorithms follow the same interface.
|
/// All emptiness-check algorithms follow the same interface.
|
||||||
|
|
|
||||||
|
|
@ -28,6 +28,7 @@
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
/// \brief Print reachable states in LBTT format.
|
/// \brief Print reachable states in LBTT format.
|
||||||
|
/// \ingroup tgba_io
|
||||||
///
|
///
|
||||||
/// \param g The automata to print.
|
/// \param g The automata to print.
|
||||||
/// \param os Where to print.
|
/// \param os Where to print.
|
||||||
|
|
|
||||||
|
|
@ -29,6 +29,7 @@
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
/// \brief Build a spot::tgba_explicit* from an LTL formula.
|
/// \brief Build a spot::tgba_explicit* from an LTL formula.
|
||||||
|
/// \ingroup tgba_ltl
|
||||||
///
|
///
|
||||||
/// This is based on the following paper.
|
/// This is based on the following paper.
|
||||||
/// \verbatim
|
/// \verbatim
|
||||||
|
|
|
||||||
|
|
@ -27,7 +27,8 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
/// Build a spot::tgba_bdd_concrete from an LTL formula.
|
/// \brief Build a spot::tgba_bdd_concrete from an LTL formula.
|
||||||
|
/// \ingroup tgba_ltl
|
||||||
///
|
///
|
||||||
/// This is based on the following paper.
|
/// This is based on the following paper.
|
||||||
/// \verbatim
|
/// \verbatim
|
||||||
|
|
|
||||||
|
|
@ -29,6 +29,7 @@
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
/// \brief Print reachable states in Spin never claim format.
|
/// \brief Print reachable states in Spin never claim format.
|
||||||
|
/// \ingroup tgba_io
|
||||||
///
|
///
|
||||||
/// \param os The output stream to print on.
|
/// \param os The output stream to print on.
|
||||||
/// \param g The degeneralized automaton to output.
|
/// \param g The degeneralized automaton to output.
|
||||||
|
|
|
||||||
|
|
@ -27,6 +27,7 @@
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
/// \brief Build a deterministic automaton, ignoring acceptance conditions.
|
/// \brief Build a deterministic automaton, ignoring acceptance conditions.
|
||||||
|
/// \ingroup tgba_misc
|
||||||
///
|
///
|
||||||
/// This create a deterministic automaton that recognize the
|
/// This create a deterministic automaton that recognize the
|
||||||
/// same language as \a aut would if its acceptance conditions
|
/// same language as \a aut would if its acceptance conditions
|
||||||
|
|
|
||||||
|
|
@ -30,6 +30,7 @@ namespace spot
|
||||||
class tgba;
|
class tgba;
|
||||||
|
|
||||||
/// \brief Project a tgba_run on a tgba.
|
/// \brief Project a tgba_run on a tgba.
|
||||||
|
/// \ingroup tgba_run
|
||||||
///
|
///
|
||||||
/// If a tgba_run has been generated on a product, or any other
|
/// If a tgba_run has been generated on a product, or any other
|
||||||
/// on-the-fly algorithm with tgba operands,
|
/// on-the-fly algorithm with tgba operands,
|
||||||
|
|
|
||||||
|
|
@ -31,6 +31,7 @@ namespace spot
|
||||||
class tgba;
|
class tgba;
|
||||||
|
|
||||||
/// \brief Construct a tgba randomly.
|
/// \brief Construct a tgba randomly.
|
||||||
|
/// \ingroup tgba_misc
|
||||||
///
|
///
|
||||||
/// \param n The number of states wanted in the automata. All states
|
/// \param n The number of states wanted in the automata. All states
|
||||||
/// will be connected, and there will be no dead state.
|
/// will be connected, and there will be no dead state.
|
||||||
|
|
|
||||||
|
|
@ -30,6 +30,7 @@
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
/// \brief Iterate over all reachable states of a spot::tgba.
|
/// \brief Iterate over all reachable states of a spot::tgba.
|
||||||
|
/// \ingroup tgba_generic
|
||||||
class tgba_reachable_iterator
|
class tgba_reachable_iterator
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
|
|
@ -92,6 +93,7 @@ namespace spot
|
||||||
|
|
||||||
/// \brief An implementation of spot::tgba_reachable_iterator that browses
|
/// \brief An implementation of spot::tgba_reachable_iterator that browses
|
||||||
/// states depth first.
|
/// states depth first.
|
||||||
|
/// \ingroup tgba_generic
|
||||||
class tgba_reachable_iterator_depth_first : public tgba_reachable_iterator
|
class tgba_reachable_iterator_depth_first : public tgba_reachable_iterator
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
|
|
@ -106,6 +108,7 @@ namespace spot
|
||||||
|
|
||||||
/// \brief An implementation of spot::tgba_reachable_iterator that browses
|
/// \brief An implementation of spot::tgba_reachable_iterator that browses
|
||||||
/// states breadth first.
|
/// states breadth first.
|
||||||
|
/// \ingroup tgba_generic
|
||||||
class tgba_reachable_iterator_breadth_first : public tgba_reachable_iterator
|
class tgba_reachable_iterator_breadth_first : public tgba_reachable_iterator
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
|
|
|
||||||
|
|
@ -32,6 +32,9 @@
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
|
||||||
|
/// \addtogroup tgba_reduction
|
||||||
|
/// @{
|
||||||
|
|
||||||
/// Options for reduce.
|
/// Options for reduce.
|
||||||
enum reduce_tgba_options
|
enum reduce_tgba_options
|
||||||
{
|
{
|
||||||
|
|
@ -327,6 +330,7 @@ namespace spot
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
||||||
|
/// @}
|
||||||
}
|
}
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
|
||||||
|
|
@ -30,6 +30,7 @@ namespace spot
|
||||||
class tgba;
|
class tgba;
|
||||||
|
|
||||||
/// \brief Replay a tgba_run on a tgba.
|
/// \brief Replay a tgba_run on a tgba.
|
||||||
|
/// \ingroup tgba_run
|
||||||
///
|
///
|
||||||
/// This is similar to print_tgba_run(), except that the run is
|
/// This is similar to print_tgba_run(), except that the run is
|
||||||
/// actually replayed on the automaton while it is printed. Doing
|
/// actually replayed on the automaton while it is printed. Doing
|
||||||
|
|
@ -43,8 +44,6 @@ namespace spot
|
||||||
/// \param debug if set the output will be more verbose and extra
|
/// \param debug if set the output will be more verbose and extra
|
||||||
/// debugging informations will be output on failure
|
/// debugging informations will be output on failure
|
||||||
/// \return true iff the run could be completed
|
/// \return true iff the run could be completed
|
||||||
///
|
|
||||||
/// \ingroup tgba_run
|
|
||||||
bool replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run,
|
bool replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run,
|
||||||
bool debug = false);
|
bool debug = false);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -31,6 +31,7 @@
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
/// \brief Highlight a spot::tgba_run on a spot::tgba.
|
/// \brief Highlight a spot::tgba_run on a spot::tgba.
|
||||||
|
/// \ingroup tgba_dotty
|
||||||
///
|
///
|
||||||
/// An instance of this class can be passed to spot::dotty_reachable.
|
/// An instance of this class can be passed to spot::dotty_reachable.
|
||||||
class tgba_run_dotty_decorator: public dotty_decorator
|
class tgba_run_dotty_decorator: public dotty_decorator
|
||||||
|
|
|
||||||
|
|
@ -28,6 +28,7 @@
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
/// \brief Save reachable states in text format.
|
/// \brief Save reachable states in text format.
|
||||||
|
/// \ingroup tgba_io
|
||||||
std::ostream& tgba_save_reachable(std::ostream& os, const tgba* g);
|
std::ostream& tgba_save_reachable(std::ostream& os, const tgba* g);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -26,6 +26,10 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
|
||||||
|
/// \addtogroup tgba_misc
|
||||||
|
/// @{
|
||||||
|
|
||||||
struct tgba_statistics
|
struct tgba_statistics
|
||||||
{
|
{
|
||||||
unsigned transitions;
|
unsigned transitions;
|
||||||
|
|
@ -34,6 +38,8 @@ namespace spot
|
||||||
|
|
||||||
/// \brief Compute statistics for an automata.
|
/// \brief Compute statistics for an automata.
|
||||||
tgba_statistics stats_reachable(const tgba* g);
|
tgba_statistics stats_reachable(const tgba* g);
|
||||||
|
|
||||||
|
/// @}
|
||||||
}
|
}
|
||||||
|
|
||||||
#endif // SPOT_TGBAALGOS_STATS_HH
|
#endif // SPOT_TGBAALGOS_STATS_HH
|
||||||
|
|
|
||||||
|
|
@ -32,6 +32,9 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
/// \addtogroup tgba_io
|
||||||
|
/// @{
|
||||||
|
|
||||||
/// \brief A parse diagnostic with its location.
|
/// \brief A parse diagnostic with its location.
|
||||||
typedef std::pair<yy::Location, std::string> tgba_parse_error;
|
typedef std::pair<yy::Location, std::string> tgba_parse_error;
|
||||||
/// \brief A list of parser diagnostics, as filled by parse.
|
/// \brief A list of parser diagnostics, as filled by parse.
|
||||||
|
|
@ -67,6 +70,8 @@ namespace spot
|
||||||
/// \return \c true iff any diagnostic was output.
|
/// \return \c true iff any diagnostic was output.
|
||||||
bool format_tgba_parse_errors(std::ostream& os,
|
bool format_tgba_parse_errors(std::ostream& os,
|
||||||
tgba_parse_error_list& error_list);
|
tgba_parse_error_list& error_list);
|
||||||
|
|
||||||
|
/// @}
|
||||||
}
|
}
|
||||||
|
|
||||||
#endif // SPOT_TGBAPARSE_PUBLIC_HH
|
#endif // SPOT_TGBAPARSE_PUBLIC_HH
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue