alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgba/bdddict.hh, src/tgba/state.hh, src/tgba/statebdd.hh,

Browse source 
src/tgba/succiter.hh, src/tgba/succiterconcrete.hh,
src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbaexplicit.hh,
src/tgba/tgbaproduct.hh, src/tgba/tgbareduc.hh,
src/tgba/tgbatba.hh, src/tgbaalgos/emptiness.hh,
src/tgbaalgos/magic.hh, src/tgbaalgos/replayrun.hh,
src/tgbaalgos/gtec/gtec.hh, iface/gspn/ssp.hh: Introduce Doxygen
groups in the documentation.  Presently this only covers the
tgba/ directory, and the emptiness-check algorithms.
* doc/Doxyfile.in (EXCLUDE_PATTERNS): Skip Bison-generated files
in src/evtgbaparse/.
This commit is contained in:
Alexandre Duret-Lutz 2004-11-16 23:47:50 +00:00
parent cac85dbcca
commit 2cd298e4b0
19 changed files with 182 additions and 70 deletions
Download patch file Download diff file Expand all files Collapse all files

15
ChangeLog
View file

@ -1,3 +1,18 @@
2004-11-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgba/bdddict.hh, src/tgba/state.hh, src/tgba/statebdd.hh,
src/tgba/succiter.hh, src/tgba/succiterconcrete.hh,
src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbaexplicit.hh,
src/tgba/tgbaproduct.hh, src/tgba/tgbareduc.hh,
src/tgba/tgbatba.hh, src/tgbaalgos/emptiness.hh,
src/tgbaalgos/magic.hh, src/tgbaalgos/replayrun.hh,
src/tgbaalgos/gtec/gtec.hh, iface/gspn/ssp.hh: Introduce Doxygen
groups in the documentation. Presently this only covers the
tgba/ directory, and the emptiness-check algorithms.
* doc/Doxyfile.in (EXCLUDE_PATTERNS): Skip Bison-generated files
in src/evtgbaparse/.
2004-11-16 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgba/tgbatba.hh (tgba_sba_proxy): New class, with the

6
doc/Doxyfile.in
View file

@ -461,9 +461,9 @@ EXCLUDE_SYMLINKS = NO
# EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude
# certain files from those directories.
EXCLUDE_PATTERNS = */tgbaparse/location.hh \
*/tgbaparse/stack.hh \
*/tgbaparse/position.hh \
EXCLUDE_PATTERNS = */*tgbaparse/location.hh \
*/*tgbaparse/stack.hh \
*/*tgbaparse/position.hh \
*/*parse/*parse*.hh \
*test/*

4
iface/gspn/ssp.hh
View file

@ -48,12 +48,16 @@ namespace spot
const ltl::declarative_environment& env_;
};
/// \defgroup emptiness_check_ssp Emptiness-check algorithms for SSP
/// \ingroup emptiness_check
/// @{
couvreur99_check* couvreur99_check_ssp_semi(const tgba* ssp_automata);
couvreur99_check* couvreur99_check_ssp_shy_semi(const tgba* ssp_automata);
couvreur99_check* couvreur99_check_ssp_shy(const tgba* ssp_automata);
couvreur99_check_result*
counter_example_ssp(const couvreur99_check_status* status);
/// @}
}
#endif // SPOT_IFACE_GSPN_SSP_GSPN_SSP_HH

1
src/tgba/bdddict.hh
View file

@ -34,6 +34,7 @@ namespace spot
{
/// Map BDD variables to formulae.
/// \ingroup tgba_essentials
class bdd_dict: public bdd_allocator
{
public:

4
src/tgba/state.hh
View file

@ -31,6 +31,7 @@ namespace spot
{
/// \brief Abstract class for states.
/// \ingroup tgba_essentials
class state
{
public:
@ -76,6 +77,7 @@ namespace spot
};
/// \brief Strict Weak Ordering for \c state*.
/// \ingroup tgba_essentials
///
/// This is meant to be used as a comparison functor for
/// STL \c map whose key are of type \c state*.
@ -98,6 +100,7 @@ namespace spot
};
/// \brief An Equivalence Relation for \c state*.
/// \ingroup tgba_essentials
///
/// This is meant to be used as a comparison functor for
/// Sgi \c hash_map whose key are of type \c state*.
@ -121,6 +124,7 @@ namespace spot
};
/// \brief Hash Function for \c state*.
/// \ingroup tgba_essentials
///
/// This is meant to be used as a hash functor for
/// Sgi's \c hash_map whose key are of type \c state*.

3
src/tgba/statebdd.hh
View file

@ -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
// et Marie Curie.
//
@ -28,6 +28,7 @@
namespace spot
{
/// A state whose representation is a BDD.
/// \ingroup tgba_representation
class state_bdd: public state
{
public:

5
src/tgba/succiter.hh
View file

@ -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
// et Marie Curie.
//
@ -26,8 +26,8 @@
namespace spot
{
/// \brief Iterate over the successors of a state.
/// \ingroup tgba_essentials
///
/// This class provides the basic functionalities required to
/// iterate over the successors of a state, as well as querying
@ -96,7 +96,6 @@ namespace spot
//@}
};
}

3
src/tgba/succiterconcrete.hh
View file

@ -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
// et Marie Curie.
//
@ -29,6 +29,7 @@
namespace spot
{
/// A concrete iterator over successors of a TGBA state.
/// \ingroup tgba_representation
class tgba_succ_iterator_concrete: public tgba_succ_iterator
{
public:

22
src/tgba/tgba.hh
View file

@ -28,7 +28,21 @@
namespace spot
{
/// \defgroup tgba TGBA (Transition-based Genealized Büchi Automaton)
///
/// Spot is centered around the spot::tgba type. This type and its
/// cousins are listed \ref tgba_essentials "here". This is an
/// abstract interface. Its implementations are either \ref
/// tgba_representation "concrete representations", or \ref
/// tgba_on_the_fly_algorithms "on-the-fly algorithms". Other
/// algorithms that work on spot::tgba are \ref tgba_algorithms
/// "listed separately".
/// \addtogroup tgba_essentials Essential TGBA types
/// \ingroup tgba
/// \brief A Transition-based Generalized Büchi Automaton.
/// \ingroup tgba_essentials
///
/// The acronym TGBA (Transition-based Generalized Büchi Automaton)
/// was coined by Dimitra Giannakopoulou and Flavio Lerda
@ -201,6 +215,14 @@ namespace spot
mutable int num_acc_;
};
/// \addtogroup tgba_representation TGBA representations
/// \ingroup tgba
/// \addtogroup tgba_on_the_fly_algorithms TGBA on-the-fly algorithms
/// \ingroup tgba
/// \addtogroup tgba_algorithms TGBA algorithms
/// \ingroup tgba
}
#endif // SPOT_TGBA_TGBA_HH

4
src/tgba/tgbabddconcrete.hh
View file

@ -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
// et Marie Curie.
//
@ -30,7 +30,7 @@
namespace spot
{
/// \brief A concrete spot::tgba implemented using BDDs.
///
/// \ingroup tgba_representation
class tgba_bdd_concrete: public tgba
{
public:

9
src/tgba/tgbabddconcreteproduct.hh
View file

@ -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
// et Marie Curie.
//
@ -26,10 +26,11 @@
namespace spot
{
/// \brief Multiplies two tgba::tgba_bdd_concrete automata.
/// \brief Multiplies two spot::tgba_bdd_concrete automata.
/// \ingroup tgba_algorithms
///
/// This function build the resulting product, as another
/// tgba::tgba_bdd_concrete automaton.
/// This function builds the resulting product as another
/// spot::tgba_bdd_concrete automaton.
tgba_bdd_concrete*
product(const tgba_bdd_concrete* left, const tgba_bdd_concrete* right);
}

3
src/tgba/tgbaexplicit.hh
View file

@ -34,6 +34,7 @@ namespace spot
class tgba_explicit_succ_iterator;
/// Explicit representation of a spot::tgba.
/// \ingroup tgba_representation
class tgba_explicit: public tgba
{
public:
@ -116,6 +117,7 @@ namespace spot
/// States used by spot::tgba_explicit.
/// \ingroup tgba_representation
class state_explicit : public spot::state
{
public:
@ -139,6 +141,7 @@ namespace spot
/// Successor iterators used by spot::tgba_explicit.
/// \ingroup tgba_representation
class tgba_explicit_succ_iterator: public tgba_succ_iterator
{
public:

1
src/tgba/tgbaproduct.hh
View file

@ -29,6 +29,7 @@ namespace spot
{
/// \brief A state for spot::tgba_product.
/// \ingroup tgba_on_the_fly_algorithms
///
/// This state is in fact a pair of state: the state from the left
/// automaton and that of the right.

6
src/tgba/tgbareduc.hh
View file

@ -47,8 +47,10 @@ namespace spot
};
class tgba_reduc: public tgba_explicit,
public tgba_reachable_iterator_breadth_first
/// Explicit automata used in reductions.
/// \ingroup tgba_representation
class tgba_reduc:
public tgba_explicit, public tgba_reachable_iterator_breadth_first
{
public:
tgba_reduc(const tgba* a,

2
src/tgba/tgbatba.hh
View file

@ -30,6 +30,7 @@ namespace spot
{
/// \brief Degeneralize a spot::tgba on the fly, producing a TBA.
/// \ingroup tgba_on_the_fly_algorithms
///
/// This class acts as a proxy in front of a spot::tgba, that should
/// be degeneralized on the fly. The result is still a spot::tgba,
@ -87,6 +88,7 @@ namespace spot
};
/// \brief Degeneralize a spot::tgba on the fly, producing an SBA.
/// \ingroup tgba_on_the_fly_algorithms
///
/// This class acts as a proxy in front of a spot::tgba, that should
/// be degeneralized on the fly.

111
src/tgbaalgos/emptiness.hh
View file

@ -29,43 +29,41 @@
namespace spot
{
/// An accepted run, for a tgba.
struct tgba_run
{
struct step {
const state* s;
bdd label;
bdd acc;
};
typedef std::list<step> steps;
steps prefix;
steps cycle;
~tgba_run();
tgba_run()
{
};
tgba_run(const tgba_run& run);
tgba_run& operator=(const tgba_run& run);
};
class tgba;
struct tgba_run;
/// \brief Display a tgba_run.
/// \addtogroup emptiness_check Emptiness-check
/// \ingroup tgba_algorithms
///
/// Output the prefix and cycle of the tgba_run \a run, even if it
/// does not corresponds to an actual run of the automaton \a a.
/// This is unlike replay_tgba_run(), which will ensure the run
/// actually exist in the automaton (and will display any transition
/// annotation).
/// All emptiness-check algorithms follow the same interface.
/// Basically once you have constructed an instance of
/// spot::emptiness_check (by instantiating a subclass, or calling a
/// functions construct such instance; see \ref
/// emptiness_check_algorithms "this list"), you should call
/// spot::emptiness_check::check() to check the automaton.
///
/// (\a a is used here only to format states and transitions.)
std::ostream& print_tgba_run(std::ostream& os,
const tgba* a,
const tgba_run* run);
/// If spot::emptiness_check::check() returns 0, then the automaton
/// was found empty. Otherwise the automaton accepts some run.
/// (Beware that some algorithms---those using bit-state
/// hashing---may found the automaton to be empty even if it is not
/// actually empty.)
///
/// When spot::emptiness_check::check() does not return 0, it
/// returns an instance of spot::emptiness_check_result. You can
/// try to call spot::emptiness_check_result::accepting_run() to
/// obtain an accepting run. For some emptiness-check algorithms,
/// spot::emptiness_check_result::accepting_run() will require some
/// extra computation. Most emptiness-check algorithms are able to
/// return such an accepting run, however this is not mandatory and
/// spot::emptiness_check_result::accepting_run() can return 0 (this
/// does not means by anyway that no accepting run exist).
///
/// The acceptance run returned by
/// spot::emptiness_check_result::accepting_run(), if any, is of
/// type spot::tgba_run. \ref tgba_run "This page" gathers existing
/// operations on these objects.
///
/// @{
/// \brief The result of an emptiness check.
///
@ -112,6 +110,53 @@ namespace spot
virtual std::ostream& print_stats(std::ostream& os) const;
};
/// @}
/// \addtogroup emptiness_check_algorithms Emptiness-check algorithms
/// \ingroup emptiness_check
/// \addtogroup tgba_run TGBA runs and supporting functions
/// \ingroup emptiness_check
/// @{
/// An accepted run, for a tgba.
struct tgba_run
{
struct step {
const state* s;
bdd label;
bdd acc;
};
typedef std::list<step> steps;
steps prefix;
steps cycle;
~tgba_run();
tgba_run()
{
};
tgba_run(const tgba_run& run);
tgba_run& operator=(const tgba_run& run);
};
/// \brief Display a tgba_run.
///
/// Output the prefix and cycle of the tgba_run \a run, even if it
/// does not corresponds to an actual run of the automaton \a a.
/// This is unlike replay_tgba_run(), which will ensure the run
/// actually exist in the automaton (and will display any transition
/// annotation).
///
/// (\a a is used here only to format states and transitions.)
std::ostream& print_tgba_run(std::ostream& os,
const tgba* a,
const tgba_run* run);
/// @}
}
#endif // SPOT_TGBAALGOS_EMPTINESS_HH

4
src/tgbaalgos/gtec/gtec.hh
View file

@ -27,6 +27,9 @@
namespace spot
{
/// \addtogroup emptiness_check_algorithms
/// @{
/// \brief Check whether the language of an automate is empty.
///
/// This is based on the following paper.
@ -149,6 +152,7 @@ namespace spot
virtual int* find_state(const state* s);
};
/// @}
}
#endif // SPOT_TGBAALGOS_GTEC_GTEC_HH

47
src/tgbaalgos/magic.hh
View file

@ -27,16 +27,20 @@
namespace spot
{
/// \brief Returns an emptiness checker on the spot::tgba automaton \a a.
/// During the visit of \a a, the returned checker stores explicitely all
/// \addtogroup emptiness_check_algorithms
/// @{
/// \brief Returns an emptiness checker on the spot::tgba automaton \a a.
/// During the visit of \a a, the returned checker stores explicitely all
/// the traversed states.
///
/// \pre The automaton \a a must have at most one accepting condition (i.e.
/// it is a TBA).
///
/// The method \a check() of the returned checker can be called several times
/// (until it returns a null pointer) to enumerate all the visited accepting
/// paths. The implemented algorithm is the following.
/// The method \a check() of the returned checker can be called several times
/// (until it returns a null pointer) to enumerate all the visited accepting
/// paths. The implemented algorithm is the following.
///
/// \verbatim
/// procedure check ()
@ -77,7 +81,7 @@ namespace spot
///
/// \verbatim
/// Article{ courcoubertis.92.fmsd,
/// author = {Costas Courcoubetis and Moshe Y. Vardi and Pierre
/// author = {Costas Courcoubetis and Moshe Y. Vardi and Pierre
/// Wolper and Mihalis Yannakakis},
/// title = {Memory-Efficient Algorithm for the Verification of
/// Temporal Properties},
@ -90,7 +94,7 @@ namespace spot
///
emptiness_check* explicit_magic_search(const tgba *a);
/// \brief Returns an emptiness checker on the spot::tgba automaton \a a.
/// \brief Returns an emptiness checker on the spot::tgba automaton \a a.
/// During the visit of \a a, the returned checker does not store explicitely
/// the traversed states but uses the bit state hashing technic. However, the
/// implemented algorithm is the same as the one of
@ -103,24 +107,24 @@ namespace spot
///
emptiness_check* bit_state_hashing_magic_search(const tgba *a, size_t size);
/// \brief Returns an emptiness check on the spot::tgba automaton \a a.
/// During the visit of \a a, the returned checker stores explicitely all
/// \brief Returns an emptiness check on the spot::tgba automaton \a a.
/// During the visit of \a a, the returned checker stores explicitely all
/// the traversed states.
///
/// \pre The automaton \a a must have at most one accepting condition (i.e.
/// it is a TBA).
///
/// The method \a check() of the returned checker can be called several times
/// (until it returns a null pointer) to enumerate all the visited accepting
/// paths. The implemented algorithm is the following:
///
///
/// The method \a check() of the returned checker can be called several times
/// (until it returns a null pointer) to enumerate all the visited accepting
/// paths. The implemented algorithm is the following:
///
/// \verbatim
/// procedure check ()
/// begin
/// weight = 0;
/// call dfs_blue(s0);
/// end;
///
///
/// procedure dfs_blue (s)
/// begin
/// s.color = cyan;
@ -134,8 +138,8 @@ namespace spot
/// if the edge (s,t) is accepting then
/// weight = weight - 1;
/// end if;
/// else if t.color == cyan and
/// (the edge (s,t) is accepting or
/// else if t.color == cyan and
/// (the edge (s,t) is accepting or
/// weight > t.weight) then
/// report cycle;
/// end if;
@ -145,7 +149,7 @@ namespace spot
/// end for;
/// s.color = blue;
/// end;
///
///
/// procedure dfs_red(s)
/// begin
/// if s.color == cyan then
@ -159,8 +163,8 @@ namespace spot
/// end for;
/// end;
/// \endverbatim
///
/// It is an adaptation to TBA (and a slight extension) of the one
///
/// It is an adaptation to TBA (and a slight extension) of the one
/// presented in
/// \verbatim
/// InProceedings{ schwoon.05.tacas,
@ -183,7 +187,7 @@ namespace spot
///
emptiness_check* explicit_se05_search(const tgba *a);
/// \brief Returns an emptiness checker on the spot::tgba automaton \a a.
/// \brief Returns an emptiness checker on the spot::tgba automaton \a a.
/// During the visit of \a a, the returned checker does not store explicitely
/// the traversed states but uses the bit state hashing technic. However, the
/// implemented algorithm is the same as the one of
@ -196,6 +200,7 @@ namespace spot
///
emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size);
/// @}
}
#endif // SPOT_TGBAALGOS_MAGIC_HH

2
src/tgbaalgos/replayrun.hh
View file

@ -43,6 +43,8 @@ namespace spot
/// \param debug if set the output will be more verbose and extra
/// debugging informations will be output on failure
/// \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 debug = false);
}